Complete Induction.v

Induction.v

@@ -836,7 +836,7 @@ Proof.
     simpl.
     rewrite <- plus_n_Sm.
     reflexivity.
-Qed.    
+Qed.
 
 (** **** Exercise: 3 stars, standard (nat_bin_nat) *)
 
@@ -895,19 +895,11 @@ Qed.
 
 (** Now define a similar doubling function for [bin]. *)
 
-(*
-Fixpoint double_bin (b:bin) : bin :=
-match b with
-| Z => Z
-| B0 Z => B1 Z
-| B1 Z => B0 (B1 Z)
-| B0 n' => B0 (double_bin n')
-| B1 n' => B1 (double_bin n')
-end.
- *)
-
 Definition double_bin (b:bin) : bin :=
-  nat_to_bin (double (bin_to_nat b)).
+  match b with
+  | Z => Z
+  | b => B0 b
+  end.
 
 (** Check that your function correctly doubles zero. *)
 
@@ -920,10 +912,11 @@ Lemma double_incr_bin : forall b,
     double_bin (incr b) = incr (incr (double_bin b)).
 Proof.
   intros b.
-  induction b as[| b0 IHb0 | b1 IHb1].
+  destruct b as[| b0 | b1].
   - reflexivity.
-  - simpl.
-    Abort.
+  - reflexivity.
+  - reflexivity.
+Qed.
 
 (** [] *)
 
@@ -944,7 +937,12 @@ Abort.
     [double_bin] that might have failed to satisfy [double_bin_zero]
     yet otherwise seem correct. *)
 
-(* FILL IN HERE *)
+(*
+  Just as we can add preceding zeros to a number and have it still be
+  the same number, we can do the same here. The simplest case is how
+  (B0 Z) is equivalent to 0. But this also goes for (B1 (B0 Z)) which
+  is equiv to (B1 Z).
+*)
 
 (** To solve that problem, we can introduce a _normalization_ function
     that selects the simplest [bin] out of all the equivalent
@@ -961,14 +959,35 @@ Abort.
     end of the [bin] and _only_ processes each bit only once. Do not
     try to "look ahead" at future bits. *)
 
-Fixpoint normalize (b:bin) : bin
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+(* Fixpoint normalize (b:bin) : bin :=
+  match b with
+  | Z => Z
+  | B1 (b') => B1 (normalize b')
+  | B0 (b') => match normalize b' with
+              | Z => Z
+              | n => B0 n
+              end
+  end. *)
+
+Fixpoint normalize (b:bin) : bin :=
+  match b with
+  | Z => Z
+  | B0 b' => double_bin (normalize b')
+  | B1 b' => incr (double_bin (normalize b'))
+  end.
 
 (** It would be wise to do some [Example] proofs to check that your definition of
     [normalize] works the way you intend before you proceed. They won't be graded,
     but fill them in below. *)
 
-(* FILL IN HERE *)
+Example normalize_0 : normalize (B0 (B0 (B0 (B0 Z)))) = Z.
+Proof. simpl. reflexivity. Qed.
+
+Example normalize_1 : normalize (B1 (B0 (B0 (B0 Z)))) = B1 Z.
+Proof. reflexivity. Qed.
+
+Example normalize_2 : normalize (B0 (B1 (B0 (B0 Z)))) = B0 (B1 Z).
+Proof. reflexivity. Qed.
 
 (** Finally, prove the main theorem. The inductive cases could be a
     bit tricky.
@@ -979,10 +998,35 @@ Fixpoint normalize (b:bin) : bin
     progress. We have one lemma for the [B0] case (which also makes
     use of [double_incr_bin]) and another for the [B1] case. *)
 
+Lemma nat_to_bin_double : forall n,
+  nat_to_bin (n + n) = double_bin (nat_to_bin n).
+Proof.
+  intros n.
+  induction n.
+  - reflexivity.
+  - simpl.
+    rewrite <- plus_n_Sm.
+    rewrite double_incr_bin.
+    rewrite <- IHn.
+    reflexivity.
+Qed.
+
 Theorem bin_nat_bin : forall b, nat_to_bin (bin_to_nat b) = normalize b.
 Proof.
-  (* FILL IN HERE *) Admitted.
-
+  intros b.
+  induction b.
+  - reflexivity.
+  - simpl.
+    rewrite add_0_r.
+    rewrite nat_to_bin_double.
+    rewrite IHb.
+    reflexivity.
+  - simpl.
+    rewrite add_0_r.
+    rewrite nat_to_bin_double.
+    rewrite IHb.
+    reflexivity.
+Qed.
 (** [] *)
 
 (* 2026-01-07 13:17 *)