Software Foundation Ch1's 'Binary' Exercise

sf_ch1_binary

Inductive bin : Type :=
  | Zero : bin
  | Twice : bin -> bin
  | TwicePlusOne : bin -> bin.

Fixpoint incr (b : bin) : bin :=
  match b with
  | Zero => TwicePlusOne Zero
  | Twice b' => TwicePlusOne b'
  | TwicePlusOne b' => Twice (incr b')
  end.

Fixpoint bin_to_nat (b : bin) : nat :=
  match b with
  | Zero => O
  | Twice b' => (bin_to_nat b') + (bin_to_nat b')
  | TwicePlusOne b' => S ((bin_to_nat b') + (bin_to_nat b'))
  end.

Lemma sn_plus_sn_eq_two_succ :
  forall (m n : nat), S m + S n = S (S (m + n)).
Proof.
  intros m n. 
  induction m as [|m' IH]. 
  induction n as [|n' IH'].
  simpl. reflexivity.
  simpl. reflexivity.
  simpl. rewrite <- IH. simpl. reflexivity.
  Qed.

Theorem conv_incr_eq :
  forall (b : bin), bin_to_nat (incr b) = S (bin_to_nat b).
Proof.
  intros b. induction b as [|b'|b' IH'].
  simpl. reflexivity.
  simpl. reflexivity.
  simpl. rewrite -> IH'. rewrite <- sn_plus_sn_eq_two_succ. reflexivity.
  Qed.

My proof for the last exercise in sf.ch1.

The lemma is to demonstrate that succ(n) + succ(m) = 2 + m + n = succ(succ(m+n)). With this in hand we can prove the invariant noted in the text (i.e. a binary value incremented and then converted to unary is equivalent to one plus a binary value converted to unary). If we did not use this lemma or mathematical induction, we would be stuck in a loop after line 36 as the cases would repeat (thanks to line 10 of our fixpoint definition of incr).