Basic.v

Inductive binnat: Type :=
| BO: binnat
| BDbl: binnat -> binnat
| BSDbl: binnat -> binnat.

Fixpoint binc (n: binnat) : binnat :=
match n with
| BO => BSDbl BO
| BDbl m => BSDbl m
| BSDbl m => BDbl (binc m)
end.

Fixpoint bin_to_nat (n: binnat) : nat :=
match n with
| BO => O
| BDbl m => 2 * (bin_to_nat m)
| BSDbl m => (2 * (bin_to_nat m)) + 1
end.

Require Import Coq.Arith.Plus.

Theorem bin_sound:
∀ (b: binnat), bin_to_nat (binc b) = (bin_to_nat b) + 1 .
Proof.
intros b.
induction b.
simpl.
reflexivity.
simpl.
reflexivity.
simpl.
replace (bin_to_nat (binc b)) with ((bin_to_nat b) + 1) .
generalize (bin_to_nat b) as n.
intros n.
replace (n + 1 + 0) with (n + 1).
replace (n + 0) with n.
replace (n + 1 + (n + 1)) with (n + n + (1 + 1)).
apply plus_assoc.
apply plus_permute_2_in_4.
replace (n + 0) with (0 + n).
apply plus_0_l .
apply plus_comm.
generalize (n + 1) as m .
intros m.
replace (m + 0) with (0 + m).
apply plus_0_l.
apply plus_comm.
Qed.