Mercurial > hg > Members > kono > Proof > automaton

changeset 263:4b8dc7e83444

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, 06 Jul 2021 22:01:02 +0900
parents cb13c38103b1
children d1e8e5eadc38
files automaton-in-agda/src/bijection.agda
diffstat 1 files changed, 67 insertions(+), 55 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/bijection.agda	Tue Jul 06 13:30:28 2021 +0900
+++ b/automaton-in-agda/src/bijection.agda	Tue Jul 06 22:01:02 2021 +0900
@@ -27,6 +27,9 @@
 
 open Bijection 
 
+--
+-- injection as an uniquneness of bijection 
+--
 b→injection0 : {n m : Level} (R : Set n) (S : Set m)  → (b : Bijection R S) → injection R S (fun→ b)
 b→injection0 R S b x y eq = begin
           x
@@ -41,14 +44,22 @@
 b→injection1 : {n m : Level} (R : Set n) (S : Set m)  → (b : Bijection R S) → injection S R (fun← b)
 b→injection1 R S b x y eq = trans (  sym ( fiso→ b x ) ) (trans (  cong (λ k → fun→ b k ) eq ) ( fiso→ b y  ))
 
+bij-combination : {n m l : Level} (R : Set n) (S : Set m) (T : Set l)  → Bijection R S → Bijection S T → Bijection R T
+bij-combination R S T rs st = record { fun← = λ x → fun← rs ( fun← st x ) ; fun→ = λ x → fun→ st ( fun→ rs x )
+    ; fiso← = λ x →  trans (cong (λ k → fun← rs k) (fiso← st (fun→ rs x))) ( fiso← rs x)
+    ; fiso→ = λ x →  trans (cong (λ k → fun→ st k) (fiso→ rs (fun← st x))) ( fiso→ st x) }
+
 --  ¬ A = A → ⊥ 
+--
+-- famous diagnostic function
+--
 
 diag : {S : Set }  (b : Bijection  ( S → Bool ) S) → S → Bool
 diag b n = not (fun← b n n)
 
 diagonal : { S : Set } → ¬ Bijection  ( S → Bool ) S
-diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
-    diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n ) 
+diagonal {S} b = diagn1 (fun→ b (λ n → diag b n) ) refl where
+    diagn1 : (n : S ) → ¬ (fun→ b (λ n → diag b n) ≡ n ) 
     diagn1 n dn = ¬t=f (diag b n ) ( begin
            not (diag b n)
         ≡⟨⟩
@@ -61,6 +72,35 @@
            diag b n 
         ∎ ) where open ≡-Reasoning
 
+b1 : (b : Bijection  ( ℕ → Bool ) ℕ) → ℕ 
+b1 b = fun→ b (diag b)
+
+b-iso : (b : Bijection  ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b)
+b-iso b = fiso← b _
+
+--
+-- ℕ <=> ℕ + 1
+--
+to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
+to1 {n} {R} b = record {
+       fun←  = to11
+     ; fun→  = to12
+     ; fiso← = to13
+     ; fiso→ = to14
+   } where
+       to11 : ⊤ ∨ R → ℕ
+       to11 (case1 tt) = 0
+       to11 (case2 x) = suc ( fun← b x )
+       to12 : ℕ → ⊤ ∨ R
+       to12 zero = case1 tt
+       to12 (suc n) = case2 ( fun→ b n)
+       to13 : (x : ℕ) → to11 (to12 x) ≡ x
+       to13 zero = refl
+       to13 (suc x) = cong suc (fiso← b x)
+       to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x
+       to14 (case1 x) = refl
+       to14 (case2 x) = cong case2 (fiso→ b x)
+
 
 open _∧_
 
@@ -68,7 +108,7 @@
   field
      j k sum stage : ℕ
      nn : j + k ≡ sum
-     ni : i ≡ j + stage 
+     ni : i ≡ j + stage   -- not used
      k1 : nxn→n j k ≡ i
      k0 : n→nxn i ≡ ⟪ j , k ⟫ 
      nn-unique : {j0 k0 : ℕ } →  nxn→n j0 k0 ≡ i  → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫ 
