Mercurial > hg > Members > kono > Proof > galois

changeset 171:825b3237169c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... on going
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Nov 2020 19:24:12 +0900
parents 53d31ba08456
children 32e2097f5702
files FLutil.agda
diffstat 1 files changed, 18 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Mon Nov 23 17:58:28 2020 +0900
+++ b/FLutil.agda	Mon Nov 23 19:24:12 2020 +0900
@@ -236,7 +236,7 @@
     af1 f0 = here refl
 ∀FList (suc n) with ∀FListP.∀list (∀FList n) | ∀FListP.x∈∀list (∀FList n) fmax
 ∀FList (suc n) | [] | ()
-∀FList (suc n) | cons a x fr | _ = record { ∀list = af4 n ≤-refl a x fr
+∀FList (suc n) | cons A X FR | _ = record { ∀list = af4 n ≤-refl A X FR
        ; x∈∀list = λ x → {!!} } where
     af0 : ∀FListP n
     af0 = ∀FList n
@@ -247,18 +247,26 @@
         → (a : FL n) → (y : FList n) → fresh (FL n) ⌊ _f<?_ ⌋ a y  
         →  FList (suc n)
     af4r  : (i : ℕ) → (i<n : i < suc n) 
-        → (a : FL n) → (y : FList n) → (fr : fresh (FL n) ⌊ _f<?_ ⌋ a y )
-        →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (af4 i i<n a y fr)
+        → (a a₁ : FL n) → a f< a₁ → (y : FList n) → (fr : fresh (FL n) ⌊ _f<?_ ⌋ a₁ y )
+        →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (af4 i i<n a₁ y fr)
     af4 zero i<n a [] fr = cons (fromℕ< i<n :: a) [] (Level.lift tt)
     af4 zero i<n a (cons a₁ y x) (lift p , fr) =
-        cons (fromℕ< i<n :: a) ( af4 zero i<n a₁ y x ) (ttf (f<t (toWitness p)) ( af4 zero i<n a₁ y x ) (af4r zero i<n a₁ y x))
-    af4 (suc i) (s≤s i<n) a' [] fr' = af4 i (<-trans i<n a<sa) a x fr
+        cons (fromℕ< i<n :: a) (af4 zero i<n a₁ y x ) (af4r zero i<n a a₁ (toWitness p) y x)
+    af4 (suc i) (s≤s i<n) a' [] fr' = af4 i (<-trans i<n a<sa) A X FR
     af4 (suc i) (s≤s i<n) a (cons a₁ y x) (lift p , fr) = 
-        cons  (fromℕ< (s≤s i<n) :: a₁) ( af4 (suc i) (s≤s i<n) a₁ y x ) ( af4r (suc i) (s≤s i<n) a₁ y x )
-    af4r zero i<n a [] fr =  {!!} , Level.lift tt
-    af4r zero i<n a (cons a₁ y x) fr = {!!} , {!!}
-    af4r (suc i) i<n a [] fr = {!!}
-    af4r (suc i) i<n a (cons a₁ y x) fr = {!!}
+        cons  (fromℕ< (s≤s i<n) :: a) ( af4 (suc i) (s≤s i<n) a₁ y x ) (af4r (suc i) (s≤s i<n) a a₁ (toWitness p) y x)
+    af4r zero i<n a a₁ a<a₁ [] fr = Level.lift (fromWitness (f<t a<a₁)) , Level.lift tt
+    af4r zero i<n a a₁ a<a₁ (cons a₂ y x) (lift p , _) = Level.lift (fromWitness (f<t a<a₁)) , af4r zero i<n a a₂ af41 y x where
+       af41 : a f< a₂
+       af41 = f<-trans a<a₁ (toWitness p)
+    af4r (suc i) (s≤s i<n) a' a₁ a<a₁ [] (lift tt) = ttf af43 (af4 i (<-trans i<n a<sa) A X FR) (af4r i (<-trans i<n a<sa) a' A af44 X FR) where
+       af43 : (fromℕ< (s≤s i<n) :: a') f< (fromℕ< (<-trans i<n a<sa) :: a')
+       af43 = {!!}
+       af44 : a' f< A
+       af44 = {!!}
+    af4r (suc i) (s≤s i<n) a a₁ a<a₁ (cons a₂ y x)  (lift p , _) =  Level.lift (fromWitness (f<t a<a₁)) , af4r (suc i) (s≤s i<n) a a₂ af42 y x where
+       af42 : a f< a₂
+       af42 = f<-trans a<a₁ (toWitness p)
 
 -- FLinsert membership