Mercurial > hg > Members > kono > Proof > galois

changeset 321:7c6f665e687f

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 Thu, 21 Sep 2023 08:23:48 +0900
parents 8fb16f9a882a
children 933255f252ce
files src/Putil.agda
diffstat 1 files changed, 37 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/Putil.agda	Tue Sep 19 11:11:38 2023 +0900
+++ b/src/Putil.agda	Thu Sep 21 08:23:48 2023 +0900
@@ -502,14 +502,47 @@
    piso← : (x : Fin n ) → p→ ( p← x ) ≡ x
    piso← x = p02 _ _ refl refl  where
       p02 : (y z : Fin n) → p← x ≡ y → p→ y ≡ z → z ≡ x
-      p02 y z px=y py=z with <-fcmp (perm ⟨$⟩ˡ (suc x)) (# 0)
+      p02 y z px=y py=z with <-fcmp (perm ⟨$⟩ˡ (suc x)) (# 0) 
       ... | tri≈ ¬a b ¬c = ⊥-elim (sh2 perm p0=0 b)
-      ... | tri> ¬a ¬b c with <-fcmp (perm ⟨$⟩ʳ (suc y)) (# 0)
+      ... | tri> ¬a ¬b c with <-fcmp (perm ⟨$⟩ʳ (suc y)) (# 0) 
       ... | tri≈ ¬a₁ b ¬c = ⊥-elim (sh1 perm p0=0 b)
       ... | tri> ¬a₁ ¬b₁ c₁ = ? where
            open ≡-Reasoning 
-           p03 : toℕ (Inverse.to perm (suc x)) ≡ suc (toℕ y)
-           p03 = ?
+           p06 : fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc x)))} (p01 x c) ≡ y
+           p06 = px=y
+           p07 : fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc y)))} (p00 y c₁) ≡ z
+           p07 = py=z
+           p03 : toℕ (Inverse.from perm (suc x)) ≡ suc (toℕ y)
+           p03 = begin 
+              toℕ (Inverse.from perm (suc x))  ≡⟨ ? ⟩
+              suc (toℕ y) ∎ 
+           p04 : toℕ (Inverse.to perm (suc y)) ≡ suc (toℕ z)
+           p04 = ?
+           p05 : Inverse.to perm ( Inverse.from perm (suc x) ) ≡ suc x
+           p05 = inverseʳ perm  
+           p09 : Data.Nat.pred (toℕ (Inverse.to perm (suc (fromℕ< (p01 x c))))) < n
+           p09 = ? 
+           p11 : Data.Nat.pred (toℕ (Inverse.to perm (Inverse.from perm (suc x)))) < n
+           p11 = ?
+           p12 : toℕ (Inverse.to perm (suc (fromℕ< (p01 x c)))) ∸ 1 ≡ toℕ (Inverse.to perm (Inverse.from perm (suc x))) ∸ 1
+           p12 = ?
+           p13 : Data.Nat.pred (suc (toℕ x)) < n
+           p13 = ?
+           p10 : Data.Nat.pred (toℕ (Inverse.to perm (suc y))) ≡ Data.Nat.pred (toℕ (Inverse.to perm (suc (fromℕ< (p01 x c))))) 
+           p10 = cong (λ k → Data.Nat.pred (toℕ (Inverse.to perm (suc k)))) (sym px=y)
+           p14 : toℕ (Inverse.to perm (Inverse.from perm (suc x))) ∸ 1 ≡ toℕ x
+           p14 = ?
+           p08 : z ≡ x
+           p08 = begin
+             z ≡⟨ sym (py=z) ⟩
+             fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc y)))} (p00 y c₁)  
+                ≡⟨ lemma10 p10 ⟩
+             fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm 
+                (suc (fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc x)))} (p01 x c))))) } p09  ≡⟨ lemma10 p12 ⟩
+             fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (Inverse.from perm (suc x))) ) } p11  ≡⟨ lemma10 ? ⟩
+             fromℕ< {Data.Nat.pred (toℕ (suc x) ) } p13  ≡⟨ lemma10 refl  ⟩
+             fromℕ< {toℕ x} fin<n  ≡⟨ fromℕ<-toℕ _ _  ⟩
+             x ∎  
 
         -- with perm ⟨$⟩ˡ (suc x) in eq 
         -- ... | t = ?