Commit 6d1a88a5 authored by Tej Chajed's avatar Tej Chajed Committed by Ralf Jung
Browse files

Support destructing exists with intro patterns

The syntax re-uses the existing support for pure names, namely the % and
%H patterns. Using "[% H]" is like `iDestruct ... as (?) "H"` and using
"[%x H]" (with the string-ident plugin) is like `iDestruct ... as (x)
"H"`.

This changes how these patterns are parsed. Previously, both would have
been handled as conjunctions (using IntoAnd or IntoSep, depending on
whether the hypothesis is persistent or not). This means it was possible
for the user to use "[% H]" to destruct a pure hypothesis ⌜φ ∧ ψ⌝ and
put only the first conjunct in the Gallina context, leaving the other
one in the IPM; such patterns will now break, since iExistDestruct
does not handle this use case.
parent c3aae082
......@@ -807,14 +807,16 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
Global Instance into_exist_intuitionistically {A} P (Φ : A PROP) name :
IntoExist P Φ name IntoExist ( P) (λ a, (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed.
(* [to_ident_name H] makes the default name [H] when [P] is introduced with [?] *)
(* [to_ident_name H] makes the default name [H] when [P] is destructed with
[iExistDestruct] *)
Global Instance into_exist_and_pure P Q φ :
IntoPureT P φ IntoExist (P Q) (λ _ : φ, Q) (to_ident_name H).
Proof.
intros (φ'&->&?). rewrite /IntoExist (into_pure P).
apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
Qed.
(* [to_ident_name H] makes the default name [H] when [P] is introduced with [?] *)
(* [to_ident_name H] makes the default name [H] when [P] is destructed with
[iExistDestruct] *)
Global Instance into_exist_sep_pure P Q φ :
IntoPureT P φ
TCOr (Affine P) (Absorbing Q)
......
......@@ -1426,6 +1426,18 @@ Tactic Notation "iModCore" constr(H) :=
(** [pat0] is the unparsed pattern, and is only used in error messages *)
Local Ltac iDestructHypGo Hz pat0 pat :=
let iAndDestructAs pat1 pat2 :=
let Hy := iFresh in
iAndDestruct Hz as Hz Hy;
iDestructHypGo Hz pat0 pat1; iDestructHypGo Hy pat0 pat2 in
let iExistDestructPure gallina_id pat2 :=
lazymatch gallina_id with
| IGallinaAnon =>
iExistDestruct Hz as ? Hz; iDestructHypGo Hz pat0 pat2
| IGallinaNamed ?s =>
let x := string_to_ident s in
iExistDestruct Hz as x Hz; iDestructHypGo Hz pat0 pat2
end in
lazymatch pat with
| IFresh =>
lazymatch Hz with
......@@ -1444,9 +1456,11 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
| IList [[IDrop; ?pat2]] =>
iAndDestructChoice Hz as Right Hz;
iDestructHypGo Hz pat0 pat2
| IList [[?pat1; ?pat2]] =>
let Hy := iFresh in iAndDestruct Hz as Hz Hy;
iDestructHypGo Hz pat0 pat1; iDestructHypGo Hy pat0 pat2
(* heuristic to fallback to [iAndDestruct] when both patterns are pure, since
the instances for [IntoAnd] are more general than for [IntoExist]. *)
| IList [[IPure ?id1; IPure ?id2]] => iAndDestructAs (IPure id1) (IPure id2)
| IList [[IPure ?gallina_id; ?pat2]] => iExistDestructPure gallina_id pat2
| IList [[?pat1; ?pat2]] => iAndDestructAs pat1 pat2
| IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
| IList [[_]] => fail "iDestruct:" pat0 "has just a single conjunct"
......
......@@ -251,6 +251,15 @@ Lemma test_iDestruct_exists_automatic_def P :
an_exists P - k, ^k P.
Proof. iDestruct 1 as (?) "H". by iExists an_exists_name. Qed.
(* use an Iris intro pattern [% H] to indicate iExistDestruct rather than (?) *)
Lemma test_exists_intro_pattern_anonymous P (Φ: nat PROP) :
P ( y:nat, Φ y) - x, P Φ x.
Proof.
iIntros "[HP1 [% HP2]]".
iExists y.
iFrame "HP1 HP2".
Qed.
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ φ P φ ψ P.
Proof. iIntros (??) "H". auto. Qed.
......@@ -1379,6 +1388,14 @@ Proof.
Fail iIntros "[H %H]".
Abort.
Lemma test_exists_intro_pattern P (Φ: nat PROP) :
P ( y:nat, Φ y) - x, P Φ x.
Proof.
iIntros "[HP1 [%y HP2]]".
iExists y.
iFrame "HP1 HP2".
Qed.
End pure_name_tests.
Section tactic_tests.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment