Skip to content

Instantly share code, notes, and snippets.

@paldepind
Created September 2, 2022 08:49
Show Gist options
  • Save paldepind/c8ed98ddbced93c93a7d76f6bb76e3c4 to your computer and use it in GitHub Desktop.
Save paldepind/c8ed98ddbced93c93a7d76f6bb76e3c4 to your computer and use it in GitHub Desktop.
From iris.bi Require Import bi.
Import bi.
From iris.proofmode Require Import tactics environments intro_patterns monpred.
Section intuit_to_spatial.
Context {PROP : bi}.
Implicit Types Γ Γp Γs : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
Lemma envs_clear_intuitionistic_sound Δ :
of_envs Δ ⊢
env_and_persistently (env_intuitionistic Δ) ∗ of_envs (envs_clear_intuitionistic Δ).
Proof.
rewrite !of_envs_eq /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
rewrite persistent_and_sep_1.
rewrite (pure_True); first by rewrite !left_id.
destruct Hwf. constructor; simpl; auto using Enil_wf.
Qed.
Lemma big_opL_and_sep (l : env PROP) : □ [∧] l -∗ [∗] l.
Proof.
iInduction (l) as [|??] "IH"; simpl; first done.
iIntros "#[$ ?]". iApply "IH". done.
Qed.
Lemma big_opL_env_and_sep `{BiAffine PROP} (l : env PROP) : env_and_persistently l -∗ [∗] l.
Proof.
iInduction (l) as [|??] "IH"; simpl; first done.
iIntros "[#$ ?]". iApply "IH". done.
Qed.
Definition envs_intuitionistic_to_spatial {PROP} (Δ : envs PROP) : option (envs PROP) :=
envs_app false (env_intuitionistic Δ) (envs_clear_intuitionistic Δ).
Lemma envs_intuitionistic_to_spatial_sound `{BiAffine PROP} Δ Δ' P :
envs_intuitionistic_to_spatial Δ = Some Δ' →
envs_entails Δ' P →
envs_entails Δ P.
Proof.
rewrite /envs_intuitionistic_to_spatial.
intros eq.
rewrite envs_entails_unseal.
intros <-.
apply envs_app_sound in eq.
apply wand_elim_l' in eq.
rewrite <- eq.
rewrite envs_clear_intuitionistic_sound.
iIntros "[? $]".
rewrite -big_opL_env_and_sep.
done.
Qed.
End intuit_to_spatial.
(* Moves the intuitionistic context to the spatial context. *)
Tactic Notation "iIntuitToSpatial" :=
eapply envs_intuitionistic_to_spatial_sound;
[ done
| cbv [ env_spatial ]].
Tactic Notation "iCrashIntro" := iIntuitToSpatial; iModIntro.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment