Commit e989ad6b authored by Robbert's avatar Robbert

Merge branch 'intro-auto-name' into 'master'

Use user-supplied names in iIntros

Closes #336

See merge request !482
parents 11678073 c1affb21
Pipeline #31812 passed with stage
in 22 minutes and 53 seconds
......@@ -14,6 +14,11 @@ lemma.
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.
* The proofmode also preserves user-supplied names in `iIntros`, for example
with `iIntros (?)` and `iIntros "%"`, as described for destructing
existentials above. As part of this change, it now uses a base name of `H` for
pure facts rather than the previous default of `a`. This also requires some
changes if you were implementing `FromForall`, in order to forward names.
## Iris 3.3.0 (released 2020-07-15)
......
......@@ -100,10 +100,23 @@ Tactic failure: iExistDestruct: cannot destruct P.
PROP : bi
Ψ : nat → PROP
a : nat
x : nat
============================
--------------------------------------∗
Ψ x → Ψ x
"test_iIntros_pure_names"
: string
1 subgoal
PROP : bi
H : True
P : PROP
x, y : nat
H0 : x = y
============================
--------------------------------------∗
Ψ a → Ψ a
P -∗ P
The command has indeed failed with message:
No applicable tactic.
......
......@@ -219,6 +219,32 @@ Lemma test_very_fast_iIntros P :
x y : nat, x = y P - P.
Proof. by iIntros. Qed.
Lemma test_iIntros_automatic_name (Φ: nat PROP) :
y, Φ y - x, Φ x.
Proof. iIntros (?) "H". by iExists y. Qed.
Lemma test_iIntros_automatic_name_proofmode_intro (Φ: nat PROP) :
y, Φ y - x, Φ x.
Proof. iIntros "% H". by iExists y. Qed.
(* even an object-level forall should get the right name *)
Lemma test_iIntros_object_forall P :
P - (y:unit), P.
Proof. iIntros "H". iIntros (?). destruct y. iAssumption. Qed.
Lemma test_iIntros_object_proofmode_intro (Φ: nat PROP) :
y, Φ y - x, Φ x.
Proof. iIntros "% H". by iExists y. Qed.
Check "test_iIntros_pure_names".
Lemma test_iIntros_pure_names (H:True) P :
x y : nat, x = y P - P.
Proof.
iIntros (???).
(* the pure hypothesis should get a sensible [H0] as its name *)
Show. auto.
Qed.
Definition tc_opaque_test : PROP := tc_opaque ( x : nat, x = x )%I.
Lemma test_iIntros_tc_opaque : tc_opaque_test.
Proof. by iIntros (x). Qed.
......
......@@ -874,29 +874,31 @@ Proof.
Qed.
(** FromForall *)
Global Instance from_forall_forall {A} (Φ : A PROP) :
FromForall ( x, Φ x) Φ.
Global Instance from_forall_forall {A} (Φ : A PROP) name :
AsIdentName Φ name FromForall (bi_forall Φ) Φ name.
Proof. by rewrite /FromForall. Qed.
Global Instance from_forall_tforall {TT : tele} (Φ : TT PROP) :
FromForall (.. x, Φ x) Φ.
Global Instance from_forall_tforall {TT : tele} (Φ : TT PROP) name :
AsIdentName Φ name FromForall (bi_tforall Φ) Φ name.
Proof. by rewrite /FromForall bi_tforall_forall. Qed.
Global Instance from_forall_pure {A} (φ : A Prop) :
@FromForall PROP A a : A, φ a (λ a, φ a )%I.
Global Instance from_forall_pure {A} (φ : A Prop) name :
AsIdentName φ name @FromForall PROP A a : A, φ a (λ a, φ a )%I name.
Proof. by rewrite /FromForall pure_forall. Qed.
Global Instance from_tforall_pure {TT : tele} (φ : TT Prop) :
@FromForall PROP TT .. x : TT, φ x (λ x, φ x )%I.
Global Instance from_tforall_pure {TT : tele} (φ : TT Prop) name :
AsIdentName φ name @FromForall PROP TT tforall φ⌝ (λ x, φ x )%I name.
Proof. by rewrite /FromForall tforall_forall pure_forall. Qed.
(* [H] is the default name for the [φ] hypothesis, in the following three instances *)
Global Instance from_forall_pure_not (φ : Prop) :
@FromForall PROP φ ¬ φ⌝ (λ a : φ, False)%I.
@FromForall PROP φ ¬ φ⌝ (λ _ : φ, False)%I (to_ident_name H).
Proof. by rewrite /FromForall pure_forall. Qed.
Global Instance from_forall_impl_pure P Q φ :
IntoPureT P φ FromForall (P Q) (λ _ : φ, Q).
IntoPureT P φ FromForall (P Q) (λ _ : φ, Q) (to_ident_name H).
Proof.
intros (φ'&->&?). by rewrite /FromForall -pure_impl_forall (into_pure P).
Qed.
Global Instance from_forall_wand_pure P Q φ :
IntoPureT P φ TCOr (Affine P) (Absorbing Q)
FromForall (P - Q) (λ _ : φ, Q)%I.
FromForall (P - Q) (λ _ : φ, Q)%I (to_ident_name H).
Proof.
intros (φ'&->&?) [|]; rewrite /FromForall; apply wand_intro_r.
- rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_r.
......@@ -904,14 +906,14 @@ Proof.
- by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
Qed.
Global Instance from_forall_intuitionistically `{BiAffine PROP} {A} P (Φ : A PROP) :
FromForall P Φ FromForall ( P) (λ a, (Φ a))%I.
Global Instance from_forall_intuitionistically `{BiAffine PROP} {A} P (Φ : A PROP) name :
FromForall P Φ name FromForall ( P) (λ a, (Φ a))%I name.
Proof.
rewrite /FromForall=> <-. setoid_rewrite intuitionistically_into_persistently.
by rewrite persistently_forall.
Qed.
Global Instance from_forall_persistently {A} P (Φ : A PROP) :
FromForall P Φ FromForall (<pers> P) (λ a, <pers> (Φ a))%I.
Global Instance from_forall_persistently {A} P (Φ : A PROP) name :
FromForall P Φ name FromForall (<pers> P) (λ a, <pers> (Φ a))%I name.
Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
(** ElimModal *)
......
......@@ -129,8 +129,8 @@ Global Instance into_forall_embed {A} P (Φ : A → PROP) :
IntoForall P Φ IntoForall P (λ a, ⎡Φ a%I).
Proof. by rewrite /IntoForall -embed_forall => <-. Qed.
Global Instance from_forall_embed {A} P (Φ : A PROP) :
FromForall P Φ FromForall P (λ a, ⎡Φ a%I).
Global Instance from_forall_embed {A} P (Φ : A PROP) name :
FromForall P Φ name FromForall P (λ a, ⎡Φ a%I) name.
Proof. by rewrite /FromForall -embed_forall => <-. Qed.
Global Instance into_inv_embed P N : IntoInv P N IntoInv P N := {}.
......
......@@ -185,16 +185,16 @@ Global Instance into_forall_except_0 {A} P (Φ : A → PROP) :
Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
(** FromForall *)
Global Instance from_forall_later {A} P (Φ : A PROP) :
FromForall P Φ FromForall ( P)%I (λ a, (Φ a))%I.
Global Instance from_forall_later {A} P (Φ : A PROP) name :
FromForall P Φ name FromForall ( P)%I (λ a, (Φ a))%I name.
Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
Global Instance from_forall_laterN {A} P (Φ : A PROP) n :
FromForall P Φ FromForall (^n P)%I (λ a, ^n (Φ a))%I.
Global Instance from_forall_laterN {A} P (Φ : A PROP) n name :
FromForall P Φ name FromForall (^n P)%I (λ a, ^n (Φ a))%I name.
Proof. rewrite /FromForall => <-. by rewrite laterN_forall. Qed.
Global Instance from_forall_except_0 {A} P (Φ : A PROP) :
FromForall P Φ FromForall ( P)%I (λ a, (Φ a))%I.
Global Instance from_forall_except_0 {A} P (Φ : A PROP) name :
FromForall P Φ name FromForall ( P)%I (λ a, (Φ a))%I name.
Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed.
(** IsExcept0 *)
......
......@@ -83,8 +83,8 @@ Global Instance into_forall_plainly {A} P (Φ : A → PROP) :
IntoForall P Φ IntoForall ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
Global Instance from_forall_plainly {A} P (Φ : A PROP) :
FromForall P Φ FromForall ( P)%I (λ a, (Φ a))%I.
Global Instance from_forall_plainly {A} P (Φ : A PROP) name :
FromForall P Φ name FromForall ( P)%I (λ a, (Φ a))%I name.
Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
Global Instance from_modal_plainly P :
......
......@@ -96,20 +96,20 @@ Proof.
Qed.
Global Instance from_forall_fupd
`{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A PROP) :
`{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A PROP) name :
(* Some cases in which [E2 ⊆ E1] holds *)
TCOr (TCEq E1 E2) (TCOr (TCEq E1 ) (TCEq E2 ))
FromForall P Φ ( x, Plain (Φ x))
FromForall (|={E1,E2}=> P)%I (λ a, |={E1,E2}=> (Φ a))%I.
FromForall P Φ name ( x, Plain (Φ x))
FromForall (|={E1,E2}=> P)%I (λ a, |={E1,E2}=> (Φ a))%I name.
Proof.
rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite fupd_plain_forall; set_solver.
Qed.
Global Instance from_forall_step_fupd
`{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A PROP) :
`{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A PROP) name :
(* Some cases in which [E2 ⊆ E1] holds *)
TCOr (TCEq E1 E2) (TCOr (TCEq E1 ) (TCEq E2 ))
FromForall P Φ ( x, Plain (Φ x))
FromForall (|={E1}[E2]=> P)%I (λ a, |={E1}[E2]=> (Φ a))%I.
FromForall P Φ name ( x, Plain (Φ x))
FromForall (|={E1}[E2]=> P)%I (λ a, |={E1}[E2]=> (Φ a))%I name.
Proof.
rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
Qed.
......
......@@ -216,11 +216,11 @@ Arguments IntoForall {_ _} _%I _%I : simpl never.
Arguments into_forall {_ _} _%I _%I {_}.
Hint Mode IntoForall + - ! - : typeclass_instances.
Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A PROP) :=
Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A PROP) (name : ident_name) :=
from_forall : ( x, Φ x) P.
Arguments FromForall {_ _} _%I _%I : simpl never.
Arguments from_forall {_ _} _%I _%I {_}.
Hint Mode FromForall + - ! - : typeclass_instances.
Arguments FromForall {_ _} _%I _%I _ : simpl never.
Arguments from_forall {_ _} _%I _%I _ {_}.
Hint Mode FromForall + - ! - - : typeclass_instances.
Class IsExcept0 {PROP : bi} (Q : PROP) := is_except_0 : Q Q.
Arguments IsExcept0 {_} _%I : simpl never.
......@@ -619,8 +619,8 @@ 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) (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 from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) (name : ident_name) :
FromForall P Φ name FromForall (tc_opaque P) Φ name := id.
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) :
IntoForall P Φ IntoForall (tc_opaque P) Φ := id.
Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}
......
......@@ -693,9 +693,11 @@ Proof.
Qed.
(** * Forall *)
Lemma tac_forall_intro {A} Δ (Φ : A PROP) Q :
FromForall Q Φ
( a, envs_entails Δ (Φ a))
Lemma tac_forall_intro {A} Δ (Φ : A PROP) Q name :
FromForall Q Φ name
( (* see [tac_exist_destruct] for an explanation of this let binding *)
let _ := name in
a, envs_entails Δ (Φ a))
envs_entails Δ Q.
Proof. rewrite envs_entails_eq /FromForall=> <-. apply forall_intro. Qed.
......
......@@ -474,7 +474,12 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
[iSolveTC ||
let P := match goal with |- FromForall ?P _ => P end in
fail "iIntro: cannot turn" P "into a universal quantifier"
|pm_prettify; intros x
|let name := lazymatch goal with
| |- let _ := (λ name, _) in _ => name
end in
pm_prettify;
let y := fresh name in
intros y; revert y; intros x
(* subgoal *)]
end).
......
......@@ -254,14 +254,14 @@ Proof. done. Qed.
Global Instance from_forall_monPred_at_wand P Q (Φ Ψ : I PROP) i :
( j, MakeMonPredAt j P (Φ j)) ( j, MakeMonPredAt j Q (Ψ j))
FromForall ((P - Q) i)%I (λ j, i j Φ j - Ψ j)%I.
FromForall ((P - Q) i)%I (λ j, i j Φ j - Ψ j)%I (to_ident_name idx).
Proof.
rewrite /FromForall /MakeMonPredAt monPred_at_wand=> H1 H2. do 2 f_equiv.
by rewrite H1 H2.
Qed.
Global Instance from_forall_monPred_at_impl P Q (Φ Ψ : I PROP) i :
( j, MakeMonPredAt j P (Φ j)) ( j, MakeMonPredAt j Q (Ψ j))
FromForall ((P Q) i)%I (λ j, i j Φ j Ψ j)%I.
FromForall ((P Q) i)%I (λ j, i j Φ j Ψ j)%I (to_ident_name idx).
Proof.
rewrite /FromForall /MakeMonPredAt monPred_at_impl=> H1 H2. do 2 f_equiv.
by rewrite H1 H2 bi.pure_impl_forall.
......@@ -321,7 +321,7 @@ Proof.
Qed.
Global Instance from_forall_monPred_at_objectively P (Φ : I PROP) i :
( i, MakeMonPredAt i P (Φ i)) FromForall ((<obj> P) i)%I Φ.
( i, MakeMonPredAt i P (Φ i)) FromForall ((<obj> P) i)%I Φ (to_ident_name idx).
Proof.
rewrite /FromForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
Qed.
......@@ -345,8 +345,8 @@ Proof.
rewrite /IntoExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
Qed.
Global Instance from_forall_monPred_at {A} P (Φ : A monPred) (Ψ : A PROP) i :
FromForall P Φ ( a, MakeMonPredAt i (Φ a) (Ψ a)) FromForall (P i) Ψ.
Global Instance from_forall_monPred_at {A} P (Φ : A monPred) name (Ψ : A PROP) i :
FromForall P Φ name ( a, MakeMonPredAt i (Φ a) (Ψ a)) FromForall (P i) Ψ name.
Proof.
rewrite /FromForall /MakeMonPredAt=><- H. setoid_rewrite <- H.
by rewrite monPred_at_forall.
......@@ -460,7 +460,7 @@ Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
Global Instance from_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ :
( i, MakeMonPredAt i P (Φ i))
FromForall (( P) i) (λ j, (Φ j))%I.
FromForall (( P) i) (λ j, (Φ j))%I (to_ident_name idx).
Proof.
rewrite /FromForall /MakeMonPredAt=>HPΦ. rewrite monPred_at_plainly.
by setoid_rewrite HPΦ.
......
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