From 76970fb98e79c59a358472b46232deb328eaac8e Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 28 Feb 2018 09:01:07 -0500 Subject: [PATCH] Small improvements to IntroToProofScripting --- IntroToProofScripting.v | 12 +++++++----- IntroToProofScripting_template.v | 5 +---- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/IntroToProofScripting.v b/IntroToProofScripting.v index e4ee2c8..7717a4b 100644 --- a/IntroToProofScripting.v +++ b/IntroToProofScripting.v @@ -373,7 +373,7 @@ Ltac completer := | [ |- _ /\ _ ] => constructor | [ |- forall x, _ ] => intro | [ |- _ -> _ ] => intro - (* Interestingly, these last two rules are redundant. + (* Interestingly, the last rule is redundant with the second-last. * See CPDT for details.... *) end. @@ -859,21 +859,23 @@ Section t7'. Qed. End t7'. +(* One more example of working with existentials: *) + Theorem t8 : exists p : nat * nat, fst p = 3. Proof. econstructor. instantiate (1 := (3, 2)). + (* ^-- We use [instantiate] to plug in a value for one of the "question-mark + * variables" in the conclusion. The [1 :=] part says "first such variable + * mentioned in the conclusion, counting from right to left." *) equality. Qed. (* A way that plays better with automation: *) -Ltac equate x y := - let dummy := constr:(eq_refl x : x = y) in idtac. - Theorem t9 : exists p : nat * nat, fst p = 3. Proof. econstructor; match goal with - | [ |- fst ?x = 3 ] => equate x (3, 2) + | [ |- fst ?x = 3 ] => unify x (3, 2) end; equality. Qed. diff --git a/IntroToProofScripting_template.v b/IntroToProofScripting_template.v index 16861c9..ef6d341 100644 --- a/IntroToProofScripting_template.v +++ b/IntroToProofScripting_template.v @@ -545,12 +545,9 @@ Qed. (* A way that plays better with automation: *) -Ltac equate x y := - let dummy := constr:(eq_refl x : x = y) in idtac. - Theorem t9 : exists p : nat * nat, fst p = 3. Proof. econstructor; match goal with - | [ |- fst ?x = 3 ] => equate x (3, 2) + | [ |- fst ?x = 3 ] => unify x (3, 2) end; equality. Qed.