From 86de92cfc7aa2012fce94928c4748f63597483f3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 9 Sep 2016 00:49:50 +0200
Subject: [PATCH] Elimination of pure facts using Coq introduction patterns for
iAssert.
---
ProofMode.md | 4 +++-
proofmode/tactics.v | 14 +++++++++++---
2 files changed, 14 insertions(+), 4 deletions(-)
diff --git a/ProofMode.md b/ProofMode.md
index ae2233edf..8137c2c6c 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -40,8 +40,10 @@ Context management
`H`.
- `iAssert P with "spat" as "ipat"` : create a new goal with conclusion `P` and
put `P` in the context of the original goal. The specialization pattern
- `spat` specifies which hypotheses will be consumed by proving `P` and the
+ `spat` specifies which hypotheses will be consumed by proving `P`. The
introduction pattern `ipat` specifies how to eliminate `P`.
+- `iAssert P with "spat" as %cpat` : assert `P` and eliminate it using the Coq
+ introduction pattern `cpat`.
Introduction of logical connectives
-----------------------------------
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 382e488ae..11ca3016c 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -833,7 +833,7 @@ Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ltac:(iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 )).
(** * Assert *)
-Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
+Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac) :=
let H := iFresh in
let Hs := spec_pat.parse Hs in
lazymatch Hs with
@@ -842,7 +842,7 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
[env_cbv; reflexivity
|(*goal*)
|apply _ || fail "iAssert:" Q "not persistent"
- |iDestructHyp H as pat]
+ |tac H]
| [SGoal ?k ?lr ?Hs] =>
eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
[match k with
@@ -851,13 +851,21 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
end
|env_cbv; reflexivity || fail "iAssert:" Hs "not found"
|env_cbv; reflexivity|
- |iDestructHyp H as pat]
+ |tac H]
| ?pat => fail "iAssert: invalid pattern" pat
end.
+Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
+ iAssertCore Q with Hs as (fun H => iDestructHyp H as pat).
Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) :=
iAssert Q with "[]" as pat.
+Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs)
+ "as" "%" simple_intropattern(pat) :=
+ iAssertCore Q with Hs as (fun H => iPure H as pat).
+Tactic Notation "iAssert" open_constr(Q) "as" "%" simple_intropattern(pat) :=
+ iAssert Q with "[]" as %pat.
+
(** * Rewrite *)
Local Ltac iRewriteFindPred :=
match goal with
--
GitLab