# HG changeset patch # User Shinji KONO # Date 1597629736 -32400 # Node ID c1b3c25d7ceff278922b5e8f0f3c941a4533955a # Parent 92a164e1f6b61579b32d49747ee3e00a05a46796 ... diff -r 92a164e1f6b6 -r c1b3c25d7cef Solvable.agda --- a/Solvable.agda Sun Aug 16 22:08:46 2020 +0900 +++ b/Solvable.agda Mon Aug 17 11:02:16 2020 +0900 @@ -4,6 +4,7 @@ open import Data.Unit open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function open import Data.Nat using (ℕ; suc; zero) open import Relation.Nullary open import Data.Empty @@ -17,28 +18,88 @@ [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where - uni : Commutator P ε - gen : {f g h : Carrier} → P g → P h → Commutator P f → Commutator P ( f ∙ [ g , h ] ) - ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g + uni : Commutator P ε + comm : {g h : Carrier} → P g → P h → Commutator P [ g , h ] + gen : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙ g ) + ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m) deriving 0 x = Lift (Level.suc n ⊔ m) ⊤ deriving (suc i) x = Commutator (deriving i) x --- deriving stage is closed on multiplication and inversion - -deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y → deriving i ( x ∙ y ) -deriving-mul {zero} {x} {y} (lift tt) (lift tt) = lift tt -deriving-mul {suc i} {ε} {ε} uni uni = ccong (Algebra.Group.sym G (proj₁ identity ε)) uni -deriving-mul {suc i} {ε} {_} uni (gen x x₁ iy) = ccong (Algebra.Group.sym G (proj₁ identity _)) (gen x x₁ iy) -deriving-mul {suc i} {_} {ε} (gen x x₁ ix) uni = ccong (Algebra.Group.sym G (proj₂ identity _)) (gen x x₁ ix) -deriving-mul {suc i} {_} {_} (gen x x₁ ix) (gen x₂ x₃ iy) = ccong {!!} (gen x₂ x₃ (gen x x₁ iy)) -deriving-mul {suc i} {_} {_} _ _ = {!!} - -deriving-inv : { i : ℕ } → { x : Carrier } → deriving i x → deriving i ( x ⁻¹ ) -deriving-inv {i} {x} ix = ? - record Solvable : Set (Level.suc n ⊔ m) where field dervied-length : ℕ end : (x : Carrier ) → deriving dervied-length x → x ≈ ε + +-- deriving stage is closed on multiplication and inversion + +import Relation.Binary.Reasoning.Setoid as EqReasoning + +gsym = Algebra.Group.sym G +grefl = Algebra.Group.refl G +lemma3 : ε ≈ ε ⁻¹ +lemma3 = begin + ε ≈⟨ gsym (proj₁ inverse _) ⟩ + ε ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩ + ε ⁻¹ + ∎ where open EqReasoning (Algebra.Group.setoid G) + +open import Data.List using ([] ; _∷_ ; List ) + +data Node (A : Set n) : Set (Level.suc n) where + leaf : A → Node A + node : Node A → Node A → Node A + +flatten : Node Carrier → List Carrier +flatten x = flatten1 x [] where + flatten1 : Node Carrier → List Carrier → List Carrier + flatten1 (leaf x) y = x ∷ [] + flatten1 (node left right) y = flatten1 left (flatten1 right y ) + +gnode : Node Carrier → Carrier +gnode (leaf x) = x +gnode (node left right) = gnode left ∙ gnode right + +glist : List Carrier → Carrier +glist [] = ε +glist (x ∷ []) = x +glist (x ∷ y) = x ∙ glist y + +gpattern : (p q : Node Carrier) → flatten p ≡ flatten q → gnode p ≈ gnode q +gpattern p q eq = gpattern1 p q (flatten p) _≡_.refl eq where + gnot1 : (x : Carrier ) → ( left right : Node Carrier ) → ¬ ( x ∷ [] ≡ flatten (node left right) ) + gnot1 x p q eq0 = {!!} + gpattern1 : (p q : Node Carrier) → (r : List Carrier ) → flatten p ≡ r → r ≡ flatten q → gnode p ≈ gnode q + gpattern1 (leaf x) (leaf x) (x ∷ []) _≡_.refl _≡_.refl = grefl + gpattern1 (leaf x) (node left right) (x ∷ []) _≡_.refl r=q = {!!} + gpattern1 (node p p₁) (leaf x) r p=r r=q = {!!} + gpattern1 (node p p₁) (node q q₁) r p=r r=q = {!!} + +deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y → deriving i ( x ∙ y ) +deriving-mul {zero} {x} {y} _ _ = lift tt +deriving-mul {suc i} {x} {y} ix iy = gen ix iy + +deriving-inv : { i : ℕ } → { x : Carrier } → deriving i x → deriving i ( x ⁻¹ ) +deriving-inv {zero} {x} (lift tt) = lift tt +deriving-inv {suc i} {ε} uni = ccong lemma3 uni +deriving-inv {suc i} {_} (comm x x₁ ) = ccong (lemma4 _ _) (comm x₁ x) where + lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹ + lemma4 g h = begin + h ⁻¹ ∙ g ⁻¹ ∙ h ∙ g ≈⟨ {!!} ⟩ + [ g , h ] ⁻¹ + ∎ where open EqReasoning (Algebra.Group.setoid G) +deriving-inv {suc i} {_} (gen x x₁ ) = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) where + lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹ + lemma5 f g = begin + g ⁻¹ ∙ f ⁻¹ ≈⟨ {!!} ⟩ + g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ {!!} ⟩ + (g ⁻¹ ∙ f ⁻¹ ∙ (f ∙ g)) ∙ (f ∙ g) ⁻¹ ≈⟨ {!!} ⟩ + (g ⁻¹ ∙ (f ⁻¹ ∙ f) ∙ g) ∙ (f ∙ g) ⁻¹ ≈⟨ {!!} ⟩ + (g ⁻¹ ∙ (ε ∙ g)) ∙ (f ∙ g) ⁻¹ ≈⟨ {!!} ⟩ + (g ⁻¹ ∙ g) ∙ (f ∙ g) ⁻¹ ≈⟨ {!!} ⟩ + ε ∙ (f ∙ g) ⁻¹ ≈⟨ {!!} ⟩ + (f ∙ g) ⁻¹ + ∎ where open EqReasoning (Algebra.Group.setoid G) +deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix ) +