Mercurial > hg > Members > kono > Proof > galois

changeset 91:482ef04890f8

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 Sat, 29 Aug 2020 07:48:45 +0900
parents bb8c5b366219
children 2e5d0b142eca
files Putil.agda fin.agda nat.agda
diffstat 3 files changed, 57 insertions(+), 30 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Fri Aug 28 22:20:39 2020 +0900
+++ b/Putil.agda	Sat Aug 29 07:48:45 2020 +0900
@@ -131,9 +131,10 @@
     pins1 : (i j : ℕ ) → j ≤ suc (suc n)  → Permutation (suc (suc (suc n ))) (suc (suc (suc n)))
     pins1 _ zero _ = pid
     pins1 zero _ _ = pid
-    pins1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j}  (s≤s (s≤s si≤n))  ∘ₚ  pins1 i j (≤-trans si≤n refl-≤s ) 
+    pins1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j}  (s≤s (s≤s si≤n))  ∘ₚ  pins1 i j (≤-trans si≤n a≤sa ) 
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+open ≡-Reasoning
 
 pins'  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
 pins' {_} {zero} _ = pid
@@ -141,7 +142,7 @@
 
    next : Fin (suc (suc n)) → Fin (suc (suc n))
    next zero = suc zero
-   next (suc x) = fromℕ< (≤-trans (fin<n {_} {x} ) refl-≤s )
+   next (suc x) = fromℕ< (≤-trans (fin<n {_} {x} ) a≤sa )
 
    p→ : Fin (suc (suc n)) → Fin (suc (suc n)) 
    p→ x with <-cmp (toℕ x) (suc m)
@@ -152,51 +153,56 @@
    p← : Fin (suc (suc n)) → Fin (suc (suc n)) 
    p← zero = fromℕ< (s≤s (s≤s m≤n))
    p← (suc x) with <-cmp (toℕ x) (suc m)
-   ... | tri< a ¬b ¬c = fromℕ< (≤-trans (fin<n {_} {x}) refl-≤s )
+   ... | tri< a ¬b ¬c = fromℕ< (≤-trans (fin<n {_} {x}) a≤sa )
    ... | tri≈ ¬a b ¬c = suc x
    ... | tri> ¬a ¬b c = suc x
 
    mm : toℕ (fromℕ< {suc m} {suc (suc n)} (s≤s (s≤s m≤n))) ≡ suc m 
    mm = toℕ-fromℕ< (s≤s (s≤s  m≤n)) 
 
-   mma : (x : Fin (suc n) ) → suc (toℕ x) ≤ suc m → toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) refl-≤s ) ) ≤ m
-   mma x (s≤s x<sm) = subst (λ k → k ≤ m) (sym (toℕ-fromℕ< (≤-trans fin<n refl-≤s ) )) x<sm
+   mma : (x : Fin (suc n) ) → suc (toℕ x) ≤ suc m → toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) a≤sa ) ) ≤ m
+   mma x (s≤s x<sm) = subst (λ k → k ≤ m) (sym (toℕ-fromℕ< (≤-trans fin<n a≤sa ) )) x<sm
    
+   p3 : (x : Fin (suc n) ) →  toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s a≤sa))) ≡ suc (toℕ x)
+   p3 x = begin
+            toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s a≤sa)))
+          ≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans fin<n  a≤sa ) ) ⟩
+            suc (toℕ x)
+          ∎ 
    piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x
    piso← zero with <-cmp (toℕ (fromℕ< (s≤s (s≤s m≤n)))) (suc m) | mm
    ... | tri< a ¬b ¬c | t = ⊥-elim ( ¬b t )
    ... | tri≈ ¬a b ¬c | t = refl
    ... | tri> ¬a ¬b c | t = ⊥-elim ( ¬b t )
    piso← (suc x) with <-cmp (toℕ x) (suc m)
-   ... | tri≈ ¬a b ¬c = ?
-   ... | tri> ¬a ¬b c = {!!}
-   ... | tri< a ¬b ¬c with <-cmp (toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) refl-≤s ) )) (suc m)
+   ... | tri> ¬a ¬b c with <-cmp (toℕ (suc x)) (suc m)
+   ... | tri< a ¬b₁ ¬c = ⊥-elim ( nat-<> a (<-trans c a<sa ) )
+   ... | tri≈ ¬a₁ b ¬c = ⊥-elim (  nat-≡< (sym b) (<-trans c a<sa ))
+   ... | tri> ¬a₁ ¬b₁ c₁ = refl
+   piso← (suc x) | tri≈ ¬a b ¬c with <-cmp (toℕ (suc x)) (suc m)
+   ... | tri< a ¬b ¬c₁ = ⊥-elim (  nat-≡< b (<-trans a<sa a) ) 
+   ... | tri≈ ¬a₁ refl ¬c₁ = ⊥-elim ( nat-≡< b a<sa )
+   ... | tri> ¬a₁ ¬b c = refl
+   piso← (suc x) | tri< a ¬b ¬c with <-cmp (toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) a≤sa ) )) (suc m)
    ... | tri≈ ¬a b ¬c₁ = ⊥-elim ( ¬a (s≤s (mma x a)))
    ... | tri> ¬a ¬b₁ c = ⊥-elim ( ¬a (s≤s (mma x a)))
    ... | tri< a₁ ¬b₁ ¬c₁ = p0 where
        p2 : suc (suc (toℕ x)) ≤ suc (suc n)
        p2 = s≤s (fin<n {suc n} {x})
