(** * InductionLecture: Proof by Induction -- Lecture Notes *)

(** These notes accompany the [Induction] chapter of _Logical Foundations_.
    They are meant to be stepped through interactively during lecture. *)

From LF Require Export Basics.

(* ################################################################# *)
(** * Why Induction? *)

(** We know [0 + n = n] by simplification, because [plus] matches on
    its _first_ argument and [0] is concrete.  But what about the
    other direction? *)

Theorem add_0_r_firsttry : forall n : nat, n + 0 = n.
Proof.
  intros n.
  simpl. (* does nothing: [n] is unknown, [match] is stuck *)
Abort.

(** [destruct] gives us two cases but gets stuck in both: *)

Theorem add_0_r_secondtry : forall n : nat, n + 0 = n.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - reflexivity.
  - simpl. (* still stuck: n' is unknown *)
Abort.

(** No finite number of [destruct] steps can handle all [n].
    We need _induction_. *)

(* ################################################################# *)
(** * The [induction] Tactic *)

(** Principle of induction on [nat]:
    To prove [P(n)] for all [n], it suffices to show
    (1) [P(0)], and
    (2) for any [n'], if [P(n')] then [P(S n')].

    The [induction] tactic splits the goal into exactly those two
    subgoals and names the induction hypothesis [IHn']. *)

Theorem add_0_r : forall n : nat, n + 0 = n.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *)
    reflexivity.
  - (* n = S n', IHn' : n' + 0 = n' *)
    simpl. rewrite -> IHn'. reflexivity.
Qed.

(** The second subgoal in slow motion:
<<
    Goal before simpl:  S n' + 0 = S n'
    After simpl:        S (n' + 0) = S n'
    After rewrite IHn': S n' = S n'    (closed by reflexivity)
>>
*)

(** Another example -- both cases need [simpl] + [rewrite]: *)

Theorem minus_n_n : forall n : nat, minus n n = 0.
Proof.
  (* WORKED IN CLASS *)
  intros n. induction n as [| n' IHn'].
  - simpl. reflexivity.
  - simpl. rewrite -> IHn'. reflexivity.
Qed.

(* ================================================================= *)
(** ** In-Class Exercises: Basic Induction *)

(** **** In-class exercise *)
Theorem mul_0_r : forall n : nat, n * 0 = 0.
Proof.
  (* FILL IN HERE *) Admitted.

(** **** In-class exercise: this lemma is useful for [add_comm] *)
Theorem plus_n_Sm : forall n m : nat, S (n + m) = n + (S m).
Proof.
  (* FILL IN HERE *) Admitted.

(** **** In-class exercise: requires [plus_n_Sm] *)
Theorem add_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m. induction n as [| n' IHn'].
  - (* n = 0 *) simpl. induction m as [| m' IHm'].
    -- reflexivity.
    -- simpl. rewrite <- IHm'. reflexivity.
  - (* n = S n' *) simpl. rewrite -> IHn'. rewrite -> plus_n_Sm. reflexivity.
Qed.

(** **** In-class exercise *)
Theorem add_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.
Proof.
  (* FILL IN HERE *) Admitted.

(* ================================================================= *)
(** ** double and its properties *)

Fixpoint double (n : nat) : nat :=
  match n with
  | O    => O
  | S n' => S (S (double n'))
  end.

(** **** In-class exercise *)
Lemma double_plus : forall n, double n = n + n.
Proof.
  (* FILL IN HERE *) Admitted.

(** **** In-class exercise: induction on [n] alone works here *)
Theorem eqb_refl : forall n : nat, (n =? n) = true.
Proof.
  induction n as [| n' IHn'].
  - simpl. reflexivity.
  - simpl. apply IHn'.
Qed.

(* ################################################################# *)
(** * The [replace] Tactic *)

(** Sometimes [rewrite] applies a lemma at the wrong occurrence.
    [replace e1 with e2] lets us say _exactly_ what to replace,
    generating a side obligation [e1 = e2]. *)

(** Example: [rewrite add_comm] rewrites the outermost [+], not
    the inner [n + m] we want. *)

Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  rewrite add_comm. (* rewrites outermost +, not what we want *)
Abort.

(** Fix: use [replace] to target exactly [n + m]: *)

Theorem plus_rearrange : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  replace (n + m) with (m + n).
  - reflexivity.
  - rewrite add_comm. reflexivity.
Qed.

(** Another use of [replace]: clear up a cluttered subexpression
    before the main proof step. *)

Theorem mult_0_plus' : forall n m : nat,
  (n + 0 + 0) * m = n * m.
Proof.
  intros n m.
  replace (n + 0 + 0) with n.
  - reflexivity.
  - rewrite add_comm. simpl. rewrite add_comm. reflexivity.
Qed.

(* ################################################################# *)
(** * Formal vs. Informal Proof *)

(** A Rocq proof is a _program_ a machine can check.  An informal proof
    is a _communication_ aimed at human readers.  The same underlying
    argument takes very different form in each style.

    Rocq proof of [add_assoc]: *)

Theorem add_assoc' : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  intros n m p. induction n as [| n' IHn'].
  - (* Base case (n = 0): both sides reduce to [m + p]. *)
    reflexivity.
  - (* Inductive case (n = S n'): [simpl] reduces both sides under
       the definition of [+]; [IHn'] closes the remaining goal. *)
    simpl. rewrite IHn'. reflexivity.
Qed.

(** Corresponding informal proof:

    _Theorem_: For all [n], [m], [p],  [n + (m + p) = (n + m) + p].

    _Proof_: By induction on [n].

    - _Base case_ ([n = 0]): [0 + (m + p) = (0 + m) + p] follows
      directly from the definition of [+].

    - _Inductive case_ ([n = S n']): Assume the induction hypothesis
      [IHn' : n' + (m + p) = (n' + m) + p].  We must show
      [(S n') + (m + p) = ((S n') + m) + p].
      By the definition of [+], both sides reduce to
      [S (n' + (m + p))] and [S ((n' + m) + p)] respectively, and
      these are equal by [IHn']. _Qed_. *)

(** Key differences:
    - The informal proof explains the _state_ at each step.
    - The formal proof relies on Rocq to track state implicitly.
    - Both have the same two-case structure; induction generates the
      same subgoals that the human proof addresses with bullet points. *)

(* ################################################################# *)
(** * More Exercises *)

(** **** In-class exercise: use [replace] -- no induction needed *)
Theorem add_shuffle3 : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
  (* FILL IN HERE *) Admitted.

(** **** In-class exercise: define a helper lemma first *)
Theorem mul_comm : forall m n : nat, m * n = n * m.
Proof.
  (* FILL IN HERE *) Admitted.

(** **** In-class exercise: classify each before proving
    (a) simpl/rewrite only?  (b) also needs destruct?  (c) also needs induction? *)

Theorem leb_refl : forall n : nat, (n <=? n) = true.
Proof. (* FILL IN HERE *) Admitted.

Theorem zero_neqb_S : forall n : nat, 0 =? (S n) = false.
Proof. (* FILL IN HERE *) Admitted.

Theorem andb_false_r : forall b : bool, andb b false = false.
Proof. (* FILL IN HERE *) Admitted.

Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
Proof. (* FILL IN HERE *) Admitted.

Theorem mult_assoc : forall n m p : nat, n * (m * p) = (n * m) * p.
Proof. (* FILL IN HERE *) Admitted.

(* ################################################################# *)
(** * Nat to Bin and Back *)

(** Recall the binary type from [Basics]: *)

Inductive bin : Type :=
  | Z
  | B0 (n : bin)
  | B1 (n : bin).

(** Note there three constructors.  One for high-impedance or nothing and one
    each for prepending [B0] and [B1].  Note that bits are ordered opposite
    of the traditional way.  [B1 B0 Z] is 01 not 10.  [Z] is nothing and nothing
    is like zero.
    
    [Z = ]
    [B0 Z = 0]
    [B0 B0 Z = 00]
    [B1 B0 B0 Z = 001]
    [B0 B0 B1 Z = 100]

    It's backwards. *)

(** Reference implementations (carry forward from [Basics] exercises).
    [incr] is the classic definition of a carry-forward increment function.
    If the leading bit is [B0] then replace it with [B1].  If it is [B1],
    replace it with [B0] amd propagate the carry by incrementing remaining
    [bin] value *)

Fixpoint incr (m : bin) : bin :=
  match m with
  | Z     => B1 Z
  | B0 m' => B1 m'
  | B1 m' => B0 (incr m')
  end.

(**
  [incr Z] = B1 Z
  [incr B0 B1 Z] = [B1 B1 Z]
  [incr B1 B1 Z] = [B0 B0 B1 Z]
  [incr B0 B1 Z] = [B1 B1 Z]
  [incr B1 B0 Z] = [B0 B1 Z]
*)

(** [bin_to_nat] does what you think it does - converts a binary number
    to a natural by shifting and adding.  Shifting once is multiply
    by 2. Shift and increment is multiple by 2 and add 1. *)

Fixpoint bin_to_nat (m : bin) : nat :=
  match m with
  | Z     => 0
  | B0 m' => 2 * bin_to_nat m'
  | B1 m' => 1 + 2 * bin_to_nat m'
  end.

(** This is why the goofy notation gets used.  You can use recursion in the
    standard way to move through the binary value.  If you use the traditiona
    notation, you would need to move from tbe back of the binary value to
    the front.*)

(** We verified [incr] and [bin_to_nat] with unit tests in [Basics].
    Now let's prove correctness: incrementing and then converting to
    [nat] gives the same result as converting and then adding 1. 

    Commuting diagram:
<<
              nat ---S------> nat
               ^               ^
               |               |
        bin_to_nat          bin_to_nat
               |               |
              bin ---incr---> bin
>>
    The diagram is _commuting_ when every path leads to the same result.
    It relates two _models_ - an _abstract_ model [nat] that specifies
    properties a _concrete_model [bin] should have.  [nat] is more abstract
    than [bin] because while [bin] has [nat]'s properties, [nat] does not
    have all of [bin]'s properties.  There is no concept of a [bit] in
    [nat].

    We like to say that [nat] is a _specification_ for [bin]. Our objective
    building software is getting from an abstract model that describes
    _requirements_ to a concrete model that describes an _implementation_
    that is executable.  This is what a compiler does and we're pretty good
    at writing those.  However, getting from system requirements to a
    compilable represent is still hard.

    AI is changing that by increasing the abstraction level where we work.
    It is not making the problem easier, but instead making it hard in a
    different way.

    Quick note here.  I had this on the board as a communting diagram starting
    from [nat] rather than [bin].  Quite similar things, but this diagram
    corresponds better with our discussion.
*)

(** **** In-class exercise *)
Theorem bin_to_nat_pres_incr : forall b : bin,
  bin_to_nat (incr b) = 1 + bin_to_nat b.
Proof.
  intros b.
  induction b.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. rewrite IHb. simpl. rewrite plus_n_Sm. rewrite add_comm. rewrite add_0_r. reflexivity.
Qed.

  (* FILL IN HERE  Admitted.*)

(** Now define conversion from [nat] to [bin]: *)

(** **** In-class exercise *)
Fixpoint nat_to_bin (n : nat) : bin :=
  match n with
  | O    => Z
  | S n' => incr (nat_to_bin n')
  end.

(** **** In-class exercise: use [bin_to_nat_pres_incr] as a lemma *)
Theorem nat_bin_nat : forall n, bin_to_nat (nat_to_bin n) = n.
Proof.
  intros n. induction n.
  - simpl. reflexivity.
  - simpl. rewrite bin_to_nat_pres_incr. rewrite IHn. reflexivity.
Qed.

(* ================================================================= *)
(** ** Why [bin_nat_bin] Fails *)

(** The opposite direction does NOT hold: *)

Theorem bin_nat_bin_fails : forall b, nat_to_bin (bin_to_nat b) = b.
Proof.
  intros. induction b.
  - simpl. reflexivity.
  - simpl.
Abort.

(** _Why?_  Binary representations are not unique.  For example,
    [B0 Z] and [Z] both represent 0, but [nat_to_bin 0 = Z], so
    [nat_to_bin (bin_to_nat (B0 Z)) = Z <> B0 Z].

    The fix is to _normalize_ [bin] values by stripping leading zeros.
    [B0 B0 B0 B0 Z] needs to be Z.
    
    There is no way to construct [B0 B0 Z] equivalent using [nat] *)

(* ================================================================= *)
(** ** Normalization *)

(** A doubling function on [bin] that preserves representation
  
  bin_to_nat (double_bin b) = 2 * bin_to_nat b :
*)

(** **** In-class exercise *)
Definition double_bin (b : bin) : bin :=
  match b with
  | Z => Z
  | _ => B0 b
  end.

(** It's simply a shift. *)

Example double_bin_zero : double_bin Z = Z. Proof. reflexivity. Qed.

Lemma double_incr_bin : forall b,
  double_bin (incr b) = incr (incr (double_bin b)).
Proof. intros b. destruct b; reflexivity. Qed.

(** A normalized form selects the canonical (leading-zero-free)
    representative.  We build it by scanning from the most-significant
    end and propagating structure via [double_bin]. *)

(** **** In-class exercise: keep it simple -- do NOT use [bin_to_nat] *)
Fixpoint normalize (b : bin) : bin :=
match b with
| Z    => Z
| B0 b' => double_bin (normalize b')
| B1 b' => B1 (normalize b')
end.

(** Sanity check -- the normalized form of [B0 Z] should be [Z]: *)
Example normalize_B0_Z : normalize (B0 Z) = Z. Proof. simpl. reflexivity. Qed.
Example normalize_B0_B0_Z : normalize (B0 (B0 Z)) = Z. Proof. simpl. reflexivity. Qed.
Example normalize_B1_B0_Z : normalize (B1 (B0 Z)) = (B1 Z). simpl. reflexivity. Qed.

(** Helper: incrementing a doubled value gives the next odd number. *)
Lemma incr_double_bin : forall b, incr (double_bin b) = B1 b.
Proof. intros b. destruct b; reflexivity. Qed.

(** Helper: converting [n + n] to bin equals doubling [nat_to_bin n]. *)
Lemma nat_to_bin_double : forall n, nat_to_bin (n + n) = double_bin (nat_to_bin n).
Proof.
  intros n. induction n as [| n' IHn'].
  - reflexivity.
  - simpl. rewrite <- plus_n_Sm. simpl.
    rewrite IHn'. rewrite double_incr_bin. reflexivity.
Qed.

(** Now the corrected round-trip theorem holds: *)

(** **** In-class exercise *)
Theorem bin_nat_bin : forall b, nat_to_bin (bin_to_nat b) = normalize b.
Proof.
  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. apply incr_double_bin.
Qed.

(** Notes from Claude

The current normalize at line 390 is wrong — B0 b' => normalize b' strips the B0 and changes the value, making bin_nat_bin unprovable. The correct definition uses double_bin to strip leading zeros while preserving value. I'll fix normalize, prove the missing lemmas, and complete the proof.

Edit InductionLecture.v
Added 11 lines
Here's what I changed and why:

normalize was wrong — B0 b' => normalize b' dropped the B0 and changed the value (e.g., normalize (B0 (B1 Z)) = B1 Z, but B0 (B1 Z) = 2 while B1 Z = 1). The fix is B0 b' => double_bin (normalize b'), which strips leading zeros by using double_bin Z = Z while preserving value.

Two helper lemmas added:

incr_double_bin : forall b, incr (double_bin b) = B1 b — follows immediately by destruct, since double_bin b = B0 b for any non-Z b, and incr (B0 x) = B1 x.
nat_to_bin_double : forall n, nat_to_bin (n + n) = double_bin (nat_to_bin n) — proved by induction using double_incr_bin.
bin_nat_bin proof strategy for each case of b:

Z: both sides reduce to Z.
B0 b': simpl gives nat_to_bin (n + (n + 0)) = double_bin (normalize b'). Strip the +0 with add_0_r, apply nat_to_bin_double, then close with IHb.
B1 b': same setup yields incr (double_bin (normalize b')) = B1 (normalize b'),
closed by incr_double_bin.
*) 

(* 2026-01-07 13:17 *)