$ rlwrap coqtop Welcome to Coq 8.1pl2 (Oct. 2007) Coq < Section Predicate_calculus. Coq < Variables P Q: Prop. P is assumed Q is assumed (* we define R to mean the conjunction of P and Q *) Coq < Definition R := P /\Q. R is defined Coq < Theorem Ex2: R -> P. 1 subgoal P : Prop Q : Prop ============================ R -> P Ex2 < intro. 1 subgoal P : Prop Q : Prop H : R ============================ P (* We can unfold the defined term R in hypothesis H *) Ex2 < unfold R in H. 1 subgoal P : Prop Q : Prop H : P /\ Q ============================ P Ex2 < elim H. 1 subgoal P : Prop Q : Prop H : P /\ Q ============================ P -> Q -> P Ex2 < intros. 1 subgoal P : Prop Q : Prop H : P /\ Q H0 : P H1 : Q ============================ P Ex2 < assumption. Proof completed. Ex2 < Save. intro. unfold R in H. elim H. intros. assumption. Ex2 is defined Coq < Theorem Ex3: P -> Q -> R. 1 subgoal P : Prop Q : Prop ============================ P -> Q -> R Ex3 < intros. 1 subgoal P : Prop Q : Prop H : P H0 : Q ============================ R (* We can unfold the definition of R in the goal using "red" *) Ex3 < red. 1 subgoal P : Prop Q : Prop H : P H0 : Q ============================ P /\ Q Ex3 < split. 2 subgoals P : Prop Q : Prop H : P H0 : Q ============================ P subgoal 2 is: Q Ex3 < assumption. 1 subgoal P : Prop Q : Prop H : P H0 : Q ============================ Q Ex3 < assumption. Proof completed. Ex3 < Save. intros. red in |- *. split. assumption. assumption. Ex3 is defined (* Here is an application of "fold" tactic. *) Coq < Theorem Ex4: (R -> P /\ Q). 1 subgoal P : Prop Q : Prop S : Prop ============================ R -> P /\ Q Ex4 < intro. 1 subgoal P : Prop Q : Prop S : Prop H : R ============================ P /\ Q (* we see that the conclusion is R by definition, so we apply fold *). Ex4 < fold R. 1 subgoal P : Prop Q : Prop S : Prop H : R ============================ R Ex4 < assumption. Proof completed. Ex4 <