plfa exercise in relation.

can.agda

module Can where

import Relation.Binary.PropositionalEquality as Eq
import Data.Nat.Properties as Pro
open Pro using (+-assoc; +-identityʳ; +-suc; +-comm)
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)


--- open import ylib.Induction using (+-suc) use the stlib



data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

-- inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil

inc : Bin → Bin 
inc  nil =  x1 nil
inc (x0 x) = x1 x
inc (x1 x) = x0 (inc x)

to : ℕ → Bin
to zero = x0 nil
to (suc n) = inc ( to n)

from : Bin → ℕ
from nil  = zero
--from (x0 nil) = zero  this case make from (x0 x) can be true
from (x0 x) =  from x +  from x
from (x1 x) = suc (from x +  from x)   --- if we use two  we will be just to comple

data One : Bin → Set
data Can  : Bin → Set

data One where

  One1 :
      ---------
      One (x1 nil)

  x0_One1  : ∀ {x : Bin}
    → One x
      ------------
    → One (x0 x)

  x1_One1  : ∀ {x : Bin}
    → One x
      ------------
    → One (x1 x)


data Can where

  Can_One   : ∀ {x : Bin}
    → One x
      -----------
    → Can x

  Can_Zero :
      ---------
     Can (x0 nil)

one_inc : ∀ {x : Bin}
  → One x
    -------------
  → One (inc x)
one_inc {x1 nil} (One1) = x0_One1(One1)
one_inc {x0 x} (x0_One1 cx) = x1_One1 cx
one_inc {x1 x} (x1_One1 cx) = x0_One1(one_inc cx)

can_inc : ∀ {x : Bin}
  → Can x
    -------------
  → Can (inc x)
can_inc {_} (Can_One cx) = Can_One(one_inc cx)
can_inc { (x0 nil) } (Can_Zero) = Can_One(One1)

can_n : ∀ (n : ℕ)
    -------------
  → Can (to n)
can_n  zero   = Can_Zero
can_n (suc n)  = can_inc (can_n n)

_b+_ :   Bin → Bin → Bin
--nil b+ nil = x0 nil  -- for double'+
--x      b+ (x0 nil)    =  x
nil b+ x = nil
x b+ nil = nil
--- (x0 nil) b+ x = x -- This is every importand to remove and add
---nil b+ nil = nil
(x0 x) b+ (x0 y) =  x0 ( x b+ y)
(x0 x) b+ (x1 y) =  x1 ( x b+ y)
(x1 x) b+ (x0 y) =  x1 ( x b+ y)
(x1 x) b+ (x1 y) = x0 ( inc (x b+ y))

double''+ : ∀ (x : Bin) → One x →  x b+ x  ≡ x0 x
double''+ (x1 nil) One1 = refl
double''+  (x0 x)  (x0_One1 cx) = 
  begin
    (x0 x)  b+ (x0 x) ≡⟨⟩
    x0 (x b+ x) ≡⟨ cong x0_ (double''+ x cx) ⟩ -- at the end we find it is the add case don't make it work
    x0 (x0 x)
  ∎

double''+  (x1 x) (x1_One1 cx)  =
  begin
    (x1 x)  b+ (x1 x) ≡⟨⟩
    x0 (inc (x b+ x)) ≡⟨ cong x0_ (cong inc  (double''+ x cx) ) ⟩
    x0 (inc (x0 x))
  ∎


one_from_to : ∀ {x : Bin}
  →  One x
    -------------
  → One (to (from x))  -- which mean x = to (from x)
  
t1 : ∀ (x : Bin)
  → One x
  -----
  → to (from x + from x) ≡ to (from x) b+ to (from x)

t2 : ∀ (x : Bin)
  → One x
  -----
  → to (from (x0 x) ) ≡ x0 (to (from x))
    
can_from : ∀ (x : Bin)
  → Can x
    -------------
  → to (from x) ≡ x
  

t2 (x1 nil) One1 = refl
t2 (x0 x) (x0_One1 cx)  =
  begin
    to (from (x0 (x0 x))) ≡⟨⟩
    to (from (x0 x) + from (x0 x)) ≡⟨ t1 (x0 x) (x0_One1 cx ) ⟩  -- double''+ (to (from (x0 x))) (one_from_to (x0_One1 cx))
    to (from (x0 x)) b+ to (from (x0 x)) ≡⟨ double''+ (to (from (x0 x))) (one_from_to (x0_One1 cx)) ⟩
    x0 (to (from (x0 x)))
  ∎
t2 (x1 x) (x1_One1 cx) =
  begin
    to (from (x0 (x1 x))) ≡⟨⟩
    to (from (x1 x) + from (x1 x)) ≡⟨ t1 (x1 x) (x1_One1 cx) ⟩
    to (from (x1 x)) b+ to (from (x1 x)) ≡⟨ double''+ (to (from (x1 x))) (one_from_to (x1_One1 cx)) ⟩
    x0 (to (from ( x1 x)))
  ∎

t1 (x1 nil) One1 = refl
t1 (x0 x) (x0_One1 cx) rewrite can_from (x0 x) (Can_One (x0_One1 cx))  =
  begin
    to (from (x0 x) + from (x0 x)) ≡⟨⟩
    to ((from x + from x) + (from x + from x)) ≡⟨⟩
    to (from (x0 (x0 x))) ≡⟨ t2 (x0 x) (x0_One1 cx) ⟩ -- we should use the small not the big direction
    x0 (to (from (x0 x))) ≡⟨ cong x0_ (t2 x cx) ⟩
    x0 (x0 (to (from x))) ≡⟨ cong x0_ (cong x0_ (can_from x (Can_One cx))) ⟩
    x0 (x0 x) ≡⟨ sym (double''+ (x0 x) (x0_One1 cx)) ⟩
    (x0 x) b+ (x0 x)
  ∎
