(* All of the theorems in this section we can prove with the tactics
   [intro] (and [intros]), [assumption], and [apply].  All of these
   lemmas are in propositional logic. *)

Section Minimal_Propositional_Logic.
  Variables P Q R T : Prop.

  Theorem imp_trans : (P->Q) -> (Q->R) -> (P->R).
   (*  Proof (fun (H1:P->Q) (H2:Q->R) (p:P) => H2 (H1 p)). *)
  (* A goal-directed proof: *)
     Proof.  auto.  Qed.

  (* More examples *)
  Lemma id_P : P -> P.
    Proof.  intros.  assumption.  Qed.
  Lemma id_PP : (P->P) -> (P->P).
    Proof.  intro H.  assumption.  Qed.
  Lemma imp_perm : (P->Q->R) -> (Q->P->R).
    Proof.  intros.  apply H.  assumption.  assumption.  Qed.
  Lemma ignore_Q : (P->R)->P->Q->R.
    Proof. intros. apply H. apply H0. Qed.
  Lemma delta_imp : (P->P->Q)->P->Q.
    Proof. intros. apply H. assumption. assumption. Qed.
  Lemma delta_impR : (P->Q)->(P->P->Q).
    Proof. intros. apply H. assumption. Qed.
  Lemma weak_peirce : ((((P->Q)->P)->P)->Q)->Q.
Proof.
    intros. apply H. intros. apply H0. intro.  apply H. intros. assumption. Qed.

End Minimal_Propositional_Logic.

(* Now type "Print delta_imp" and notice how P, Q, R, etc. are all quantified. 
   This illustrates that the underlying proof language, in these cases
   is actually System F (where P, Q, R etc. are type variables).  *)

(* To handle first-order logic, which uses quantification, we need dependent types. *)
   
Section firstorder.

Variable A : Set.
Variables P : A -> Prop.
Variable e : A.

Theorem indeed : (forall x:A, P x) -> P e.
intros.
apply (H e).
Qed.

End firstorder.

(* Printing indeed yields

indeed = 
fun (A : Set) (P : A -> Prop) (e : A) (H : forall x : A, P x) => H e
     : forall (A : Set) (P : A -> Prop) (e : A), (forall x : A, P x) -> P e

The "fun ..." part is the proof, and the "forall (A : Set) ..." part is the
proposition being proved.  Notice how in the forall x : A, P x, that x is a TERM
that is bound in the type P x.  This is a dependent type.

*)