Mercurial > hg > Members > kono > Proof > galois

changeset 102:00a711f99096

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 Tue, 01 Sep 2020 12:11:11 +0900
parents 92f3c9b926bd
children 7595ee384b3d
files Putil.agda
diffstat 1 files changed, 13 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Tue Sep 01 08:27:40 2020 +0900
+++ b/Putil.agda	Tue Sep 01 12:11:11 2020 +0900
@@ -296,11 +296,20 @@
 
 px=x : {n : ℕ }  → (x : Fin (suc n)) → pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) ≡ x
 px=x {n} zero = refl
-px=x {suc n} (suc x) = p001 (# 0) x refl where
-     pprev : {!!} -- pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) ≡ x
+px=x {suc n} (suc x) = trans p001 (cong suc pprev ) where
+     pprev : pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) ≡ x
      pprev = px=x x
-     p001 : (x m : Fin (suc n))  → x ≡ # 0  → (pins (toℕ≤pred[n] (suc m)) ⟨$⟩ʳ x) ≡ (suc m)
-     p001 x m eq = {!!}
+     m<n : toℕ x ≤ n
+     m<n = toℕ≤pred[n] x
+     p001 :  (pins (toℕ≤pred[n] (suc x)) ⟨$⟩ʳ (# 0)) ≡ suc (pins (toℕ≤pred[n] x) ⟨$⟩ʳ (# 0))
+     p001 with <-cmp 0 (toℕ (Data.Fin.pred x))
+     ... | tri< a ¬b ¬c = cong suc ?
+     ... | tri≈ ¬a b ¬c = cong suc ?
+--      p001 = cong suc ( begin
+--            fromℕ< (≤-pred (s≤s (s≤s (toℕ≤pred[n] x))))
+--         ≡⟨ {!!} ⟩
+--            pins (toℕ≤pred[n] x) ⟨$⟩ʳ (# 0)
+--         ∎ )
 
 
 -- pp : {n : ℕ }  → (perm : Permutation (suc n) (suc n) ) →  Fin (suc n)