(*
An apparently wrong induction principle used
in mathematics classrooms is indeed correct... huh wrong?
*)

Section sec_general.

Variable T: Type.

Lemma ex_forall : 
  forall (P: T -> Prop) (Q: Prop),
  (exists x0, P x0 -> Q) -> (forall x0, P x0) -> Q.
Proof.
intros P Q ex f. destruct ex as (x0, q). apply q; apply f. 
Qed.


Lemma ex2_forall : 
  forall (P: T -> Prop) (Q: Prop),
  (exists x0, exists x1, P x0 -> P x1 -> Q) -> (forall x, P x) -> Q.
Proof.
intros P Q ex f. destruct ex as (x0, (x1, q)). apply q; apply f. 
Qed.

(* The converse does not hold, hence the following principles are stricly 
   weaker than corresponding principles where the induction hypothesis is
   (forall n, (forall x', P x' n) -> P x (S n)) *)


Section sec_P.

(** printing xx %\cstxx{}% *)

Variable P : T -> nat -> Prop.
Variable xx : T.

(** * Parametric principles *)

Definition par_principle := 
  P xx 0 -> (forall n, exists y, P y n -> P xx (S n)) -> forall n, P xx n.

Definition wk_par_principle := 
  (forall x, P x 0) -> (forall n, exists y, P y n -> P xx (S n)) -> forall n, P xx n.

Lemma wk_par_principle_is_weaker : par_principle -> wk_par_principle.
Proof.
unfold par_principle, wk_par_principle. intros; firstorder.
Qed.

Definition par_principle2 := 
  P xx 0 -> (forall n, exists y, P y n -> P xx n -> P xx (S n)) -> forall n, P xx n.

Lemma par_principle2_is_stronger : par_principle2 -> par_principle.
Proof.
unfold par_principle, par_principle2. intros. firstorder. 
Qed.

(** * Quantified principles *)

Definition quantif_principle := 
  (forall x, P x 0) -> (forall x n, exists y, P y n -> P x (S n)) -> forall n, P xx n.

Definition fct_principle := 
  (forall x, P x 0) -> (exists f0, forall n, forall x, P (f0 x) n -> P x (S n)) -> forall n, P xx n.

Definition fct_principle2 := 
  (forall x, P x 0) -> (exists f0, forall n, forall x, P (f0 x) n -> P x n -> P x (S n)) -> forall n, P xx n.

Definition dep_fct_principle := 
  (forall x, P x 0) -> (exists f0, forall n, forall x, P (f0 n x) n -> P x (S n)) -> forall n, P xx n. 

Lemma quantif_dep_fct : quantif_principle -> dep_fct_principle.
Proof.
intros qp p0 indhyp n. apply qp; clear qp. 
  exact p0. 
  clear n. intros x n. destruct indhyp as (f0, pSn). 
    exists (f0 n x). apply pSn. 
Qed.

Lemma indep_fct : dep_fct_principle -> fct_principle.
Proof.
intros qp p0 indhyp n. apply qp; clear qp. 
  exact p0. 
  clear n. destruct indhyp as (f0, pSn). 
    exists (fun (n:nat) x => f0 x). exact pSn. 
Qed.

Lemma par_quantif : wk_par_principle -> quantif_principle.
Proof.
intros pp p0 indhyp n. apply pp. 
  exact p0. 
  exact (indhyp xx). 
Qed.

(* the converse does not hold
Lemma quantif_par : quantif_principle -> forall x, par_principle x.
*)

(** * Proofs of [quantif_principle] *)
(** ** Bulldozer proof *)
(* quantif_principle always holds *)
Theorem quantif_principle_bulldozer_proof : quantif_principle.
Proof.
intros p0 indhyp n; generalize xx; clear xx. (** Goal: [forall x : T, P x n] *)
induction n as [|n IHn].
  exact p0. 
  intro x; generalize (indhyp x n). intros (y, pn). apply pn. apply IHn. 
Qed.

(** ** Minimal proof *)

Require Import diag_induction. 

Fixpoint iter (n: nat) (f: T->T) : T -> T :=
  fun x => 
  match n with
  | O => x
  | S n => f (iter n f x)
  end.

Theorem fct_principle_minimal_proof : fct_principle.
Proof.
intros p0 (f0, step).
intros n. generalize (p0 (iter n f0 xx)).
pattern n at 1, 0; apply diag_induction_0_n; simpl.
  trivial. 
  intros p q e hrec P_iterp. apply hrec. apply step. exact P_iterp. 
Qed.

End sec_P.

(** * Wrongness of [wk_par_principle] *)

(** ** General case : [T] has 2 different inhabitants *)
(* Counter example to wk_par_principle, and hence to par_principle *)

Section sec_wk_par_principle_is_wrong.

Variable u v : T.
Hypothesis diff : u <> v.

Inductive L_shape : T -> nat -> Prop :=
  | L0 : forall x, L_shape x 0
  | L1 : L_shape u 1.

Lemma L_shape_step : forall n, exists y, L_shape y n -> L_shape u (S n).
Proof.
intro n; exists v. intros Ln. generalize diff; clear diff. case Ln; clear Ln. 
  intros; apply L1. 
  intro diff; case diff; reflexivity. 
Qed. 

Hypothesis pp_L : forall P x, wk_par_principle P x.

Lemma coroll_par : forall n, L_shape u n. 
Proof.
intros n. apply pp_L. 
  apply L0. 
  exact L_shape_step. 
Qed.

Theorem wrong : False.
Proof. 
generalize (coroll_par 2); intro L2. generalize (refl_equal 2). 
pattern u, 2 at 2; case L2; intros; discriminate. 
Qed.


End sec_wk_par_principle_is_wrong. 


End sec_general.


(** ** Application : [T] is [nat -> nat] *)
Section sec_wk_par_principle_is_wrong_on_nat_arrow_nat.

Definition unn := fun n : nat => 0.
Definition vnn := fun n : nat => 1.

Remark diff_nn : unn <> vnn. 
Proof.
intro e. assert (d: 0 = 1). 
  change (unn 0 = vnn 0). case e. reflexivity. 
  discriminate. 
Qed.

Hypothesis pp_L_nat_nat : forall P f, wk_par_principle (nat -> nat) P f.
Theorem wrong_nn : False.
Proof.
apply (wrong _ unn vnn diff_nn). exact pp_L_nat_nat. 
Qed.

End sec_wk_par_principle_is_wrong_on_nat_arrow_nat.