# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606045381 -32400
# Node ID 047efc82be47256b2c1ab344c1b8e0bd1e181c3d
# Parent  254f3acb2091ad564dd2a39f0375242357543671
sized fresh list

diff -r 254f3acb2091 -r 047efc82be47 FLutil.agda
--- a/FLutil.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/FLutil.agda	Sun Nov 22 20:43:01 2020 +0900
@@ -5,7 +5,7 @@
 open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ ; _≟_)
 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
 open import Data.Fin.Permutation
-open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
+open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero; s≤s ; z≤n )
 open import Data.Nat.Properties
 open import Relation.Binary.PropositionalEquality 
 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
@@ -132,10 +132,28 @@
 open import Relation.Binary as B hiding (Decidable; _⇔_)
 open import Data.Sum.Base as Sum --  inj₁
 open import Relation.Nary using (⌊_⌋)
-open import Data.List.Fresh
+
+open import Size 
+
+open import Data.Unit.Polymorphic.Base using (⊤)
+
+module _ {a r : Level } (A : Set a) (R : Rel A r) where
+
+  data List# (i : Size) : Set (a ⊔ r)
+  fresh :  ∀{i} (a : A) (as : List# i ) → Set r
 
-FList : (n : ℕ ) → Set
-FList n = List# (FL n) ⌊ _f<?_ ⌋
+  data List# i where
+    []   : List# i
+    cons : {j : Size< i} (a : A) (as : List# j) → fresh a as → List# i
+
+  infixr 5 _∷#_
+  pattern _∷#_ x xs = cons x xs _
+
+  fresh a []        = ⊤
+  fresh a (x ∷# xs) = R a x × fresh a xs
+
+FList : (n : ℕ ) → { i : Size} → Set
+FList n {i} = List# (FL n) ⌊ _f<?_ ⌋ i
 
 fr1 : FList 3
 fr1 =
@@ -146,130 +164,16 @@
    ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
    []
 
-open import Data.Product
-open import Relation.Nullary.Decidable hiding (⌊_⌋)
-open import Data.Bool hiding (_<_ ; _≤_ )
-open import Data.Unit.Base using (⊤ ; tt)
-
---  fresh a []        = ⊤
---  fresh a (x ∷# xs) = R a x × fresh a xs
-
--- toWitness
--- ttf< :  {n : ℕ } → {x a : FL n } → x f< a  → T (isYes (x f<? a))
--- ttf< {n} {x} {a} x<a with x f<? a
--- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
--- ... | no nn = ⊥-elim ( nn x<a )
-
-ttf : {n : ℕ } {x a : FL (suc n)} → x f< a → (y : FList (suc n)) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
-ttf _ [] fr = Level.lift tt
-ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where 
-       ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
-       ttf1 t x<a = f<-trans x<a (toWitness t)
-
--- by https://gist.github.com/aristidb/1684202
-
-FLinsert : {n : ℕ } → FL n → FList n  → FList n 
-FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x
-     → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
-FLinsert {zero} f0 y = f0 ∷# []
-FLinsert {suc n} x [] = x ∷# []
-FLinsert {suc n} x (cons a y x₁) with FLcmp x a
-... | tri≈ ¬a b ¬c  = cons a y x₁
-... | tri< lt ¬b ¬c  = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y  x₁) 
-FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt  = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
-FLinsert {suc n} x (cons a y yr)  | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr )
-
-FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
-FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
-... | tri< x<b ¬b ¬c  = Level.lift (fromWitness a<x) , Level.lift a<b , Level.lift tt
-... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt
-... | tri> ¬a ¬b b<x =  Level.lift a<b  ,  Level.lift (fromWitness  (f<-trans (toWitness a<b) b<x))  , Level.lift tt
-FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b
-... | tri< x<b ¬b ¬c =  Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br
-... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , ttf a<x y br
-FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
-    Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
-FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
-    Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y
-
-fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 
-
--- open import Data.List.Fresh.Relation.Unary.All
--- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] )
+fr0 : FList 0
+fr0 = []
 
