Commit c25f4d65 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename `prop_of_env` → `env_to_prop`

All the `env` operations are prefixed `env_`, so this is more consistent.
parent 6b0f250f
......@@ -431,12 +431,12 @@ Section proof_mode.
Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
Timeless (PROP:=PROP) emp
TCForall Laterable (env_to_list Γs)
P = prop_of_env Γs
P = env_to_prop Γs
envs_entails (Envs Γp Γs n) (atomic_acc Eo Ei α P β Φ)
envs_entails (Envs Γp Γs n) (atomic_update Eo Ei α β Φ).
Proof.
intros ? HΓs ->. rewrite envs_entails_eq of_envs_eq' /atomic_acc /=.
setoid_rewrite prop_of_env_sound =>HAU.
setoid_rewrite env_to_prop_sound =>HAU.
apply aupd_intro; [apply _..|]. done.
Qed.
End proof_mode.
......
......@@ -601,11 +601,11 @@ Qed.
(** * Accumulate hypotheses *)
Lemma tac_accu Δ P :
prop_of_env (env_spatial Δ) = P
env_to_prop (env_spatial Δ) = P
envs_entails Δ P.
Proof.
rewrite envs_entails_eq=><-.
rewrite prop_of_env_sound /of_envs and_elim_r sep_elim_r //.
rewrite env_to_prop_sound /of_envs and_elim_r sep_elim_r //.
Qed.
(** * Fresh *)
......
......@@ -335,7 +335,7 @@ Definition envs_split {PROP} (d : direction)
''(Δ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 :=
Definition env_to_prop {PROP : bi} (Γ : env PROP) : PROP :=
let fix aux Γ acc :=
match Γ with Enil => acc | Esnoc Γ _ P => aux Γ (P acc)%I end
in
......@@ -659,7 +659,7 @@ Proof.
destruct d; simplify_eq/=; solve_sep_entails.
Qed.
Lemma prop_of_env_sound Γ : prop_of_env Γ [] Γ.
Lemma env_to_prop_sound Γ : env_to_prop Γ [] Γ.
Proof.
destruct Γ as [|Γ ? P]; simpl; first done.
revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
......
......@@ -13,7 +13,7 @@ Declare Reduction pm_eval := cbv [
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
envs_split_go envs_split env_to_prop
(* PM option combinators *)
pm_option_bind pm_from_option pm_option_fun
].
......
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