Mercurial > hg > Members > kono > Proof > galois

comparison sym3n.agda @ 182:eb94265d2a39 fresh-list

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Any based proof computation done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 26 Nov 2020 13:13:58 +0900
parents 57d475583f74
children 59d12d02dfa8
comparison
equal deleted inserted replaced
181:7423f0fc124a 182:eb94265d2a39
35 open import Relation.Nary using (⌊_⌋) 35 open import Relation.Nary using (⌊_⌋)
36 36
37 p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid 37 p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
38 p0id = pleq _ _ refl 38 p0id = pleq _ _ refl
39 39
40 t1 : FList 3 → FList 3 40 open import Data.List.Fresh.Relation.Unary.Any
41 t1 x = tl2 x x [] where 41 open import FLComm
42 tl3 : (FL 3) → ( z : FList 3) → FList 3 → FList 3
43 tl3 h [] w = w
44 tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w )
45 tl2 : ( x z : FList 3) → FList 3 → FList 3
46 tl2 [] _ x = x
47 tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
48 42
49 stage10 : FList 3 43 stage3FList : CommFListN 3 2 ≡ cons (zero :: zero :: zero :: f0) [] (Level.lift tt)
50 stage10 = {!!} -- t1 (Flist (fmax )) 44 stage3FList = refl
51 45
52 p0 = FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) 46 solved1 : (x : Permutation 3 3) → deriving 2 x → x =p= pid
53 p1 = FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) 47 solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList pf solved2 where
54 p2 = FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) 48 -- p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
55 p3 = FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) 49 pf : perm→FL x ≡ FL0 → x =p= pid
56 p4 = FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) 50 pf eq = ptrans pf2 (ptrans pf0 p0id ) where
57 p5 = FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) 51 pf2 : x =p= FL→perm (perm→FL x)
58 t0 = plist p0 ∷ plist p1 ∷ plist p2 ∷ plist p3 ∷ plist p4 ∷ plist p5 ∷ [] 52 pf2 = psym (FL←iso x)
59 53 pf0 : FL→perm (perm→FL x) =p= FL→perm FL0
60 tt4 = plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷ plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷ plist [ p5 , p1 ] ∷ 54 pf0 = pcong-Fp eq
61 plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷ plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷ plist [ p5 , p1 ] ∷ 55 solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 )
62 plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷ plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷ plist [ p5 , p2 ] ∷ 56 solved2 = CommStage→ 3 2 x dr
63 plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷ plist [ p5 , p3 ] ∷
64 plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p4 ] ∷
65 plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p5 ] ∷
66 []
67
68 open _=p=_
69
70 stage1 : (x : Permutation 3 3) → Set (Level.suc Level.zero)
71 stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x
72
73 open import logic
74
75 pFL : ( g : Permutation 3 3) → { x : FL 3 } → perm→FL g ≡ x → g =p= FL→perm x
76 pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl )
77
78 open ≡-Reasoning
79
80 -- st01 : ( x y : Permutation 3 3) → x =p= p3 → y =p= p3 → x ∘ₚ y =p= p4
81 -- st01 x y s t = record { peq = λ q → ( begin
82 -- (x ∘ₚ y) ⟨$⟩ʳ q
83 -- ≡⟨ peq ( presp s t ) q ⟩
84 -- ( p3 ∘ₚ p3 ) ⟨$⟩ʳ q
85 -- ≡⟨ peq p33=4 q ⟩
86 -- p4 ⟨$⟩ʳ q
87 -- ∎ ) }
88
89 st00 = perm→FL [ FL→perm ((suc zero) :: (suc zero :: (zero :: f0 ))) , FL→perm ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) ]
90
91
92 stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
93 stage12 = {!!}
94 57
95 58
96 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
97 solved1 _ uni = prefl
98 solved1 x (gen {f} {g} d d₁) with solved1 f d | solved1 g d₁
99 ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where
100 genlem : ( q : Fin 3 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q
101 genlem q = begin
102 g ⟨$⟩ʳ ( f ⟨$⟩ʳ q )
103 ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩
104 f ⟨$⟩ʳ q
105 ≡⟨ f=e q ⟩
106 q
107 ∎
108 solved1 x (ccong {f} {g} (record {peq = f=g}) d) with solved1 f d
109 ... | record { peq = f=e } = record { peq = λ q → cc q } where
110 cc : ( q : Fin 3 ) → x ⟨$⟩ʳ q ≡ q
111 cc q = begin
112 x ⟨$⟩ʳ q
113 ≡⟨ sym (f=g q) ⟩
114 f ⟨$⟩ʳ q
115 ≡⟨ f=e q ⟩
116 q
117 ∎
118 solved1 _ (comm {g} {h} x y) = {!!}
119