Mercurial > hg > Members > kono > Proof > galois

changeset 323:558c33f7f8e0

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 Fri, 22 Sep 2023 08:22:56 +0900
parents 933255f252ce
children 42eeb9f299eb
files src/Putil.agda
diffstat 1 files changed, 43 insertions(+), 44 deletions(-) [+]
line wrap: on
line diff
--- a/src/Putil.agda	Thu Sep 21 08:40:43 2023 +0900
+++ b/src/Putil.agda	Fri Sep 22 08:22:56 2023 +0900
@@ -498,6 +498,24 @@
    p← x | tri≈ ¬a b ¬c = ⊥-elim (sh2 perm p0=0 b)
    p← x | tri> ¬a ¬b c = fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc x)))} (p01 x c)
 
+   p11 : {n : ℕ } → (y : Fin (suc n)) → 0 < toℕ y → (y<n : Data.Nat.pred (toℕ y) < n) → suc (fromℕ< y<n) ≡ y 
+   p11 {.(suc _)} zero () (s≤s z≤n)
+   p11 {suc n} (suc zero) 0<y (s≤s z≤n) = refl
+   p11 {suc n} (suc (suc y)) 0<y y<n = p13 where
+      p14 : toℕ (suc y) < suc n
+      p14 = y<n
+      sy<n : Data.Nat.pred (toℕ (suc y)) < n
+      sy<n = px≤py ( begin 
+         suc (suc (toℕ y))  ≡⟨ refl ⟩
+         suc (toℕ (suc y))  ≤⟨ p14 ⟩
+         suc n  ∎ ) where open ≤-Reasoning 
+      p12 : suc (fromℕ< sy<n ) ≡ suc y 
+      p12 = p11 (suc y) (s≤s z≤n) sy<n
+      p16 : fromℕ< y<n ≡ suc (fromℕ< sy<n)
+      p16 = lemma10 refl 
+      p13 : suc (fromℕ< y<n) ≡ suc (suc y)
+      p13 = cong suc (trans p16 p12  )
+
    --  using "with" something binded in ≡ is prohibited
    piso← : (x : Fin n ) → p→ ( p← x ) ≡ x
    piso← x = p02 _ _ refl refl  where
@@ -506,16 +524,14 @@
       ... | tri≈ ¬a b ¬c = ⊥-elim (sh2 perm p0=0 b)
       ... | 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
+      ... | tri> ¬a₁ ¬b₁ c₁ = p08 where
            open ≡-Reasoning 
-           p11 : {n : ℕ } → (y : Fin (suc n)) → (y<n : Data.Nat.pred (toℕ y) < n) → suc (fromℕ< y<n) ≡ y 
-           p11 = ?
            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 (suc (fromℕ< (p01 x c)))) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.to perm k)  ∸ 1) (p11 _ c (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ℕ (suc x) ∸ 1  ≡⟨ refl ⟩
               toℕ x ∎
            p08 : z ≡ x
            p08 = begin
@@ -524,46 +540,29 @@
              fromℕ< {toℕ x} fin<n  ≡⟨ fromℕ<-toℕ _ _  ⟩
              x ∎  
 
-        -- with perm ⟨$⟩ˡ (suc x) in eq 
-        -- ... | t = ?
---        ... | zero = ⊥-elim ( sh2 perm p0=0 {y} eq )
---        ... | suc s with perm ⟨$⟩ˡ (suc x) in eq1
---        ... | zero = ⊥-elim ( sh1 perm p0=0 eq1 )
---        ... | suc t1 = begin
---             ? ≡⟨ ? ⟩
---             ? ∎  where
---              open ≡-Reasoning
---              plem0 :  suc t1 ≡ suc x → t1 ≡ x
---              plem0 refl = refl
---              plem1 :  suc t1 ≡ suc x
---              plem1 = begin
---                   suc t1                                  ≡⟨ sym eq1 ⟩
---                   Inverse.to perm  _                      ≡⟨ cong (λ k →  Inverse.to perm k ) (sym ?) ⟩
---                   Inverse.to perm ( Inverse.from perm _ ) ≡⟨ inverseʳ perm   ⟩
---                   suc x
---                ∎ 
--- 
    piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x
-   piso→ x = ?
---   with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x)
---   piso→ x | zero  | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e )
---   piso→ x | suc t | _ with perm ⟨$⟩ˡ (suc t) | inspect (_⟨$⟩ˡ_ perm ) (suc t)
---   piso→ x | suc t | _ | zero |  record { eq = e } =  ⊥-elim ( sh2 perm p0=0 e )
---   piso→ x | suc t |  record { eq = e0 } | suc t1 |  record { eq = e1 } = begin
---          t1
---       ≡⟨ plem2 plem3 ⟩
---          x
---       ∎ where
---          plem2 :  suc t1 ≡ suc x → t1 ≡ x
---          plem2 refl = refl
---          plem3 :  suc t1 ≡ suc x
---          plem3 = begin
---               suc t1 ≡⟨ sym e1 ⟩
---               Inverse.from perm (suc t)  ≡⟨ cong (λ k →  Inverse.from perm k ) (sym e0 ) ⟩
---               Inverse.from perm ((Inverse.to perm (suc x)) ) ≡⟨ cong (λ k →  Inverse.from perm (Inverse.to perm (suc x)) ) (sym e0 ) ⟩
---               Inverse.from perm ( Inverse.to perm  _ ) ≡⟨ inverseˡ perm   ⟩
---               suc 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) 
+      ... | tri≈ ¬a b ¬c = ⊥-elim (sh1 perm p0=0 b)
+      ... | tri> ¬a ¬b c with <-fcmp (perm ⟨$⟩ˡ (suc y)) (# 0) 
+      ... | tri≈ ¬a₁ b ¬c = ⊥-elim (sh2 perm p0=0 b)
+      ... | tri> ¬a₁ ¬b₁ c₁ = p08 where
+           open ≡-Reasoning 
+           p15 : toℕ (Inverse.from perm (suc y)) ∸ 1 ≡ toℕ x
+           p15 = begin
+              toℕ (Inverse.from perm (suc y)) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.from perm (suc k))  ∸ 1   ) (sym px=y) ⟩
+              toℕ (Inverse.from perm (suc (fromℕ< (p00 x c)))) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.from perm k)  ∸ 1) (p11 _ c (p00 x c) ) ⟩
+              toℕ (Inverse.from perm (Inverse.to perm (suc x))) ∸ 1  ≡⟨ cong (λ k → toℕ k  ∸ 1) (inverseˡ perm) ⟩
+              toℕ (suc x) ∸ 1  ≡⟨ refl ⟩
+              toℕ x ∎
+           p08 : z ≡ x
+           p08 = begin
+             z ≡⟨ sym (py=z) ⟩
+             fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc y)))} (p01 y c₁)  ≡⟨ lemma10 p15 ⟩
+             fromℕ< {toℕ x} fin<n  ≡⟨ fromℕ<-toℕ _ _  ⟩
+             x ∎  
+
 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm)  refl =p=  perm
 shrink-iso {n} {perm} = record { peq = λ q → ? }