Mercurial > hg > Members > kono > Proof > galois

changeset 322:933255f252ce

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:40:43 +0900
parents 7c6f665e687f
children 558c33f7f8e0
files src/Putil.agda
diffstat 1 files changed, 9 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/src/Putil.agda	Thu Sep 21 08:23:48 2023 +0900
+++ b/src/Putil.agda	Thu Sep 21 08:40:43 2023 +0900
@@ -508,39 +508,19 @@
       ... | tri≈ ¬a₁ b ¬c = ⊥-elim (sh1 perm p0=0 b)
       ... | tri> ¬a₁ ¬b₁ c₁ = ? where
            open ≡-Reasoning 
-           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 : {n : ℕ } → (y : Fin (suc n)) → (y<n : Data.Nat.pred (toℕ y) < n) → suc (fromℕ< y<n) ≡ y 
            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 = ?
+           p15 : toℕ (Inverse.to perm (suc y)) ∸ 1 ≡ toℕ x
+           p15 = begin
+              toℕ (Inverse.to perm (suc y)) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.to perm (suc k))  ∸ 1   ) (sym px=y) ⟩
+              toℕ (Inverse.to perm (suc (fromℕ< (p01 x c)))) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.to perm k)  ∸ 1) (p11 _ (p01 x c) ) ⟩
+              toℕ (Inverse.to perm (Inverse.from perm (suc x))) ∸ 1  ≡⟨ cong (λ k → toℕ k  ∸ 1) (inverseʳ perm) ⟩
+              toℕ (suc x) ∸ 1  ≡⟨ ? ⟩
+              toℕ x ∎
            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ℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc y)))} (p00 y c₁)  ≡⟨ lemma10 p15 ⟩
              fromℕ< {toℕ x} fin<n  ≡⟨ fromℕ<-toℕ _ _  ⟩
              x ∎