-       p6 : suc (toℕ (fromℕ< (≤-trans (fin<n {_} {suc x}) (s≤s refl-≤s)))) ≤ suc (suc n)
+       p6 : suc (toℕ (fromℕ< (≤-trans (fin<n {_} {suc x}) (s≤s a≤sa)))) ≤ suc (suc n)
        p6 = s≤s (≤-trans a₁ (s≤s m≤n))
-
-       p3 :   toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s refl-≤s))) ≡ suc (toℕ x)
-       p3 = begin
-            toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s refl-≤s)))
-          ≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans fin<n  refl-≤s ) ) ⟩
-            suc (toℕ x)
-          ∎ where open ≡-Reasoning
        p0 : fromℕ< (≤-trans (s≤s  a₁) (s≤s (s≤s  m≤n) ))  ≡ suc x
        p0 = begin
              fromℕ< (≤-trans (s≤s  a₁) (s≤s (s≤s  m≤n) ))
           ≡⟨⟩
              fromℕ< (s≤s (≤-trans a₁ (s≤s m≤n))) 
-          ≡⟨ lemma10 p3 {p6} {p2} ⟩
+          ≡⟨ lemma10 (p3 x) {p6} {p2} ⟩
              fromℕ< ( s≤s (fin<n {suc n} {x}) )
-          ≡⟨ lemma3 {toℕ x} {suc n} (fin<n {suc (n)} {x})  ⟩
+          ≡⟨⟩
              suc (fromℕ< (fin<n {suc n} {x} )) 
-          ≡⟨ cong suc (fromℕ<-toℕ x (fin<n {suc n} {x}) ) ⟩
+          ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
              suc x
-          ∎ where open ≡-Reasoning
+          ∎ 
 
 
    piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
@@ -252,8 +258,7 @@
           y ⟨$⟩ʳ zero
        ≡⟨ cong ( λ k → y ⟨$⟩ʳ k ) (sym (toℕ-injective b )) ⟩
           y ⟨$⟩ʳ q
-       ∎ where
-          open ≡-Reasoning
+       ∎ 
   pleq1 (suc i) (s≤s i<sn) eq q q<i with <-cmp (toℕ q) (suc i)
   ... | tri< a ¬b ¬c = pleq1 i (<-trans i<sn a<sa ) (taileq eq) q a
   ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c q<i )
@@ -266,7 +271,6 @@
        ≡⟨ cong (λ k → y ⟨$⟩ʳ k) (sym (pleq3 b)) ⟩
             y ⟨$⟩ʳ q
        ∎ where
-          open ≡-Reasoning
           pleq3 : toℕ q ≡ suc i → q ≡ suc (fromℕ< i<sn)
           pleq3 tq=si = toℕ-injective ( begin
                   toℕ  q
@@ -276,7 +280,7 @@
                   toℕ (fromℕ< (s≤s i<sn))
                ≡⟨⟩
                   toℕ (suc (fromℕ< i<sn))
-               ∎ ) where open ≡-Reasoning
+               ∎ ) 
           pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) )
           pleq2 = headeq eq
 
@@ -292,7 +296,7 @@
           suc ( y ⟨$⟩ʳ q )
         ≡⟨⟩
           pprep y ⟨$⟩ʳ suc q
-        ∎  where open ≡-Reasoning
+        ∎  
 
 pprep-dist : {n  : ℕ} → {x y : Permutation n n } → pprep (x ∘ₚ y) =p= (pprep x ∘ₚ pprep y)
 pprep-dist {n} {x} {y} = record { peq = pprep-dist1 } where
@@ -313,7 +317,7 @@
           suc (suc (y ⟨$⟩ʳ q))
         ≡⟨⟩
           pswap y ⟨$⟩ʳ suc (suc q)
-        ∎  where open ≡-Reasoning
+        ∎  
  
 pswap-dist : {n  : ℕ} → {x y : Permutation n n } → pprep (pprep (x ∘ₚ y)) =p= (pswap x ∘ₚ pswap y)
 pswap-dist {n} {x} {y} = record { peq = pswap-dist1 } where
