Complete most of Induction.v

Basics.v

@@ -345,18 +345,35 @@ Compute (invert bw_white).
     over [simpl] and go directly to [reflexivity]. We'll explain
     what's happening later in the chapter. *)
 
-Definition nandb (b1:bool) (b2:bool) : bool
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition nandb (b1:bool) (b2:bool) : bool :=
+  match b1 with
+    | true => negb b2
+    | false => true
+  end.
 
 Example test_nandb1:               (nandb true false) = true.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_nandb2:               (nandb false false) = true.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_nandb3:               (nandb false true) = true.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_nandb4:               (nandb true true) = false.
-(* FILL IN HERE *) Admitted.
-(** [] *)
+Proof.
+  simpl.
+  reflexivity.
+Qed.
 
 (** **** Exercise: 1 star, standard (andb3)
 
@@ -364,18 +381,36 @@ Example test_nandb4:               (nandb true true) = false.
     return [true] when all of its inputs are [true], and [false]
     otherwise. *)
 
-Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
+  match b1, b2, b3 with
+  | true, true, true => true
+  | _, _, _ => false
+  end.
+
 
 Example test_andb31:                 (andb3 true true true) = true.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_andb32:                 (andb3 false true true) = false.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_andb33:                 (andb3 true false true) = false.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_andb34:                 (andb3 true true false) = false.
-(* FILL IN HERE *) Admitted.
-(** [] *)
+Proof.
+  simpl.
+  reflexivity.
+Qed.
 
 (* ================================================================= *)
 (** ** Types *)
@@ -816,14 +851,23 @@ Fixpoint exp (base power : nat) : nat :=
     factorial was not found in the current environment," it means
     you've forgotten the [:=]. *)
 
-Fixpoint factorial (n:nat) : nat
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Fixpoint factorial (n:nat) : nat :=
+  match n with
+  | O => S O
+  | S p => mult (S p) (factorial p)
+  end.
 
 Example test_factorial1:          (factorial 3) = 6.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_factorial2:          (factorial 5) = (mult 10 12).
-(* FILL IN HERE *) Admitted.
-(** [] *)
+Proof.
+  simpl.
+  reflexivity.
+Qed.
 
 (** Again, we can make numerical expressions easier to read and write
     by introducing notations for addition, subtraction, and
@@ -917,18 +961,36 @@ Proof. simpl. reflexivity.  Qed.
     function.  It can be done with just one previously defined
     function, but you can use two if you want. *)
 
-Definition ltb (n m : nat) : bool
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition ltb (n m : nat) : bool :=
+  if m <=? n then false else true.
+  (* match n, m with *)
+  (* | S n', S m' => ltb n' m' *)
+  (* | _, O => false *)
+  (* | O, _ => true *)
+  (* end. *)
+
 
 Notation "x <? y" := (ltb x y) (at level 70) : nat_scope.
 
 Example test_ltb1:             (ltb 2 2) = false.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 Example test_ltb2:             (ltb 2 4) = true.
-(* FILL IN HERE *) Admitted.
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
+
 Example test_ltb3:             (ltb 4 2) = false.
