Mercurial > hg > Members > kono > Proof > automaton

changeset 260:eddc2c1be16f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lb<
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 06 Jul 2021 01:40:18 +0900
parents ad08d9e83a60
children 57fd08c16e25
files automaton-in-agda/src/bijection.agda automaton-in-agda/src/nat.agda
diffstat 2 files changed, 54 insertions(+), 75 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/bijection.agda	Mon Jul 05 23:19:59 2021 +0900
+++ b/automaton-in-agda/src/bijection.agda	Tue Jul 06 01:40:18 2021 +0900
@@ -328,6 +328,35 @@
      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
+
+lb+1 : List Bool → List Bool
+lb+1 [] =  false ∷ [] 
+lb+1 (false ∷ t) = true ∷ t 
+lb+1 (true ∷ t) =  false ∷ lb+1 t
+
+lb-1 : List Bool → List Bool
+lb-1 [] =  []
+lb-1 (true ∷ t) = false ∷ t 
+lb-1 (false ∷ t) with lb-1 t
+... | [] = 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 
@@ -340,48 +369,45 @@
      lton1 (true ∷ t) = suc (lton1 t + lton1 t)
      lton1 (false ∷ t) = lton1 t + lton1 t
      lton : List Bool → ℕ
-     lton [] = 0
      lton x  = pred (lton1 x)
 
+     lton1>0 : (x : List Bool ) → 0 < lton1 x 
+     lton1>0 x = {!!}
+
      lb : (n : ℕ) → LB n lton
-     lb zero = record { nlist = [] ; isBin = refl ; isUnique = {!!} }
+     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 = {!!}
      lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) 
      ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = {!!} ; 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 open ≡-Reasoning
+       suc n ∎ }  where
+         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
         lb01 : lton (true ∷ t) ≡ suc n
         lb01 = begin
            lton (true ∷ t)  ≡⟨ refl ⟩ 
-           lton1 t + lton1 t   ≡⟨ {!!} ⟩ 
+           lton1 t + lton1 t   ≡⟨ sym ( sucprd {!!} ) ⟩ 
            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
-        lb05 :  1 < length (true ∷ t)
-        lb05 = {!!}
         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
 
-        lb+1 : List Bool → List Bool
-        lb+1 [] =  false ∷ [] 
-        lb+1 (false ∷ t) = true ∷ t 
-        lb+1 (true ∷ t) =  false ∷ lb+1 t
-
-        lb-1 : List Bool → List Bool
-        lb-1 [] =  []
-        lb-1 (true ∷ t) = false ∷ t 
-        lb-1 (false ∷ t) with lb-1 t
-        ... | [] = true ∷ []
-        ... | x ∷ t1 = true ∷ x ∷ t1
-
         add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc  (x1 + x1))
         add11 zero = refl
         add11 (suc x) = cong (λ k → suc (suc k)) (trans (+-comm x _) (cong suc (+-comm _ x)))
@@ -395,64 +421,14 @@
            suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0  ) ⟩ 
            lton1 (lb+1 t0) + lton1 (lb+1 t0) ∎  where
               open ≡-Reasoning
-        tt1 : (t : List Bool) → Set
-        tt1 t = suc (lton1 t) ≡ lton1 (lb+1 t) 
-        tt2 = tt1 []
-        tt3 = tt1 (true ∷ [])
-        tt4 = tt1 (true ∷ true ∷ [])
-        tt6 : (n : ℕ) → List Bool
-        tt6 zero = []
-        tt6 (suc n) = lb+1 (tt6 n)
-        tt61 : (n : ℕ) → List (List Bool)
-        tt61 zero = []
-        tt61 (suc n) = lb+1 (tt6 n) ∷ tt61 n
-        tt7 : (n : ℕ) → Set
-        tt7 n = tt1 ( tt6 n )
-        tt9 : (n : ℕ) → List Bool → List Bool
-        tt9 zero x = x 
-        tt9 (suc n) x = lb-1 (tt9 n x)
-        tta : (n m : ℕ) →  List Bool
-        tta n m = tt9 m ( tt6 n)
-        ttb = Data.List.map lb-1 (tt61 10)
-        ttc = Data.List.map lb+1 (tt61 10)
-        ttd = Data.List.map lton (tt61 200)
-        ttf = tt61 128
-        tt5 = {!!}
 
         lb02 : (t : List Bool) → lton t ≡ n → lton (lb+1 t) ≡ suc n
         lb02 [] refl = refl
