(* -------------------------------------------------------------------- *)
Require Import ssreflect eqtype ssrbool ssrnat ssrfun path.

(* -------------------------------------------------------------------- *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* -------------------------------------------------------------------- *)
(* For this section:                                                    *)
(*   only move=> h, move/V: h => h, case/V: h, by ... allowed           *)
(* -------------------------------------------------------------------- *)
Goal forall (P Q : Prop), (P <-> Q) -> P -> Q.
Proof.
(*D*) move=> P Q h hp. by move/h: hp => hp.
Qed.

Goal forall (P : nat -> Prop) (Q : Prop),
     (P 0 -> Q)
  -> (forall n, P n.+1 -> P n)
  -> P 4 -> Q.
Proof.
(*D*) move=> P Q P0Q Pp P4.
(*D*) move/Pp: P4 => P3.
(*D*) move/Pp: P3 => P2.
(*D*) move/Pp: P2 => P1.
(*D*) move/Pp: P1 => P0.
(*D*) by move/P0Q: P0.
Qed.

Goal forall (b b1 b2 : bool), (b1 -> b) -> (b2 -> b) -> b1 || b2 -> b.
Proof. (* No case analysis on b, b1, b2 allowed *)
(*D*) move=> b b1 b2 h1 h2 h. case/orP: h.
(*D*)   by move/h1.
(*D*)   by move/h2.
Qed.

Goal forall (Q : nat -> Prop) (p1 p2 : nat -> bool) x,
  ((forall y, Q y -> p1 y /\ p2 y) /\ Q x) -> p1 x && p2 x.
Proof.
(*D*) move=> Q p1 p2 x h. case: h. move=> /(_ x) h qx.
(*D*) move/h: qx. by move/andP.
Qed.

Goal forall (Q : nat -> Prop) (p1 p2 : nat -> bool) x,
  ((forall y, Q y -> p1 y \/ p2 y) /\ Q x) -> p1 x || p2 x.
Proof.
(*D*) move=> Q p1 p2 x h. case: h. move=> /(_ x) h qx.
(*D*) move/h: qx. by move/orP.
Qed.

(* -------------------------------------------------------------------- *)
(* No xxxP lemmas allowed                                               *)
(* -------------------------------------------------------------------- *)
Lemma myidP: forall (b : bool), reflect b b.
Proof.
(*D*) move=> b. case: b.
(*D*)   exact: ReflectT.
(*D*)   exact: ReflectF.
Qed.

Lemma mynegP: forall (b : bool), reflect (~ b) (~~ b).
Proof.
(*D*) move=> b. case: b.
(*D*)   exact: ReflectF.
(*D*)   exact: ReflectT.
Qed.

Lemma myandP: forall (b1 b2 : bool), reflect (b1 /\ b2) (b1 && b2).
Proof.
(*D*) move=> b1 b2. case: b1.
(*D*)  case b2.
(*D*)    exact: ReflectT.
(*D*)    apply: ReflectF. move=> h. by case: h.
(*D*)  case b2.
(*D*)    apply: ReflectF. move=> h. by case: h.
(*D*)    apply: ReflectF. move=> h. by case: h.
Qed.

Lemma myiffP:
  forall (P Q : Prop) (b : bool),
    reflect P b -> (P -> Q) -> (Q -> P) -> reflect Q b.
Proof.
(*D*) move=> P Q b Pb PQ QP. move: Pb. case: b.
(*D*)   move=> h. case: h.
(*D*)     move/PQ=> hp. by apply: ReflectT.
(*D*)     move=> hNp. apply: ReflectF. move/QP=> hp.
(*D*)     by move/hNp: hp.
(*D*)   move=> h. case: h.
(*D*)     move/PQ=> hq. by apply: ReflectT.
(*D*)     move=> hNp. apply: ReflectF. move/QP=> hp.
(*D*)     by move/hNp: hp.
Qed.

(* -------------------------------------------------------------------- *)
Fixpoint len (n m : nat) : bool :=
  match n, m with
  | 0    , _     => true
  | n'.+1, 0     => false
  | n'.+1, m'.+1 => len n' m'
  end.

