Mercurial > hg > Members > kono > Proof > automaton

changeset 261:57fd08c16e25

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 11:07:11 +0900
parents eddc2c1be16f
children cb13c38103b1
files automaton-in-agda/src/bijection.agda automaton-in-agda/src/nat.agda
diffstat 2 files changed, 66 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/bijection.agda	Tue Jul 06 01:40:18 2021 +0900
+++ b/automaton-in-agda/src/bijection.agda	Tue Jul 06 11:07:11 2021 +0900
@@ -372,16 +372,50 @@
      lton x  = pred (lton1 x)
 
      lton1>0 : (x : List Bool ) → 0 < lton1 x 
-     lton1>0 x = {!!}
+     lton1>0 [] = a<sa
+     lton1>0 (true ∷ x₁) = 0<s
+     lton1>0 (false ∷ t) = ≤-trans (lton1>0 t) x≤x+y
+
+     2lton1>0 : (t : List Bool ) →  0 < lton1 t + lton1 t
+     2lton1>0 t = ≤-trans (lton1>0 t) x≤x+y
+
+     lton-cons>0 : {x : Bool} {y : List Bool } → 0 < lton (x ∷ y)
+     lton-cons>0 {true} {[]} = refl-≤s
+     lton-cons>0 {true} {x ∷ y} =  {!!}
+     lton-cons>0 {false} {[]} = refl-≤
+     lton-cons>0 {false} {x ∷ y} = {!!}
+
+     lb=0 : {x y : ℕ } → pred x  < pred y → suc (x + x ∸ 1) < suc (y + y ∸ 1)
+     lb=0 {0} {suc y} lt = s≤s (subst (λ k → 0 < k ) (+-comm (suc y) y ) 0<s)
+     lb=0 {suc x} {suc y} lt = begin
+            suc (suc ((suc x + suc x) ∸ 1)) ≡⟨ refl  ⟩
+            suc (suc x) + suc x ≡⟨ refl ⟩
+            suc (suc x + suc x) ≤⟨ <-plus (s≤s lt) ⟩
+            suc y + suc x <⟨ <-plus-0 {suc x} {suc y} {suc y} (s≤s lt) ⟩
+            suc y + suc y ≡⟨ refl ⟩
+            suc ((suc y + suc y) ∸ 1) ∎  where open ≤-Reasoning
+     lb=1 : {x y : List Bool} {z : Bool} → lton (z ∷ x) ≡ lton (z ∷ y) → lton x ≡ lton y 
+     lb=1 {x} {y} {true} eq = {!!}
+     lb=1 {x} {y} {false} eq with <-cmp (lton x) (lton y)
+     ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=0 {lton1 x} {lton1 y} a))
+     ... | tri≈ ¬a b ¬c = b
+     ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=0 {lton1 y} {lton1 x} c))
+
+     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 = {!!}
+     lb=b (false ∷ x) (true ∷ y) 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
      lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where
          lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x
-         lb05 [] refl = refl
-         lb05 (true ∷ t) eq = {!!}
-         lb05 (false ∷ t) eq = {!!}
+         lb05 x eq = lb=b [] x (sym eq)
      lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) 
-     ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = {!!} ; isBin = begin
+     ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = begin
        lton (false ∷ []) ≡⟨ refl ⟩ 
        suc 0  ≡⟨ refl ⟩ 
        suc (lton [])   ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ 
@@ -396,17 +430,23 @@
         lb01 : lton (true ∷ t) ≡ suc n
         lb01 = begin
            lton (true ∷ t)  ≡⟨ refl ⟩ 
-           lton1 t + lton1 t   ≡⟨ sym ( sucprd {!!} ) ⟩ 
+           lton1 t + lton1 t   ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩ 
            suc (pred (lton1 t + lton1 t ))  ≡⟨ refl ⟩ 
            suc (lton (false ∷ t))   ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩ 
            suc (lton (LB.nlist (lb n))) ≡⟨  cong suc (LB.isBin (lb n)) ⟩ 
            suc n ∎  where open ≡-Reasoning
