Mercurial > hg > Members > kono > Proof > galois

changeset 11:9dae7ef74342

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, 17 Aug 2020 14:40:54 +0900
parents 04f40fc4eb69
children d960f2ea902f
files Solvable.agda
diffstat 1 files changed, 25 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/Solvable.agda	Mon Aug 17 14:02:04 2020 +0900
+++ b/Solvable.agda	Mon Aug 17 14:40:54 2020 +0900
@@ -38,6 +38,7 @@
 
 gsym = Algebra.Group.sym G
 grefl = Algebra.Group.refl G
+gtrans = Algebra.Group.trans G
 
 lemma3 : ε ≈ ε ⁻¹
 lemma3 = begin
@@ -56,6 +57,9 @@
      f
    ∎ where open EqReasoning (Algebra.Group.setoid G)
 
+≡→≈ : {f g : Carrier } → f ≡ g → f ≈ g
+≡→≈ refl = grefl
+
 data MP  : Carrier → Set (Level.suc n) where
     am  : (x : Carrier )   →  MP  x
     _o_ : {x y : Carrier } →  MP  x →  MP  y → MP  ( x ∙ y )
@@ -66,16 +70,30 @@
 
 mp-flatten : {x : Carrier } → (m : MP x ) → Carrier 
 mp-flatten {x} m = mpf {x} m ε 
-
+  
 ∙-flatten : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten m
 ∙-flatten {x} (am x) = gsym (proj₂ identity _)
 ∙-flatten {_} (am x o q) = ∙-cong grefl ( ∙-flatten q )
-∙-flatten (_o_ {_} {z} (_o_ {x} {y} p q) r) with ∙-flatten (p o q )   -- t : x ∙ y ≈ mpf p (mpf q ε)
-... | t = begin
-     x ∙ y ∙ z                    ≈⟨ ∙-cong t grefl  ⟩
-     mpf p (mpf q ε) ∙ z          ≈⟨ {!!} ⟩
-     mpf p (mpf q (mpf r ε))
-   ∎ where open EqReasoning (Algebra.Group.setoid G)
+∙-flatten (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ ( ∙-flatten {x ∙ y } (p o q )) ( ∙-flatten {z} r ) where
+   mp-cong : {p q r : Carrier} → (P : MP p)  → q ≈ r → mpf P q ≈ mpf P r
+   mp-cong (am x) q=r = ∙-cong grefl q=r
+   mp-cong (P o P₁) q=r = mp-cong P ( mp-cong P₁ q=r )
+   mp-assoc : {p q r : Carrier} → (P : MP p)  → mpf P q ∙ r ≈ mpf P (q ∙ r )
+   mp-assoc (am x) = assoc _ _ _ 
+   mp-assoc {p} {q} {r} (P o P₁) = begin
+       mpf P (mpf  P₁ q) ∙ r      ≈⟨ mp-assoc P ⟩
+       mpf P (mpf P₁ q ∙ r)       ≈⟨ mp-cong P (mp-assoc P₁)  ⟩
+       mpf P ((mpf  P₁) (q ∙ r))
+    ∎ where open EqReasoning (Algebra.Group.setoid G)
+   lemma9 : (x y z : Carrier) →  x ∙ y ≈ mpf p (mpf q ε) → z ≈ mpf r ε →  x ∙ y ∙ z ≈ mp-flatten ((p o q) o r)
+   lemma9 x y z t s = begin
+       x ∙ y ∙ z                    ≈⟨ ∙-cong t grefl  ⟩
+       mpf p (mpf q ε) ∙ z          ≈⟨ mp-assoc p ⟩
+       mpf p (mpf q ε ∙ z)          ≈⟨ mp-cong p (mp-assoc q ) ⟩
+       mpf p (mpf q (ε ∙ z))        ≈⟨ mp-cong p (mp-cong q (proj₁ identity _  )) ⟩
+       mpf p (mpf q z)              ≈⟨ mp-cong p (mp-cong q s) ⟩
+       mpf p (mpf q (mpf r ε))
+    ∎ where open EqReasoning (Algebra.Group.setoid G)
 
 
 lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