-Flist1 :  {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
-Flist1 zero i<n [] _ = []
-Flist1 zero i<n (a ∷# x ) z  = FLinsert ( zero :: a ) (Flist1 zero i<n x z )
-Flist1 (suc i) (s≤s i<n) [] z  = Flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z 
-Flist1 (suc i) i<n (a ∷# x ) z  = FLinsert ((fromℕ< i<n ) :: a ) (Flist1 (suc i) i<n x z )
-
-∀Flist : {n : ℕ } → FL n → FList n
-∀Flist {zero} f0 = f0 ∷# [] 
-∀Flist {suc n} (x :: y)  = Flist1 n a<sa (∀Flist y) (∀Flist y)   
-
-fr8 : FList 4
-fr8 = ∀Flist fmax
-
-open import Data.List.Fresh.Relation.Unary.Any 
-open import Data.List.Fresh.Relation.Unary.All 
-
-x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_ ) (FLinsert x xs)
-x∈FLins {zero} f0 [] = here refl
-x∈FLins {zero} f0 (cons f0 xs x) = here refl
-x∈FLins {suc n} x [] = here refl
-x∈FLins {suc n} x (cons a xs x₁) with FLcmp x a
-... | tri< x<a ¬b ¬c = here refl
-... | tri≈ ¬a b ¬c   = here b
-x∈FLins {suc n} x (cons a [] x₁)              | tri> ¬a ¬b a<x = there ( here refl )
-x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) )
-
-open import fin
-
-record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where
-  field
-    ∀list :   FList n 
-    x∈∀list : (x : FL n ) → Any (x ≡_ ) ∀list 
-
-∀FList : (n : ℕ )  → ∀FListP n
-∀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
-    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)) 
-    af2 : (x : FL (suc n)) → (y : FList (suc n)) → Any (_≡_ x) y
-    af2 = {!!}
+frn : (n : ℕ) → FList n → FList (suc n)
+frn n fl = frn1 fmax fl [] where
+   frn1 : (f : FL n) →  FList n →  FList (suc n) →  FList (suc n)
+   frn1 f0 _ x =  x
+   frn1 (v :: f) x = {!!}
 
 
--- FLinsert membership
-
-module FLMB { n : ℕ } where
-
-  FL-Setoid : Setoid Level.zero Level.zero
-  FL-Setoid  = record { Carrier = FL n ; _≈_ = _≡_ ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }}
+-- ∀Flist : {n : ℕ } → FL n → FList n
 
-  open import Data.List.Fresh.Membership.Setoid FL-Setoid
 
-  FLinsert-mb :  (x : FL n ) → (xs : FList n)  → x ∈ FLinsert x xs
-  FLinsert-mb x xs = x∈FLins {n} x xs 
-
-  
diff -r 254f3acb2091 -r 047efc82be47 Putil.agda
--- a/Putil.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/Putil.agda	Sun Nov 22 20:43:01 2020 +0900
@@ -197,7 +197,8 @@
             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}))  ⟩
+              -- ≡⟨ fromℕ<-irrelevant _ _ p12 _ (s≤s (fin<n {suc n}))  ⟩
+              ≡⟨ {!!}  ⟩
                suc (fromℕ< (fin<n {suc n} {x} )) 
               ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
                suc x
@@ -278,7 +279,8 @@
           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)) ) ⟩
+             -- ≡⟨  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)) ) ⟩
+             ≡⟨  {!!} ⟩
                 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
diff -r 254f3acb2091 -r 047efc82be47 Solvable.agda
--- a/Solvable.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/Solvable.agda	Sun Nov 22 20:43:01 2020 +0900
@@ -19,7 +19,6 @@
 [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h 
 
 data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
-  uni   : Commutator P ε
   comm  : {g h : Carrier} → P g → P h  → Commutator P [ g , h ] 
   gen   : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙  g  )
   ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g
@@ -64,7 +63,6 @@
 
 deriving-inv : { i : ℕ } → { x  : Carrier } → deriving i x → deriving i ( x ⁻¹ )
 deriving-inv {zero} {x} (lift tt) = lift tt
-deriving-inv {suc i} {ε} uni = ccong lemma3 uni
 deriving-inv {suc i} {_} (comm x x₁ )   = ccong (lemma4 _ _) (comm x₁ x) 
 deriving-inv {suc i} {_} (gen x x₁ )    = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) 
 deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix )
