Complete most of Induction.v

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.
 
 (** [] *)