Commit 272f29d3 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/rec' into 'master'

add wp proof rule for recursive functions

See merge request !425
parents 64bed0ca 71be71b2
...@@ -213,12 +213,26 @@ Proof. solve_pure_exec. Qed. ...@@ -213,12 +213,26 @@ Proof. solve_pure_exec. Qed.
Section lifting. Section lifting.
Context `{!heapG Σ}. Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ. Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ. Implicit Types Φ Ψ : val iProp Σ.
Implicit Types efs : list expr. Implicit Types efs : list expr.
Implicit Types σ : state. Implicit Types σ : state.
Implicit Types v : val. Implicit Types v : val.
Implicit Types l : loc. Implicit Types l : loc.
(** Recursive functions: we do not use this lemmas as it is easier to use Löb
induction directly, but this demonstrates that we can state the expected
reasoning principle for recursive functions, without any visible ▷. *)
Lemma wp_rec_löb s E f x e Φ Ψ :
(( v, Ψ v - WP (rec: f x := e)%V v @ s; E {{ Φ }}) -
v, Ψ v - WP (subst' x v (subst' f (rec: f x := e) e)) @ s; E {{ Φ }}) -
v, Ψ v - WP (rec: f x := e)%V v @ s; E {{ Φ }}.
Proof.
iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ".
iApply lifting.wp_pure_step_later; first done.
iNext. iApply ("Hrec" with "[] HΨ"). iIntros (w) "HΨ".
iApply ("IH" with "HΨ").
Qed.
(** Fork: Not using Texan triples to avoid some unnecessary [True] *) (** Fork: Not using Texan triples to avoid some unnecessary [True] *)
Lemma wp_fork s E e Φ : Lemma wp_fork s E e Φ :
WP e @ s; {{ _, True }} - Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}. WP e @ s; {{ _, True }} - Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
......
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