Mercurial > hg > Members > kono > Proof > galois

changeset 162:57d475583f74

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 00:48:18 +0900
parents 254f3acb2091
children d3d2083643d6
files FLutil.agda Putil.agda sym3.agda sym3n.agda sym4.agda
diffstat 5 files changed, 21 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/FLutil.agda	Mon Nov 23 00:48:18 2020 +0900
@@ -234,28 +234,24 @@
 ∀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 = af1 (suc n) ≤-refl ; x∈∀list = λ x → af2 x (af1 (suc n) ≤-refl ) } where
+∀FList (suc n) = record { ∀list = af4 n ≤-refl (∀FListP.∀list af0) []
+       ; x∈∀list = λ x → af2 x  ( af4 n ≤-refl (∀FListP.∀list af0) [] ) } 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
-    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 ) (∀FListP.∀list af0 ) ( af1 i (≤-trans i<n a≤sa)) 
+    af4r : (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
+    af4r zero i<n y [] a = Level.lift tt
+    af4r zero i<n y (cons a₁ y1 x) a = {!!} , af4r zero i<n y y1 a 
+    af4r (suc i) i<n y [] a = Level.lift tt
+    af4r (suc i) i<n y (cons a₁ y1 x) a = {!!} , af4r (suc i) i<n y y1 a 
+    af4  : (i : ℕ) → (i<n : i < suc n) → ( y : FList n ) → (y1 : FList (suc n)) →  FList (suc n)
+    af4 zero i<n [] y1 = y1
+    af4 (suc i) (s≤s i<n) [] y1 = af4 i (≤-trans i<n a≤sa) (∀FListP.∀list af0) y1
+    af4 zero (s≤s i<n) (cons a y x) y1 = af4 zero 0<s y (cons (fromℕ< (s≤s i<n) :: a) y1 (af4r zero (s≤s i<n) y y1 a))
+    af4 (suc i) (s≤s i<n) (cons a y x) y1 = af4 i (≤-trans i<n a≤sa) y (cons (fromℕ< (s≤s i<n) :: a) y1 (af4r (suc i) (s≤s i<n) y y1 a))
     af2 : (x : FL (suc n)) → (y : FList (suc n)) → Any (_≡_ x) y
     af2 = {!!}
 
--- a/Putil.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/Putil.agda	Mon Nov 23 00:48:18 2020 +0900
@@ -197,7 +197,7 @@
             p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x
             p11 = begin
                fromℕ< (≤-trans (fin<n {_} {y}) a≤sa )
-              ≡⟨ fromℕ<-irrelevant _ _ p12 _ (s≤s (fin<n {suc n}))  ⟩
+              ≡⟨ lemma10  p12  ⟩
                suc (fromℕ< (fin<n {suc n} {x} )) 
               ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
                suc x
@@ -278,7 +278,7 @@
           p004 = p003  (fromℕ< (s≤s (s≤s m≤n))) (
              begin
                 fromℕ< (s≤s (s≤s m≤n))
-             ≡⟨  fromℕ<-irrelevant _ _ (cong suc meq) (s≤s (s≤s m≤n)) (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩
+             ≡⟨  lemma10  (cong suc meq) {s≤s (s≤s m≤n)} {subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) } ⟩
                 fromℕ< (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) )
              ≡⟨ fromℕ<-toℕ {suc (suc n)} (suc t) (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩
                 suc t
--- a/sym3.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/sym3.agda	Mon Nov 23 00:48:18 2020 +0900
@@ -13,6 +13,7 @@
 
 open import Gutil 
 open import Putil 
+open import FLutil 
 open import Solvable using (solvable)
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
@@ -122,7 +123,7 @@
    ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0))| record { eq = ge } |  record { eq = he } =   
            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
    ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } = 
-            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+          case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
    ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } = 
             case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
    ... | ((suc zero) :: (zero :: (zero :: f0 ))) | ((suc (suc zero)) :: (zero :: (zero :: f0 )))| record { eq = ge } |  record { eq = he } =  
--- a/sym3n.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/sym3n.agda	Mon Nov 23 00:48:18 2020 +0900
@@ -47,7 +47,7 @@
        tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
 
    stage10  :  FList 3
-   stage10  =  t1 (Flist (fmax ))
+   stage10  =  {!!} -- t1 (Flist (fmax ))
 
    p0 =  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) 
    p1 =  FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) 
--- a/sym4.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/sym4.agda	Mon Nov 23 00:48:18 2020 +0900
@@ -96,6 +96,9 @@
        tl2 [] _ x = x
        tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
 
+   Flist : FL 4 → FList 4
+   Flist = {!!}
+   
    stage1  :  FList 4
    stage1  =  t1 (Flist (fmax ))