Mercurial > hg > Members > kono > Proof > galois

changeset 55:111c561ae90c

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 Sun, 23 Aug 2020 17:53:18 +0900
parents 8224694a4dda
children e26f784cd6b1
files Putil.agda
diffstat 1 files changed, 6 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Sun Aug 23 17:22:34 2020 +0900
+++ b/Putil.agda	Sun Aug 23 17:53:18 2020 +0900
@@ -140,17 +140,17 @@
        sh31 : toℕ x ≡ n
        sh31 = begin
            toℕ x 
-        ≡⟨ {!!}  ⟩
+        ≡⟨ sym fin+1-toℕ ⟩
             toℕ (fin+1 x)
         ≡⟨ cong (λ k → toℕ k ) (sym ( inverseʳ perm))  ⟩
             toℕ (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ (fin+1 x)))
-        ≡⟨ {!!}  ⟩
+        ≡⟨ cong (λ k →  toℕ (perm ⟨$⟩ʳ k )) (sym (toℕ→from eq)) ⟩
             toℕ (perm ⟨$⟩ʳ fromℕ n)
         ≡⟨ cong ( λ k → toℕ (perm ⟨$⟩ʳ k )) (sym pn=n) ⟩
             toℕ (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ (fromℕ n) ))
         ≡⟨ cong (λ k → toℕ k ) ( inverseʳ perm ) ⟩
             toℕ (fromℕ n)
-        ≡⟨ {!!}  ⟩
+        ≡⟨ toℕ-fromℕ _ ⟩
             n 
         ∎ where 
         open ≡-Reasoning
@@ -160,15 +160,15 @@
        sh41 : toℕ x ≡ n
        sh41 = begin
             toℕ x
-        ≡⟨ {!!}  ⟩
+        ≡⟨ sym fin+1-toℕ ⟩
             toℕ (fin+1 x)
         ≡⟨ cong (λ k → toℕ k ) (sym ( inverseˡ perm))  ⟩
             toℕ (perm ⟨$⟩ˡ (perm ⟨$⟩ʳ (fin+1 x)))
-        ≡⟨ {!!}  ⟩
+        ≡⟨ cong (λ k →  toℕ (perm ⟨$⟩ˡ k )) (sym (toℕ→from eq)) ⟩
             toℕ ((perm ⟨$⟩ˡ fromℕ n))
         ≡⟨ cong (λ k → toℕ k) pn=n ⟩
             toℕ (fromℕ n)
-        ≡⟨ {!!}  ⟩
+        ≡⟨ toℕ-fromℕ _ ⟩
             n 
         ∎ where 
         open ≡-Reasoning