Mercurial > hg > Members > kono > Proof > galois
changeset 80:b0c344ece453
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 26 Aug 2020 18:19:40 +0900 |
| parents | 75e2dd8f4e00 |
| children | 59aaf2000591 |
| files | Putil.agda sym5.agda |
| diffstat | 2 files changed, 72 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/Putil.agda Wed Aug 26 12:31:04 2020 +0900 +++ b/Putil.agda Wed Aug 26 18:19:40 2020 +0900 @@ -13,7 +13,7 @@ open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) open import Data.Nat.Properties -- using (<-trans) open import Relation.Binary.PropositionalEquality -open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ) renaming (reverse to rev ) +open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev ) open import nat open import Symmetric @@ -22,6 +22,7 @@ open import Relation.Nullary open import Data.Empty open import Relation.Binary.Core +open import Relation.Binary.Definitions open import fin -- An inductive construction of permutation @@ -127,13 +128,61 @@ pins1 zero _ _ = pid pins1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j} (s≤s (s≤s si≤n)) ∘ₚ pins1 i j (≤-trans si≤n refl-≤s ) +plist1 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ +plist1 {n} perm zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ< {zero} (s≤s z≤n))) ∷ [] +plist1 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ< (s≤s lt))) ∷ plist1 perm i (<-trans lt a<sa) + plist : {n : ℕ} → Permutation n n → List ℕ plist {0} perm = [] -plist {suc j} perm = rev (plist1 j a<sa) where - n = suc j - plist1 : (i : ℕ ) → i < n → List ℕ - plist1 zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ< {zero} (s≤s z≤n))) ∷ [] - plist1 (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ< (s≤s lt))) ∷ plist1 i (<-trans lt a<sa) +plist {suc n} perm = rev (plist1 perm n a<sa) + +plist2 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ +plist2 {n} perm zero _ = toℕ ( perm ⟨$⟩ʳ (fromℕ< {zero} (s≤s z≤n))) ∷ [] +plist2 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ʳ (fromℕ< (s≤s lt))) ∷ plist2 perm i (<-trans lt a<sa) + +plist0 : {n : ℕ} → Permutation n n → List ℕ +plist0 {0} perm = [] +plist0 {suc n} perm = plist2 perm n a<sa + + +headeq : {A : Set } → {x y : A } → {xt yt : List A } → (x ∷ xt) ≡ (y ∷ yt) → x ≡ y +headeq refl = refl + +taileq : {A : Set } → {x y : A } → {xt yt : List A } → (x ∷ xt) ≡ (y ∷ yt) → xt ≡ yt +taileq refl = refl + +pleq : {n : ℕ} → (x y : Permutation n n ) → plist0 x ≡ plist0 y → x =p= y +pleq {0} x y refl = record { peq = λ q → pleq0 q } where + pleq0 : (q : Fin 0 ) → (x ⟨$⟩ʳ q) ≡ (y ⟨$⟩ʳ q) + pleq0 () +pleq {suc n} x y eq = record { peq = λ q → pleq1 n a<sa eq q fin<n } where + pleq1 : (i : ℕ ) → (i<sn : i < suc n ) → plist2 x i i<sn ≡ plist2 y i i<sn → (q : Fin (suc n)) → toℕ q < suc i → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q + pleq1 zero i<sn eq q (s≤s q<i) = {!!} + pleq1 (suc i) (s≤s i<sn) eq q q<i with <-cmp (toℕ q) (suc i) + ... | tri< a ¬b ¬c = pleq1 i (<-trans i<sn a<sa ) (taileq eq) q a + ... | tri≈ ¬a b ¬c = begin + x ⟨$⟩ʳ q + ≡⟨ cong (λ k → x ⟨$⟩ʳ k) (pleq3 b) ⟩ + x ⟨$⟩ʳ (suc (fromℕ< i<sn)) + ≡⟨ toℕ-injective pleq2 ⟩ + y ⟨$⟩ʳ (suc (fromℕ< i<sn)) + ≡⟨ cong (λ k → y ⟨$⟩ʳ k) (sym (pleq3 b)) ⟩ + y ⟨$⟩ʳ q + ∎ where + open ≡-Reasoning + pleq3 : toℕ q ≡ suc i → q ≡ suc (fromℕ< i<sn) + pleq3 tq=si = toℕ-injective ( begin + toℕ q + ≡⟨ b ⟩ + suc i + ≡⟨ sym (toℕ-fromℕ< (s≤s i<sn)) ⟩ + toℕ (fromℕ< (s≤s i<sn)) + ≡⟨⟩ + toℕ (suc (fromℕ< i<sn)) + ∎ ) where open ≡-Reasoning + pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) + pleq2 = headeq eq + ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c q<i ) data FL : (n : ℕ )→ Set where f0 : FL 0
--- a/sym5.agda Wed Aug 26 12:31:04 2020 +0900 +++ b/sym5.agda Wed Aug 26 18:19:40 2020 +0900 @@ -62,13 +62,17 @@ aec : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 aec i<3 j<4 = ins2 (pinv 3rot) i<3 j<4 + fin≤n : {n : ℕ} (f : Fin n) → toℕ f ≤ n + fin≤n {_} zero = z≤n + fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f) + record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) : Set where field dba0<3 : Fin 3 dba1<4 : Fin 4 aec0<3 : Fin 3 aec1<4 : Fin 4 - abc= : abc i<3 j<4 =p= [ dba (fin<n {3} {dba0<3}) (fin<n {4} {dba1<4}) , aec (fin<n {3} {aec0<3}) (fin<n {4} {aec1<4}) ] + abc= : abc i<3 j<4 =p= [ dba (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , aec (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] open Triple -- d e a b c @@ -114,7 +118,7 @@ tt8 = plist ( dba (fin<n {3} {# 0}) (fin<n {4} {# 3})) tt9 : fin<n {4} {# 3} ≡ n≤ 4 tt9 = refl - tta : fin<n {3} {# 0} ≡ n≤ 1 + tta : fin≤n {3} (# 1) ≡ n≤ 1 tta = refl triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 @@ -137,17 +141,17 @@ triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = {!!} triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = {!!} triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = {!!} - triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = ? - -- record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = ? } - -- tt7 : abc (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) =p= - -- [ dba (fin<n {3} {# 1})(fin<n {4} {# 4}) , aec (fin<n {3} {# 0}) (fin<n {4} {# 3}) ] - -- tt7 = record { peq = λ q → lll q } where - -- lll : (q : Fin 5) → {!!} - -- lll zero = {!!} - -- lll (suc zero) = refl - -- lll (suc (suc zero)) = {!!} - -- lll (suc (suc (suc zero))) = {!!} - -- lll (suc (suc (suc (suc zero)))) = refl + triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = + record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = tt7 } where + tt7 : abc (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) =p= + [ dba (fin≤n {3} (# 1))(fin≤n {4} (# 4)) , aec (fin≤n {3} (# 0)) (fin≤n {4} (# 3)) ] + tt7 = record { peq = λ q → lll q } where + lll : (q : Fin 5) → _ + lll zero = refl + lll (suc zero) = refl + lll (suc (suc zero)) = refl + lll (suc (suc (suc zero))) = refl + lll (suc (suc (suc (suc zero)))) = refl dervie-any-3rot : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (abc i<3 j<4 )