CoC Tactics 和 Typing Rules 的關係

H:P  intros H    hypothesis

apply H  (H may contain arrow)

assumption h:P direct of the form

***

Parameter H:Type.

Axiom h:H.

Theorem h' : H.

Proof.

  apply h.

Qed.

***

Example below:

Section Minimal_prop_logic.

  Variables P Q R T : Prop.

  Theorem imp_trans : (P->Q)->(Q->R)->P->R.

  Proof.

    intros H H' p.

    apply H'.

    apply H.

    assumption.  (* p : P hypothesis *)

  Qed.

  Theorem delta : (P->P->Q)->P->Q.

  Proof.

    exact (fun (H:P->P->Q)(p:P) => H p p).

  Qed.

End Minimal_prop_logic.