@@ -121,6 +161,7 @@
           suc j + suc (suc k) ∎ where open ≡-Reasoning
      nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} )
 
+     -- increment in ths same stage
      nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
      nid2 zero zero = refl
      nid2 zero (suc j) = refl
@@ -136,8 +177,7 @@
              nid3 (suc i) = begin
                  suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩
                  suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k →  suc (i + suc (suc k))) (nid3 i) ⟩
-                 suc (i + suc (suc (i + suc (nxn→n i 0))))
-              ∎
+                 suc (i + suc (suc (i + suc (nxn→n i 0)))) ∎
      nid2 (suc i) (suc j) = begin
           suc (nxn→n (suc i) (suc (suc j)))  ≡⟨ refl ⟩
           suc (suc (i + suc (suc j) + suc (nxn→n i (suc (suc j)))))  ≡⟨ cong (λ k → suc (suc (i + suc (suc j) + k))) (nid2 i (suc j)) ⟩
@@ -146,6 +186,7 @@
           nxn→n (suc (suc i)) (suc j) ∎ where
              open ≡-Reasoning
 
+     -- increment ths stage
      nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i) 
      nid00 zero = refl
      nid00 (suc i) = begin
@@ -156,6 +197,10 @@
         suc ((i + 1) + (i + suc (nxn→n 0 i))) ≡⟨ cong suc (+-assoc i 1 (i + suc (nxn→n 0 i))) ⟩
         suc (i + suc (i + suc (nxn→n 0 i))) ∎ where open ≡-Reasoning
 
+     -----
+     --
+     -- create the invariant NN for all n
+     --
      nn : ( i  : ℕ) → NN i nxn→n n→nxn
      nn zero = record { j = 0 ; k = 0 ; sum = 0 ; stage = 0 ; nn = refl ; ni = refl ; k1 = refl ; k0 = refl
         ;  nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) }
@@ -163,6 +208,9 @@
      ... | zero | record { eq = eq } = record { k = suc (NN.sum (nn i)) ; j = 0 ; sum = suc  (NN.sum (nn i)) ; stage = suc  (NN.sum (nn i)) + (NN.stage (nn i))
          ; nn = refl
          ; ni = nn01 ; k1 = nn02 ; k0 = nn03 ;  nn-unique = nn04 } where
+            ---
+            --- increment the stage
+            ---
             sum = NN.sum (nn i)
             stage = NN.stage (nn i)
             j = NN.j (nn i)
@@ -224,6 +272,9 @@
                nn06 = NN.nn-unique (nn i)
      ... | suc k  | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; sum = NN.sum (nn i) ; stage = NN.stage (nn i) ; nn = nn10
          ; ni = cong suc (NN.ni (nn i)) ; k1 = nn11 ; k0 = nn12 ;  nn-unique = nn13 } where
+            ---
+            --- increment in a stage
+            ---
             nn10 : suc (NN.j (nn i)) + k ≡ NN.sum (nn i)
             nn10 = begin
                 suc (NN.j (nn i)) + k ≡⟨ cong (λ x → x + k) (+-comm 1 _)  ⟩
@@ -284,37 +335,6 @@
           ⟪ j , k ⟫ ∎  where open ≡-Reasoning
 
 
-b1 : (b : Bijection  ( ℕ → Bool ) ℕ) → ℕ 
-b1 b = fun→ b (diag b)
-
-b-iso : (b : Bijection  ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b)
-b-iso b = fiso← b _
-
-to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
-to1 {n} {R} b = record {
-       fun←  = to11
-     ; fun→  = to12
-     ; fiso← = to13
-     ; fiso→ = to14
-   } where
-       to11 : ⊤ ∨ R → ℕ
-       to11 (case1 tt) = 0
-       to11 (case2 x) = suc ( fun← b x )
-       to12 : ℕ → ⊤ ∨ R
-       to12 zero = case1 tt
-       to12 (suc n) = case2 ( fun→ b n)
-       to13 : (x : ℕ) → to11 (to12 x) ≡ x
-       to13 zero = refl
-       to13 (suc x) = cong suc (fiso← b x)
-       to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x
-       to14 (case1 x) = refl
-       to14 (case2 x) = cong case2 (fiso→ b x)
-
-open _∧_
-
-open import nat
-
-
 --   []     0
 --   0    → 1
 --   1    → 2