-        lb02 (false ∷ t) eq = begin
-           lton (lb+1 (false ∷ t))  ≡⟨ {!!} ⟩ 
-           suc (suc (lton1 t + lton1 t))  ≡⟨ cong suc {!!} ⟩ 
-           suc n ∎  where open ≡-Reasoning
-        lb02 (true ∷ []) eq = ?
-        lb02 (true ∷ (t1 ∷ t2) ) eq1 =  begin
-           lton (lb+1 (true ∷ t0))  ≡⟨ {!!} ⟩ 
-           suc (lton1 (lb+1 t0) + lton1 (lb+1 t0)) ≡⟨ cong (λ k → suc (k + k )) (sym (lb04 t0)) ⟩  -- suc (suc (lton1 t + lton1 t)) ≡ n
-           suc (suc (lton1 t0) + suc (lton1 t0)) ≡⟨ cong suc (add11 (lton1 t0) ) ⟩ 
-           suc (suc (suc (lton1 t0 + lton1 t0)))  ≡⟨ cong suc {!!} ⟩  
-           suc n ∎  where
-             open ≡-Reasoning
-             t0 = t1 ∷ t2
-
+        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 {!!} ) ⟩
+            suc (pred (lton1 t)) ≡⟨ refl ⟩
+            suc (lton t) ≡⟨ cong suc eq1  ⟩
+            suc n ∎  where open ≡-Reasoning
 
-     ntol : ℕ → List Bool 
-     ntol 0 = []
-     ntol 1 = false ∷ []
-     ntol (suc n) = {!!}
-     xx :   (x : ℕ ) → List Bool ∧ ℕ
-     xx x = ⟪ (ntol x) , lton ((ntol x))  ⟫
-     add12 : (x1 x : ℕ ) → suc x1 + x ≡ x1 + suc x
-     add12 zero x = refl
-     add12 (suc x1) x = cong suc (add12 x1 x)
-     ---- div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
-     div20 : (x x1 : ℕ ) → div2 (suc x) ≡ ⟪ x1 , false ⟫ → x1 + x1 ≡ suc x
-     div20 x x1 eq = begin
-         x1 + x1 ≡⟨ cong (λ k → div2-rev k ) (sym eq) ⟩
-         div2-rev (div2 (suc x)) ≡⟨ div2-eq _ ⟩
-         suc x ∎ where open ≡-Reasoning
-     div21 : (x x1 : ℕ ) → div2 (suc x) ≡ ⟪ x1 , true ⟫  → suc  (x1 + x1) ≡ suc x
-     div21 x x1 eq = begin
-         suc  (x1 + x1) ≡⟨ cong (λ k → div2-rev k ) (sym eq) ⟩
-         div2-rev (div2 (suc x)) ≡⟨ div2-eq _ ⟩
-         suc x ∎ where open ≡-Reasoning
--- a/automaton-in-agda/src/nat.agda	Mon Jul 05 23:19:59 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Tue Jul 06 01:40:18 2021 +0900
@@ -89,6 +89,9 @@
      suc (suc (div2-rev (div2 x)))      ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ 
      suc (suc x) ∎  where open ≡-Reasoning
 
+sucprd : {i : ℕ } → 0 < i  → suc (pred i) ≡ i
+sucprd {suc i} 0<i = refl
+
 minus : (a b : ℕ ) →  ℕ
 minus a zero = a
 minus zero (suc b) = zero