Commit 7d0bb151 authored by Tej Chajed's avatar Tej Chajed Committed by Robbert

Use user names when destructing existentials

When running `iDestruct "H" as (?) "H"`, use the name of the binder in
"H". For example, if "H" has type `∃ y, Φ y`,  we now use `y` as the
name of the variable after freshening. Previously the name was always
the equivalent of running `fresh H`.

The implementation achieves this by forwarding the desired identifier
name through the `IntoExist` typeclass. Identifiers are serialized in
Gallina by using them as the name of a function of type `ident_name :=
unit -> unit`.
parent ecad6c9f
......@@ -3,6 +3,18 @@ way the logic is used on paper. We also document changes in the Coq
development; every API-breaking change should be listed, but not every new
lemma.
## Iris master
**Changes in `proofmode`:**
* The proofmode now preserves user-supplied names for existentials when using
`iDestruct ... as (?) "..."`. This is backwards-incompatible if you were
relying on the previous automatic names (which were always "H", possibly
freshened). It also requires some changes if you were implementing `IntoExist`
yourself, since the typeclass now forwards names. If your instance transforms
one `IntoExist` into another, you can generally just forward the name from the
premise.
## Iris 3.3.0 (released 2020-07-15)
This release does not have any outstanding highlights, but contains a large
......
......@@ -127,6 +127,7 @@ theories/heap_lang/lib/diverge.v
theories/heap_lang/lib/arith.v
theories/heap_lang/lib/array.v
theories/proofmode/base.v
theories/proofmode/ident_name.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
theories/proofmode/ltac_tactics.v
......
......@@ -77,6 +77,23 @@
--------------------------------------∗
Q
"test_iDestruct_exists_not_exists"
: string
The command has indeed failed with message:
Tactic failure: iExistDestruct: cannot destruct P.
"test_iDestruct_exists_intuitionistic"
: string
1 subgoal
PROP : bi
P : PROP
Φ : nat → PROP
y : nat
============================
"H" : Φ y ∧ P
--------------------------------------□
P
"test_iIntros_forall_pure"
: string
1 subgoal
......
......@@ -112,6 +112,85 @@ Qed.
Lemma test_iDestruct_spatial_noop Q : Q - Q.
Proof. iIntros "-#HQ". done. Qed.
Lemma test_iDestruct_exists (Φ: nat PROP) :
( y, Φ y) - n, Φ n.
Proof. iIntros "H". iDestruct "H" as (y) "H". by iExists y. Qed.
Lemma test_iDestruct_exists_automatic (Φ: nat PROP) :
( y, Φ y) - n, Φ n.
Proof.
iIntros "H".
iDestruct "H" as (?) "H".
(* the automatic name should by [y] *)
by iExists y.
Qed.
Lemma test_iDestruct_exists_automatic_multiple (Φ: nat PROP) :
( y n baz, Φ (y+n+baz)) - n, Φ n.
Proof. iDestruct 1 as (???) "H". by iExists (y+n+baz). Qed.
Lemma test_iDestruct_exists_freshen (y:nat) (Φ: nat PROP) :
( y, Φ y) - n, Φ n.
Proof.
iIntros "H".
iDestruct "H" as (?) "H".
(* the automatic name is the freshened form of [y] *)
by iExists y0.
Qed.
Check "test_iDestruct_exists_not_exists".
Lemma test_iDestruct_exists_not_exists P :
P - P.
Proof. Fail iDestruct 1 as (?) "H". Abort.
Lemma test_iDestruct_exists_explicit_name (Φ: nat PROP) :
( y, Φ y) - n, Φ n.
Proof.
(* give an explicit name that isn't the binder name *)
iDestruct 1 as (foo) "?".
by iExists foo.
Qed.
Lemma test_iDestruct_exists_pure (Φ: nat Prop) :
y, Φ y @{PROP} n, ⌜Φ n.
Proof.
iDestruct 1 as (?) "H".
by iExists y.
Qed.
Lemma test_iDestruct_exists_and_pure (H: True) P :
False P - False.
Proof.
(* this automatic name uses [fresh H] as a sensible default (it's a hypothesis
in [Prop] and the user cannot supply a name in their code) *)
iDestruct 1 as (?) "H".
contradict H0.
Qed.
Check "test_iDestruct_exists_intuitionistic".
Lemma test_iDestruct_exists_intuitionistic P (Φ: nat PROP) :
( y, Φ y P) - P.
Proof.
iDestruct 1 as (?) "#H". Show.
iDestruct "H" as "[_ $]".
Qed.
Lemma test_iDestruct_exists_freshen_local_name (Φ: nat PROP) :
let y := 0 in
( y, Φ y) - n, Φ (y+n).
Proof.
iIntros (y) "#H".
iDestruct "H" as (?) "H".
iExists y0; auto.
Qed.
Definition an_exists P : PROP := ( (an_exists_name:nat), ^an_exists_name P)%I.
(* should use the name from within [an_exists] *)
Lemma test_iDestruct_exists_automatic_def P :
an_exists P - k, ^k P.
Proof. iDestruct 1 as (?) "H". by iExists an_exists_name. Qed.
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ φ P φ ψ P.
Proof. iIntros (??) "H". auto. Qed.
......
......@@ -21,6 +21,9 @@ Section basic_tests.
Lemma test_iAssumption_tforall {TT : tele} (Φ : TT PROP) :
(.. x, Φ x) - .. x, Φ x.
Proof. iIntros "H" (x). iAssumption. Qed.
Lemma test_exist_texist_auto_name {TT : tele} (Φ : TT PROP) :
(.. y, Φ y) - .. x, Φ x.
Proof. iDestruct 1 as (?) "H". by iExists y. Qed.
Lemma test_pure_texist {TT : tele} (φ : TT Prop) :
(.. x, φ x ) - .. x, φ x : PROP.
Proof. iIntros (H) "!%". done. Qed.
......
......@@ -784,38 +784,49 @@ Global Instance from_exist_persistently {A} P (Φ : A → PROP) :
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
(** IntoExist *)
Global Instance into_exist_exist {A} (Φ : A PROP) : IntoExist ( a, Φ a) Φ.
(* These three instances [into_exist_exist], [into_exist_pure], and
[into_exist_texist] need to be written without notations, for example
[bi_exist Φ] and not [∃ a, Φ a], so that [AsIdentName] is always passed the
entire body of the exists with the binder. *)
Global Instance into_exist_exist {A} (Φ : A PROP) name :
AsIdentName Φ name IntoExist (bi_exist Φ) Φ name.
Proof. by rewrite /IntoExist. Qed.
Global Instance into_exist_texist {TT : tele} (Φ : TT PROP) :
IntoExist (.. a, Φ a) Φ | 10.
Proof. by rewrite /IntoExist bi_texist_exist. Qed.
Global Instance into_exist_pure {A} (φ : A Prop) :
@IntoExist PROP A x, φ x (λ a, ⌜φ a)%I.
Global Instance into_exist_pure {A} (φ : A Prop) name :
AsIdentName φ name
@IntoExist PROP A ex φ⌝ (λ a, ⌜φ a)%I name.
Proof. by rewrite /IntoExist pure_exist. Qed.
Global Instance into_exist_affinely {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist (<affine> P) (λ a, <affine> (Φ a))%I.
Global Instance into_exist_texist {TT : tele} (Φ : TT PROP) name :
AsIdentName Φ name IntoExist (bi_texist Φ) Φ name | 10.
Proof. by rewrite /IntoExist bi_texist_exist. Qed.
Global Instance into_exist_affinely {A} P (Φ : A PROP) name :
IntoExist P Φ name IntoExist (<affine> P) (λ a, <affine> (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
Global Instance into_exist_intuitionistically {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist ( P) (λ a, (Φ a))%I.
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 [?] *)
Global Instance into_exist_and_pure P Q φ :
IntoPureT P φ IntoExist (P Q) (λ _ : φ, 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 [?] *)
Global Instance into_exist_sep_pure P Q φ :
IntoPureT P φ TCOr (Affine P) (Absorbing Q) IntoExist (P Q) (λ _ : φ, Q).
IntoPureT P φ
TCOr (Affine P) (Absorbing Q)
IntoExist (P Q) (λ _ : φ, Q) (to_ident_name H).
Proof.
intros (φ'&->&?) ?. rewrite /IntoExist.
eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
rewrite -exist_intro //. apply sep_elim_r, _.
Qed.
Global Instance into_exist_absorbingly {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist (<absorb> P) (λ a, <absorb> (Φ a))%I.
Global Instance into_exist_absorbingly {A} P (Φ : A PROP) name :
IntoExist P Φ name IntoExist (<absorb> P) (λ a, <absorb> (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
Global Instance into_exist_persistently {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist (<pers> P) (λ a, <pers> (Φ a))%I.
Global Instance into_exist_persistently {A} P (Φ : A PROP) name :
IntoExist P Φ name IntoExist (<pers> P) (λ a, <pers> (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
(** IntoForall *)
......
......@@ -121,8 +121,8 @@ Global Instance from_exist_embed {A} P (Φ : A → PROP) :
FromExist P Φ FromExist P (λ a, ⎡Φ a%I).
Proof. by rewrite /FromExist -embed_exist => <-. Qed.
Global Instance into_exist_embed {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist P (λ a, ⎡Φ a%I).
Global Instance into_exist_embed {A} P (Φ : A PROP) name :
IntoExist P Φ name IntoExist P (λ a, ⎡Φ a%I) name.
Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
Global Instance into_forall_embed {A} P (Φ : A PROP) :
......
......@@ -161,14 +161,14 @@ Global Instance from_exist_except_0 {A} P (Φ : A → PROP) :
Proof. rewrite /FromExist=> <-. by rewrite except_0_exist_2. Qed.
(** IntoExist *)
Global Instance into_exist_later {A} P (Φ : A PROP) :
IntoExist P Φ Inhabited A IntoExist ( P) (λ a, (Φ a))%I.
Global Instance into_exist_later {A} P (Φ : A PROP) name :
IntoExist P Φ name Inhabited A IntoExist ( P) (λ a, (Φ a))%I name.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
Global Instance into_exist_laterN {A} n P (Φ : A PROP) :
IntoExist P Φ Inhabited A IntoExist (^n P) (λ a, ^n (Φ a))%I.
Global Instance into_exist_laterN {A} n P (Φ : A PROP) name :
IntoExist P Φ name Inhabited A IntoExist (^n P) (λ a, ^n (Φ a))%I name.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP laterN_exist. Qed.
Global Instance into_exist_except_0 {A} P (Φ : A PROP) :
IntoExist P Φ Inhabited A IntoExist ( P) (λ a, (Φ a))%I.
Global Instance into_exist_except_0 {A} P (Φ : A PROP) name :
IntoExist P Φ name Inhabited A IntoExist ( P) (λ a, (Φ a))%I name.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
(** IntoForall *)
......
......@@ -75,8 +75,8 @@ Global Instance from_exist_plainly {A} P (Φ : A → PROP) :
FromExist P Φ FromExist ( P) (λ a, (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
Global Instance into_exist_plainly `{!BiPlainlyExist PROP} {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist ( P) (λ a, (Φ a))%I.
Global Instance into_exist_plainly `{!BiPlainlyExist PROP} {A} P (Φ : A PROP) name :
IntoExist P Φ name IntoExist ( P) (λ a, (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
Global Instance into_forall_plainly {A} P (Φ : A PROP) :
......
From stdpp Require Import namespaces.
From iris.bi Require Export bi.
From iris.proofmode Require Import base.
From iris.proofmode Require Export modalities.
From iris.proofmode Require Export ident_name modalities.
Set Default Proof Using "Type".
Import bi.
......@@ -204,11 +204,11 @@ Arguments FromExist {_ _} _%I _%I : simpl never.
Arguments from_exist {_ _} _%I _%I {_}.
Hint Mode FromExist + - ! - : typeclass_instances.
Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A PROP) :=
Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A PROP) (name: ident_name) :=
into_exist : P x, Φ x.
Arguments IntoExist {_ _} _%I _%I : simpl never.
Arguments into_exist {_ _} _%I _%I {_}.
Hint Mode IntoExist + - ! - : typeclass_instances.
Arguments IntoExist {_ _} _%I _%I _ : simpl never.
Arguments into_exist {_ _} _%I _%I _ {_}.
Hint Mode IntoExist + - ! - - : typeclass_instances.
Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A PROP) :=
into_forall : P x, Φ x.
......@@ -617,8 +617,8 @@ Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
IntoOr P Q1 Q2 IntoOr (tc_opaque P) Q1 Q2 := id.
Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) :
FromExist P Φ FromExist (tc_opaque P) Φ := id.
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) :
IntoExist P Φ IntoExist (tc_opaque P) Φ := id.
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) (name: ident_name) :
IntoExist P Φ name IntoExist (tc_opaque P) Φ name := id.
Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) :
FromForall P Φ FromForall (tc_opaque P) Φ := id.
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) :
......
......@@ -726,9 +726,13 @@ Proof.
rewrite -(from_exist P). eauto using exist_intro'.
Qed.
Lemma tac_exist_destruct {A} Δ i p j P (Φ : A PROP) Q :
envs_lookup i Δ = Some (p, P) IntoExist P Φ
( a,
Lemma tac_exist_destruct {A} Δ i p j P (Φ : A PROP) (name: ident_name) Q :
envs_lookup i Δ = Some (p, P) IntoExist P Φ name
( (* this let binding makes it easy for the tactic [iExistDestruct] to use
[name] (from resolving [IntoExist] in an earlier subgoal) within this
goal *)
let _ := name in
a,
match envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ with
| Some Δ' => envs_entails Δ' Q
| None => False
......
From stdpp Require Import base.
(** [ident_name] is a way to remember an identifier within the binder of a
(trivial) function, which can be constructed and retrieved with Ltac but is easy
to forward around opaquely in Gallina (through typeclasses, for example) *)
Definition ident_name := unit unit.
(** [to_ident_name id] returns a constr of type [ident_name] that holds [id] in
the binder name *)
Ltac to_ident_name id :=
eval cbv in (ltac:(clear; intros id; assumption) : unit unit).
(** to_ident_name is a Gallina-level version of [to_ident_name] for constructing
[ident_name] literals. *)
Notation to_ident_name id := (λ id:unit, id) (only parsing).
(** The idea of [AsIdentName] is to convert the binder in [f], which should be a
lambda, to an [ident_name] representing the name of the binder. It has only
one instance, a [Hint Extern] which implements that conversion to resolve
[name] in Ltac (see [solve_as_ident_name]).
This typeclass can produce the fallback identifier [__unknown] when applied
to an identifier rather than a lambda; for example, if the user writes
[bi_exist Φ], there is no binder anywhere to extract. *)
Class AsIdentName {A B} (f : A B) (name : ident_name) := as_ident_name {}.
Arguments as_ident_name {A B f} name : assert.
Ltac solve_as_ident_name :=
lazymatch goal with
| |- AsIdentName (λ x, _) _ =>
let name := to_ident_name x in
notypeclasses refine (as_ident_name name)
| _ => notypeclasses refine (to_ident_name __unknown)
end.
Hint Extern 1 (AsIdentName _ _) => solve_as_ident_name : typeclass_instances.
......@@ -1327,14 +1327,18 @@ Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
Local Tactic Notation "iExistDestruct" constr(H)
"as" simple_intropattern(x) constr(Hx) :=
eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
eapply tac_exist_destruct with H _ Hx _ _ _; (* (i:=H) (j:=Hx) *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iExistDestruct:" H "not found"
|iSolveTC ||
let P := match goal with |- IntoExist ?P _ => P end in
let P := match goal with |- IntoExist ?P _ _ => P end in
fail "iExistDestruct: cannot destruct" P|];
let y := fresh in
let name := lazymatch goal with
| |- let _ := (λ name, _) in _ => name
end in
intros _;
let y := fresh name in
intros y; pm_reduce;
match goal with
| |- False =>
......
......@@ -313,8 +313,8 @@ Proof.
rewrite /FromExist /MakeMonPredAt=><- H. setoid_rewrite <- H.
by rewrite monPred_at_exist.
Qed.
Global Instance into_exist_monPred_at {A} P (Φ : A monPred) (Ψ : A PROP) i :
IntoExist P Φ ( a, MakeMonPredAt i (Φ a) (Ψ a)) IntoExist (P i) Ψ.
Global Instance into_exist_monPred_at {A} P (Φ : A monPred) name (Ψ : A PROP) i :
IntoExist P Φ name ( a, MakeMonPredAt i (Φ a) (Ψ a)) IntoExist (P i) Ψ name.
Proof.
rewrite /IntoExist /MakeMonPredAt=>-> H. setoid_rewrite <- H.
by rewrite monPred_at_exist.
......@@ -336,8 +336,11 @@ Global Instance from_exist_monPred_at_ex P (Φ : I → PROP) i :
Proof.
rewrite /FromExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
Qed.
(* TODO: this implementation uses [idx] as the automatic name for the index. In
theory a monPred could define an appropriate metavariable for indices with an
[ident_name] argument to [MakeMonPredAt], but this is not implemented. *)
Global Instance into_exist_monPred_at_ex P (Φ : I PROP) i :
( i, MakeMonPredAt i P (Φ i)) IntoExist ((<subj> P) i) Φ.
( i, MakeMonPredAt i P (Φ i)) IntoExist ((<subj> P) i) Φ (to_ident_name idx).
Proof.
rewrite /IntoExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
Qed.
......
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