Commit e896ce1a authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Jacques-Henri Jourdan
Browse files

Make iEmpIntro succeed in a non-empty, but affine, spatial context.

parent 13dc3369
...@@ -435,13 +435,6 @@ Proof. ...@@ -435,13 +435,6 @@ Proof.
Qed. Qed.
(** * Basic rules *) (** * Basic rules *)
Lemma tac_emp_intro Δ :
env_spatial_is_nil Δ = true
Δ emp.
Proof.
intros. by rewrite (env_spatial_is_nil_bare_persistently Δ) // (affine ( Δ)).
Qed.
Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ. Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
Global Instance affine_env_nil : AffineEnv Enil. Global Instance affine_env_nil : AffineEnv Enil.
Proof. constructor. Qed. Proof. constructor. Qed.
...@@ -453,6 +446,14 @@ Instance affine_env_spatial Δ : ...@@ -453,6 +446,14 @@ Instance affine_env_spatial Δ :
TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ)) Affine ([] env_spatial Δ). TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ)) Affine ([] env_spatial Δ).
Proof. destruct 1 as [?|H]. apply _. induction H; simpl; apply _. Qed. Proof. destruct 1 as [?|H]. apply _. induction H; simpl; apply _. Qed.
Lemma tac_emp_intro Δ :
(* Establishing [AffineEnv (env_spatial Δ)] is rather expensive (linear in the
size of the context), so first check whether the whole BI is affine (which
takes constant time). *)
TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ))
Δ emp.
Proof. intros [?|?]; by rewrite (affine Δ). Qed.
Lemma tac_assumption Δ Δ' i p P Q : Lemma tac_assumption Δ Δ' i p P Q :
envs_lookup_delete i Δ = Some (p,P,Δ') envs_lookup_delete i Δ = Some (p,P,Δ')
FromAssumption p P Q FromAssumption p P Q
......
...@@ -202,7 +202,8 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) := ...@@ -202,7 +202,8 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
Tactic Notation "iEmpIntro" := Tactic Notation "iEmpIntro" :=
iStartProof; iStartProof;
eapply tac_emp_intro; eapply tac_emp_intro;
[env_reflexivity || fail "iEmpIntro: spatial context is non-empty"]. [env_cbv; apply _ ||
fail "iEmpIntro: spatial context contains non-affine hypotheses"].
Tactic Notation "iPureIntro" := Tactic Notation "iPureIntro" :=
iStartProof; iStartProof;
......
...@@ -91,6 +91,10 @@ Lemma test_iSpecialize_auto_frame P Q R : ...@@ -91,6 +91,10 @@ Lemma test_iSpecialize_auto_frame P Q R :
(P - True - True - Q - R) - P - Q - R. (P - True - True - Q - R) - P - Q - R.
Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed. Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
P - Q R - emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
(* Check coercions *) (* Check coercions *)
Lemma test_iExist_coercion (P : Z PROP) : ( x, P x) - x, P x. Lemma test_iExist_coercion (P : Z PROP) : ( x, P x) - x, P x.
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed. Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). 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