-(* FILL IN HERE *) Admitted.
-(** [] *)
+Proof.
+  simpl.
+  reflexivity.
+Qed.
+
 
 (* ################################################################# *)
 (** * Proof by Simplification *)
@@ -1091,8 +1153,10 @@ Proof.
 Theorem plus_id_exercise : forall n m o : nat,
   n = m -> m = o -> n + m = m + o.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros n m o H1 H2.
+  rewrite -> H1, H2.
+  reflexivity.
+Qed.
 
 (** The [Admitted] command tells Rocq that we want to skip trying
     to prove this theorem and just accept it as a given.  This is
@@ -1142,9 +1206,11 @@ Proof.
 Theorem mult_n_1 : forall p : nat,
   p * 1 = p.
 Proof.
-  (* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros n.
+  rewrite <- mult_n_Sm.
+  rewrite <- mult_n_O.
+  reflexivity.
+Qed.
 
 (* ################################################################# *)
 (** * Proof by Case Analysis *)
@@ -1348,8 +1414,16 @@ Qed.
 Theorem andb_true_elim2 : forall b c : bool,
   andb b c = true -> c = true.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros b c.
+  destruct b eqn:Eb.
+  - simpl.
+    intros H.
+    rewrite <- H.
+    reflexivity.
+  - simpl.
+    intros H.
+    discriminate H.
+Qed.
 
 (** Before closing the chapter, we should mention one final
     convenience.  As you may have noticed, many proofs perform case
@@ -1389,8 +1463,10 @@ Qed.
 Theorem zero_nbeq_plus_1 : forall n : nat,
   0 =? (n + 1) = false.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros [].
+  - reflexivity.
+  - reflexivity.
+Qed.
 
 (* ================================================================= *)
 (** ** More on Notation (Optional) *)
@@ -1474,9 +1550,14 @@ Fixpoint plus' (n : nat) (m : nat) : nat :=
     homework assignment, make sure you comment out your solution so
     that it doesn't cause Rocq to reject the whole file!) *)
 
-(* FILL IN HERE
-
-    [] *)
+(*
+Fixpoint rejectme (a b: nat) : nat :=
+  match a, b with
+  | O, _ => b
+  | _, O => a
+  | S a', S b' => if even a then rejectme a' b else rejectme a b'
+  end.
+*)
 
 (* ################################################################# *)
 (** * More Exercises *)
@@ -1494,9 +1575,10 @@ Theorem identity_fn_applied_twice :
   (forall (x : bool), f x = x) ->
   forall (b : bool), f (f b) = b.
 Proof.
-  (* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros f H b.
+  rewrite -> H, H.
+  reflexivity.
+Qed.
 
 (** **** Exercise: 1 star, standard (negation_fn_applied_twice)
 
@@ -1504,7 +1586,16 @@ Proof.
     to the previous one but where the hypothesis says that the
     function [f] has the property that [f x = negb x]. *)
 
-(* FILL IN HERE *)
+Theorem negation_fn_applied_twice :
+  forall (f : bool -> bool),
+  (forall (x : bool), f x = negb x) ->
+  forall (b : bool), f (f b) = b.
+Proof.
+  intros f H b.
+  rewrite -> H, H.
+  rewrite -> negb_involutive.
+  reflexivity.
+Qed.
 
 (* Do not modify the following line: *)
 Definition manual_grade_for_negation_fn_applied_twice : option (nat*string) := None.
@@ -1519,12 +1610,48 @@ Definition manual_grade_for_negation_fn_applied_twice : option (nat*string) := N
     [destruct] and [rewrite], but destructing everything in sight is
     not the best way.) *)
 
+Theorem orb_true : forall (b : bool), true || b = true.
+Proof.
+  destruct b.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+Theorem andb_true : forall (b : bool), true && b = b.
+Proof.
+  destruct b.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+Theorem orb_false : forall (b : bool), false || b = b.
+Proof.
+  destruct b.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+Theorem andb_false : forall (b : bool), false && b = false.
+Proof.
+  destruct b.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
 Theorem andb_eq_orb :
   forall (b c : bool),
   (andb b c = orb b c) ->
   b = c.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros b c H.
+  destruct b.
+  - rewrite andb_true, orb_true in H.
+    rewrite <- H.
+    reflexivity.
+  - rewrite andb_false, orb_false in H.
+    rewrite <- H.
+    reflexivity.
+Qed.
 
 (** [] *)
 
@@ -1627,8 +1754,13 @@ Compute letter_comparison B F.
 Theorem letter_comparison_Eq :
   forall l, letter_comparison l l = Eq.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  destruct l.
+  reflexivity.
+  reflexivity.
+  reflexivity.
+  reflexivity.
+  reflexivity.
+Qed.
 
 (** We can follow the same strategy to define the comparison operation
     for two grade modifiers.  We consider them to be ordered as
@@ -1658,29 +1790,34 @@ Definition modifier_comparison (m1 m2 : modifier) : comparison :=
     of a suitable call to [letter_comparison] to end up with just [3]
     possibilities. *)
 
-Definition grade_comparison (g1 g2 : grade) : comparison
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition grade_comparison (g1 g2 : grade) : comparison :=
+  match g1, g2 with
+  | Grade l1 m1, Grade l2 m2 =>
+    match letter_comparison l1 l2 with
+    | Gt => Gt
+    | Lt => Lt
+    | Eq => modifier_comparison m1 m2
+    end
+  end.
 
 (** The following "unit tests" of your [grade_comparison] function
     should pass once you have defined it correctly. *)
 
 Example test_grade_comparison1 :
   (grade_comparison (Grade A Minus) (Grade B Plus)) = Gt.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_grade_comparison2 :
   (grade_comparison (Grade A Minus) (Grade A Plus)) = Lt.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_grade_comparison3 :
   (grade_comparison (Grade F Plus) (Grade F Plus)) = Eq.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_grade_comparison4 :
   (grade_comparison (Grade B Minus) (Grade C Plus)) = Gt.
-(* FILL IN HERE *) Admitted.
-
-(** [] *)
+Proof. reflexivity. Qed.
 
 (** Now that we have a definition of grades and how they compare to
     one another, let us implement a late-penalty fuction. *)
@@ -1736,9 +1873,14 @@ Theorem lower_letter_lowers:
     letter_comparison F l = Lt ->
     letter_comparison (lower_letter l) l = Lt.
 Proof.
-(* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros l H.
+  destruct l.
+  - simpl. reflexivity.
+  - simpl. reflexivity.
+  - simpl. reflexivity.
+  - simpl. reflexivity.
+  - rewrite <- H. simpl. reflexivity.
+Qed.
 
 (** **** Exercise: 2 stars, standard (lower_grade)
 
@@ -1757,61 +1899,47 @@ Proof.
     cases.
 
     Our solution is under 10 lines of code total. *)
-Definition lower_grade (g : grade) : grade
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition lower_grade (g : grade) : grade :=
+  match g with
+  | Grade F Minus => Grade F Minus
+  | Grade l Plus => Grade l Natural
+  | Grade l Natural => Grade l Minus
+  | Grade l Minus => Grade (lower_letter l) Plus
+  end.
 
 Example lower_grade_A_Plus :
   lower_grade (Grade A Plus) = (Grade A Natural).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_A_Natural :
   lower_grade (Grade A Natural) = (Grade A Minus).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_A_Minus :
   lower_grade (Grade A Minus) = (Grade B Plus).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_B_Plus :
   lower_grade (Grade B Plus) = (Grade B Natural).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_F_Natural :
   lower_grade (Grade F Natural) = (Grade F Minus).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_twice :
   lower_grade (lower_grade (Grade B Minus)) = (Grade C Natural).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example lower_grade_thrice :
   lower_grade (lower_grade (lower_grade (Grade B Minus))) = (Grade C Minus).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 (** Rocq makes no distinction between an [Example] and a [Theorem]. We
     state the following as a [Theorem] only as a hint that we will use
     it in proofs below. *)
 Theorem lower_grade_F_Minus : lower_grade (Grade F Minus) = (Grade F Minus).
-Proof.
-(* FILL IN HERE *) Admitted.
-
-(* GRADE_THEOREM 0.25: lower_grade_A_Plus *)
-(* GRADE_THEOREM 0.25: lower_grade_A_Natural *)
-(* GRADE_THEOREM 0.25: lower_grade_A_Minus *)
-(* GRADE_THEOREM 0.25: lower_grade_B_Plus *)
-(* GRADE_THEOREM 0.25: lower_grade_F_Natural *)
-(* GRADE_THEOREM 0.25: lower_grade_twice *)
-(* GRADE_THEOREM 0.25: lower_grade_thrice *)
-(* GRADE_THEOREM 0.25: lower_grade_F_Minus
-
-    [] *)
+Proof. reflexivity. Qed.
 
 (** **** Exercise: 3 stars, standard (lower_grade_lowers)
 
@@ -1830,9 +1958,10 @@ Theorem lower_grade_lowers :
     grade_comparison (Grade F Minus) g = Lt ->
     grade_comparison (lower_grade g) g = Lt.
 Proof.
-  (* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros [].
+  simpl.
+  destruct l, m; simpl; intros H; apply H.
+Qed.
 
 (** Now that we have implemented and tested a function that lowers a
     grade by one step, we can implement a specific late-days policy.
@@ -1886,9 +2015,10 @@ Theorem no_penalty_for_mostly_on_time :
     (late_days <? 9 = true) ->
     apply_late_policy late_days g = g.
 Proof.
-  (* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros.
+  rewrite -> apply_late_policy_unfold, H.
+  reflexivity.
+Qed.
 
 (** The following theorem states that, if a student has between 9 and
     16 late days, their final grade is lowered by one step. *)
@@ -1900,9 +2030,11 @@ Theorem grade_lowered_once :
     (late_days <? 17 = true) ->
     (apply_late_policy late_days g) = (lower_grade g).
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros.
+  rewrite -> apply_late_policy_unfold, H, H0.
+  reflexivity.
+Qed.
 
-(** [] *)
 End LateDays.
 
 (* ================================================================= *)
@@ -1945,11 +2077,19 @@ Inductive bin : Type :=
     for binary numbers, and a function [bin_to_nat] to convert
     binary numbers to unary numbers. *)
 
-Fixpoint incr (m:bin) : bin
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Fixpoint incr (m:bin) : bin :=
+  match m with
+  | Z => B1 Z
+  | B0 b => B1 b
+  | B1 b => B0 (incr b)
+  end.
 
-Fixpoint bin_to_nat (m:bin) : nat
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Fixpoint bin_to_nat (m:bin) : nat :=
+  match m with
+  | Z => O
+  | B0 m' => 2 * (bin_to_nat m')
+  | B1 m' => S (2 * (bin_to_nat m'))
+  end.
 
 (** The following "unit tests" of your increment and binary-to-unary
     functions should pass after you have defined those functions correctly.
@@ -1958,29 +2098,27 @@ Fixpoint bin_to_nat (m:bin) : nat
     next chapter. *)
 
 Example test_bin_incr1 : (incr (B1 Z)) = B0 (B1 Z).
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr2 : (incr (B0 (B1 Z))) = B1 (B1 Z).
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr3 : (incr (B1 (B1 Z))) = B0 (B0 (B1 Z)).
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr4 : bin_to_nat (B0 (B1 Z)) = 2.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr5 :
         bin_to_nat (incr (B1 Z)) = 1 + bin_to_nat (B1 Z).
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr6 :
         bin_to_nat (incr (incr (B1 Z))) = 2 + bin_to_nat (B1 Z).
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_bin_incr7 : bin_to_nat (B0 (B0 (B0 (B1 Z)))) = 8.
-(* FILL IN HERE *) Admitted.
-
-(** [] *)
+Proof. reflexivity. Qed.
 
 (* ################################################################# *)
 (** * Optional: Testing Your Solutions *)

Induction.v

@@ -243,23 +243,38 @@ Proof.
 Theorem mul_0_r : forall n:nat,
   n * 0 = 0.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n.
+  induction n as [| n' IHn'].
+  - simpl. reflexivity.
+  - simpl. rewrite -> IHn'. reflexivity.
+Qed.
 
 Theorem plus_n_Sm : forall n m : nat,
   S (n + m) = n + (S m).
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n m.
+  induction n as [| n' IHn'].
+  - simpl. reflexivity.
+  - simpl. rewrite -> IHn'. reflexivity.
+Qed.
 
 Theorem add_comm : forall n m : nat,
   n + m = m + n.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n m.
+  induction n as [| n' IHn'].
+  - simpl. rewrite -> add_0_r. reflexivity.
+  - simpl. rewrite -> IHn', plus_n_Sm. reflexivity.
+Qed.
 
 Theorem add_assoc : forall n m p : nat,
   n + (m + p) = (n + m) + p.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros n m p.
+  induction n as [| n' IHn'].
+  - simpl. reflexivity.
+  - simpl. rewrite -> IHn'. reflexivity.
+Qed.
 
 (** **** Exercise: 2 stars, standard (double_plus)
 
@@ -275,8 +290,11 @@ Fixpoint double (n:nat) :=
 
 Lemma double_plus : forall n, double n = n + n .
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros n.
+  induction n as [| n' IHn'].
+  - reflexivity.
+  - simpl. rewrite -> IHn', plus_n_Sm. reflexivity.
+Qed.
 
 (** **** Exercise: 2 stars, standard (eqb_refl)
 
@@ -286,8 +304,11 @@ Proof.
 Theorem eqb_refl : forall n : nat,
   (n =? n) = true.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros n.
+  induction n as [| n' IHn'].
+  - reflexivity.
+  - simpl. rewrite -> IHn'. reflexivity.
+Qed.
 
 (** **** Exercise: 2 stars, standard, optional (even_S)
 
@@ -301,8 +322,11 @@ Proof.
 Theorem even_S : forall n : nat,
   even (S n) = negb (even n).
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros.
+  induction n as [| n' IHn'].
+  - reflexivity.
+  - rewrite -> IHn', negb_involutive. simpl. reflexivity.
+Qed.
 
 (* ################################################################# *)
 (** * Proofs Within Proofs *)
@@ -488,7 +512,48 @@ Proof.
 
     Theorem: Addition is commutative.
 
-    Proof: (* FILL IN HERE *)
+    Theorem add_comm : forall n m : nat,
+      n + m = m + n.
+    Proof.
+      intros n m.
+      induction n as [| n' IHn'].
+      - simpl. rewrite -> add_0_r. reflexivity.
+      - simpl. rewrite -> IHn', plus_n_Sm. reflexivity.
+    Qed.
+
+    Theorem: For any natural number [n] and [m],
+
+      n + m = m + n
+
+    Proof: By induction on [n].
+
+    - First, suppose [n = 0]. We must show that
+
+      0 + m = m + 0
+
+      This follows directly from the definition of [+] and [add_0_r].
+
+    - Next, suppose [n = S n'], where
+
+      n' + m = m + n'
+
+      We must now show that
+
+      S(n') + m = m + S(n')
+
+      By the definition of [+], we have that
+
+      S(n' + m) = m + S(n')
+
+      By [plus_n_Sm], we further have that
+
+      S(n' + m) = S(m + n')
+
+      By the induction hypothesis, we can see that
+
+      S(m + n') = S(m + n')
+
+      _Qed_.
 *)
 
 (* Do not modify the following line: *)
@@ -521,7 +586,12 @@ Definition manual_grade_for_eqb_refl_informal : option (nat*string) := None.
 Theorem add_shuffle3 : forall n m p : nat,
   n + (m + p) = m + (n + p).
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n m p.
+  rewrite -> add_assoc, add_assoc.
+  replace (m + n) with (n + m).
+  - reflexivity.
+  - rewrite -> add_comm. reflexivity.
+Qed.
 
 (** Now prove commutativity of multiplication.  You will probably want
     to look for (or define and prove) a "helper" theorem to be used in
@@ -530,8 +600,17 @@ Proof.
 Theorem mul_comm : forall m n : nat,
   m * n = n * m.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros m n.
+  induction n as [| n' IHn'].
+  - rewrite -> mul_0_r.
+    simpl.
+    reflexivity.
+  - simpl.
+    rewrite <- IHn'.
+    replace (m * S n') with (m + m * n').
+    + reflexivity.
+    + rewrite <- mult_n_Sm, add_comm. reflexivity.
+Qed.
 
 (** **** Exercise: 3 stars, standard, optional (more_exercises)
 
@@ -543,30 +622,117 @@ Proof.
     to turn in your piece of paper; this is just to encourage you to
     reflect before you hack!) *)
 
+(*
+  This seems like it would need to be proven for all numbers,
+  so it probably requires induction (c).
+
+  "Why is it not (b)?"
+
+  Because even if we destruct n into its variants and get rid of
+  the S() in the second variant, we're left n' + n' which requires our
+  original hypothesis.
+*)
 Theorem leb_refl : forall n:nat,
   (n <=? n) = true.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n.
+  induction n as [| n' IHn'].
+  - reflexivity.
+  - simpl. rewrite IHn'. reflexivity.
+Qed.
 
+(*
+  Here, it probably holds to just prove this for both variants of nat,
+  so maybe (b)
+
+  "Why is it not (a)?"
+
+  The terms are not just a syntactic reordering of each other.
+*)
 Theorem zero_neqb_S : forall n:nat,
   0 =? (S n) = false.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n.
+  destruct n.
+  - reflexivity.
+  - reflexivity.
+Qed.
 
+(*
+  This also seems like it would need to be proven for both variants of bool.
+  Maybe (b)
+
+  "Why is it not (a)?"
+
+  The terms here are not just a syntactic reordering of each other either.
+*)
 Theorem andb_false_r : forall b : bool,
   andb b false = false.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros b.
+  destruct b.
+  - reflexivity.
+  - reflexivity.
+Qed.
 
+(*
+  This follows from the definition of nat, so maybe (a)
+*)
 Theorem S_neqb_0 : forall n:nat,
   (S n) =? 0 = false.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n.
+  reflexivity.
+Qed.
 
+(*
+  This needs to be proven for all n, so maybe (c)
+
+  "Why is it not (b)?"
+
+  Even if we destruct n, we're going to end up needing the very theorem itself
+  to get rid of "1 *". Usually, when you require the theorem you're trying to prove
+  while you're proving it, it's a sign that you should be using induction.
+*)
 Theorem mult_1_l : forall n:nat, 1 * n = n.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n.
+  destruct n.
+  - reflexivity.
+  - simpl. rewrite add_comm, plus_O_n. reflexivity.
+Qed.
+(*
+  My prediction here was wrong, I noticed while I was solving with induction
+  and I suddenly didn't need the induction hypothesis. Not quite sure why simpl is
+  able to replace the "1 *" part.
+*)
 
+
+
+(* helper theorems for [all3_spec] *)
+Theorem negb_or_negb : forall b c : bool, negb b || negb c = negb (b && c).
+Proof.
+  intros b c.
+  destruct b.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+Theorem a_or_negb_a : forall b : bool, b || negb b = true.
+Proof.
+  intros b.
+  destruct b.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+(*
+  This is probably (b), it does not follow from the definition of the bool structure
+  itself. We'll have to show that it works for all combinations. We _could_ possibly
+  rewrite the expression in terms of previously proven theorems about tautologies and
+  falsums of the logical operators, but that would just be outsourcing the
+  "check all combinations" work.
+*)
 Theorem all3_spec : forall b c : bool,
   orb
     (andb b c)
@@ -574,18 +740,37 @@ Theorem all3_spec : forall b c : bool,
          (negb c))
   = true.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros b c.
+  rewrite negb_or_negb, a_or_negb_a.
+  reflexivity.
+Qed.
 
+(*
+  I believe this one requires induction to move all the [S()] constructors
+  from one side to the other, for all possible [nat]s
+*)
 Theorem mult_plus_distr_r : forall n m p : nat,
   (n + m) * p = (n * p) + (m * p).
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n m p.
+  induction n as [| n' IHn'].
+  - reflexivity.
+  - simpl. rewrite IHn'. rewrite add_assoc. reflexivity.
+Qed.
 
+(*
+  I believe this one also requires induction. For (b), we would have to destruct the number
+  all the way to its base in order to move around the constructors, which effectively
+  means we would be doing induction.
+*)
 Theorem mult_assoc : forall n m p : nat,
   n * (m * p) = (n * m) * p.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros n m p.
+  induction n as [| n IHn'].
+  - reflexivity.
+  - simpl. rewrite IHn', mult_plus_distr_r. reflexivity.
+Qed.
 
 (* ################################################################# *)
 (** * Nat to Bin and Back to Nat *)
@@ -602,11 +787,19 @@ Inductive bin : Type :=
     from [Basics].  That will make it possible for this file to
     be graded on its own. *)
 
-Fixpoint incr (m:bin) : bin
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Fixpoint incr (m:bin) : bin :=
+  match m with
+  | Z => B1 Z
+  | B0 b => B1 b
+  | B1 b => B0 (incr b)
+  end.
 
-Fixpoint bin_to_nat (m:bin) : nat
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Fixpoint bin_to_nat (m:bin) : nat :=
+  match m with
+  | Z => O
+  | B0 m' => 2 * (bin_to_nat m')
+  | B1 m' => S (2 * (bin_to_nat m'))
+  end.
 
 (** In [Basics], we did some unit testing of [bin_to_nat], but we
     didn't prove its correctness. Now we'll do so. *)
@@ -634,16 +827,26 @@ Fixpoint bin_to_nat (m:bin) : nat
 Theorem bin_to_nat_pres_incr : forall b : bin,
   bin_to_nat (incr b) = 1 + bin_to_nat b.
 Proof.
-  (* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros b.
+  induction b as [| b' _| b'' IHb''].
+  - reflexivity.
+  - reflexivity.
+  - simpl.
+    rewrite IHb''.
+    simpl.
+    rewrite <- plus_n_Sm.
+    reflexivity.
+Qed.    
 
 (** **** Exercise: 3 stars, standard (nat_bin_nat) *)
 
 (** Write a function to convert natural numbers to binary numbers. *)
 
-Fixpoint nat_to_bin (n:nat) : bin
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Fixpoint nat_to_bin (n:nat) : bin :=
+  match n with
+  | O => Z
+  | S n' => incr (nat_to_bin n')
+  end.
 
 (** Prove that, if we start with any [nat], convert it to [bin], and
     convert it back, we get the same [nat] which we started with.
@@ -657,9 +860,11 @@ Fixpoint nat_to_bin (n:nat) : bin
 
 Theorem nat_bin_nat : forall n, bin_to_nat (nat_to_bin n) = n.
 Proof.
-  (* FILL IN HERE *) Admitted.
-
-(** [] *)
+  intros n.
+  induction n as [| n' IHn'].
+  - reflexivity.
+  - simpl. rewrite bin_to_nat_pres_incr, IHn'. reflexivity.
+Qed.
 
 (* ################################################################# *)
 (** * Bin to Nat and Back to Bin (Advanced) *)
@@ -682,24 +887,43 @@ Abort.
 
 Lemma double_incr : forall n : nat, double (S n) = S (S (double n)).
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros n.
+  destruct n.
+  - reflexivity.
+  - reflexivity.
+Qed.
 
 (** Now define a similar doubling function for [bin]. *)
 
-Definition double_bin (b:bin) : bin
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+(*
+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)).
 
 (** Check that your function correctly doubles zero. *)
 
 Example double_bin_zero : double_bin Z = Z.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 (** Prove this lemma, which corresponds to [double_incr]. *)
 
 Lemma double_incr_bin : forall b,
     double_bin (incr b) = incr (incr (double_bin b)).
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros b.
+  induction b as[| b0 IHb0 | b1 IHb1].
+  - reflexivity.
+  - simpl.
+    Abort.
 
 (** [] *)