Mercurial > hg > Members > kono > Proof > galois

changeset 22:ae586c068d01

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 Wed, 19 Aug 2020 02:02:17 +0900
parents 270b28c96154
children b133ef55b395
files Symmetric.agda
diffstat 1 files changed, 12 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/Symmetric.agda	Wed Aug 19 01:00:46 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 02:02:17 2020 +0900
@@ -110,11 +110,11 @@
    fn (suc n) zero _ = refl
    fn (suc n) (suc i) (s≤s i<n) = cong (λ k → suc k ) (fn (suc n) i (<-trans i<n a<sa ))
 
-record Pincl (i j : ℕ ) (p→i : Fin j → Fin j) : Set (Level.suc Level.zero ) where
+record Pincl (i j : ℕ ) (p→i : Fin (suc (suc j)) → Fin (suc (suc j))) : Set (Level.suc Level.zero ) where
    field
-     p←i     :  Fin j  → Fin j
-     piso←i  : ( x : Fin j ) → (i≤x : i ≤ toℕ x) → p←i ( p→i x) i≤x ≡ x
-     piso→i  : ( x : Fin j ) → (i≤x : i ≤ toℕ x) → p→i ( p←i i≤x x) ≡ x
+     p←i     : (x : Fin (suc (suc j)) )    → (i≤x : toℕ x < i )       → Fin (suc (suc j))
+     piso←i  : ( x : Fin (suc (suc j)) ) → (i≤x : toℕ (p→i x) < i ) → p←i (p→i x) i≤x   ≡ x
+     piso→i  : ( x : Fin (suc (suc j)) )   → (i≤x : toℕ x < i )       → p→i ( p←i x i≤x ) ≡ x
       
 
 fperm  : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
@@ -128,19 +128,15 @@
    p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
    p→ x | tri> ¬a ¬b c =  fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  )))
 
-   pincl : Pincl (suc (suc n)) (suc (suc n)) p→ 
-   pincl = pincl1 (suc n) ? ?  where
-     pincl1 : (i : ℕ ) → i < suc (suc n)  → Pincl i → Pincl (suc i)
-     pincl1 0 = ?
+   pincl : Pincl (suc (suc n)) n p→ 
+   pincl = pincl1 (suc (suc n)) {!!}  where
+     pincl1 : (i : ℕ ) → i < suc n  → Pincl i n p→ 
+     pincl1 0 _  = {!!}
+     pincl1 (suc i) i<n  = {!!}
 
    p← : Fin (suc (suc n)) → Fin (suc (suc n))
-   p← x = find (fromℕ≤ a<sa) where
-       find : (y : Fin (suc (suc n))) → Fin (suc (suc n))
-       find y with fcmp x ( p→ y )
-       find y | tri< a ¬b ¬c = {!!}
-       find y | tri≈ ¬a b ¬c = y
-       find y | tri> ¬a ¬b c = {!!}
+   p← x = Pincl.p←i pincl x {!!}
    piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
-   piso← x = {!!}
+   piso← x = Pincl.piso←i pincl  x fin<n
    piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
-   piso→ x = {!!}
+   piso→ x = Pincl.piso→i pincl x fin<n