Commit bfdeefd3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make statements of split lemmas nicer.

parent ccf74b05
...@@ -122,14 +122,14 @@ Module uPred_reflection. Section uPred_reflection. ...@@ -122,14 +122,14 @@ Module uPred_reflection. Section uPred_reflection.
Qed. Qed.
Lemma split_l Σ e l k : Lemma split_l Σ e l k :
remove_all l (flatten e) = Some k remove_all l (flatten e) = Some k
eval Σ e eval Σ (ESep (to_expr l) (to_expr k)). eval Σ e (eval Σ (to_expr l) eval Σ (to_expr k))%I.
Proof. Proof.
intros He%remove_all_permutation. intros He%remove_all_permutation.
by rewrite eval_flatten He fmap_app big_sep_app /= !eval_to_expr. by rewrite eval_flatten He fmap_app big_sep_app !eval_to_expr.
Qed. Qed.
Lemma split_r Σ e l k : Lemma split_r Σ e l k :
remove_all l (flatten e) = Some k remove_all l (flatten e) = Some k
eval Σ e eval Σ (ESep (to_expr k) (to_expr l)). eval Σ e (eval Σ (to_expr k) eval Σ (to_expr l))%I.
Proof. intros. rewrite /= comm. by apply split_l. Qed. Proof. intros. rewrite /= comm. by apply split_l. Qed.
Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}. Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
......
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