From 686f5740062b26fe32089baa6a4de8ca29895d4b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 30 Jan 2017 13:56:38 +0100
Subject: [PATCH] Support introduction patterns /=, {H}, {$H} in iDestruct.
This fixes issue #57.
I considered supporting these introduction patterns also in a nested fashion --
for example allowing `iDestruct foo as [H1 [{H1} H1 /= H2|H2]` -- but that
turned out to be quite difficult.
Where should we allow `/=`, `{H}` and `{$H}` exactly. Clearly something like
`>/=` makes no sense, unless we adopt to some kind of 'stack like' semantics
for introduction patterns as in ssreflect. Alternatively, we could only allow
these patterns in the branches of the destructing introduction pattern
`[... | ... | ...]` but that brings other complications, e.g.:
- What to do with `(H1 & /= & H3)`?
- How to distinguish the introduction patterns `[H _]` and `[_ H]` for
destructing a spatial conjunction? We cannot simply match on the shape of the
introduction pattern anymore, because one could also write `[_ H /=]`.
---
theories/proofmode/tactics.v | 22 ++++++++++++++++++++--
1 file changed, 20 insertions(+), 2 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 675436b3a..aec6cbf8d 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -672,8 +672,26 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| IAlwaysElim ?pat => iPersistent Hz; go Hz pat
| IModalElim ?pat => iModCore Hz; go Hz pat
| _ => fail "iDestruct:" pat "invalid"
- end
- in let pat := intro_pat.parse_one pat in go H pat.
+ end in
+ let rec find_pat found pats :=
+ lazymatch pats with
+ | [] =>
+ match found with
+ | true => idtac
+ | false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
+ end
+ | ISimpl :: ?pats => simpl; find_pat found pats
+ | IClear ?H :: ?pats => iClear H; find_pat found pats
+ | IClearFrame ?H :: ?pats => iFrame H; find_pat found pats
+ | ?pat :: ?pats =>
+ match found with
+ | false => go H pat; find_pat true pats
+ | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
+ end
+ | _ => fail "hallo" pats
+ end in
+ let pats := intro_pat.parse pat in
+ find_pat false pats.
Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
--
GitLab