Mercurial > hg > Members > kono > Proof > galois

changeset 164:85bf5c283469

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 Mon, 23 Nov 2020 03:24:28 +0900
parents d3d2083643d6
children 16ad3c7aa287
files FLutil.agda
diffstat 1 files changed, 16 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Mon Nov 23 02:35:37 2020 +0900
+++ b/FLutil.agda	Mon Nov 23 03:24:28 2020 +0900
@@ -234,21 +234,27 @@
 ∀FList zero = record { ∀list = f0 ∷# [] ; x∈∀list = af1 } where
     af1 : (x : FL zero) → Any  (_≡_ x) (cons f0 [] (Level.lift tt))
     af1 f0 = here refl
-∀FList (suc n) = record { ∀list = af4 n ≤-refl (∀FListP.∀list af0) [] 
-       ; x∈∀list = λ x → af2 x  ( af4 n ≤-refl (∀FListP.∀list af0) [] ) } where
+∀FList (suc n) = record { ∀list = af4 n ≤-refl (∀FListP.∀list af0) [] fmax (Level.lift tt)
+       ; x∈∀list = λ x → af2 x  ( af4 n ≤-refl (∀FListP.∀list af0) [] fmax (Level.lift tt)) } where
     af0 : ∀FListP n
     af0 = ∀FList n
     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
-    af4r  : (i : ℕ) → (i<n : i < suc n) → ( y : FList n ) → (y1 : FList (suc n))
-         → (a : FL n) →  fresh (FL (n)) ⌊ _f<?_ ⌋ a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) y1
-    af4r = {!!}
-    af4  : (i : ℕ) → (i<n : i < suc n) → ( y : FList n ) → (y1 : FList (suc n)) →  FList (suc n)
-    af4 zero i<n [] y1 = y1
-    af4 zero (s≤s i<n) (cons a' y x) y1 = af4 zero 0<s y (cons (zero :: a') y1 (af4r zero 0<s y y1 a' x))
-    af4 (suc i) (s≤s i<n) [] y1 = af4 i (≤-trans i<n a≤sa) (∀FListP.∀list af0) y1 
-    af4 (suc i) (s≤s i<n) (cons a' y x) y1 = af4 (suc i) (s≤s i<n) y (cons (fromℕ< (s≤s i<n) :: a') y1 (af4r (suc i) (s≤s i<n) y y1 a' x))
+    af4  : (i : ℕ) → (i<n : i < suc n) → ( y : FList n ) → (y1 : FList (suc n))
+        → (a : FL n) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) y1 →  FList (suc n)
+    af4 zero i<n [] y1 a fr = y1
+    af4 zero (s≤s i<n) (cons a' y x) y1 a fr =
+      af4 zero 0<s y (cons (zero :: a') y1 (af41 a fr {!!})) a' ({!!} , af41 a fr {!!} ) where 
+       af41 : (a : FL n) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a) y1 → a' f< a  → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a') y1
+       af41 a fr lt = ttf (f<t lt) y1 fr
+    af4 (suc i) (s≤s i<n) [] y1 a fr = af4 i (≤-trans i<n a≤sa) (∀FListP.∀list af0) y1 fmax (af42 fr) where
+       af42 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a) y1 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (≤-trans i<n a≤sa) :: fmax) y1
+       af42 = {!!}
+    af4 (suc i) (s≤s i<n) (cons a' y x) y1 a fr = af4 (suc i) (s≤s i<n) y (cons (fromℕ< (s≤s i<n) :: a') y1 {!!}) a' ({!!} , {!!} ) where -- 
+       af43 : (a : FL n) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a) y1 → a' f< a
+          → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a') y1
+       af43 a fr lt = ttf (f<t lt) y1 fr
     af2 : (x : FL (suc n)) → (y : FList (suc n)) → Any (_≡_ x) y
     af2 = {!!}