Commit 73e86fad authored by Lennard Gäher's avatar Lennard Gäher
Browse files

move rule

parent 99126c39
......@@ -101,15 +101,6 @@ Proof.
- eauto.
Qed.
Lemma hoare_value' P v :
{{ P }} v {{ w, P w = v}}.
Proof.
eapply hoare_con; last apply hoare_value with (Φ := (λ v', P v' = v)%I).
- etrans; first apply ent_sep_true. rewrite ent_sep_comm. apply ent_sep_split; first done.
by apply ent_prove_pure.
- done.
Qed.
Lemma hoare_rec P Φ f x e v:
({{ P }} subst' x v (subst' f (rec: f x := e) e) {{Φ}})
{{ P }} (rec: f x := e)%V v {{Φ}}.
......@@ -419,6 +410,15 @@ Check ent_sep_assoc.
Check ent_pointsto_sep.
Check ent_exists_sep.
Lemma hoare_value' P v :
{{ P }} v {{ w, P w = v}}.
Proof.
eapply hoare_con; last apply hoare_value with (Φ := (λ v', P v' = v)%I).
- etrans; first apply ent_sep_true. rewrite ent_sep_comm. apply ent_sep_split; first done.
by apply ent_prove_pure.
- done.
Qed.
(** Note: the separating conjunction can be typed with `\sep` *)
......
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