# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1625545828 -32400
# Node ID cb13c38103b174dc0f7df1d759d08dfeea7e85e8
# Parent  57fd08c16e259b27d869746f21c12fe8e1f30f0a
LBℕ : Bijection ℕ ( List Bool ) done

diff -r 57fd08c16e25 -r cb13c38103b1 automaton-in-agda/src/bijection.agda
--- a/automaton-in-agda/src/bijection.agda	Tue Jul 06 11:07:11 2021 +0900
+++ b/automaton-in-agda/src/bijection.agda	Tue Jul 06 13:30:28 2021 +0900
@@ -379,11 +379,14 @@
      2lton1>0 : (t : List Bool ) →  0 < lton1 t + lton1 t
      2lton1>0 t = ≤-trans (lton1>0 t) x≤x+y
 
+     lb=3 : {x y : ℕ} → 0 < x → 0 < y → 1 ≤ pred (x + y)
+     lb=3 {suc x} {suc y} (s≤s 0<x) (s≤s 0<y) = subst (λ k → 1 ≤ k ) (+-comm (suc y) _ ) (s≤s z≤n)
+
      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 {true} {x ∷ y} = ≤-trans ( lb=3 (lton1>0 (x ∷ y)) (lton1>0 (x ∷ y))) px≤x
      lton-cons>0 {false} {[]} = refl-≤
-     lton-cons>0 {false} {x ∷ y} = {!!}
+     lton-cons>0 {false} {x ∷ y} = lb=3 (lton1>0 (x ∷ y)) (lton1>0 (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)
@@ -394,19 +397,50 @@
             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=2 : {x y : ℕ } → pred x  < pred y → suc (x + x ) < suc (y + y )
+     lb=2 {zero} {suc y} lt = s≤s 0<s
+     lb=2 {suc x} {suc y} lt = s≤s (lb=0 {suc x} {suc y} lt)
      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} {true} eq with <-cmp (lton x) (lton y)
+     ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=2 {lton1 x} {lton1 y} a))
+     ... | tri≈ ¬a b ¬c = b
+     ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=2 {lton1 y} {lton1 x} c))
      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-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
+        lb=01 : {x y : ℕ } → x  < y → x + x  < (y + y ∸ 1)
+        lb=01 {x} {y} x<y = begin
+            suc (x + x) ≡⟨ refl  ⟩
+            suc x + x ≤⟨ ≤-plus x<y ⟩
+            y + x ≡⟨ refl ⟩
+            pred (suc y + x) ≡⟨ cong (λ k → pred ( k + x)) (+-comm 1 y) ⟩
+            pred ((y + 1) + x ) ≡⟨ cong pred (+-assoc y 1 x)  ⟩
+            pred (y + suc x) ≤⟨ px≤py (≤-plus-0 {suc x} {y} {y} x<y) ⟩
+            (y + y) ∸ 1  ∎  where open ≤-Reasoning
+     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (lb=02 c) ) where
+        lb=02 : {x y : ℕ } → x  < y → x + x ∸ 1 < y + y
+        lb=02 {0} {y} lt = ≤-trans lt x≤x+y 
+        lb=02 {suc x} {y} lt = begin
+            suc ( suc x + suc x ∸ 1 ) ≡⟨ refl ⟩
+            suc x + suc x  ≤⟨ ≤-plus {suc x} (<to≤ lt) ⟩
+            y + suc x  ≤⟨ ≤-plus-0 (<to≤ lt) ⟩
+            y + y  ∎  where open ≤-Reasoning
+     ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (sym eq) ( begin
+            suc (lton1 y + lton1 y ∸ 1) ≡⟨ sucprd ( 2lton1>0 y) ⟩
+            lton1 y + lton1 y  ≡⟨  cong (λ k → k + k ) (sym b)  ⟩
+            lton1 x + lton1 x ∎  )) where open ≤-Reasoning
+
      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) (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 (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq)) 
 
@@ -415,18 +449,18 @@
          lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x
          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 = lb06 ; isBin = begin
-       lton (false ∷ []) ≡⟨ refl ⟩ 
-       suc 0  ≡⟨ refl ⟩ 
-       suc (lton [])   ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ 
-       suc (lton (LB.nlist (lb n)))  ≡⟨ cong suc (LB.isBin (lb n) ) ⟩ 
-       suc n ∎ }  where
+     ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where
+         open ≡-Reasoning
+         lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n
+         lb10 = begin
+           lton (false ∷ []) ≡⟨ refl ⟩ 
+           suc 0  ≡⟨ refl ⟩ 
+           suc (lton [])   ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ 
+           suc (lton (LB.nlist (lb n)))  ≡⟨ cong suc (LB.isBin (lb n) ) ⟩ 
+           suc n ∎    
          lb06 :  (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x
-         lb06 (true ∷ t) eq = {!!}
-         lb06 (false ∷ []) eq = refl 
-         lb06 (false ∷ x ∷ t) eq = {!!}
-         open ≡-Reasoning
-     ... | false ∷ t | record { eq = eq } =  record { nlist = true ∷ t ; isBin = lb01 ; isUnique = {!!}  } where
+         lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x
+     ... | false ∷ t | record { eq = eq } =  record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where
         lb01 : lton (true ∷ t) ≡ suc n
         lb01 = begin
            lton (true ∷ t)  ≡⟨ refl ⟩ 
@@ -435,18 +469,14 @@
            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
+        lb09 :  (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x
+        lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) --  lton (true ∷ t) ≡ lton x
      ... | 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
@@ -472,3 +502,5 @@
             suc (lton t) ≡⟨ cong suc eq1  ⟩
             suc n ∎  where open ≡-Reasoning
 
+        lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x
+        lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1)) 
diff -r 57fd08c16e25 -r cb13c38103b1 automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Tue Jul 06 11:07:11 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Tue Jul 06 13:30:28 2021 +0900
@@ -210,6 +210,14 @@
 ≤→= {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 )
 
+px≤x : {x  : ℕ } → pred x ≤ x 
+px≤x {zero} = refl-≤
+px≤x {suc x} = refl-≤s
+
+px≤py : {x y : ℕ } → x ≤ y → pred x  ≤ pred y 
+px≤py {zero} {zero} lt = refl-≤
+px≤py {zero} {suc y} lt = z≤n
+px≤py {suc x} {suc y} (s≤s lt) = lt 
 
 open import Data.Product