@@ -322,16 +342,14 @@
 --   11   → 4
 --   ...
 
+--
+-- binary invariant
+--
 record LB (n : ℕ) (lton : List Bool → ℕ ) : Set where
   field
      nlist : List Bool
      isBin : lton nlist ≡ n
-     isUnique :  (x : List Bool) → lton x ≡ n → nlist  ≡ x 
-
-data _lb≤_ : (x y : List Bool ) → Set where
-    lb-s≤s : {x y : List Bool } → {z : Bool } → x lb≤ x → (z ∷ x) lb≤  (z ∷ y)
-    lb-f<t : {x : List Bool } → (false ∷ x) lb≤  (true ∷ x)
-    lb-z≤n : {x : List Bool } → [] lb≤  x
+     isUnique :  (x : List Bool) → lton x ≡ n → nlist  ≡ x -- we don't need this
 
 lb+1 : List Bool → List Bool
 lb+1 [] =  false ∷ [] 
@@ -345,18 +363,6 @@
 ... | [] = true ∷ []
 ... | x ∷ t1 = true ∷ x ∷ t1
 
-lb< :  (x y : List Bool ) → Set
-lb< x y = lb+1 x lb≤ y
-
--- lb<-cmp :  Trichotomous  _≡_  _lb≤_
--- lb<-cmp [] [] =  tri≈ {!!} refl {!!}
--- lb<-cmp [] (x ∷ y) = {!!}
--- lb<-cmp (x ∷ y) [] = {!!}
--- lb<-cmp (x ∷ y) (x₁ ∷ y₁) with lb<-cmp y y₁
--- ... | tri< a ¬b ¬c = {!!}
--- ... | tri> ¬a ¬b c = {!!}
--- ... | tri≈ ¬a b ¬c = {!!}
-
 LBℕ : Bijection ℕ ( List Bool ) 
 LBℕ = record {
        fun←  = λ x → lton x 
@@ -410,6 +416,9 @@
      ... | tri≈ ¬a b ¬c = b
      ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=0 {lton1 y} {lton1 x} c))
 
+     ---
+     --- lton is unique in a head
+     ---
      lb-tf : {x y : List Bool } → ¬ (lton (true ∷ x) ≡ lton (false ∷ y))
      lb-tf {x} {y} eq with <-cmp (lton1 x) (lton1 y)
      ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (lb=01 a)) where
@@ -435,13 +444,16 @@
             lton1 y + lton1 y  ≡⟨  cong (λ k → k + k ) (sym b)  ⟩
             lton1 x + lton1 x ∎  )) where open ≤-Reasoning
 
+     ---
+     --- lton uniqueness
+     ---
      lb=b : (x y : List Bool) → lton x ≡ lton y → x ≡ y
      lb=b [] [] eq = refl
      lb=b [] (x ∷ y) eq = ⊥-elim ( nat-≡< eq (lton-cons>0 {x} {y} ))
      lb=b (x ∷ y) [] eq = ⊥-elim ( nat-≡< (sym eq) (lton-cons>0 {x} {y} ))
      lb=b (true ∷ x) (false ∷ y) eq = ⊥-elim ( lb-tf {x} {y} eq )
      lb=b (false ∷ x) (true ∷ y) eq = ⊥-elim ( lb-tf {y} {x} (sym eq) )
-     lb=b (true ∷ x) (true ∷ y) eq = cong (λ k → true ∷ k ) (lb=b x y (lb=1 {x} {y} {true} eq)) 
+     lb=b (true ∷ x)  (true ∷ y)  eq = cong (λ k → true ∷ k  ) (lb=b x y (lb=1 {x} {y} {true}  eq)) 
      lb=b (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq)) 
 
      lb : (n : ℕ) → LB n lton