Mercurial > hg > Members > kono > Proof > galois

changeset 329:5d7a811ee428

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, 24 Sep 2023 18:10:44 +0900
parents e9de2bfef88d
children 1ff0b95e437f
files Galois.agda-lib src/FLComm.agda src/Putil.agda src/fin.agda src/logic.agda
diffstat 5 files changed, 62 insertions(+), 41 deletions(-) [+]
line wrap: on
line diff
--- a/Galois.agda-lib	Sat Sep 23 22:43:47 2023 +0900
+++ b/Galois.agda-lib	Sun Sep 24 18:10:44 2023 +0900
@@ -1,5 +1,5 @@
 name: Galois
-depend: standard-library
+depend: standard-library-2.0
 include: src 
 flags:
   --warning=noUnsupportedIndexedMatch
--- a/src/FLComm.agda	Sat Sep 23 22:43:47 2023 +0900
+++ b/src/FLComm.agda	Sun Sep 24 18:10:44 2023 +0900
@@ -131,7 +131,7 @@
      anyC = anyComm (anyFL05 a<sa) (allFL (anyFL01 n)) (λ p q → FLpos p :: q )
      anyFL02 : (x : FL (suc (suc n))) → Any (_≡_ x) (commList anyC)
      anyFL02 (x :: y) = commAny anyC (x :: FL0) y
-                       (subst (λ k → Any (_≡_ (k :: FL0) ) _) (fromℕ<-toℕ _ _) (anyFL06 a<sa (fromℕ< x≤n) fin<n) ) (anyP (anyFL01 n) y) where
+                       (subst (λ k → Any (_≡_ (k :: FL0) ) _) (fromℕ<-toℕ _ _) (anyFL06 a<sa (fromℕ< x≤n) (fin<n _)) ) (anyP (anyFL01 n) y) where
          x≤n : suc (toℕ x)  ≤ suc (suc n)
          x≤n = toℕ<n x
 
--- a/src/Putil.agda	Sat Sep 23 22:43:47 2023 +0900
+++ b/src/Putil.agda	Sun Sep 24 18:10:44 2023 +0900
@@ -128,7 +128,7 @@
 
    next : Fin (suc (suc n)) → Fin (suc (suc n))
    next zero = suc zero
-   next (suc x) = fromℕ< (≤-trans (fin<n {_} {x} ) a≤sa )
+   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)
@@ -139,20 +139,20 @@
    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}) a≤sa )
+   ... | 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}) a≤sa ) ) ≤ m
-   mma x (s≤s x<sm) = subst (λ k → k ≤ m) (sym (toℕ-fromℕ< (≤-trans fin<n a≤sa ) )) 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 : 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 ) ) ⟩
+            toℕ (fromℕ< (≤-trans (fin<n {_} (suc x) ) (s≤s a≤sa)))
+          ≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans (fin<n _) a≤sa ) ) ⟩
             suc (toℕ x)
           ∎ where open ≡-Reasoning
 
@@ -191,11 +191,11 @@
           p15 : p← (suc y) ≡ suc x
           p15 with <-cmp (toℕ y) (suc m) -- eq : suc y ≡ suc (suc (fromℕ< (≤-pred (≤-trans a (s≤s m≤n))))) ,  a : suc x < suc m
           ... | tri< a₁ ¬b ¬c = p11 where
-            p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x
+            p11 : fromℕ< (≤-trans (fin<n {_} y) a≤sa ) ≡ suc x
             p11 = begin
-               fromℕ< (≤-trans (fin<n {_} {y}) a≤sa )
-              ≡⟨ lemma10 {suc (suc n)} {_} {_} p12 {≤-trans (fin<n {_} {y}) a≤sa} {s≤s (fin<n {suc n} {x} )}  ⟩
-               suc (fromℕ< (fin<n {suc n} {x} )) 
+               fromℕ< (≤-trans (fin<n {_} y) a≤sa )
+              ≡⟨ lemma10 {suc (suc n)} {_} {_} p12 {≤-trans (fin<n {_} y) a≤sa} {s≤s (fin<n {suc n} x )}  ⟩
+               suc (fromℕ< (fin<n {suc n} x )) 
               ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
                suc x
               ∎ where open ≡-Reasoning