@@ -102,6 +100,10 @@
        ε
      ∎ 
 
+deriving-ε : { i : ℕ } → deriving i ε 
+deriving-ε {zero} = lift tt
+deriving-ε {suc i} = ccong (comm-refl grefl )( comm (deriving-ε {i}) (deriving-ε {i}) ) 
+
 comm-resp : {g h g1 h1  : Carrier } → g ≈ g1  → h ≈ h1 → [ g , h ] ≈ [ g1 , h1 ] 
 comm-resp {g} {h} {g1} {h1} g=g1 h=h1 =  ∙-cong (∙-cong (∙-cong (⁻¹-cong g=g1 ) (⁻¹-cong h=h1 )) g=g1 ) h=h1
 
diff -r 254f3acb2091 -r 047efc82be47 sym2.agda
--- a/sym2.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/sym2.agda	Sun Nov 22 20:43:01 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 ( [_] )
 
@@ -96,7 +97,6 @@
               g=h :  g =p= h
               g=h =  FL-inject (trans g=00 (sym h=00))
    solved :  (x : Permutation 2 2) → Commutator  (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
-   solved x uni = prefl
    solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h  } 
    solved x (gen {f} {g} d d₁) with solved f d | solved g d₁
    ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where
diff -r 254f3acb2091 -r 047efc82be47 sym3.agda
--- a/sym3.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/sym3.agda	Sun Nov 22 20:43:01 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 ( [_] )
 
@@ -155,7 +156,6 @@
           case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
    
    stage12  :  (x : Permutation 3 3) → stage1 x →  ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
-   stage12 x uni = case1 prefl
    stage12 x (comm {g} {h} x1 y1 ) = st02 g h
    stage12 _ (gen {x} {y} sx sy) with stage12 x sx | stage12 y sy 
    ... | case1 t | case1 s = case1 ( record { peq = λ q → peq (presp t s) q} )
@@ -174,7 +174,6 @@
 
 
    solved1 :  (x : Permutation 3 3) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
-   solved1 _ uni = prefl
    solved1 x (gen {f} {g} d d₁) with solved1 f d | solved1 g d₁
    ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where
       genlem : ( q : Fin 3 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q
diff -r 254f3acb2091 -r 047efc82be47 sym3n.agda
--- a/sym3n.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/sym3n.agda	Sun Nov 22 20:43:01 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))) 
@@ -94,7 +94,6 @@
 
 
    solved1 :  (x : Permutation 3 3) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
-   solved1 _ uni = prefl
    solved1 x (gen {f} {g} d d₁) with solved1 f d | solved1 g d₁
    ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where
       genlem : ( q : Fin 3 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q
diff -r 254f3acb2091 -r 047efc82be47 sym4.agda
--- a/sym4.agda	Sun Sep 20 10:34:54 2020 +0900
+++ b/sym4.agda	Sun Nov 22 20:43:01 2020 +0900
@@ -97,7 +97,7 @@
        tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
 
    stage1  :  FList 4
-   stage1  =  t1 (Flist (fmax ))
+   stage1  =  {!!} -- t1 (Flist (fmax ))
 
    -- stage2 ( Kline )
    --  k0  p0  zero :: zero :: zero :: zero :: f0 ∷                                   (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) ∷
@@ -108,7 +108,7 @@
    tb = plist ( FL→perm p0) ∷ plist ( FL→perm p3) ∷ plist ( FL→perm p8) ∷ plist ( FL→perm pb) ∷ []
 
    stage2  :   FList 4
-   stage2   =  t1 (t1 (Flist (fmax ))) -- ( p0 ∷# p1 ∷# p2 ∷# p3 ∷# p4 ∷# p5 ∷# p6 ∷# p7 ∷# p8 ∷# p9 ∷# pa ∷# pb ∷# [] ) 
+   stage2   =  {!!} -- t1 (t1 (Flist (fmax ))) -- ( p0 ∷# p1 ∷# p2 ∷# p3 ∷# p4 ∷# p5 ∷# p6 ∷# p7 ∷# p8 ∷# p9 ∷# pa ∷# pb ∷# [] ) 
    
    solved1 :  (x : Permutation 4 4) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
    solved1 = {!!}