Commit 7fe2a5e1 authored by Ralf Jung's avatar Ralf Jung
Browse files

document what needs to be in pm_eval

parent 5b54ac28
Pipeline #66090 passed with stage
in 6 minutes and 50 seconds
......@@ -863,14 +863,13 @@ Proof.
- rewrite /= IH (comm _ Q _) assoc. done.
Qed.
Lemma env_to_prop_and_pers_sound Γ :
env_to_prop_and Γ <affine> [] (env_map_pers Γ).
Lemma env_to_prop_and_pers_sound Γ i P :
env_to_prop_and (Esnoc Γ i P) <affine> [] (env_map_pers (Esnoc Γ i P)).
Proof.
destruct Γ as [|Γ i P]; simpl.
{ rewrite /bi_intuitionistically persistent_persistently //. }
revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
- by rewrite right_id.
- rewrite /= IH (comm _ Q _) assoc. f_equiv.
rewrite persistently_and. done.
- rewrite /= IH. clear IH. f_equiv. simpl.
rewrite assoc. f_equiv.
rewrite persistently_and comm. done.
Qed.
End envs.
......@@ -4,7 +4,9 @@ From iris.prelude Require Import options.
(** Called by all tactics to perform computation to lookup items in the
context. We avoid reducing anything user-visible here to make sure we
do not reduce e.g. before unification happens in [iApply].*)
do not reduce e.g. before unification happens in [iApply].
This needs to contain all definitions used in the user-visible statements in
[coq_tactics], and their dependencies. *)
Declare Reduction pm_eval := cbv [
(* base *)
base.negb base.beq
......
Supports Markdown
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