@@ -216,13 +216,13 @@
    ... | 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)
+   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 a≤sa)))) ≤ suc (suc n)
+       p2 = s≤s (fin<n {suc n} x)
+       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))
        p0 : fromℕ< (≤-trans (s≤s  a₁) (s≤s (s≤s  m≤n) ))  ≡ suc x
        p0 = begin
@@ -230,9 +230,9 @@
           ≡⟨⟩
              fromℕ< (s≤s (≤-trans a₁ (s≤s m≤n))) 
           ≡⟨ lemma10 {suc (suc n)} (p3 x) {p6} {p2} ⟩
-             fromℕ< ( s≤s (fin<n {suc n} {x}) )
+             fromℕ< ( s≤s (fin<n {suc n} x) )
           ≡⟨⟩
-             suc (fromℕ< (fin<n {suc n} {x} )) 
+             suc (fromℕ< (fin<n {suc n} x )) 
           ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
              suc x
           ∎ where open ≡-Reasoning
@@ -364,7 +364,7 @@
 pleq  {0} x y refl = record { peq = λ q → pleq0 q } where
   pleq0 : (q : Fin 0 ) → (x ⟨$⟩ʳ q) ≡ (y ⟨$⟩ʳ q)
   pleq0 ()
-pleq  {suc n} x y eq = record { peq = λ q → pleq1 n a<sa eq q fin<n } where
+pleq  {suc n} x y eq = record { peq = λ q → pleq1 n a<sa eq q (fin<n _) } where
   pleq1 : (i : ℕ ) → (i<sn : i < suc n ) →  plist2 x i i<sn ≡ plist2 y i i<sn → (q : Fin (suc n)) → toℕ q < suc i → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q
   pleq1 zero i<sn eq q q<i with  <-cmp (toℕ q) zero
   ... | tri< () ¬b ¬c
@@ -500,7 +500,7 @@
      → Data.Nat.pred (toℕ x) < n
 0<x→px<n {n} x c = sx≤py→x≤y ( begin
      suc (suc (Data.Nat.pred (toℕ x))) ≡⟨ cong suc (sucprd c) ⟩
-     suc (toℕ x) <⟨ fin<n ⟩
+     suc (toℕ x) <⟨ fin<n _  ⟩
      suc n ∎ ) where
         open Data.Nat.Properties.≤-Reasoning
 
@@ -508,7 +508,7 @@
        → Data.Nat.pred (toℕ (Inverse.to perm (suc x))) < n
 sh1p<n {n} perm x c = sx≤py→x≤y ( begin
      suc (suc (Data.Nat.pred (toℕ (Inverse.to perm (suc x))))) ≡⟨ cong suc (sucprd c) ⟩
-     suc (toℕ (Inverse.to perm (suc x))) ≤⟨ fin<n ⟩
+     suc (toℕ (Inverse.to perm (suc x))) ≤⟨ fin<n _ ⟩
      suc n ∎ ) where
         open Data.Nat.Properties.≤-Reasoning
 
@@ -516,7 +516,7 @@
        → Data.Nat.pred (toℕ (Inverse.from perm (suc x))) < n
 sh2p<n {n} perm x c = sx≤py→x≤y ( begin
      suc (suc (Data.Nat.pred (toℕ (Inverse.from perm (suc x))))) ≡⟨ cong suc (sucprd c) ⟩
-     suc (toℕ (Inverse.from perm (suc x))) ≤⟨ fin<n ⟩
+     suc (toℕ (Inverse.from perm (suc x))) ≤⟨ fin<n  _ ⟩
      suc n ∎ ) where
         open Data.Nat.Properties.≤-Reasoning
 
@@ -556,7 +556,7 @@
            p08 = begin
              z ≡⟨ sym (py=z) ⟩
              fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc y)))} (sh1p<n perm  y c₁)  ≡⟨ lemma10 p15 ⟩
