From b4ffd07a914e7d97c3db04a1d7fe2d95210a68c4 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 6 Sep 2010 16:20:06 +0000 Subject: Update for current Coq syntax --- etc/coq/naming.v | 57 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 29 insertions(+), 28 deletions(-) (limited to 'etc/coq') diff --git a/etc/coq/naming.v b/etc/coq/naming.v index ee078a60..53455239 100644 --- a/etc/coq/naming.v +++ b/etc/coq/naming.v @@ -1,49 +1,50 @@ (* Coq theorems, etc can be named at the top .... *) -Theorem and_comms: (A,B:Prop)(A /\ B) -> (B /\ A). - Intros A B H. - Induction H. - Apply conj. - Assumption. - Assumption. +Theorem and_comms: forall (A B:Prop),(A /\ B) -> (B /\ A). + intros A B H. + induction H. + apply conj. + assumption. + assumption. Qed. (* at the bottom... *) -Goal (A,B:Prop)(A /\ B) -> (B /\ A). - Intros A B H. - Induction H. - Apply conj. - Assumption. - Assumption. +Goal forall (A B:Prop),(A /\ B) -> (B /\ A). + intros A B H. + induction H. + apply conj. + assumption. + assumption. Save and_comms2. (* or not at all! *) (* Coq calls this "Unamed_thm", so must forget it like any other *) (* test: do, undo, then check shell buffer to see "Reset Unnamed_thm" *) -Goal (A,B:Prop)(A /\ B) -> (B /\ A). - Intros A B H. - Induction H. - Apply conj. - Assumption. - Assumption. +Goal forall (A B:Prop),(A /\ B) -> (B /\ A). + intros A B H. + induction H. + apply conj. + assumption. + assumption. Save. -(* Odd side effect: two unnamed theorems in a row are not possible! *) +(* Odd side effect: two unnamed theorems in a row are not possible! + Latest: with Coq 8.2, we get Unamed_thm0, Unamed_thm1, ... *) +Goal forall (A B:Prop),(A /\ B) -> (B /\ A). + intros A B H. + induction H. + apply conj. + assumption. + assumption. +Save. (* TESTING: notice output window behaviour here with different settings: exact output displayed also depends on how many steps are issued at once. *) -Goal (A,B:Prop)(and A B) -> (and B A). -Intros A B H. -Induction H. -Apply conj. -Assumption. -Assumption. +Goal forall (A B:Prop),(A /\ B) -> (B /\ A). +tauto. Save. - - - -- cgit v1.2.3