t1 (x1 x) (x1_One1 cx) rewrite can_from (x1 x) (Can_One (x1_One1 cx))  =
  begin
    to (from (x1 x) + from (x1 x)) ≡⟨⟩
    to (suc(from x + from x) + suc(from x + from x)) ≡⟨⟩
    to (suc(from x + from x + suc(from x + from x) )) ≡⟨⟩
    inc (to ((from x + from x) + suc(from x + from x))) ≡⟨ cong inc (cong to (+-suc (from x + from x) (from x + from x))) ⟩ 
    inc (to (suc ((from x + from x) + (from x + from x)))) ≡⟨⟩
    inc (inc (to ((from x + from x) + (from x + from x)))) ≡⟨⟩
    inc (inc (to (from (x0 (x0 x))))) ≡⟨ cong inc (cong inc ( t2 (x0 x)  (x0_One1 cx))) ⟩
    inc (inc (x0 (to (from (x0 x))))) ≡⟨ cong inc (cong inc (cong x0_ ( t2 x cx))) ⟩
    inc (inc (x0 (x0 (to (from x))))) ≡⟨ cong inc (cong inc (cong x0_ ( cong x0_ (can_from x (Can_One cx))))) ⟩
    inc (x1 (x0 x)) ≡⟨⟩
    x0 (inc (x0 x)) ≡⟨⟩
    x0 (x1 x) ≡⟨ sym (double''+ (x1 x) (x1_One1 cx)) ⟩
    (x1 x) b+ (x1 x)
  ∎

  
one_from_to { (x1 nil) } (One1) = One1
one_from_to { (x0 x) } (x0_One1 cx) rewrite can_from (x0 x) (Can_One (x0_One1 cx)) = x0_One1 cx
one_from_to { (x1 x) } (x1_One1 cx) rewrite can_from (x1 x) (Can_One (x1_One1 cx)) = x1_One1 cx


can_from (x0 nil) Can_Zero = refl
can_from (x1 nil) (Can_One One1) = refl
can_from (x0 x) (Can_One (x0_One1 cx)) =
  begin
   to (from (x0 x)) ≡⟨⟩
   to (from x + from x) ≡⟨ t1 x cx ⟩
   to (from x) b+ to (from x) ≡⟨ double''+ (to (from x)) (one_from_to cx) ⟩
   x0 (to (from x)) ≡⟨ cong x0_ (can_from x  (Can_One cx)) ⟩
   (x0 x)
  ∎
can_from (x1 x) (Can_One (x1_One1 cx)) =
  begin
   to (from (x1 x)) ≡⟨⟩
   to (suc (from x + from x)) ≡⟨⟩
   inc (to (from x + from x)) ≡⟨⟩
   inc (to (from (x0 x))) ≡⟨ cong inc (t2 x cx) ⟩
   inc (x0 (to (from x))) ≡⟨⟩
   inc(x0 (to (from x))) ≡⟨ cong inc (cong x0_ (can_from x (Can_One cx))) ⟩
   inc (x0 x)
  ∎
  

----------- the from_to  ----------

+-suc-swap : ∀ (m n : ℕ) → suc m + n ≡ m + suc n
+-suc-swap zero n = refl
+-suc-swap (suc m) n =
  begin
  suc (suc m + n) 
  ≡⟨ cong suc (+-suc-swap m n )⟩
  suc (m + suc n)
  ≡⟨⟩
    suc m + suc n
  ∎

r0 : ∀ (x : Bin) → x1 x ≡ inc (x0 x)
r0 x = refl

r1 : ∀ (x : Bin) → suc (from x) ≡ from (inc x)
r1 nil = refl
r1 (x0 x) =
  begin
    suc (from (x0 x)) ≡⟨⟩
    suc (from x + from x)
  ∎
r1 (x1 x) =
  begin
    suc (from (x1 x)) ≡⟨ cong suc (cong from (r0 x))⟩
    suc (suc (from x + from x))  ≡⟨ sym(cong suc (+-suc (from x) (from x))) ⟩
    suc (from x + suc (from x)) ≡⟨ sym(+-suc (from x) ( suc ( from x))) ⟩
    from x + suc (suc (from x)) ≡⟨ cong ((from x +_)) (cong suc (r1 x)) ⟩
    from x + suc (from (inc x)) ≡⟨ sym(+-suc-swap (from x) (from (inc x))) ⟩
    suc(from x) + from (inc x) ≡⟨ cong (_+ from (inc x)) (r1 x) ⟩
    from(inc x) + from(inc x) ≡⟨⟩
    from (x0 (inc x)) ≡⟨⟩
    from (inc (x1 x))
  ∎


r3 : ∀ (x : ℕ) → from (to x) ≡ x
r3 zero = refl 
r3 (suc x) = begin
  from (to (suc x)) ≡⟨⟩
  from (inc (to x)) ≡⟨ sym (r1 (to x))⟩
  suc (from (to x)) ≡⟨ cong suc (r3 x)⟩
  suc (x)
 ∎