-             fromℕ< {toℕ x} fin<n  ≡⟨ fromℕ<-toℕ _ _  ⟩
+             fromℕ< {toℕ x} (fin<n _)  ≡⟨ fromℕ<-toℕ _ _  ⟩
              x ∎  
 
    piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x
@@ -579,7 +579,7 @@
            p08 = begin
              z ≡⟨ sym (py=z) ⟩
              fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc y)))} (sh2p<n perm y c₁)  ≡⟨ lemma10 p15 ⟩
-             fromℕ< {toℕ x} fin<n  ≡⟨ fromℕ<-toℕ _ _  ⟩
+             fromℕ< {toℕ x} (fin<n _)  ≡⟨ fromℕ<-toℕ _ _  ⟩
              x ∎  
 
 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm)  refl =p=  perm
@@ -587,17 +587,17 @@
     s001 : (x : Fin n) → shrink (pprep perm) refl ⟨$⟩ʳ x ≡ perm ⟨$⟩ʳ x
     s001 zero with <-fcmp (suc (perm ⟨$⟩ʳ zero)) (# 0) 
     ... | tri> ¬a ¬b c = s002 where
-        s002 :  fromℕ< (≤-trans fin<n (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡ perm ⟨$⟩ʳ zero
+        s002 :  fromℕ< (≤-trans (fin<n _) (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡ perm ⟨$⟩ʳ zero
         s002 = begin
-            fromℕ< (≤-trans fin<n (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡⟨ lemma10 refl ⟩ 
-            fromℕ< fin<n  ≡⟨ fromℕ<-toℕ (perm ⟨$⟩ʳ zero) fin<n ⟩ 
+            fromℕ< (≤-trans (fin<n _) (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡⟨ lemma10 refl ⟩ 
+            fromℕ< (fin<n  _) ≡⟨ fromℕ<-toℕ (perm ⟨$⟩ʳ zero) (fin<n _) ⟩ 
             perm ⟨$⟩ʳ zero ∎ where open ≡-Reasoning
     s001 (suc x) with <-fcmp (suc (perm ⟨$⟩ʳ (suc x))) (# 0) 
     ... | tri> ¬a ¬b c = s002 where
-        s002 :  fromℕ< (≤-trans fin<n (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡ perm ⟨$⟩ʳ (suc x)
+        s002 :  fromℕ< (≤-trans (fin<n _) (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡ perm ⟨$⟩ʳ (suc x)
         s002 = begin
-            fromℕ< (≤-trans fin<n (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡⟨ lemma10 refl ⟩ 
-            fromℕ< fin<n  ≡⟨ fromℕ<-toℕ (perm ⟨$⟩ʳ (suc x)) fin<n ⟩ 
+            fromℕ< (≤-trans (fin<n _) (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡⟨ lemma10 refl ⟩ 
+            fromℕ< (fin<n _) ≡⟨ fromℕ<-toℕ (perm ⟨$⟩ʳ (suc x)) (fin<n _) ⟩ 
             perm ⟨$⟩ʳ (suc x) ∎ where open ≡-Reasoning
 
 shrink-iso2 : { n : ℕ } → {perm : Permutation (suc n) (suc n)} 
@@ -783,10 +783,10 @@
     pf5 zero = refl
     pf5 (suc q) with <-fcmp ((pid ⟨$⟩ʳ (suc q))) (# 0) 
     ... | tri> ¬a ¬b c = pf6 where
-      pf6 : suc (fromℕ< (≤-trans (fin<n {_} {q}) (Data.Nat.Properties.≤-reflexive refl))) ≡ suc q
+      pf6 : suc (fromℕ< (≤-trans (fin<n {_} q) (Data.Nat.Properties.≤-reflexive refl))) ≡ suc q
       pf6 = cong suc ( begin
-          fromℕ< (≤-trans (fin<n {_} {q}) (Data.Nat.Properties.≤-reflexive refl)) ≡⟨ lemma10 refl  ⟩ 
-          fromℕ< fin<n ≡⟨  fromℕ<-toℕ _ fin<n  ⟩ 
+          fromℕ< (≤-trans (fin<n {_} q) (Data.Nat.Properties.≤-reflexive refl)) ≡⟨ lemma10 refl  ⟩ 
+          fromℕ< (fin<n _) ≡⟨  fromℕ<-toℕ _ (fin<n  _) ⟩ 
           q ∎  ) where 
              open ≡-Reasoning 
 
--- a/src/fin.agda	Sat Sep 23 22:43:47 2023 +0900
+++ b/src/fin.agda	Sun Sep 24 18:10:44 2023 +0900
@@ -12,9 +12,9 @@
 
 
 -- 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})
+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
@@ -23,7 +23,7 @@
 
 pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0  → Data.Nat.pred (toℕ f) < n
 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
+pred<n {suc n} {suc f} (s≤s z≤n) = fin<n _
 
 fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n
 fin<asa = toℕ-fromℕ< nat.a<sa
@@ -44,6 +44,9 @@
 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) )
 
+fin1≡0 : (f : Fin 1) → # 0 ≡ f
+fin1≡0 zero = refl
+
 -- raise 1
 fin+1 :  { n : ℕ } → Fin n → Fin (suc n)
 fin+1  zero = zero 
@@ -108,8 +111,8 @@
 fpred-comm {suc n} zero = refl
 fpred-comm {suc n} (suc x) = begin
        toℕ (Data.Fin.pred (suc x)) ≡⟨ sym ( toℕ-fromℕ< _ ) ⟩
-       toℕ (fromℕ< fin<n ) ≡⟨ cong toℕ (lemma10 (toℕ-inject₁ _ ) ) ⟩
-       toℕ (fromℕ< (<-trans fin<n a<sa) ) ≡⟨  toℕ-fromℕ< _ ⟩
+       toℕ (fromℕ< (fin<n _) ) ≡⟨ cong toℕ (lemma10 (toℕ-inject₁ _ ) ) ⟩
+       toℕ (fromℕ< (<-trans (fin<n _) a<sa) ) ≡⟨  toℕ-fromℕ< _ ⟩
        toℕ (suc x) ∸ 1 ∎  where open ≡-Reasoning
 
 -- lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
@@ -251,7 +254,7 @@
           ... | tri< a ¬b ¬c₁ = f1-phase1 qs p (case2 q1)
           ... | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (fdup-10 b b₁) where
                fdup-10 : fromℕ< a<sa ≡ x → fin+1 i ≡ x → ⊥
-               fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) fin<n ) 
+               fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) (fin<n _) ) 
           ... | tri> ¬a₁ ¬b c = f1-phase1 qs p (case2 q1)
           f1-phase1 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x
           ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case1 q1)
--- a/src/logic.agda	Sat Sep 23 22:43:47 2023 +0900
+++ b/src/logic.agda	Sun Sep 24 18:10:44 2023 +0900
@@ -46,7 +46,6 @@
 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
 dont-orb {A} {B} (case1 a) ¬B = a
 
-
 infixr  130 _∧_
 infixr  140 _∨_
 infixr  150 _⇔_
@@ -73,6 +72,25 @@
 
 open import Relation.Binary.PropositionalEquality
 
+record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
+   field
+       fun←  :  S → R
+       fun→  :  R → S
+       fiso← : (x : R)  → fun← ( fun→ x )  ≡ x
+       fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x
+
+injection :  {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
+injection R S f = (x y : R) → f x ≡ f y → x ≡ y
+
+
+not-not-bool : { b : Bool } → not (not b) ≡ b
+not-not-bool {true} = refl
+not-not-bool {false} = refl
+
+¬t=f : (t : Bool ) → ¬ ( not t ≡ t) 
+¬t=f true ()
+¬t=f false ()
+
 ≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
 ≡-Bool-func {true} {true} a→b b→a = refl
 ≡-Bool-func {false} {true} a→b b→a with b→a refl