Mercurial > hg > Members > kono > Proof > galois

changeset 66:442873eaf80b

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 Mon, 24 Aug 2020 14:40:11 +0900
parents aeb6b588db01
children 3825082ebdbd
files Putil.agda
diffstat 1 files changed, 9 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Mon Aug 24 14:20:51 2020 +0900
+++ b/Putil.agda	Mon Aug 24 14:40:11 2020 +0900
@@ -282,24 +282,25 @@
 -- FL←iso {0} perm = record { peq = λ () }
 -- FL←iso {suc n} perm = {!!}
 
+lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
+lem2 i≤n = ≤-trans i≤n ( refl-≤s )
+
 ∀-FL : {n : ℕ } → Fin n → List (FL n)
 ∀-FL  x  = ∀-FL1 x  where
-    ∀-FL2 : { n : ℕ } → Fin (suc n) → List (FL n)  → List (FL (suc n)) → List (FL (suc n))
-    ∀-FL2 zero [] t = t
-    ∀-FL2 zero (x ∷ fls) t = ∀-FL2 zero fls (( zero :: x )  ∷ t ) 
-    ∀-FL2 (suc x) [] t = t
-    ∀-FL2 (suc x) (y ∷ fls) t = ∀-FL2 (suc x) fls (( (suc x) :: y )  ∷ t ) 
+    ∀-FL2 : { n : ℕ } → Fin (suc n) → (i : ℕ ) → i ≤ n → List (FL n)  → List (FL (suc n)) → List (FL (suc n))
+    ∀-FL2 y zero z≤n [] t = t
+    ∀-FL2 y zero z≤n (x ∷ fls) t = ∀-FL2 y zero z≤n fls (( zero :: x )  ∷ t ) 
+    ∀-FL2 y (suc i) (s≤s lt) [] t = t
+    ∀-FL2 y (suc i) (s≤s lt) (fl ∷ fls) t = ∀-FL2 y i (lem2 lt) (fl ∷ fls) (( fromℕ≤ (s≤s (s≤s lt)) :: fl )  ∷ t ) 
     ∀-FL1 : {n : ℕ } → (Fin n) →  List (FL n) 
     ∀-FL1 zero    = []
-    ∀-FL1 (suc x) =  ∀-FL2 (suc x) ( ∀-FL1 x) []
+    ∀-FL1 (suc x) =  ∀-FL2 (suc x) (toℕ x) (≤-trans refl-≤s fin<n ) ( ∀-FL1 x) []
 
 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) )
 all-perm n = pls6 n where
    lem1 : {i n : ℕ } → i ≤ n → i < suc n
    lem1 z≤n = s≤s z≤n
    lem1 (s≤s lt) = s≤s (lem1 lt)
-   lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
-   lem2 i≤n = ≤-trans i≤n ( refl-≤s )
    pls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
    pls4 zero n i≤n perm x = (pprep perm ∘ₚ pins i≤n ) ∷ x
    pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (pprep perm ∘ₚ pins {n} {suc i} i≤n  ∷ x)