Mercurial > hg > Members > kono > Proof > galois
annotate src/Gutil.agda @ 328:e9de2bfef88d
fix done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 23 Sep 2023 22:43:47 +0900 |
| parents | fff18d4a063b |
| children |
| rev | line source |
|---|---|
|
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
279
diff
changeset
|
1 {-# OPTIONS --cubical-compatible --safe #-} |
|
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
279
diff
changeset
|
2 |
| 0 | 3 open import Level hiding ( suc ; zero ) |
| 4 open import Algebra | |
| 14 | 5 module Gutil {n m : Level} (G : Group n m ) where |
| 0 | 6 |
| 4 | 7 open import Data.Unit |
| 8 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) | |
| 6 | 9 open import Function |
| 7 | 10 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) |
| 4 | 11 open import Relation.Nullary |
| 12 open import Data.Empty | |
| 5 | 13 open import Data.Product |
| 14 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 15 | |
| 0 | 16 |
| 4 | 17 open Group G |
| 0 | 18 |
| 6 | 19 import Relation.Binary.Reasoning.Setoid as EqReasoning |
| 20 | |
| 21 gsym = Algebra.Group.sym G | |
| 22 grefl = Algebra.Group.refl G | |
| 11 | 23 gtrans = Algebra.Group.trans G |
| 8 | 24 |
| 279 | 25 ε≈ε⁻¹ : ε ≈ ε ⁻¹ |
| 26 ε≈ε⁻¹ = begin | |
| 6 | 27 ε ≈⟨ gsym (proj₁ inverse _) ⟩ |
| 28 ε ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩ | |
| 29 ε ⁻¹ | |
| 30 ∎ where open EqReasoning (Algebra.Group.setoid G) | |
| 31 | |
| 279 | 32 f⁻¹⁻¹≈f : {f : Carrier } → ( f ⁻¹ ) ⁻¹ ≈ f |
| 33 f⁻¹⁻¹≈f {f} = begin | |
| 8 | 34 ( f ⁻¹ ) ⁻¹ ≈⟨ gsym ( proj₁ identity _) ⟩ |
| 35 ε ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩ | |
| 36 (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ assoc _ _ _ ⟩ | |
| 37 f ∙ ( f ⁻¹ ∙ ( f ⁻¹ ) ⁻¹ ) ≈⟨ ∙-cong grefl (proj₂ inverse _) ⟩ | |
| 38 f ∙ ε ≈⟨ proj₂ identity _ ⟩ | |
| 39 f | |
| 40 ∎ where open EqReasoning (Algebra.Group.setoid G) | |
| 6 | 41 |
| 11 | 42 ≡→≈ : {f g : Carrier } → f ≡ g → f ≈ g |
| 43 ≡→≈ refl = grefl | |
| 44 | |
| 279 | 45 car : {f g h : Carrier } → f ≈ g → f ∙ h ≈ g ∙ h |
| 46 car f=g = ∙-cong f=g grefl | |
| 15 | 47 |
| 279 | 48 cdr : {f g h : Carrier } → f ≈ g → h ∙ f ≈ h ∙ g |
| 49 cdr f=g = ∙-cong grefl f=g | |
| 15 | 50 |
| 279 | 51 -- module _ where |
| 52 -- open EqReasoning (Algebra.Group.setoid G) | |
| 53 -- _≈⟨⟩_ : (a : Carrier ) → {b : Carrier} → a IsRelatedTo b → a IsRelatedTo b | |
| 54 -- _ ≈⟨⟩ a = a | |
| 15 | 55 |
| 279 | 56 open import Tactic.MonoidSolver using (solve; solve-macro) |
| 15 | 57 |
| 8 | 58 lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹ |
| 59 lemma5 f g = begin | |
| 12 | 60 g ⁻¹ ∙ f ⁻¹ ≈⟨ gsym (proj₂ identity _) ⟩ |
| 61 g ⁻¹ ∙ f ⁻¹ ∙ ε ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩ | |
| 271 | 62 g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ solve monoid ⟩ |
| 63 g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))) ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩ | |
| 64 g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)) ≈⟨ solve monoid ⟩ | |
| 65 (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε) ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩ | |
| 66 (f ∙ g) ⁻¹ ∙ ε ≈⟨ solve monoid ⟩ | |
| 67 (f ∙ g) ⁻¹ | |
| 68 ∎ where open EqReasoning (Algebra.Group.setoid G) | |
| 69 | |
| 279 | 70 |