Mercurial > hg > Members > kono > Proof > galois

changeset 7:ec1cb153af22

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 11:30:12 +0900
parents c1b3c25d7cef
children 4e275f918e63
files PermGroup.agda Solvable.agda Symmetric.agda
diffstat 3 files changed, 97 insertions(+), 90 deletions(-) [+]
line wrap: on
line diff
--- a/PermGroup.agda	Mon Aug 17 11:02:16 2020 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,86 +0,0 @@
-module PermGroup where
-
-open import Level hiding ( suc ; zero )
-open import Algebra
-open import Algebra.Structures
-open import Data.Fin
-open import Data.Product
-open import Data.Fin.Permutation
-open import Function hiding (id ; flip)
-open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
-open import Function.LeftInverse  using ( _LeftInverseOf_ )
-open import Function.Equality using (Π)
-open import Data.Nat using (ℕ; suc; zero)
-open import Relation.Binary.PropositionalEquality
-
-f1 : Fin 3 → Fin 3
-f1 zero = suc (suc zero)
-f1 (suc zero) = zero
-f1 (suc (suc zero)) = suc zero
-
-lemma1  : Permutation 3 3
-lemma1  = permutation f1 ( f1 ∘ f1 ) lemma2 where
-   lemma3 : (x : Fin 3 ) → f1 (f1 (f1 x)) ≡ x
-   lemma3 zero = refl
-   lemma3 (suc zero) = refl
-   lemma3 (suc (suc zero)) = refl
-   lemma2 : :→-to-Π (λ x → f1 (f1 x)) InverseOf :→-to-Π f1
-   lemma2 = record { left-inverse-of = λ x → lemma3 x ; right-inverse-of = λ x → lemma3 x }
-
-fid : {p : ℕ } → Fin p → Fin p
-fid x = x
-
--- Data.Fin.Permutation.id
-pid : {p : ℕ } → Permutation p p
-pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
-
--- Data.Fin.Permutation.flip
-pinv : {p : ℕ } → Permutation p p → Permutation p p
-pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }
-
-record _=p=_ {p : ℕ } ( x y : Permutation p p )  : Set where
-    field
-       peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q
-
-open _=p=_
-
-prefl : {p : ℕ } { x  : Permutation p p } → x =p= x
-peq (prefl {p} {x}) q = refl
-
-psym : {p : ℕ } { x y : Permutation p p } → x =p= y →  y =p= x
-peq (psym {p} {x} {y}  eq ) q = sym (peq eq q)
-
-ptrans : {p : ℕ } { x y z : Permutation p p } → x =p= y  → y =p= z →  x =p= z
-peq (ptrans {p} {x} {y} x=y y=z ) q = trans (peq x=y q) (peq y=z q)
-
-Pgroup : ℕ → Group  Level.zero Level.zero
-Pgroup p = record {
-      Carrier        = Permutation p p
-    ; _≈_            = _=p=_
-    ; _∙_            = _∘ₚ_
-    ; ε              = pid
-    ; _⁻¹            = pinv
-    ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = record {refl = prefl ; trans = ptrans ; sym = psym }
-       ; ∙-cong = presp }
-       ; assoc = passoc }
-       ; identity = ( (λ q → record { peq = λ q → refl } ) , (λ q → record { peq = λ q → refl } ))  }
-       ; inverse   = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} ))  
-       ; ⁻¹-cong   = λ i=j → record { peq = λ q → p-inv i=j q }
-      }
-   } where
-       presp : {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v)
-       presp {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where
-           lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q)
-           lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
-       passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p=  (x ∘ₚ (y ∘ₚ z))
-       passoc x y z = record { peq = λ q → refl }
-       p-inv : {i j : Permutation p p} →  i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q
-       p-inv {i} {j} i=j q = begin
-           i ⟨$⟩ˡ q                      ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j)  )  ⟩
-           i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ cong (λ k  →  i ⟨$⟩ˡ k) (sym (peq i=j _ ))  ⟩
-           i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ inverseˡ i  ⟩
-           j ⟨$⟩ˡ q
-           ∎ where open ≡-Reasoning
-
-
--- a/Solvable.agda	Mon Aug 17 11:02:16 2020 +0900
+++ b/Solvable.agda	Mon Aug 17 11:30:12 2020 +0900
@@ -5,7 +5,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 Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
 open import Relation.Nullary
 open import Data.Empty
 open import Data.Product
@@ -45,7 +45,7 @@
      ε ⁻¹
    ∎ where open EqReasoning (Algebra.Group.setoid G)
 
-open import Data.List using ([] ; _∷_ ; List )
+open import Data.List using ([] ; _∷_ ; List ; length )
 
 data Node (A : Set n) : Set (Level.suc n) where
    leaf : A → Node A
@@ -54,7 +54,7 @@
 flatten : Node Carrier → List Carrier
 flatten x = flatten1 x [] where
    flatten1 : Node Carrier → List Carrier → List Carrier
