Mercurial > hg > Members > kono > Proof > galois
changeset 86:c5329963c583
(x : Permutation 1 1 ) → x =p= pid
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 27 Aug 2020 08:29:56 +0900 |
| parents | 2d79a2c06c6c |
| children | c68956f6c3ad |
| files | Putil.agda sym5.agda |
| diffstat | 2 files changed, 30 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/Putil.agda Thu Aug 27 01:19:32 2020 +0900 +++ b/Putil.agda Thu Aug 27 08:29:56 2020 +0900 @@ -146,6 +146,9 @@ open _=p=_ +-- +-- plist cong +-- ←pleq : {n : ℕ} → (x y : Permutation n n ) → x =p= y → plist0 x ≡ plist0 y ←pleq {zero} x y eq = refl ←pleq {suc n} x y eq = ←pleq1 n a<sa where @@ -159,6 +162,9 @@ taileq : {A : Set } → {x y : A } → {xt yt : List A } → (x ∷ xt) ≡ (y ∷ yt) → xt ≡ yt taileq refl = refl +-- +-- plist equalizer +-- 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) @@ -204,6 +210,29 @@ pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) pleq2 = headeq eq +pprep-cong : {n : ℕ} → (x y : Permutation n n ) → x =p= y → pprep x =p= pprep y +pprep-cong {n} x y x=y = {!!} where + pprep-cong02 : (x : Permutation 1 1 ) → (q : Fin 1) → (x ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) + pprep-cong02 x zero with x ⟨$⟩ʳ zero | inspect (_⟨$⟩ʳ_ x) zero + ... | zero | record { eq = e } = refl + pprep-cong01 : (x : Permutation 1 1 ) → x =p= pid + pprep-cong01 x = record { peq = pprep-cong02 x } + pprep-cong0 : (n : ℕ) → (x : Permutation (suc n) (suc n) ) → toℕ (x ⟨$⟩ʳ fromℕ< a<sa ) ≡ n + pprep-cong0 zero x = begin + toℕ (x ⟨$⟩ʳ fromℕ< a<sa) + ≡⟨⟩ + toℕ (x ⟨$⟩ʳ zero) + ≡⟨ cong (λ k → toℕ k) (pprep-cong02 x zero) ⟩ + toℕ {suc zero} zero + ≡⟨⟩ + zero + ∎ where open ≡-Reasoning + pprep-cong0 (suc n) x = {!!} + t1 = plist0 (pprep (pid {3})) + pprep-cong1 : (n : ℕ) → (x : Permutation n n ) → plist0 (pprep x) ≡ n ∷ plist0 x + pprep-cong1 zero x = refl + pprep-cong1 (suc n) x = {!!} + data FL : (n : ℕ )→ Set where f0 : FL 0 _::_ : { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)