Mercurial > hg > Members > kono > Proof > galois

changeset 160:254f3acb2091

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 20 Sep 2020 10:34:54 +0900
parents 28a985c263dc
children 047efc82be47 57d475583f74
files FLutil.agda
diffstat 1 files changed, 14 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Sun Sep 20 09:48:35 2020 +0900
+++ b/FLutil.agda	Sun Sep 20 10:34:54 2020 +0900
@@ -240,20 +240,22 @@
     af3 : (w : Fin (suc n)) (x y : FL n) → Level.Lift Level.zero (True (x f<? y )) → (w :: x ) f< (w :: y )
     af3 w x y (Level.lift z) with x f<? y
     ... | yes x<y = f<t x<y
-    af4 : (i : ℕ) → (i<n : i < suc n) →  ( y : FList n ) → ( z : FList (suc n)) →  FList (suc n)
-    af4r : (i : ℕ) → (i<n : i < suc n) → (a : FL n) → ( y : FList n ) → ( z : FList (suc n))
-       → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (af4 i i<n y z ) 
-    af4 i i<n [] z = z
-    af4 zero (s≤s i<n) (cons a y x) z  = cons (fromℕ< (s≤s i<n) :: a) (af4 zero 0<s y z ) (af4r zero  0<s a y z)
-    af4 (suc i) (s≤s i<n) (cons a y x) z  = cons (fromℕ< (s≤s i<n) :: a) (af4 i (≤-trans i<n a≤sa) y z ) af5 where
-        af6 : fromℕ< (≤-trans i<n a≤sa) ≡ fromℕ< (s≤s i<n)
-        af6 = {!!}
-        af5 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a) (af4 i (≤-trans i<n a≤sa) y z)
-        af5 = subst (λ k → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (k :: a) (af4 i (≤-trans i<n a≤sa) y z)) af6 (af4r i (≤-trans i<n a≤sa) a y z)
-    af4r = {!!}
+    af4 : (i : ℕ) → (i<n : i < suc n) →  ( y y1 : FList n ) → ( z : FList (suc n)) →  FList (suc n)
+    af4r : (i : ℕ) → (i<n : i < suc n) → (a : FL n) → ( y y1 : FList n ) → ( z : FList (suc n))
+       → fresh (FL n) ⌊ _f<?_ ⌋ a y
+       → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (af4 i i<n y y1 z ) 
+    af4 zero i<n [] _ z = z
+    af4 (suc i) (s≤s i<n) [] y z = af4 i (≤-trans i<n a≤sa) y y z
+    af4 zero (s≤s i<n) (cons a y x) y1 z  = cons (fromℕ< (s≤s i<n) :: a) (af4 zero 0<s y y1 z ) (af4r zero  0<s a y y1 z x)
+    af4 (suc i) (s≤s i<n) (cons a y x) y1 z  = cons (fromℕ< (≤-trans i<n a≤sa) :: a) (af4 i (≤-trans i<n a≤sa) y y1 z ) (af4r i (≤-trans i<n a≤sa) a y y1 z x) 
+    -- fresh (FL n) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (af4 i i<n y y1 z)
+    af4r zero (s≤s z≤n) a [] y1 [] (lift tt) = Level.lift tt
+    af4r zero (s≤s z≤n) a [] y1 (cons a₁ z x) (lift tt) = {!!} , af4r zero (s≤s z≤n) a [] y1 z (Level.lift tt)
+    af4r zero (s≤s z≤n) a (cons a₁ y x₁) y1 z x = {!!}
+    af4r (suc i) i<n a y y1 z x = {!!}
     af1 : (i : ℕ ) → i ≤ suc n  → FList (suc n)
     af1 zero i<n  = Data.List.Fresh.map (zero ::_ ) (λ {x} {x₁} xr → Level.lift (fromWitness (af3 zero x x₁ xr ) )) (∀FListP.∀list af0 )
-    af1 (suc i) (s≤s i<n) = af4 i (s≤s i<n) (∀FListP.∀list af0 ) ( af1 i (≤-trans i<n a≤sa)) 
+    af1 (suc i) (s≤s i<n) = af4 i (s≤s i<n) (∀FListP.∀list af0 ) (∀FListP.∀list af0 ) ( af1 i (≤-trans i<n a≤sa)) 
     af2 : (x : FL (suc n)) → (y : FList (suc n)) → Any (_≡_ x) y
     af2 = {!!}