(** * IndPrinciples: Induction Principles *)

(** With the Curry-Howard correspondence and its realization in Coq in
    mind, we can now take a deeper look at induction principles. *)

Set Warnings "-notation-overridden,-parsing".
From LF Require Export ProofObjects.

(* ################################################################# *)
(** * Basics *)

(** The automatically generated _induction principle_ for [nat]: *)

Check nat_ind :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, P n -> P (S n)) ->
    forall n : nat, P n.

(** In English: Suppose [P] is a property of natural numbers (that is,
      [P n] is a [Prop] for every [n]). To show that [P n] holds of all
      [n], it suffices to show:

      - [P] holds of [0]
      - for any [n], if [P] holds of [n], then [P] holds of [S n]. *)

(** We can directly use the induction principle with [apply]: *)

Theorem mult_0_r' : forall n:nat,
  n * 0 = 0.
Proof.
  apply nat_ind.
  - (* n = O *) reflexivity.
  - (* n = S n' *) simpl. intros n' IHn'. rewrite -> IHn'.
    reflexivity.  Qed.

(** Why the [induction] tactic is nicer than [apply]:
     - [apply] requires extra manual bookkeeping (the [intros] in the
       inductive case)
     - [apply] requires [n] to be left universally quantified
     - [apply] requires us to manually specify the name of the induction
       principle. *)

(** Coq generates induction principles for every datatype defined with
    [Inductive], including those that aren't recursive. *)

(** If we define type [t] with constructors [c1] ... [cn],
    Coq generates:

    t_ind : forall P : t -> Prop,
              ... case for c1 ... ->
              ... case for c2 ... -> ...
              ... case for cn ... ->
              forall n : t, P n

    The specific shape of each case depends on the arguments to the
    corresponding constructor. *)

(** An example with no constructor arguments: *)

Inductive time : Type :=
  | day
  | night.

Check time_ind :
  forall P : time -> Prop,
    P day ->
    P night ->
    forall t : time, P t.

(** An example with constructor arguments: *)

Inductive natlist : Type :=
  | nnil
  | ncons (n : nat) (l : natlist).

Check natlist_ind :
  forall P : natlist -> Prop,
    P nnil  ->
    (forall (n : nat) (l : natlist),
        P l -> P (ncons n l)) ->
    forall l : natlist, P l.

(** In general, the automatically generated induction principle for
    inductive type [t] is formed as follows:

    - Each constructor [c] generates one case of the principle.
    - If [c] takes no arguments, that case is:

      "P holds of c"

    - If [c] takes arguments [x1:a1] ... [xn:an], that case is:

      "For all x1:a1 ... xn:an,
          if [P] holds of each of the arguments of type [t],
          then [P] holds of [c x1 ... xn]"

      But that oversimplifies a little.  An assumption about [P]
      holding of an argument [x] of type [t] actually occurs
      immediately after the quantification of [x].
*)

(** For example, suppose we had written the definition of [natlist] a little
    differently: *)

Inductive natlist' : Type :=
  | nnil'
  | nsnoc (l : natlist') (n : nat).

(** Now the induction principle case for [nsnoc1] is a bit different
    than the earlier case for [ncons]: *)

Check natlist'_ind :
  forall P : natlist' -> Prop,
    P nnil' ->
    (forall l : natlist', P l -> forall n : nat, P (nsnoc l n)) ->
    forall n : natlist', P n.



(* ################################################################# *)
(** * Induction Principles for Propositions *)

(** Inductive definitions of propositions also cause Coq to generate
    induction priniciples.  For example, recall our proposition [ev],
    repeated here as [ev'']: *)

Inductive ev'' : nat -> Prop :=
| ev_0 : ev'' 0
| ev_SS (n : nat) : ev'' n -> ev'' (S (S n)).

Check ev''_ind :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, ev'' n -> P n -> P (S (S n))) ->
    forall n : nat, ev'' n -> P n.

(** In English, [ev''_ind] says: Suppose [P] is a property of natural
    numbers.  To show that [P n] holds whenever [n] is even, it suffices
    to show:

      - [P] holds for [0],

      - for any [n], if [n] is even and [P] holds for [n], then [P]
        holds for [S (S n)]. *)

(** The precise form of an [Inductive] definition can affect the
    induction principle Coq generates. *)

Inductive le1 : nat -> nat -> Prop :=
     | le1_n : forall n, le1 n n
     | le1_S : forall n m, (le1 n m) -> (le1 n (S m)).

Notation "m <=1 n" := (le1 m n) (at level 70).

(** [n] could instead be a parameter:  *)

Inductive le2 (n:nat) : nat -> Prop :=
  | le2_n : le2 n n
  | le2_S m (H : le2 n m) : le2 n (S m).

Notation "m <=2 n" := (le2 m n) (at level 70).

Check le1_ind :
  forall P : nat -> nat -> Prop,
    (forall n : nat, P n n) ->
    (forall n m : nat, n <=1 m -> P n m -> P n (S m)) ->
    forall n n0 : nat, n <=1 n0 -> P n n0.

Check le2_ind :
  forall (n : nat) (P : nat -> Prop),
    P n ->
    (forall m : nat, n <=2 m -> P m -> P (S m)) ->
    forall n0 : nat, n <=2 n0 -> P n0.

(** The latter is simpler, and corresponds to Coq's own
    definition. *)

(* ################################################################# *)
(** * Explicit Proof Objects for Induction (Optional) *)

(** Recall again the induction principle on naturals that Coq generates for
    us automatically from the Inductive declation for [nat]. *)

Check nat_ind :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, P n -> P (S n)) ->
    forall n : nat, P n.

(** There's nothing magic about this induction lemma: it's just
   another Coq lemma that requires a proof.  Coq generates the proof
   automatically too...  *)

Print nat_ind.

(** We can rewrite that more tidily as follows: *)
Fixpoint build_proof
         (P : nat -> Prop)
         (evPO : P 0)
         (evPS : forall n : nat, P n -> P (S n))
         (n : nat) : P n :=
  match n with
  | 0 => evPO
  | S k => evPS k (build_proof P evPO evPS k)
  end.

Definition nat_ind_tidy := build_proof.

(** Recursive function [build_proof] thus pattern matches against
    [n], recursing all the way down to 0, and building up a proof
    as it returns. *)