Lemma lenP: forall n m, reflect (exists k, k + n = m) (len n m).
Proof.
(*D*) move=> n; elim: n.
(*D*)   move=> m. apply: (iffP idP).
(*D*)     move=> _. by exists m.
(*D*)     by [].
(*D*)   move=> n IH m. apply: (iffP idP).
(*D*)     case: m. by [].
(*D*)       move=> m /= le_nm. move/IH: le_nm=> le_nm.
(*D*)       case: le_nm. move=> k eq_xk_m. exists k.
(*D*)       by rewrite -eq_xk_m addnS.
(*D*)     case: m.
(*D*)       case. move=>k. by rewrite addnS.
(*D*)       move=> m h. case: h => k.
(*D*)       rewrite addnS. move=> eq_kSn_k. case: eq_kSn_k.
(*D*)       move=> eq_kn_m. apply/IH. by exists k.
Qed.


(* --------------------------------------------------------------------*)
Lemma snat_ind : forall (P : nat -> Prop),
  (forall x, (forall y, y < x -> P y) -> P x)
  -> forall x, P x.
Proof.
  (* Hint: strengthen P x into (forall y, y <= x -> P y) and then
   *       perform the induction on x. *)
(*D*) move=> P ind x; move: {-2}x (leqnn x); elim: x.
(*D*)   + move=> x. rewrite leqn0. move/eqP=> z_x.
(*D*)     rewrite z_x. by apply: ind.
(*D*)   + move=> n IHn x. rewrite leq_eqVlt. move=> h. case/orP: h.
(*D*)     * move=> eq_x_Sn. rewrite (eqP eq_x_Sn). apply ind.
(*D*)       move=> y. rewrite ltnS. by move/IHn.
(*D*)     * rewrite ltnS. by move/IHn.
Qed.

Lemma odd_ind : forall (P : nat -> Prop),
  P 0 -> P 1 -> (forall x, P x  -> P x.+2)
  -> forall x, P x. 
Proof.
(*D*) move=> P p0 p1 ind. elim/snat_ind.
(*D*) move=> x; case: x.
(*D*)   + by [].
(*D*)   + move=> x; case: x.
(*D*)     * by [].
(*D*)     * move=> x h. apply ind. by apply h.
Qed.

Lemma oddSS : forall n, odd n.+2 = odd n.
Proof.
(*D*) move=> n. by rewrite /= negbK.
Qed.

Lemma odd_add : forall m n, odd (m + n)  = odd m (+) odd n. (* using odd_ind *)
Proof.
(*D*) elim/odd_ind.
(*D*) + by [].
(*D*) + by [].
(*D*) + move=> m IHm n. by rewrite !oddSS IHm.
Qed.

(* -------------------------------------------------------------------- *)
Lemma nat_ind2: forall (P : nat -> Prop),
  P 0 -> P 1 -> (forall p, P p -> P p.+1 -> P p.+2)
  -> forall n, P n.
Proof.
(*D*) move=> P p0 p1 ind. elim/snat_ind.
(*D*) move=> x; case: x.
(*D*)   + by [].
(*D*)   + move=> x; case: x.
(*D*)     * by [].
(*D*)     * move=> x h. apply ind.
(*D*)       by apply h. by apply h.
Qed.

Fixpoint fib n :=
  match n with
  | 0              => 1
  | 1              => 1
  | (n.+1 as p).+1 => fib p + fib n
  end.

Lemma fib0: fib 0 = 1.
Proof. by []. Qed.

Lemma fib1: fib 1 = 1.
Proof. by []. Qed.

Lemma fibSS: forall n, fib n.+2 = fib n.+1 + fib n.
Proof. by []. Qed.

Goal
  forall p q,
    (fib (p.+1 + q.+1))
    = (fib p.+1) * (fib q.+1) + (fib p) * (fib q).
Proof.
(*D*) elim/nat_ind2.
(*D*)   move=> q. by rewrite add1n fib1 fib0 !mul1n fibSS.
(*D*)   move=> q. rewrite add2n !fibSS !fib1 !fib0.
(*D*)   by rewrite add1n mul2n mul1n -addnn addnAC.
(*D*)   move=> p IHp IHSp q.
(*D*)   rewrite 2!addSn fibSS -addSn IHp IHSp.
(*D*)   rewrite !fibSS !muln_addl -!addnA.
(*D*)   by rewrite (addnCA (fib p.+1 * fib q) _ _).
Qed.

(* 
*** Local Variables: ***
*** coq-load-path: ("ssreflect" ".") ***
*** End: ***
 *)