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

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

(* -------------------------------------------------------------------- *)
Section MoveHyp.
  Variable T : Type.
  Variable P : T -> Prop.
  Variable Q : T -> Prop.

  Hypothesis P2Q: forall x, P x -> Q x.

  Goal forall a, P a -> False.
  Proof.
    move=> a h. move/P2Q: h=> h.
  Abort.
End MoveHyp.

Section MoveHyp2.
  Variable T : Type.
  Variable P : T -> Prop.
  Variable Q : T -> Prop.

  Hypothesis P2Q: forall x, P x <-> Q x.

  Goal forall a, P a -> False.
  Proof.
    move=> a h. move/P2Q: h=> h.
  Abort.
End MoveHyp2.

Section CaseHyp.
  Variable P : nat -> Prop.
  Variable Q : nat -> Prop.

  Hypothesis QP:
    forall n, Q n -> (P n) \/ (P n.+1).

  Goal forall a, Q a -> False.
  Proof.
    move=> a h. case/QP: h.
  Abort.
End CaseHyp.

Section AppGoal.
  Variable T : Type.
  Variable P : T -> Prop.
  Variable Q : T -> Prop.

  Hypothesis P2Q: forall x, P x <-> Q x.

  Goal forall a, P a.
  Proof.
    move=> a. apply/P2Q. apply/P2Q.
  Abort.
End AppGoal.

Section HypSpec.
  Variable P : nat -> Prop.

  Goal (forall n, P (2 * n)) -> False.
  Proof.
    move/(_ 3).
  Abort.
End HypSpec.

(* -------------------------------------------------------------------- *)
Goal
  forall (b1 b2 G1 G2 : bool),
    if b1 && b2 then G1 else G2.
Proof.
  move=> b1 b2 G1 G2. case: (@andP b1 b2).
Abort.

Goal forall (b1 b2 G : bool), b1 && b2 -> G.
Proof.
  move=> b1 b2 G h. move/andP: h => h.
Abort.

Goal forall (b1 b2 G : bool), b1 && b2 -> G.
Proof.
  move=> b1 b2 G h. case/andP: h.
Abort.

Goal forall (b1 b2 : bool), b1 /\ b2.
Proof.
  move=> b1 b2. apply/andP.
Abort.

Goal forall (b : bool), reflect b b.
Proof.
  move=> b; case: b.
    exact: ReflectT.
    exact: ReflectF.
Qed.

(* -------------------------------------------------------------------- *)
Goal forall (b1 b2 b3 : bool), b1 = ~~ (b2 || b3).
Proof.
  move=> b1 b2 b3. apply/idP/norP.
Abort.

(* -------------------------------------------------------------------- *)
Goal forall (f : nat -> nat) (n1 n2 : nat), n1 == n2 -> f n1 = f n2.
Proof.
  move=> f n1 n2 eq. rewrite (eqP eq). by [].
Qed.

(* -------------------------------------------------------------------- *)
Lemma nat_sind (P : nat -> Prop):
  (forall p, (forall n, n < p -> P n) -> P p) ->
    forall n, P n.
Proof.
  move=> ind n; move: {-2}n (leqnn n).
  elim: n => [|n IH] k le_k; apply ind=> p.
  + by move: le_k; rewrite leqn0=> /eqP ->.
  by move=> le_pk; apply IH; rewrite -ltnS (@leq_trans k).
Qed.

Lemma nat_ind2 (P : nat -> Prop):
  P 0 -> P 1 -> (forall p, P p -> P p.+1 -> P p.+2)
  -> forall n, P n.
Proof.  
  move=> P0 P1 ind; elim/nat_sind; case=> [//|[//|p IH]].
  by apply: ind; apply IH.
Qed.

Goal forall n, exists p, p = 2 * n.
Proof.
  elim/nat_sind.
Abort.

Goal forall n, exists p, p = 2 * n.
Proof.
  elim/nat_ind2.
Abort.

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