(**
   Additional simple exercises on the tactics [apply] and [refine],
   for exploiting hypotheses (or theorems) which are implications
   or universally quantified.
*)

(* ---------------------------------------------------------------------- *)
(** * Reminders *)

(** Tactics [refine], [intro] [apply] and [revert]

- [intro x]
  is the same as
  [refine (fun x => _)]

- [revert x] is the converse of [intro x];
  it is essentially the same as
  [refine (_ x); clear x].
  The effect of [clear x] is to remove [x] from the visible environment
  (its scope is closed).

- [apply f]
  is the same as
  [refine f], or
  [refine (f _)], or
  [refine (f _ _)], etc.
  according to the type of [f].

  Example
<<
  f : T1 -> T2
  ============
  T2
>>
  Here we can use [refine (f _)], then we still have to find
  something of type [T1].

  - [destruct E as [ (* Cons1 *) x | (* Cons2 *) | (* Cons3 *) y z] )
  - [destruct E as [ x |  |  y z] )
  - [destruct E as [  |  | ] )  (* NOT RECOMMENDED! *)
    is the same as
<<
    refine (match E with
             | Cons1 x => _
             | Cons2 => _
             | Cons3 y z => _
             end).
    refine (match E with
             | Cons2 => _
             | _ => _default
             end).
>>
    where the type of [E] is an inductive type with constructors [Cons1],
    [Cons2] and [Cons3] having respectively 1, 0 and 2 arguments.
 *)

(** ** The universe Prop *)
(**
    Proof trees are in an universe which is "parallel" to [Set],
    called [Prop].

    In particular, equalities are in [Prop].
 *)
Check (nat -> nat).
Check (2 = 2).
Check (2 = 3).

Check Set.
Check Prop.
Check Type.
(* Cumulative "floating" hierarchy of universes *)

Section sec_ABC.
  (** Consider arbitrary propositions [A] [B] [C]... *)
  Variable A B C : Prop.
  (** ... and arbitrary predicates [P] [Q] [R] over [nat] *)
  Variable P Q R : nat -> Prop.
  Check (nat -> Prop).

 (** Exercise: prove the following using only [refine] or [intro] or [apply]. *)
 (** Use the command [Show Proof] after each tactic to see how the proof tree
     (as a function) develops step by step. *)
  Lemma impl_trans:
    (A -> B) -> (B -> C) -> (A -> C).
  Proof.
    (** START WITH a sequence of [intro] and/or [refine]  *)


    (** FINISH WITH a sequence of [apply] and/or [refine]  *)

  Admitted.

  Lemma combi_S:   (A -> B -> C) -> (A -> B) -> A -> C.
  Proof.
    (* PLEASE COMPLETE *)

  Admitted.

  Lemma forall_impl_trans:
    (forall n:nat, P n -> Q n) ->
    (forall n:nat, Q n -> R n) ->
    (forall n:nat, P n -> R n).
  Proof.
    (* PLEASE COMPLETE *)

  Admitted.

End sec_ABC.