-   flatten1 (leaf x)  y = x ∷ []
+   flatten1 (leaf x)  y = x ∷ y
    flatten1 (node left right)  y = flatten1 left (flatten1 right y )
 
 gnode : Node Carrier → Carrier
@@ -68,13 +68,20 @@
 
 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
+   gnot0 : ( left right : Node Carrier ) →  length (flatten (node left right) ) > 1
+   gnot0 (leaf x) (leaf x₁) = s≤s ( s≤s z≤n)
+   gnot0 (leaf x) (node q q₁) = {!!}
+   gnot0 (node p p₁) q = {!!}
    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 = {!!}
+   gpattern1 (node (leaf x) p₁) (node (leaf x₁) q₁) r p=r r=q = {!!}
+   gpattern1 (node (leaf x) p₁) (node (node q q₂) q₁) r p=r r=q = {!!}
+   gpattern1 (node (node p p₂) p₁) (node (leaf x) q₁) r p=r r=q = {!!}
+   gpattern1 (node (node p p₂) p₁) (node (node q 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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Symmetric.agda	Mon Aug 17 11:30:12 2020 +0900
@@ -0,0 +1,86 @@
+module Symmetric where
+
+open import Level hiding ( suc ; zero )
+open import Algebra
+open import Algebra.Structures
+open import Data.Fin
+open import Data.Product
+open import Data.Fin.Permutation
+open import Function hiding (id ; flip)
+open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
+open import Function.LeftInverse  using ( _LeftInverseOf_ )
+open import Function.Equality using (Π)
+open import Data.Nat using (ℕ; suc; zero)
+open import Relation.Binary.PropositionalEquality
+
+f1 : Fin 3 → Fin 3
+f1 zero = suc (suc zero)
+f1 (suc zero) = zero
+f1 (suc (suc zero)) = suc zero
+
+lemma1  : Permutation 3 3
+lemma1  = permutation f1 ( f1 ∘ f1 ) lemma2 where
+   lemma3 : (x : Fin 3 ) → f1 (f1 (f1 x)) ≡ x
+   lemma3 zero = refl
+   lemma3 (suc zero) = refl
+   lemma3 (suc (suc zero)) = refl
+   lemma2 : :→-to-Π (λ x → f1 (f1 x)) InverseOf :→-to-Π f1
+   lemma2 = record { left-inverse-of = λ x → lemma3 x ; right-inverse-of = λ x → lemma3 x }
+
+fid : {p : ℕ } → Fin p → Fin p
+fid x = x
+
+-- Data.Fin.Permutation.id
+pid : {p : ℕ } → Permutation p p
+pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
+
+-- Data.Fin.Permutation.flip
+pinv : {p : ℕ } → Permutation p p → Permutation p p
+pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }
+
+record _=p=_ {p : ℕ } ( x y : Permutation p p )  : Set where
+    field
+       peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q
+
+open _=p=_
+
+prefl : {p : ℕ } { x  : Permutation p p } → x =p= x
+peq (prefl {p} {x}) q = refl
+
+psym : {p : ℕ } { x y : Permutation p p } → x =p= y →  y =p= x
+peq (psym {p} {x} {y}  eq ) q = sym (peq eq q)
+
+ptrans : {p : ℕ } { x y z : Permutation p p } → x =p= y  → y =p= z →  x =p= z
+peq (ptrans {p} {x} {y} x=y y=z ) q = trans (peq x=y q) (peq y=z q)
+
+Symmetric : ℕ → Group  Level.zero Level.zero
+Symmetric p = record {
+      Carrier        = Permutation p p
+    ; _≈_            = _=p=_
+    ; _∙_            = _∘ₚ_
+    ; ε              = pid
+    ; _⁻¹            = pinv
+    ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
+       isEquivalence = record {refl = prefl ; trans = ptrans ; sym = psym }
+       ; ∙-cong = presp }
+       ; assoc = passoc }
+       ; identity = ( (λ q → record { peq = λ q → refl } ) , (λ q → record { peq = λ q → refl } ))  }
+       ; inverse   = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} ))  
+       ; ⁻¹-cong   = λ i=j → record { peq = λ q → p-inv i=j q }
+      }
+   } where
+       presp : {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v)
+       presp {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where
+           lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q)
+           lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
+       passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p=  (x ∘ₚ (y ∘ₚ z))
+       passoc x y z = record { peq = λ q → refl }
+       p-inv : {i j : Permutation p p} →  i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q
+       p-inv {i} {j} i=j q = begin
+           i ⟨$⟩ˡ q                      ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j)  )  ⟩
+           i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ cong (λ k  →  i ⟨$⟩ˡ k) (sym (peq i=j _ ))  ⟩
+           i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ inverseˡ i  ⟩
+           j ⟨$⟩ˡ q
+           ∎ where open ≡-Reasoning
+
+