Mercurial > hg > Members > kono > Proof > galois

comparison src/Gutil.agda @ 271:c209aebeab2a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fundamental again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 24 Jan 2023 16:40:39 +0900
parents 6d1619d9f880
children 386ece574509
comparison
equal deleted inserted replaced
270:0081e1ed5ead 271:c209aebeab2a
126 (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε) ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩ 126 (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε) ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩
127 (f ∙ g) ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩ 127 (f ∙ g) ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩
128 (f ∙ g) ⁻¹ 128 (f ∙ g) ⁻¹
129 ∎ where open EqReasoning (Algebra.Group.setoid G) 129 ∎ where open EqReasoning (Algebra.Group.setoid G)
130 130
131 open import Tactic.MonoidSolver using (solve; solve-macro)
132
133 lemma7 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
134 lemma7 f g = begin
135 g ⁻¹ ∙ f ⁻¹ ≈⟨ gsym (proj₂ identity _) ⟩
136 g ⁻¹ ∙ f ⁻¹ ∙ ε ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩
137 g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ solve monoid ⟩
138 g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))) ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩
139 g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)) ≈⟨ solve monoid ⟩
140 (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε) ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩
141 (f ∙ g) ⁻¹ ∙ ε ≈⟨ solve monoid ⟩
142 (f ∙ g) ⁻¹
143 ∎ where open EqReasoning (Algebra.Group.setoid G)
144