Mercurial > hg > Members > kono > Proof > galois

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Gutil.agda	Mon Aug 17 15:24:58 2020 +0900
@@ -0,0 +1,94 @@
+open import Level hiding ( suc ; zero )
+open import Algebra
+module Gutil {n m : Level} (G : Group n m ) where
+
+open import Data.Unit
+open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
+open import Function
+open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
+open import Relation.Nullary
+open import Data.Empty
+open import Data.Product
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+
+open Group G
+
+import Relation.Binary.Reasoning.Setoid as EqReasoning
+
+gsym = Algebra.Group.sym G
+grefl = Algebra.Group.refl G
+gtrans = Algebra.Group.trans G
+
+lemma3 : ε ≈ ε ⁻¹
+lemma3 = begin
+     ε          ≈⟨ gsym (proj₁ inverse _) ⟩
+     ε ⁻¹ ∙ ε   ≈⟨ proj₂ identity _ ⟩
+     ε ⁻¹
+   ∎ where open EqReasoning (Algebra.Group.setoid G)
+
+lemma6 : {f : Carrier } →  ( f ⁻¹ ) ⁻¹  ≈ f
+lemma6 {f} = begin
+     ( f ⁻¹ ) ⁻¹   ≈⟨ gsym ( proj₁ identity _) ⟩
+      ε  ∙ ( f ⁻¹ ) ⁻¹   ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩
+     (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹   ≈⟨ assoc _ _ _ ⟩
+     f ∙ ( f ⁻¹  ∙ ( f ⁻¹ ) ⁻¹ )  ≈⟨ ∙-cong grefl (proj₂ inverse _) ⟩
+     f ∙ ε  ≈⟨ proj₂ identity _ ⟩
+     f
+   ∎ where open EqReasoning (Algebra.Group.setoid G)
+
+≡→≈ : {f g : Carrier } → f ≡ g → f ≈ g
+≡→≈ refl = grefl
+
+---
+-- to avoid assoc storm, flatten multiplication according to the template
+--
+
+data MP  : Carrier → Set (Level.suc n) where
+    am  : (x : Carrier )   →  MP  x
+    _o_ : {x y : Carrier } →  MP  x →  MP  y → MP  ( x ∙ y )
+
+mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier
+mpf {x} (am x) y = x ∙ y
+mpf (m o m₁) y = mpf m ( mpf m₁ y )
+
+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) = 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) ⁻¹
+lemma5 f g = begin
+     g ⁻¹ ∙ f ⁻¹                                     ≈⟨ gsym (proj₂ identity _) ⟩
+     g ⁻¹ ∙ f ⁻¹  ∙ ε                                ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩
+     g ⁻¹ ∙ f ⁻¹  ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ )         ≈⟨ ∙-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))  ⟩
+     g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))))    ≈⟨ ∙-cong grefl (gsym (assoc _ _ _ )) ⟩
+     g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))    ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩
+     g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))                   ≈⟨ gsym (assoc _ _ _) ⟩
+     (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε)                  ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩
+     (f ∙ g) ⁻¹ ∙ ε                                  ≈⟨ proj₂ identity _ ⟩
+     (f ∙ g) ⁻¹
+     ∎ where open EqReasoning (Algebra.Group.setoid G)
+
--- a/Solvable.agda	Mon Aug 17 15:12:36 2020 +0900
+++ b/Solvable.agda	Mon Aug 17 15:24:58 2020 +0900
@@ -13,6 +13,7 @@


 open Group G
+open import Gutil G

 [_,_] :  Carrier   → Carrier   → Carrier
 [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h
@@ -36,78 +37,6 @@

 import Relation.Binary.Reasoning.Setoid as EqReasoning

-gsym = Algebra.Group.sym G
-grefl = Algebra.Group.refl G
-gtrans = Algebra.Group.trans G
-
-lemma3 : ε ≈ ε ⁻¹
-lemma3 = begin
-     ε          ≈⟨ gsym (proj₁ inverse _) ⟩
-     ε ⁻¹ ∙ ε   ≈⟨ proj₂ identity _ ⟩
-     ε ⁻¹
-   ∎ where open EqReasoning (Algebra.Group.setoid G)
-
-lemma6 : {f : Carrier } →  ( f ⁻¹ ) ⁻¹  ≈ f
-lemma6 {f} = begin
-     ( f ⁻¹ ) ⁻¹   ≈⟨ gsym ( proj₁ identity _) ⟩
-      ε  ∙ ( f ⁻¹ ) ⁻¹   ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩
-     (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹   ≈⟨ assoc _ _ _ ⟩
-     f ∙ ( f ⁻¹  ∙ ( f ⁻¹ ) ⁻¹ )  ≈⟨ ∙-cong grefl (proj₂ inverse _) ⟩
-     f ∙ ε  ≈⟨ proj₂ identity _ ⟩
-     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 )
-
-mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier
-mpf {x} (am x) y = x ∙ y
-mpf (m o m₁) y = mpf m ( mpf m₁ y )
-
-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) = 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) ⁻¹
-lemma5 f g = begin
-     g ⁻¹ ∙ f ⁻¹                                     ≈⟨ gsym (proj₂ identity _) ⟩
-     g ⁻¹ ∙ f ⁻¹  ∙ ε                                ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩
-     g ⁻¹ ∙ f ⁻¹  ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ )         ≈⟨ ∙-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))  ⟩
-     g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))))    ≈⟨ ∙-cong grefl (gsym (assoc _ _ _ )) ⟩
-     g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))    ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩
-     g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))                   ≈⟨ gsym (assoc _ _ _) ⟩
-     (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε)                  ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩
-     (f ∙ g) ⁻¹ ∙ ε                                  ≈⟨ proj₂ identity _ ⟩
-     (f ∙ g) ⁻¹
-     ∎ where open EqReasoning (Algebra.Group.setoid G)
-
 lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
 lemma4 g h = begin
        [ h , g ]                               ≈⟨ grefl ⟩