Binary addition

binary.v

Section Binary.

Inductive Bits : nat -> Set :=
| xO : forall {m : nat}, Bits m -> Bits (S m)
| xI : forall {m : nat}, Bits m -> Bits (S m)
| xo : Bits 0
| xi : Bits 0.

Fixpoint to_nat {n : nat} (b : Bits n) : nat := match b with
| xi => 1
| xo => 0
| xI b' => 1 + 2 * to_nat b'
| xO b' => 2 * to_nat b'
end.

Eval compute in (to_nat (xO xi)).

Fixpoint addc {n : nat} : Bits n -> Bits n -> bool -> Bits (S n) :=
match n with
| 0 => fun (b0 b1 : Bits 0) (c : bool) =>
  match b0, b1, c with
    |xo, xo, false => xO xo
    |xo, xo, true => xI xo
    |xo, xi, false => xI xo
    |xo, xi, true => xO xi
    |xi, xo, false => xI xo
    |xi, xo, true => xO xi
    |xi, xi, false => xO xi
    |xi, xi, true => xI xi
  end
| S n' => fun (b0 b1 : Bits (S n')) c =>
  let h : forall (m0 m1 : nat), Bits m0 -> Bits m1 -> (Bits n' -> Bits n' -> Bits (S (S n'))) -> (S m0 = S n' -> S m1 = S n' -> Bits (S (S n')))
    := fun (m0 m1 : nat) b0' b1' (p : Bits n' -> Bits n' -> Bits (S (S n')))
    => (fun H0 : S m0 = S n'
    => let b0'' : Bits n' := eq_rec m0 Bits b0' n' (eq_add_S m0 n' H0) in
    fun H1 : S m1 = S n'
    => let b1'' : Bits n' := eq_rec m1 Bits b1' n' (eq_add_S m1 n' H1) in  p b0'' b1'') in
  (match b0 in Bits m0, b1 in Bits m1, c return m0 = S n' -> m1 = S n' -> Bits (S (S n')) with
    | @xO m0 b0', @xO m1 b1', false => h m0 m1 b0' b1' (fun b0'' b1'' => xO (addc b0'' b1'' false))
    | @xO m0 b0', @xO m1 b1', true  => h m0 m1 b0' b1' (fun b0'' b1'' => xI (addc b0'' b1'' false))
    | @xO m0 b0', @xI m1 b1', false => h m0 m1 b0' b1' (fun b0'' b1'' => xI (addc b0'' b1'' false))
    | @xO m0 b0', @xI m1 b1', true  => h m0 m1 b0' b1' (fun b0'' b1'' => xO (addc b0'' b1'' true))
    | @xI m0 b0', @xO m1 b1', false => h m0 m1 b0' b1' (fun b0'' b1'' => xI (addc b0'' b1'' false))
    | @xI m0 b0', @xO m1 b1', true  => h m0 m1 b0' b1' (fun b0'' b1'' => xO (addc b0'' b1'' true))
    | @xI m0 b0', @xI m1 b1', false => h m0 m1 b0' b1' (fun b0'' b1'' => xO (addc b0'' b1'' true))
    | @xI m0 b0', @xI m1 b1', true  => h m0 m1 b0' b1' (fun b0'' b1'' => xI (addc b0'' b1'' true))
    | xo, _, _ => (fun (H0 : 0 = S n') H1 => False_rec (Bits (S (S n'))) (O_S n' H0))
    | xi, _, _ => (fun (H0 : 0 = S n') H1 => False_rec (Bits (S (S n'))) (O_S n' H0))
    | _, xo, _ => (fun H0 (H1 : 0 = S n') => False_rec (Bits (S (S n'))) (O_S n' H1))
    | _, xi, _ => (fun H0 (H1 : 0 = S n') => False_rec (Bits (S (S n'))) (O_S n' H1))
  end) eq_refl eq_refl
end.

Eval compute in (addc (xO xi) (xI xi) false).

Require Import Program Omega.

Goal forall (n : nat) (b0 b1 : Bits n) (c : bool),
  to_nat (addc b0 b1 c) = (if c then 1 else 0) + to_nat b0 + to_nat b1.
Proof.
induction n;intros b0 b1 c.
case c;dependent destruction b0;dependent destruction b1;reflexivity.
case c;dependent destruction b0;dependent destruction b1;simpl;rewrite IHn;omega.
Qed.

End Binary.