@@ -473,13 +477,13 @@
 -- FL←iso {suc n} perm = {!!}
 
 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
-lem2 i≤n = ≤-trans i≤n ( refl-≤s )
+lem2 i≤n = ≤-trans i≤n ( a≤sa )
 
 ∀-FL : (n : ℕ ) → List (FL (suc n))
 ∀-FL  x  = fls6 x  where
    fls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → FL  n → List (FL  (suc n))  → List (FL  (suc n)) 
    fls4 zero n i≤n perm x = (zero :: perm ) ∷ x
-   fls4 (suc i) n i≤n  perm x = fls4 i n (≤-trans refl-≤s i≤n ) perm ((fromℕ< (s≤s i≤n) :: perm ) ∷ x)
+   fls4 (suc i) n i≤n  perm x = fls4 i n (≤-trans a≤sa i≤n ) perm ((fromℕ< (s≤s i≤n) :: perm ) ∷ x)
    fls5 :  ( n : ℕ ) → List (FL n) → List (FL  (suc n))  → List (FL (suc n)) 
    fls5 n [] x = x
    fls5 n (h ∷ x) y = fls5  n x (fls4 n n lem0 h y)
@@ -494,7 +498,7 @@
    lem1 (s≤s lt) = s≤s (lem1 lt)
    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)
+   pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans a≤sa i≤n ) perm (pprep perm ∘ₚ pins {n} {suc i} i≤n  ∷ x)
    pls5 :  ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
    pls5 n [] x = x
    pls5 n (h ∷ x) y = pls5  n x (pls4 n n lem0 h y)
--- a/fin.agda	Fri Aug 28 22:20:39 2020 +0900
+++ b/fin.agda	Sat Aug 29 07:48:45 2020 +0900
@@ -18,10 +18,12 @@
 <→m≤n {suc m} {zero} ()
 <→m≤n {suc m} {suc n} (s≤s lt) = s≤s (<→m≤n lt)
 
+-- toℕ<n
 fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
 fin<n {_} {zero} = s≤s z≤n
 fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
 
+-- toℕ≤n
 fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n
 fin≤n {_} zero = z≤n
 fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f)
@@ -30,14 +32,17 @@
 pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n
 pred<n {suc n} {suc f} (s≤s z≤n) = fin<n
 
+-- fromℕ<-toℕ
 toℕ→from : {n : ℕ} {x : Fin (suc n)} → toℕ x ≡ n → fromℕ n ≡ x
 toℕ→from {0} {zero} refl = refl
 toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq ))
 
+-- toℕ-injective
 i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
 i=j {suc n} zero zero refl = refl
 i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) )
 
+-- raise 1
 fin+1 :  { n : ℕ } → Fin n → Fin (suc n)
 fin+1  zero = zero 
 fin+1  (suc x) = suc (fin+1 x)
@@ -67,25 +72,39 @@
 fin-1-xs zero ne = ⊥-elim ( ne refl )
 fin-1-xs (suc x) ne = refl
 
+-- suc-injective
 -- suc-eq : {n : ℕ } {x y : Fin n} → Fin.suc x ≡ Fin.suc y  → x ≡ y
 -- suc-eq {n} {x} {y} eq = subst₂ (λ j k → j ≡ k ) {!!} {!!} (cong (λ k → Data.Fin.pred k ) eq )
 
+-- this is refl
 lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
 lemma3 (s≤s lt) = refl
+
+-- fromℕ<-toℕ 
 lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ< n<m 
 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
-lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3 n<m) ) ( cong ( λ k → suc k ) ( lemma12 {n} {m} n<m f refl  ) )
+lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl =  cong suc ( lemma12 {n} {m} n<m f refl  ) 
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 open import Data.Fin.Properties
 
+-- <-irrelevant
+<-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
+<-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
+<-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl  )
+
 lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
 lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
 lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )
+
+-- fromℕ<-irrelevant 
 lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
 lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl  ))
+
 lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
 lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
+
+-- toℕ-fromℕ<
 lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
 lemma11 {n} {m} {x} n<m  = begin
               toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
--- a/nat.agda	Fri Aug 28 22:20:39 2020 +0900
+++ b/nat.agda	Sat Aug 29 07:48:45 2020 +0900
@@ -34,6 +34,10 @@
 refl-≤s {zero} = z≤n
 refl-≤s {suc x} = s≤s (refl-≤s {x})
 
+a≤sa : {x : ℕ } → x ≤ suc x
+a≤sa {zero} = z≤n
+a≤sa {suc x} = s≤s (a≤sa {x})
+
 =→¬< : {x : ℕ  } → ¬ ( x < x )
 =→¬< {zero} ()
 =→¬< {suc x} (s≤s lt) = =→¬< lt