-     ... | true ∷ t | record { eq = eq } = record { nlist =  lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = {!!}  } where
+     ... | true ∷ t | record { eq = eq } = record { nlist =  lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where
         lb03 : lton (true ∷ t) ≡ n
         lb03 = begin
            lton (true ∷ t)   ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩ 
            lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩ 
            n ∎  where open ≡-Reasoning
+        -- eq : LB.nlist (lb n) ≡ true ∷ t ,  eq1 : pred (suc (lton1 t1 + lton1 t1)) ≡ suc n
+        lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x
+        lb07 (true ∷ t1) eq1 = ⊥-elim (nat-≡< eq1  (begin
+           lton1 (true ∷ t1) ≤⟨ {!!} ⟩
+           suc n ∎ )) where open ≤-Reasoning  -- lton1 (true ∷ t) ∸ 1 ≡ n, lton1 t1 + lton1 t1 ≡ suc n
+        lb07 (false ∷ t1) eq1 = {!!}
 
         add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc  (x1 + x1))
         add11 zero = refl
@@ -427,7 +467,7 @@
         lb02 t eq1 = begin
             lton (lb+1 t) ≡⟨ refl ⟩
             pred (lton1 (lb+1 t)) ≡⟨ cong pred (sym (lb04 t)) ⟩
-            pred (suc (lton1 t))  ≡⟨ sym (sucprd {!!} ) ⟩
+            pred (suc (lton1 t))  ≡⟨ sym (sucprd (lton1>0 t)) ⟩
             suc (pred (lton1 t)) ≡⟨ refl ⟩
             suc (lton t) ≡⟨ cong suc eq1  ⟩
             suc n ∎  where open ≡-Reasoning
--- a/automaton-in-agda/src/nat.agda	Tue Jul 06 01:40:18 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Tue Jul 06 11:07:11 2021 +0900
@@ -92,6 +92,14 @@
 sucprd : {i : ℕ } → 0 < i  → suc (pred i) ≡ i
 sucprd {suc i} 0<i = refl
 
+0<s : {x : ℕ } → zero < suc x
+0<s {_} = s≤s z≤n 
+
+px<py : {x y : ℕ } → pred x  < pred y → x < y
+px<py {zero} {suc y} lt = 0<s
+px<py {suc zero} {suc (suc y)} (s≤s lt) = s≤s 0<s
+px<py {suc (suc x)} {suc (suc y)} (s≤s lt) = s≤s (px<py {suc x} {suc y} lt)
+
 minus : (a b : ℕ ) →  ℕ
 minus a zero = a
 minus zero (suc b) = zero
@@ -133,9 +141,6 @@
            suc x
         ∎  where open ≡-Reasoning
 
-0<s : {x : ℕ } → zero < suc x
-0<s {_} = s≤s z≤n 
-
 <-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
 <-minus-0 {x} {suc _} {zero} lt = lt
 <-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt
@@ -201,6 +206,11 @@
 x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
 x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)
 
+≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j
+≤→= {0} {0} z≤n z≤n = refl
+≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i )
+
+
 open import Data.Product
 
 i-j=0→i=j : {i j  : ℕ } → j ≤ i  → i - j ≡ 0 → i ≡ j
@@ -209,6 +219,11 @@
 i-j=0→i=j {suc i} {zero} z≤n ()
 i-j=0→i=j {suc i} {suc j} (s≤s lt) eq = cong suc (i-j=0→i=j {i} {j} lt eq)
 
+m*n=0⇒m=0∨n=0 : {i j : ℕ} → i * j ≡ 0 → (i ≡ 0) ∨ ( j ≡ 0 )
+m*n=0⇒m=0∨n=0 {zero} {j} refl = case1 refl
+m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl
+
+
 minus+1 : {x y  : ℕ } → y ≤ x  → suc (minus x y)  ≡ minus (suc x) y 
 minus+1 {zero} {zero} y≤x = refl
 minus+1 {suc x} {zero} y≤x = refl