diff --git a/_CoqProject b/_CoqProject
index 1c6bf74ca80877a9eeb8858e30a552b7395cc1c1..c52dfe67b2e57a9a5b4729e13981ef3ba996410b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -99,6 +99,7 @@ theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
theories/proofmode/ltac_tactics.v
theories/proofmode/environments.v
+theories/proofmode/reduction.v
theories/proofmode/intro_patterns.v
theories/proofmode/spec_patterns.v
theories/proofmode/sel_patterns.v
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index eaaf2684543c866b007254ddce68f0c14f7f417c..317ac0b316706dcce9bba9ad46399a41dfdc9e8c 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -103,7 +103,7 @@
--------------------------------------â–¡
"Hown1" : na_own t E1
"Hown2" : na_own t (E2 ∖ ↑N)
- "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ id (na_own t E2)
+ "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
--------------------------------------∗
|={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 14e925e3c022d64f88d905cbe4ff3f3134c1c303..04ce30fa91f670e28ad18573bc53cadb27962f17 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -1,7 +1,7 @@
From iris.bi Require Export bi updates.
From iris.bi.lib Require Import fixpoint laterable.
From stdpp Require Import coPset namespaces.
-From iris.proofmode Require Import coq_tactics tactics.
+From iris.proofmode Require Import coq_tactics tactics reduction.
Set Default Proof Using "Type".
(** Conveniently split a conjunction on both assumption and conclusion. *)
@@ -160,8 +160,8 @@ Section lemmas.
Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X → PROP) γ' α β Pas Φ :
ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
(atomic_acc E1 Ei α Pas β Φ)
- (λ x', atomic_acc E2 Ei α (β' x' ∗ coq_tactics.maybe_wand (γ' x') Pas)%I β
- (λ x y, β' x' ∗ coq_tactics.maybe_wand (γ' x') (Φ x y)))%I.
+ (λ x', atomic_acc E2 Ei α (β' x' ∗ pm_maybe_wand (γ' x') Pas)%I β
+ (λ x y, β' x' ∗ pm_maybe_wand (γ' x') (Φ x y)))%I.
Proof.
rewrite /ElimAcc.
(* FIXME: Is there any way to prevent maybe_wand from unfolding?
@@ -281,5 +281,5 @@ Tactic Notation "iAuIntro" :=
iStartProof; eapply tac_aupd_intro; [
iSolveTC || fail "iAuIntro: emp is not timeless"
| iSolveTC || fail "iAuIntro: not all spatial assumptions are laterable"
- | (* P = ...: make the P pretty *) env_reflexivity
+ | (* P = ...: make the P pretty *) pm_reflexivity
| (* the new proof mode goal *) ].
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 7631e8a85b63bc9ee4996e5fb2112e0a780d4caf..66694a32bce54ce966a3a46cd879f26c01781380 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -1,5 +1,5 @@
From iris.program_logic Require Export weakestpre total_weakestpre.
-From iris.proofmode Require Import coq_tactics.
+From iris.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Export tactics lifting.
From iris.heap_lang Require Import notation.
@@ -319,7 +319,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
let finish _ :=
first [intros l | fail 1 "wp_alloc:" l "not fresh"];
eexists; split;
- [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
+ [pm_reflexivity || fail "wp_alloc:" H "not fresh"
|wp_expr_simpl; try wp_value_head] in
iStartProof;
lazymatch goal with
@@ -379,7 +379,7 @@ Tactic Notation "wp_store" :=
|fail 1 "wp_store: cannot find 'Store' in" e];
[iSolveTC
|solve_mapsto ()
- |env_cbv; reflexivity
+ |pm_reflexivity
|finish ()]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
@@ -387,7 +387,7 @@ Tactic Notation "wp_store" :=
eapply (tac_twp_store _ _ _ _ _ K); [iSolveTC|..])
|fail 1 "wp_store: cannot find 'Store' in" e];
[solve_mapsto ()
- |env_cbv; reflexivity
+ |pm_reflexivity
|finish ()]
| _ => fail "wp_store: not a 'wp'"
end.
@@ -432,7 +432,7 @@ Tactic Notation "wp_cas_suc" :=
[iSolveTC
|solve_mapsto ()
|try congruence
- |env_cbv; reflexivity
+ |pm_reflexivity
|simpl; try wp_value_head]
| |- envs_entails _ (twp ?E ?e ?Q) =>
first
@@ -441,7 +441,7 @@ Tactic Notation "wp_cas_suc" :=
|fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
[solve_mapsto ()
|try congruence
- |env_cbv; reflexivity
+ |pm_reflexivity
|wp_expr_simpl; try wp_value_head]
| _ => fail "wp_cas_suc: not a 'wp'"
end.
@@ -459,7 +459,7 @@ Tactic Notation "wp_faa" :=
|fail 1 "wp_faa: cannot find 'CAS' in" e];
[iSolveTC
|solve_mapsto ()
- |env_cbv; reflexivity
+ |pm_reflexivity
|wp_expr_simpl; try wp_value_head]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
@@ -467,7 +467,7 @@ Tactic Notation "wp_faa" :=
eapply (tac_twp_faa _ _ _ _ _ K); [iSolveTC|..])
|fail 1 "wp_faa: cannot find 'CAS' in" e];
[solve_mapsto ()
- |env_cbv; reflexivity
+ |pm_reflexivity
|wp_expr_simpl; try wp_value_head]
| _ => fail "wp_faa: not a 'wp'"
end.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 19934800d69a260eea91fdb1711832165f4097b2..39ce518ad7b96f30fc5e6b77c0e27c5784fc46e5 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -392,9 +392,9 @@ Section proofmode_classes.
Atomic (stuckness_to_atomicity s) e →
ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
α β γ (WP e @ s; E1 {{ Φ }})
- (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
+ (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ coq_tactics.pm_maybe_wand (γ x) (Φ v) }})%I.
Proof.
- intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
+ intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.pm_maybe_wand_sound.
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
@@ -403,9 +403,9 @@ Section proofmode_classes.
Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
ElimAcc (X:=X) (fupd E E) (fupd E E)
α β γ (WP e @ s; E {{ Φ }})
- (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
+ (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ coq_tactics.pm_maybe_wand (γ x) (Φ v) }})%I.
Proof.
- rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
+ rewrite /ElimAcc. setoid_rewrite coq_tactics.pm_maybe_wand_sound.
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iApply wp_fupd.
iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index a889f5924601ba44acc84646d1fcf1cf723a7f04..1e8dff0089b80b8a70371894daee16ff0ecb49b6 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -3,6 +3,8 @@ From iris.algebra Require Export base.
From Coq Require Import Ascii.
Set Default Proof Using "Type".
+(** * Utility definitions used by the proofmode *)
+
(* Directions of rewrites *)
Inductive direction := Left | Right.
@@ -84,11 +86,18 @@ Qed.
Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
-(** Copies of some definitions so we can control their unfolding *)
-Definition option_bind {A B} (f : A → option B) (mx : option A) : option B :=
+(** Copies of some [option] combinators for better reduction control. *)
+Definition pm_option_bind {A B} (f : A → option B) (mx : option A) : option B :=
match mx with Some x => f x | None => None end.
-Arguments option_bind {_ _} _ !_ / : assert.
+Arguments pm_option_bind {_ _} _ !_ /.
-Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
+Definition pm_from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
match mx with None => y | Some x => f x end.
-Arguments from_option {_ _} _ _ !_ / : assert.
+Arguments pm_from_option {_ _} _ _ !_ /.
+
+Definition pm_option_fun {A B} (f : option (A → B)) (x : A) : option B :=
+ match f with None => None | Some f => Some (f x) end.
+Arguments pm_option_fun {_ _} !_ _ /.
+
+(* Can't write [id] here as that would not reduce. *)
+Notation pm_default := (pm_from_option (λ x, x)).
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 0aec0913e85ce03b9377b1092048c85271c09832..70692eb2ee9eea5d8c8c336cab0cbb339fa15775 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -1,12 +1,13 @@
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import modality_instances classes ltac_tactics.
+From iris.proofmode Require Import base modality_instances classes ltac_tactics.
Set Default Proof Using "Type".
Import bi.
Section bi_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
+Implicit Types mP : option PROP.
(** AsEmpValid *)
Global Instance as_emp_valid_emp_valid {PROP : bi} (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0.
@@ -999,7 +1000,8 @@ Global Instance elim_inv_acc_with_close {X : Type}
IntoAcc Pinv φ1 Pin M1 M2 α β mγ →
(∀ R, ElimModal φ2 false false (M1 R) R Q Q') →
ElimInv (X:=X) (φ1 ∧ φ2) Pinv Pin
- α (Some (λ x, β x -∗ M2 (proofmode.base.from_option id emp (mγ x))))%I
+ α
+ (Some (λ x, β x -∗ M2 (pm_default emp (mγ x))))%I
Q (λ _, Q').
Proof.
rewrite /ElimAcc /IntoAcc /ElimInv.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index d84af6751b38e90029172a748d058f804d38660e..6c9e2203bf4becce845734e07c2923d51619500b 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -1,6 +1,6 @@
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import modality_instances classes class_instances_bi ltac_tactics.
+From iris.proofmode Require Import modality_instances classes class_instances_bi coq_tactics ltac_tactics.
Set Default Proof Using "Type".
Import bi.
@@ -499,9 +499,9 @@ Global Instance elim_acc_fupd `{BiFUpd PROP} {X} E1 E2 E α β mγ Q :
(* FIXME: Why %I? ElimAcc sets the right scopes! *)
ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β mγ
(|={E1,E}=> Q)
- (λ x, |={E2}=> β x ∗ (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q)))%I.
+ (λ x, |={E2}=> β x ∗ (pm_maybe_wand (mγ x) (|={E1,E}=> Q)))%I.
Proof.
- rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
+ rewrite /ElimAcc. setoid_rewrite pm_maybe_wand_sound.
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 9d94d8cff1f5b6f60e5d886d59cbeb4fd926c631..1a3f4043343459629e1a162c2ee7a78c56d8c38c 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -1,4 +1,5 @@
From iris.bi Require Export bi.
+From iris.proofmode Require Import base.
From iris.proofmode Require Export modalities.
From stdpp Require Import namespaces.
Set Default Proof Using "Type".
@@ -526,7 +527,7 @@ Hint Mode IntoInv + ! - : typeclass_instances.
instances to recognize the [emp] case and make it look nicer. *)
Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
(α β : X → PROP) (mγ : X → option PROP) : PROP :=
- M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (mγ x))))%I.
+ M1 (∃ x, α x ∗ (β x -∗ M2 (pm_default emp (mγ x))))%I.
(* Typeclass for assertions around which accessors can be elliminated.
Inputs: [Q], [E1], [E2], [α], [β], [γ]
@@ -582,7 +583,7 @@ Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
(Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))
(Q : PROP) (Q' : X → PROP) :=
- elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
+ elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (pm_default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 444dd0a8dc9c94b38606f72829eb50527b61269f..20abcb4fc6d5550a654e2a3e82e5cbbd26898e53 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -7,140 +7,7 @@ Import env_notations.
Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
-Record envs (PROP : bi) :=
- Envs { env_intuitionistic : env PROP; env_spatial : env PROP; env_counter : positive }.
-Add Printing Constructor envs.
-Arguments Envs {_} _ _ _.
-Arguments env_intuitionistic {_} _.
-Arguments env_spatial {_} _.
-Arguments env_counter {_} _.
-
-Record envs_wf {PROP} (Δ : envs PROP) := {
- env_intuitionistic_valid : env_wf (env_intuitionistic Δ);
- env_spatial_valid : env_wf (env_spatial Δ);
- envs_disjoint i : env_intuitionistic Δ !! i = None ∨ env_spatial Δ !! i = None
-}.
-
-Definition of_envs {PROP} (Δ : envs PROP) : PROP :=
- (⌜envs_wf Δ⌠∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I.
-Instance: Params (@of_envs) 1.
-Arguments of_envs : simpl never.
-
-(* We seal [envs_entails], so that it does not get unfolded by the
- proofmode's own tactics, such as [iIntros (?)]. *)
-Definition envs_entails_aux : seal (λ PROP (Δ : envs PROP) (Q : PROP), (of_envs Δ ⊢ Q)).
-Proof. by eexists. Qed.
-Definition envs_entails := envs_entails_aux.(unseal).
-Definition envs_entails_eq : envs_entails = _ := envs_entails_aux.(seal_eq).
-Arguments envs_entails {PROP} Δ Q%I : rename.
-Instance: Params (@envs_entails) 1.
-
-Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
- env_intuitionistic_Forall2 : env_Forall2 R (env_intuitionistic Δ1) (env_intuitionistic Δ2);
- env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
-}.
-
-Definition envs_dom {PROP} (Δ : envs PROP) : list ident :=
- env_dom (env_intuitionistic Δ) ++ env_dom (env_spatial Δ).
-
-Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
- let (Γp,Γs,n) := Δ in
- match env_lookup i Γp with
- | Some P => Some (true, P)
- | None => P ↠env_lookup i Γs; Some (false, P)
- end.
-
-Definition envs_delete {PROP} (remove_persistent : bool)
- (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
- let (Γp,Γs,n) := Δ in
- match p with
- | true => Envs (if remove_persistent then env_delete i Γp else Γp) Γs n
- | false => Envs Γp (env_delete i Γs) n
- end.
-
-Definition envs_lookup_delete {PROP} (remove_persistent : bool)
- (i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
- let (Γp,Γs,n) := Δ in
- match env_lookup_delete i Γp with
- | Some (P,Γp') => Some (true, P, Envs (if remove_persistent then Γp' else Γp) Γs n)
- | None => ''(P,Γs') ↠env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
- end.
-
-Fixpoint envs_lookup_delete_list {PROP} (remove_persistent : bool)
- (js : list ident) (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
- match js with
- | [] => Some (true, [], Δ)
- | j :: js =>
- ''(p,P,Δ') ↠envs_lookup_delete remove_persistent j Δ;
- ''(q,Hs,Δ'') ↠envs_lookup_delete_list remove_persistent js Δ';
- Some ((p:bool) && q, P :: Hs, Δ'')
- end.
-
-Definition envs_snoc {PROP} (Δ : envs PROP)
- (p : bool) (j : ident) (P : PROP) : envs PROP :=
- let (Γp,Γs,n) := Δ in
- if p then Envs (Esnoc Γp j P) Γs n else Envs Γp (Esnoc Γs j P) n.
-
-Definition envs_app {PROP : bi} (p : bool)
- (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
- let (Γp,Γs,n) := Δ in
- match p with
- | true => _ ↠env_app Γ Γs; Γp' ↠env_app Γ Γp; Some (Envs Γp' Γs n)
- | false => _ ↠env_app Γ Γp; Γs' ↠env_app Γ Γs; Some (Envs Γp Γs' n)
- end.
-
-Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
- (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
- let (Γp,Γs,n) := Δ in
- match p with
- | true => _ ↠env_app Γ Γs; Γp' ↠env_replace i Γ Γp; Some (Envs Γp' Γs n)
- | false => _ ↠env_app Γ Γp; Γs' ↠env_replace i Γ Γs; Some (Envs Γp Γs' n)
- end.
-
-Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
- (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
- if Bool.eqb p q then envs_simple_replace i p Γ Δ
- else envs_app q Γ (envs_delete true i p Δ).
-
-Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
- if env_spatial Δ is Enil then true else false.
-
-Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
- Envs (env_intuitionistic Δ) Enil (env_counter Δ).
-
-Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
- Envs Enil (env_spatial Δ) (env_counter Δ).
-
-Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
- Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos.succ (env_counter Δ)).
-
-Fixpoint envs_split_go {PROP}
- (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
- match js with
- | [] => Some (Δ1, Δ2)
- | j :: js =>
- ''(p,P,Δ1') ↠envs_lookup_delete true j Δ1;
- if p : bool then envs_split_go js Δ1 Δ2 else
- envs_split_go js Δ1' (envs_snoc Δ2 false j P)
- end.
-(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
- if [d = Left] then [result = (hyps named js, remaining hyps)] *)
-Definition envs_split {PROP} (d : direction)
- (js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
- ''(Δ1,Δ2) ↠envs_split_go js Δ (envs_clear_spatial Δ);
- if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
-
-Definition prop_of_env {PROP : bi} (Γ : env PROP) : PROP :=
- let fix aux Γ acc :=
- match Γ with Enil => acc | Esnoc Γ _ P => aux Γ (P ∗ acc)%I end
- in
- match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
-
-Definition maybe_wand {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
- match mP with
- | None => Q
- | Some P => (P -∗ Q)%I
- end.
+Notation pm_maybe_wand mP Q := (pm_from_option (λ P, P -∗ Q)%I Q%I mP).
(* Coq versions of the tactics *)
Section bi_tactics.
@@ -343,7 +210,7 @@ Lemma envs_replace_sound' Δ Δ' i p q Γ :
envs_replace i p q Γ Δ = Some Δ' →
of_envs (envs_delete true i p Δ) ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
Proof.
- rewrite /envs_replace; destruct (Bool.eqb _ _) eqn:Hpq.
+ rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
- apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
- apply envs_app_sound.
Qed.
@@ -449,8 +316,8 @@ Proof.
- rewrite /= IH (comm _ Q _) assoc. done.
Qed.
-Lemma maybe_wand_sound (mP : option PROP) Q :
- maybe_wand mP Q ⊣⊢ (default emp mP -∗ Q).
+Lemma pm_maybe_wand_sound mP Q :
+ pm_maybe_wand mP Q ⊣⊢ (default emp mP -∗ Q).
Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
Global Instance envs_Forall2_refl (R : relation PROP) :
@@ -751,7 +618,6 @@ Proof.
rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_singleton_sound Δ2) //; simpl.
rewrite HP1 into_wand /= -(add_modal P1' P1 Q). cancel [P1'].
-
apply wand_intro_l. by rewrite assoc !wand_elim_r.
Qed.
@@ -1109,7 +975,10 @@ Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X
φ →
(∀ R, ∃ Δ'',
envs_app false (Esnoc Enil j
- (Pin -∗ (∀ x, Pout x -∗ from_option (λ Pclose, Pclose x -∗ Q' x) (Q' x) Pclose) -∗ R)%I) Δ'
+ (Pin -∗
+ (∀ x, Pout x -∗ pm_maybe_wand (pm_option_fun Pclose x) (Q' x)) -∗
+ R
+ )%I) Δ'
= Some Δ'' ∧
envs_entails Δ'' R) →
envs_entails Δ Q.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 4816f938a0daae36ba3b2bcd964b00bb3936b3a9..e27df470449a17b583c0258200d1aa2ad7ecd3fa 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -1,5 +1,6 @@
From iris.proofmode Require Import base.
From iris.algebra Require Export base.
+From iris.bi Require Export bi.
Set Default Proof Using "Type".
Inductive env (A : Type) : Type :=
@@ -17,7 +18,7 @@ Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
end.
Module env_notations.
- Notation "y ≫= f" := (option_bind f y).
+ Notation "y ≫= f" := (pm_option_bind f y).
Notation "x ↠y ; z" := (y ≫= λ x, z).
Notation "' x1 .. xn ↠y ; z" := (y ≫= (λ x1, .. (λ xn, z) .. )).
Notation "Γ !! j" := (env_lookup j Γ).
@@ -93,8 +94,8 @@ Ltac simplify :=
| _ => progress simplify_eq/=
| H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
| |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
- | H : context [option_bind _ ?x] |- _ => destruct x eqn:?
- | |- context [option_bind _ ?x] => destruct x eqn:?
+ | H : context [pm_option_bind _ ?x] |- _ => destruct x eqn:?
+ | |- context [pm_option_bind _ ?x] => destruct x eqn:?
| _ => case_match
end.
@@ -205,3 +206,132 @@ Global Instance env_to_list_subenv_proper :
Proper (env_subenv ==> sublist) (@env_to_list A).
Proof. induction 1; simpl; constructor; auto. Qed.
End env.
+
+Record envs (PROP : bi) :=
+ Envs { env_intuitionistic : env PROP; env_spatial : env PROP; env_counter : positive }.
+Add Printing Constructor envs.
+Arguments Envs {_} _ _ _.
+Arguments env_intuitionistic {_} _.
+Arguments env_spatial {_} _.
+Arguments env_counter {_} _.
+
+Record envs_wf {PROP} (Δ : envs PROP) := {
+ env_intuitionistic_valid : env_wf (env_intuitionistic Δ);
+ env_spatial_valid : env_wf (env_spatial Δ);
+ envs_disjoint i : env_intuitionistic Δ !! i = None ∨ env_spatial Δ !! i = None
+}.
+
+Definition of_envs {PROP} (Δ : envs PROP) : PROP :=
+ (⌜envs_wf Δ⌠∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I.
+Instance: Params (@of_envs) 1.
+Arguments of_envs : simpl never.
+
+(* We seal [envs_entails], so that it does not get unfolded by the
+ proofmode's own tactics, such as [iIntros (?)]. *)
+Definition envs_entails_aux : seal (λ PROP (Δ : envs PROP) (Q : PROP), (of_envs Δ ⊢ Q)).
+Proof. by eexists. Qed.
+Definition envs_entails := envs_entails_aux.(unseal).
+Definition envs_entails_eq : envs_entails = _ := envs_entails_aux.(seal_eq).
+Arguments envs_entails {PROP} Δ Q%I : rename.
+Instance: Params (@envs_entails) 1.
+
+Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
+ env_intuitionistic_Forall2 : env_Forall2 R (env_intuitionistic Δ1) (env_intuitionistic Δ2);
+ env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
+}.
+
+Definition envs_dom {PROP} (Δ : envs PROP) : list ident :=
+ env_dom (env_intuitionistic Δ) ++ env_dom (env_spatial Δ).
+
+Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
+ let (Γp,Γs,n) := Δ in
+ match env_lookup i Γp with
+ | Some P => Some (true, P)
+ | None => P ↠env_lookup i Γs; Some (false, P)
+ end.
+
+Definition envs_delete {PROP} (remove_persistent : bool)
+ (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
+ let (Γp,Γs,n) := Δ in
+ match p with
+ | true => Envs (if remove_persistent then env_delete i Γp else Γp) Γs n
+ | false => Envs Γp (env_delete i Γs) n
+ end.
+
+Definition envs_lookup_delete {PROP} (remove_persistent : bool)
+ (i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
+ let (Γp,Γs,n) := Δ in
+ match env_lookup_delete i Γp with
+ | Some (P,Γp') => Some (true, P, Envs (if remove_persistent then Γp' else Γp) Γs n)
+ | None => ''(P,Γs') ↠env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
+ end.
+
+Fixpoint envs_lookup_delete_list {PROP} (remove_persistent : bool)
+ (js : list ident) (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
+ match js with
+ | [] => Some (true, [], Δ)
+ | j :: js =>
+ ''(p,P,Δ') ↠envs_lookup_delete remove_persistent j Δ;
+ ''(q,Hs,Δ'') ↠envs_lookup_delete_list remove_persistent js Δ';
+ Some ((p:bool) && q, P :: Hs, Δ'')
+ end.
+
+Definition envs_snoc {PROP} (Δ : envs PROP)
+ (p : bool) (j : ident) (P : PROP) : envs PROP :=
+ let (Γp,Γs,n) := Δ in
+ if p then Envs (Esnoc Γp j P) Γs n else Envs Γp (Esnoc Γs j P) n.
+
+Definition envs_app {PROP : bi} (p : bool)
+ (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
+ let (Γp,Γs,n) := Δ in
+ match p with
+ | true => _ ↠env_app Γ Γs; Γp' ↠env_app Γ Γp; Some (Envs Γp' Γs n)
+ | false => _ ↠env_app Γ Γp; Γs' ↠env_app Γ Γs; Some (Envs Γp Γs' n)
+ end.
+
+Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
+ (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
+ let (Γp,Γs,n) := Δ in
+ match p with
+ | true => _ ↠env_app Γ Γs; Γp' ↠env_replace i Γ Γp; Some (Envs Γp' Γs n)
+ | false => _ ↠env_app Γ Γp; Γs' ↠env_replace i Γ Γs; Some (Envs Γp Γs' n)
+ end.
+
+Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
+ (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
+ if beq p q then envs_simple_replace i p Γ Δ
+ else envs_app q Γ (envs_delete true i p Δ).
+
+Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
+ if env_spatial Δ is Enil then true else false.
+
+Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
+ Envs (env_intuitionistic Δ) Enil (env_counter Δ).
+
+Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
+ Envs Enil (env_spatial Δ) (env_counter Δ).
+
+Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
+ Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos.succ (env_counter Δ)).
+
+Fixpoint envs_split_go {PROP}
+ (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
+ match js with
+ | [] => Some (Δ1, Δ2)
+ | j :: js =>
+ ''(p,P,Δ1') ↠envs_lookup_delete true j Δ1;
+ if p : bool then envs_split_go js Δ1 Δ2 else
+ envs_split_go js Δ1' (envs_snoc Δ2 false j P)
+ end.
+(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
+ if [d = Left] then [result = (hyps named js, remaining hyps)] *)
+Definition envs_split {PROP} (d : direction)
+ (js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
+ ''(Δ1,Δ2) ↠envs_split_go js Δ (envs_clear_spatial Δ);
+ if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
+
+Definition prop_of_env {PROP : bi} (Γ : env PROP) : PROP :=
+ let fix aux Γ acc :=
+ match Γ with Enil => acc | Esnoc Γ _ P => aux Γ (P ∗ acc)%I end
+ in
+ match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 92a316b4dfc8918bc08a7da5d786b39da2807d20..f7b1df2917cc50a752909f712c6a163db9dd119a 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import coq_tactics.
+From iris.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
From iris.bi Require Export bi.
From stdpp Require Import namespaces.
@@ -7,22 +7,6 @@ From stdpp Require Import hlist pretty.
Set Default Proof Using "Type".
Export ident.
-(** These are all proofmode-internal definitions and hence unfolding them should
-not affect the user's goal. *)
-(* TODO: Can we option_bind, from_option, maybe_wand reduce only if applied to a constructor? *)
-Declare Reduction env_cbv := cbv [
- option_bind from_option
- beq ascii_beq string_beq positive_beq Pos.succ ident_beq
- env_lookup env_lookup_delete env_delete env_app env_replace env_dom
- env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
- envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
- envs_simple_replace envs_replace envs_split
- envs_clear_spatial envs_clear_persistent envs_incr_counter
- envs_split_go envs_split prop_of_env maybe_wand].
-Ltac env_cbv :=
- match goal with |- ?u => let v := eval env_cbv in u in change v end.
-Ltac env_reflexivity := env_cbv; exact eq_refl.
-
(** For most of the tactics, we want to have tight control over the order and
way in which type class inference is performed. To that end, many tactics make
use of [notypeclasses refine] and the [iSolveTC] tactic to manually invoke type
@@ -54,12 +38,12 @@ Ltac iMissingHyps Hs :=
| |- envs_entails ?Δ _ => Δ
| |- context[ envs_split _ _ ?Δ ] => Δ
end in
- let Hhyps := eval env_cbv in (envs_dom Δ) in
+ let Hhyps := pm_eval (envs_dom Δ) in
eval vm_compute in (list_difference Hs Hhyps).
Ltac iTypeOf H :=
let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
- eval env_cbv in (envs_lookup H Δ).
+ pm_eval (envs_lookup H Δ).
Tactic Notation "iMatchHyp" tactic1(tac) :=
match goal with
@@ -105,11 +89,11 @@ Ltac iFresh :=
side-effect. See https://stackoverflow.com/a/46178884 *)
let do_incr :=
lazymatch goal with
- | _ => iStartProof; eapply tac_fresh; first by (env_reflexivity)
+ | _ => iStartProof; eapply tac_fresh; first by (pm_reflexivity)
end in
lazymatch goal with
|- envs_entails ?Δ _ =>
- let n := eval env_cbv in (env_counter Δ) in
+ let n := pm_eval (env_counter Δ) in
constr:(IAnon n)
end.
@@ -123,9 +107,9 @@ Tactic Notation "iEval" tactic(t) :=
Tactic Notation "iEval" tactic(t) "in" constr(H) :=
iStartProof;
eapply tac_eval_in with _ H _ _ _;
- [env_reflexivity || fail "iEval:" H "not found"
+ [pm_reflexivity || fail "iEval:" H "not found"
|let x := fresh in intros x; t; unfold x; reflexivity
- |env_reflexivity
+ |pm_reflexivity
|].
Tactic Notation "iSimpl" := iEval simpl.
@@ -142,8 +126,8 @@ possible in Ltac2. *)
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
- [env_reflexivity || fail "iRename:" H1 "not found"
- |env_reflexivity || fail "iRename:" H2 "not fresh"|].
+ [pm_reflexivity || fail "iRename:" H1 "not found"
+ |pm_reflexivity || fail "iRename:" H2 "not fresh"|].
Local Inductive esel_pat :=
| ESelPure
@@ -154,15 +138,15 @@ Ltac iElaborateSelPat_go pat Δ Hs :=
| [] => eval cbv in Hs
| SelPure :: ?pat => iElaborateSelPat_go pat Δ (ESelPure :: Hs)
| SelPersistent :: ?pat =>
- let Hs' := eval env_cbv in (env_dom (env_intuitionistic Δ)) in
- let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
+ let Hs' := pm_eval (env_dom (env_intuitionistic Δ)) in
+ let Δ' := pm_eval (envs_clear_persistent Δ) in
iElaborateSelPat_go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
| SelSpatial :: ?pat =>
- let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
- let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
+ let Hs' := pm_eval (env_dom (env_spatial Δ)) in
+ let Δ' := pm_eval (envs_clear_spatial Δ) in
iElaborateSelPat_go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
| SelIdent ?H :: ?pat =>
- lazymatch eval env_cbv in (envs_lookup_delete false H Δ) with
+ lazymatch pm_eval (envs_lookup_delete false H Δ) with
| Some (?p,_,?Δ') => iElaborateSelPat_go pat Δ' (ESelIdent p H :: Hs)
| None => fail "iElaborateSelPat:" H "not found"
end
@@ -175,8 +159,8 @@ Ltac iElaborateSelPat pat :=
Local Ltac iClearHyp H :=
eapply tac_clear with _ H _ _; (* (i:=H) *)
- [env_reflexivity || fail "iClear:" H "not found"
- |env_cbv; iSolveTC ||
+ [pm_reflexivity || fail "iClear:" H "not found"
+ |pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iClear:" H ":" P "not affine and the goal not absorbing"
|].
@@ -196,11 +180,11 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
eapply tac_assumption with _ H _ _; (* (i:=H) *)
- [env_reflexivity || fail "iExact:" H "not found"
+ [pm_reflexivity || fail "iExact:" H "not found"
|iSolveTC ||
let P := match goal with |- FromAssumption _ ?P _ => P end in
fail "iExact:" H ":" P "does not match goal"
- |env_cbv; iSolveTC ||
+ |pm_reduce; iSolveTC ||
fail "iExact:" H "not absorbing and the remaining hypotheses not affine"].
Tactic Notation "iAssumptionCore" :=
@@ -210,13 +194,13 @@ Tactic Notation "iAssumptionCore" :=
end in
match goal with
| |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some (_, ?P) =>
- first [is_evar i; fail 1 | env_reflexivity]
+ first [is_evar i; fail 1 | pm_reflexivity]
| |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some (_, ?P) =>
- is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
+ is_evar i; first [find Γp i P | find Γs i P]; pm_reflexivity
| |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
- first [is_evar i; fail 1 | env_reflexivity]
+ first [is_evar i; fail 1 | pm_reflexivity]
| |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
- is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
+ is_evar i; first [find Γp i P | find Γs i P]; pm_reflexivity
end.
Tactic Notation "iAssumption" :=
@@ -226,13 +210,13 @@ Tactic Notation "iAssumption" :=
| Esnoc ?Γ ?j ?P => first
[pose proof (_ : FromAssumption p P Q) as Hass;
eapply (tac_assumption _ _ j p P);
- [env_reflexivity
+ [pm_reflexivity
|apply Hass
- |env_cbv; iSolveTC ||
+ |pm_reduce; iSolveTC ||
fail 1 "iAssumption:" j "not absorbing and the remaining hypotheses not affine"]
|assert (P = False%I) as Hass by reflexivity;
apply (tac_false_destruct _ j p P);
- [env_reflexivity
+ [pm_reflexivity
|exact Hass]
|find p Γ Q]
end in
@@ -248,22 +232,22 @@ Tactic Notation "iExFalso" := apply tac_ex_falso.
(** * Making hypotheses persistent or pure *)
Local Tactic Notation "iPersistent" constr(H) :=
eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
- [env_reflexivity || fail "iPersistent:" H "not found"
+ [pm_reflexivity || fail "iPersistent:" H "not found"
|iSolveTC ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in
fail "iPersistent:" P "not persistent"
- |env_cbv; iSolveTC ||
+ |pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iPersistent:" P "not affine and the goal not absorbing"
- |env_reflexivity|].
+ |pm_reflexivity|].
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
- [env_reflexivity || fail "iPure:" H "not found"
+ [pm_reflexivity || fail "iPure:" H "not found"
|iSolveTC ||
let P := match goal with |- IntoPure ?P _ => P end in
fail "iPure:" P "not pure"
- |env_cbv; iSolveTC ||
+ |pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iPure:" P "not affine and the goal not absorbing"
|intros pat].
@@ -271,13 +255,13 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
Tactic Notation "iEmpIntro" :=
iStartProof;
eapply tac_emp_intro;
- [env_cbv; iSolveTC ||
+ [pm_reduce; iSolveTC ||
fail "iEmpIntro: spatial context contains non-affine hypotheses"].
Tactic Notation "iPureIntro" :=
iStartProof;
eapply tac_pure_intro;
- [env_reflexivity
+ [pm_reflexivity
|iSolveTC ||
let P := match goal with |- FromPure _ ?P _ => P end in
fail "iPureIntro:" P "not pure"
@@ -301,7 +285,7 @@ Local Ltac iFramePure t :=
Local Ltac iFrameHyp H :=
iStartProof;
eapply tac_frame with _ H _ _ _;
- [env_reflexivity || fail "iFrame:" H "not found"
+ [pm_reflexivity || fail "iFrame:" H "not found"
|iSolveTC ||
let R := match goal with |- Frame _ ?R _ _ => R end in
fail "iFrame: cannot frame" R
@@ -407,17 +391,17 @@ Local Tactic Notation "iIntro" constr(H) :=
[ (* (?Q → _) *)
eapply tac_impl_intro with _ H _ _ _; (* (i:=H) *)
[iSolveTC
- |env_cbv; iSolveTC ||
+ |pm_reduce; iSolveTC ||
let P := lazymatch goal with |- Persistent ?P => P end in
fail 1 "iIntro: introducing non-persistent" H ":" P
"into non-empty spatial context"
- |env_reflexivity || fail 1 "iIntro:" H "not fresh"
+ |pm_reflexivity || fail 1 "iIntro:" H "not fresh"
|iSolveTC
|]
| (* (_ -∗ _) *)
eapply tac_wand_intro with _ H _ _; (* (i:=H) *)
[iSolveTC
- | env_reflexivity || fail 1 "iIntro:" H "not fresh"
+ | pm_reflexivity || fail 1 "iIntro:" H "not fresh"
|]
| fail "iIntro: nothing to introduce" ].
@@ -430,7 +414,7 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
|iSolveTC ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in
fail 1 "iIntro:" P "not persistent"
- |env_reflexivity || fail 1 "iIntro:" H "not fresh"
+ |pm_reflexivity || fail 1 "iIntro:" H "not fresh"
|]
| (* (?P -∗ _) *)
eapply tac_wand_intro_persistent with _ H _ _ _; (* (i:=H) *)
@@ -441,7 +425,7 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
|iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail 1 "iIntro:" P "not affine and the goal not absorbing"
- |env_reflexivity || fail 1 "iIntro:" H "not fresh"
+ |pm_reflexivity || fail 1 "iIntro:" H "not fresh"
|]
| fail "iIntro: nothing to introduce" ].
@@ -504,14 +488,14 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
| hnil => idtac
| hcons ?x ?xs =>
notypeclasses refine (tac_forall_specialize _ _ H _ _ _ _ _ _ _);
- [env_reflexivity || fail "iSpecialize:" H "not found"
+ [pm_reflexivity || fail "iSpecialize:" H "not found"
|iSolveTC ||
let P := match goal with |- IntoForall ?P _ => P end in
fail "iSpecialize: cannot instantiate" P "with" x
|lazymatch goal with (* Force [A] in [ex_intro] to deal with coercions. *)
| |- ∃ _ : ?A, _ =>
notypeclasses refine (@ex_intro A _ x (conj _ _))
- end; [shelve..|env_reflexivity|go xs]]
+ end; [shelve..|pm_reflexivity|go xs]]
end in
go xs.
@@ -535,32 +519,32 @@ Ltac iSpecializePat_go H1 pats :=
iSpecializePat_go H1 pats
| SIdent ?H2 :: ?pats =>
notypeclasses refine (tac_specialize _ _ _ H2 _ H1 _ _ _ _ _ _ _ _ _ _);
- [env_reflexivity || fail "iSpecialize:" H2 "not found"
- |env_reflexivity || fail "iSpecialize:" H1 "not found"
+ [pm_reflexivity || fail "iSpecialize:" H2 "not found"
+ |pm_reflexivity || fail "iSpecialize:" H1 "not found"
|iSolveTC ||
let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
fail "iSpecialize: cannot instantiate" P "with" Q
- |env_reflexivity|iSpecializePat_go H1 pats]
+ |pm_reflexivity|iSpecializePat_go H1 pats]
| SPureGoal ?d :: ?pats =>
notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
- [env_reflexivity || fail "iSpecialize:" H1 "not found"
+ [pm_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|iSolveTC ||
let Q := match goal with |- FromPure _ ?Q _ => Q end in
fail "iSpecialize:" Q "not pure"
- |env_reflexivity
+ |pm_reflexivity
|solve_done d (*goal*)
|iSpecializePat_go H1 pats]
| SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
- [env_reflexivity || fail "iSpecialize:" H1 "not found"
+ [pm_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|iSolveTC ||
let Q := match goal with |- Persistent ?Q => Q end in
fail "iSpecialize:" Q "not persistent"
|iSolveTC
- |env_reflexivity
+ |pm_reflexivity
|iFrame Hs_frame; solve_done d (*goal*)
|iSpecializePat_go H1 pats]
| SGoal (SpecGoal GPersistent _ _ _ _) :: ?pats =>
@@ -568,30 +552,30 @@ Ltac iSpecializePat_go H1 pats :=
| SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
notypeclasses refine (tac_specialize_assert _ _ _ _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _ _ _);
- [env_reflexivity || fail "iSpecialize:" H1 "not found"
+ [pm_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|lazymatch m with
| GSpatial => notypeclasses refine (add_modal_id _ _)
| GModal => iSolveTC || fail "iSpecialize: goal not a modality"
end
- |env_reflexivity ||
+ |pm_reflexivity ||
let Hs' := iMissingHyps Hs' in
fail "iSpecialize: hypotheses" Hs' "not found"
|iFrame Hs_frame; solve_done d (*goal*)
|iSpecializePat_go H1 pats]
| SAutoFrame GPersistent :: ?pats =>
notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
- [env_reflexivity || fail "iSpecialize:" H1 "not found"
+ [pm_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|iSolveTC ||
let Q := match goal with |- Persistent ?Q => Q end in
fail "iSpecialize:" Q "not persistent"
- |env_reflexivity
+ |pm_reflexivity
|solve [iFrame "∗ #"]
|iSpecializePat_go H1 pats]
| SAutoFrame ?m :: ?pats =>
notypeclasses refine (tac_specialize_frame _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
- [env_reflexivity || fail "iSpecialize:" H1 "not found"
+ [pm_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|lazymatch m with
| GSpatial => notypeclasses refine (add_modal_id _ _)
@@ -641,18 +625,18 @@ Tactic Notation "iSpecializeCore" open_constr(H)
| true =>
(* FIXME: do something reasonable when the BI is not affine *)
notypeclasses refine (tac_specialize_persistent_helper _ _ H _ _ _ _ _ _ _ _ _ _ _);
- [env_reflexivity || fail "iSpecialize:" H "not found"
+ [pm_reflexivity || fail "iSpecialize:" H "not found"
|iSpecializePat H pat;
[..
|refine (tac_specialize_persistent_helper_done _ H _ _ _);
- env_reflexivity]
+ pm_reflexivity]
|iSolveTC ||
let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
fail "iSpecialize:" Q "not persistent"
- |env_cbv; iSolveTC ||
+ |pm_reduce; iSolveTC ||
let Q := match goal with |- TCAnd _ (Affine ?Q) => Q end in
fail "iSpecialize:" Q "not affine"
- |env_reflexivity
+ |pm_reflexivity
|(* goal *)]
| false => iSpecializePat H pat
end
@@ -748,13 +732,13 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
lazymatch type of t with
| ident =>
eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
- [env_reflexivity || fail "iPoseProof:" t "not found"
- |env_reflexivity || fail "iPoseProof:" Htmp "not fresh"
+ [pm_reflexivity || fail "iPoseProof:" t "not found"
+ |pm_reflexivity || fail "iPoseProof:" Htmp "not fresh"
|goal_tac ()]
| _ =>
eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
[iIntoEmpValid t
- |env_reflexivity || fail "iPoseProof:" Htmp "not fresh"
+ |pm_reflexivity || fail "iPoseProof:" Htmp "not fresh"
|goal_tac ()]
end;
try iSolveTC in
@@ -767,9 +751,9 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
Tactic Notation "iApplyHyp" constr(H) :=
let rec go H := first
[eapply tac_apply with _ H _ _ _;
- [env_reflexivity
+ [pm_reflexivity
|iSolveTC
- |lazy beta (* reduce betas created by instantiation *)]
+ |pm_reduce (* reduce redexes created by instantiation *)]
|iSpecializePat H "[]"; last go H] in
iExact H ||
go H ||
@@ -804,8 +788,8 @@ Tactic Notation "iRevert" constr(Hs) :=
go Hs
| ESelIdent _ ?H :: ?Hs =>
eapply tac_revert with _ H _ _; (* (i:=H2) *)
- [env_reflexivity || fail "iRevert:" H "not found"
- |env_cbv; go Hs]
+ [pm_reflexivity || fail "iRevert:" H "not found"
+ |pm_reduce; go Hs]
end in
let Hs := iElaborateSelPat Hs in iStartProof; go Hs.
@@ -870,12 +854,12 @@ Tactic Notation "iRight" :=
Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
- [env_reflexivity || fail "iOrDestruct:" H "not found"
+ [pm_reflexivity || fail "iOrDestruct:" H "not found"
|iSolveTC ||
let P := match goal with |- IntoOr ?P _ _ => P end in
fail "iOrDestruct: cannot destruct" P
- |env_reflexivity || fail "iOrDestruct:" H1 "not fresh"
- |env_reflexivity || fail "iOrDestruct:" H2 "not fresh"
+ |pm_reflexivity || fail "iOrDestruct:" H1 "not fresh"
+ |pm_reflexivity || fail "iOrDestruct:" H2 "not fresh"
| |].
(** * Conjunction and separating conjunction *)
@@ -894,7 +878,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
[iSolveTC ||
let P := match goal with |- FromSep _ ?P _ _ => P end in
fail "iSplitL:" P "not a separating conjunction"
- |env_reflexivity ||
+ |pm_reflexivity ||
let Hs := iMissingHyps Hs in
fail "iSplitL: hypotheses" Hs "not found"
| |].
@@ -907,7 +891,7 @@ Tactic Notation "iSplitR" constr(Hs) :=
[iSolveTC ||
let P := match goal with |- FromSep _ ?P _ _ => P end in
fail "iSplitR:" P "not a separating conjunction"
- |env_reflexivity ||
+ |pm_reflexivity ||
let Hs := iMissingHyps Hs in
fail "iSplitR: hypotheses" Hs "not found"
| |].
@@ -917,23 +901,23 @@ Tactic Notation "iSplitR" := iSplitL "".
Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
eapply tac_and_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
- [env_reflexivity || fail "iAndDestruct:" H "not found"
- |env_cbv; iSolveTC ||
+ [pm_reflexivity || fail "iAndDestruct:" H "not found"
+ |pm_reduce; iSolveTC ||
let P :=
lazymatch goal with
| |- IntoSep ?P _ _ => P
| |- IntoAnd _ ?P _ _ => P
end in
fail "iAndDestruct: cannot destruct" P
- |env_reflexivity || fail "iAndDestruct:" H1 "or" H2 " not fresh"|].
+ |pm_reflexivity || fail "iAndDestruct:" H1 "or" H2 " not fresh"|].
Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :=
eapply tac_and_destruct_choice with _ H _ d H' _ _ _;
- [env_reflexivity || fail "iAndDestructChoice:" H "not found"
- |env_cbv; iSolveTC ||
+ [pm_reflexivity || fail "iAndDestructChoice:" H "not found"
+ |pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (IntoAnd _ ?P _ _) _ => P end in
fail "iAndDestructChoice: cannot destruct" P
- |env_reflexivity || fail "iAndDestructChoice:" H' " not fresh"|].
+ |pm_reflexivity || fail "iAndDestructChoice:" H' " not fresh"|].
(** * Existential *)
Tactic Notation "iExists" uconstr(x1) :=
@@ -968,13 +952,13 @@ 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) *)
- [env_reflexivity || fail "iExistDestruct:" H "not found"
+ [pm_reflexivity || fail "iExistDestruct:" H "not found"
|iSolveTC ||
let P := match goal with |- IntoExist ?P _ => P end in
fail "iExistDestruct: cannot destruct" P|];
let y := fresh in
intros y; eexists; split;
- [env_reflexivity || fail "iExistDestruct:" Hx "not fresh"
+ [pm_reflexivity || fail "iExistDestruct:" Hx "not fresh"
|revert y; intros x].
(** * Modality introduction *)
@@ -995,7 +979,7 @@ Tactic Notation "iModIntro" uconstr(sel) :=
| MIEnvForall ?C => fail "iModIntro: spatial context does not satisfy" C
| MIEnvIsEmpty => fail "iModIntro: spatial context is non-empty"
end
- |env_cbv; iSolveTC ||
+ |pm_reduce; iSolveTC ||
fail "iModIntro: cannot filter spatial context when goal is not absorbing"
|].
Tactic Notation "iModIntro" := iModIntro _.
@@ -1008,13 +992,13 @@ Tactic Notation "iNext" := iModIntro (â–·^_ _)%I.
(** * Update modality *)
Tactic Notation "iModCore" constr(H) :=
eapply tac_modal_elim with _ H _ _ _ _ _ _;
- [env_reflexivity || fail "iMod:" H "not found"
+ [pm_reflexivity || fail "iMod:" H "not found"
|iSolveTC ||
let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
fail "iMod: cannot eliminate modality " P "in" Q
|iSolveSideCondition
- |env_reflexivity|].
+ |pm_reflexivity|].
(** * Basic destruct tactic *)
Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
@@ -1098,11 +1082,11 @@ Tactic Notation "iCombine" constr(Hs) "as" constr(pat) :=
let Hs := eval vm_compute in (INamed <$> Hs) in
let H := iFresh in
eapply tac_combine with _ _ Hs _ _ H _;
- [env_reflexivity ||
+ [pm_reflexivity ||
let Hs := iMissingHyps Hs in
fail "iCombine: hypotheses" Hs "not found"
|iSolveTC
- |env_reflexivity || fail "iCombine:" H "not fresh"
+ |pm_reflexivity || fail "iCombine:" H "not fresh"
|iDestructHyp H as pat].
Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(pat) :=
@@ -1568,7 +1552,7 @@ Tactic Notation "iInductionCore" constr(x) "as" simple_intropattern(pat) constr(
lazymatch goal with
| H : context [envs_entails _ _] |- _ =>
eapply (tac_revert_ih _ _ _ H _);
- [env_reflexivity
+ [pm_reflexivity
|| fail "iInduction: spatial context not empty, this should not happen"
|clear H];
fix_ihs ltac:(fun j =>
@@ -1673,7 +1657,7 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
not have this issue. *)
notypeclasses refine (tac_löb _ _ IH _ _ _ _);
[reflexivity || fail "iLöb: spatial context not empty, this should not happen"
- |env_reflexivity || fail "iLöb:" IH "not fresh"|].
+ |pm_reflexivity || fail "iLöb:" IH "not fresh"|].
Tactic Notation "iLöbRevert" constr(Hs) "with" tactic(tac) :=
iRevertIntros Hs with (
@@ -1745,7 +1729,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
end;
let H := iFresh in
eapply tac_assert with _ H Q;
- [env_reflexivity
+ [pm_reflexivity
|iSpecializeCore H with hnil pats as p; [..|tac H]].
Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic(tac) :=
@@ -1806,7 +1790,7 @@ Local Ltac iRewriteFindPred :=
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
iPoseProofCore lem as true true (fun Heq =>
eapply (tac_rewrite _ Heq _ _ lr);
- [env_reflexivity || fail "iRewrite:" Heq "not found"
+ [pm_reflexivity || fail "iRewrite:" Heq "not found"
|iSolveTC ||
let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
fail "iRewrite:" P "not an equality"
@@ -1819,14 +1803,14 @@ Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore Left lem.
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) :=
iPoseProofCore lem as true true (fun Heq =>
eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
- [env_reflexivity || fail "iRewrite:" Heq "not found"
- |env_reflexivity || fail "iRewrite:" H "not found"
+ [pm_reflexivity || fail "iRewrite:" Heq "not found"
+ |pm_reflexivity || fail "iRewrite:" H "not found"
|iSolveTC ||
let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
fail "iRewrite:" P "not an equality"
|iRewriteFindPred
|intros ??? ->; reflexivity
- |env_reflexivity|lazy beta; iClearHyp Heq]).
+ |pm_reflexivity|lazy beta; iClearHyp Heq]).
Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
iRewriteCore Right lem in H.
@@ -1895,7 +1879,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
end in
lazymatch goal with
| |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some _ =>
- first [find Γp i|find Γs i]; env_reflexivity
+ first [find Γp i|find Γs i]; pm_reflexivity
end.
(* The argument [select] is the namespace [N] or hypothesis name ["H"] of the
@@ -1929,11 +1913,13 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
let I := match goal with |- ElimInv _ ?I _ _ _ _ _ => I end in
fail "iInv: cannot eliminate invariant " I
|iSolveSideCondition
- |let R := fresh in intros R; eexists; split; [env_reflexivity|];
+ |let R := fresh in intros R; eexists; split; [pm_reflexivity|];
(* Now we are left proving [envs_entails Δ'' R]. *)
iSpecializePat H pats; last (
- iApplyHyp H; clear R; env_cbv;
- (* Now the goal is [∀ x, Pout x -∗ maybe_wand (Pclose x) (Q' x)] *)
+ iApplyHyp H; clear R; pm_reduce;
+ (* Now the goal is
+ [∀ x, Pout x -∗ pm_maybe_wand (pm_option_fun Pclose x) (Q' x)],
+ reduced because we can rely on Pclose being a constructor. *)
let x := fresh in
iIntros (x);
iIntro H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
@@ -2088,7 +2074,7 @@ Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
(** Miscellaneous *)
Tactic Notation "iAccu" :=
- iStartProof; eapply tac_accu; [env_reflexivity || fail "iAccu: not an evar"].
+ iStartProof; eapply tac_accu; [pm_reflexivity || fail "iAccu: not an evar"].
(** Automation *)
Hint Extern 0 (_ ⊢ _) => iStartProof.
@@ -2112,6 +2098,7 @@ Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
rewrite envs_entails_eq; apply big_sepMS_empty'.
+(* These introduce as much as possible at once, for better performance. *)
Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros.
Hint Extern 0 (envs_entails _ (_ → _)) => iIntros.
Hint Extern 0 (envs_entails _ (_ -∗ _)) => iIntros.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 68ac02005f481b7dda6bf611da17874c48434bc1..3dcd333e73d5aee1d08fe0151f4556d6fe0321ba 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -1,6 +1,6 @@
From iris.bi Require Export monpred.
From iris.bi Require Import plainly.
-From iris.proofmode Require Import tactics modality_instances.
+From iris.proofmode Require Import tactics modality_instances coq_tactics.
Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
(P : monPred I PROP) (ð“Ÿ : PROP) :=
@@ -555,12 +555,12 @@ Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
(* This instances are awfully specific, but that's what is needed. *)
Global Instance elim_acc_at_fupd `{BiFUpd PROP} {X : Type} E1 E2 E
- M1 M2 α β mγ Q (Q' : X → monPred) i :
+ M1 M2 α β (mγ : X → option PROP) Q (Q' : X → monPred) i :
ElimAcc (X:=X) M1 M2 α β mγ (|={E1,E}=> Q i)
- (λ x, |={E2}=> β x ∗ (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q' x i)))%I →
+ (λ x, |={E2}=> β x ∗ (pm_maybe_wand (mγ x) (|={E1,E}=> Q' x i)))%I →
ElimAcc (X:=X) M1 M2 α β mγ ((|={E1,E}=> Q) i)
(λ x, (|={E2}=> ⎡β x⎤ ∗
- (coq_tactics.maybe_wand
+ (pm_maybe_wand
(match mγ x with Some ð“Ÿ => Some ⎡ð“ŸâŽ¤ | None => None end)
(|={E1,E}=> Q' x))) i)%I
| 1.
@@ -575,10 +575,10 @@ fails. *)
Global Instance elim_acc_at_fupd_unit `{BiFUpd PROP} E1 E2 E
M1 M2 α β mγ Q Q' i :
ElimAcc (X:=unit) M1 M2 α β mγ (|={E1,E}=> Q i)
- (λ x, |={E2}=> β x ∗ (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q' i)))%I →
+ (λ x, |={E2}=> β x ∗ (pm_maybe_wand (mγ x) (|={E1,E}=> Q' i)))%I →
ElimAcc (X:=unit) M1 M2 α β mγ ((|={E1,E}=> Q) i)
(λ x, (|={E2}=> ⎡β x⎤ ∗
- (coq_tactics.maybe_wand
+ (pm_maybe_wand
(match mγ x with Some ð“Ÿ => Some ⎡ð“ŸâŽ¤ | None => None end)
(|={E1,E}=> Q'))) i)%I
| 0.
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
new file mode 100644
index 0000000000000000000000000000000000000000..2133bd59368dc98e5f946cce26c16c417a47ed04
--- /dev/null
+++ b/theories/proofmode/reduction.v
@@ -0,0 +1,24 @@
+From iris.bi Require Import bi.
+From iris.proofmode Require Import base environments.
+
+Declare Reduction pm_cbv := cbv [
+ (* base *)
+ pm_option_bind pm_from_option pm_option_fun
+ base.beq base.ascii_beq base.string_beq base.positive_beq base.ident_beq
+ (* environments *)
+ env_lookup env_lookup_delete env_delete env_app env_replace
+ env_dom env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
+ envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
+ envs_simple_replace envs_replace envs_split
+ envs_clear_spatial envs_clear_persistent envs_incr_counter
+ envs_split_go envs_split prop_of_env
+ (* other modules. TODO: we should probably make copies of these,
+ but what will that break? *)
+ Pos.succ
+].
+Ltac pm_eval t :=
+ let u := eval pm_cbv in t in
+ u.
+Ltac pm_reduce :=
+ match goal with |- ?u => let v := pm_eval u in change v end.
+Ltac pm_reflexivity := pm_reduce; exact eq_refl.