Commit 8a6c5109 authored by Dan Frumin's avatar Dan Frumin

Fix lemmas for functions with one argument

parent 92085d3a
......@@ -66,39 +66,35 @@ Section proofs.
iApply "H".
Qed.
Lemma a_if_spec R Φ Ψ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
Lemma a_if_spec R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
AsVal e1 ->
AsVal e2 ->
awp e R Ψ -
( v, Ψ v - (v = #true awp (e1 #()) R Φ)
awp e R (λ v, (v = #true awp (e1 #()) R Φ)
(v = #false awp (e2 #()) R Φ)) -
awp (a_if e e1 e2) R Φ.
Proof.
iIntros ([v1 <-%of_to_val] [v2 <-%of_to_val]) "H".
iIntros ([v1 <-%of_to_val] [v2 <-%of_to_val]) "H".
awp_apply (a_wp_awp with "H"). iIntros (v) "H". do 3 awp_lam.
iApply awp_bind. iApply (awp_wand with "H"). clear v.
iIntros (v) "HΨ". awp_lam.
iDestruct ("HΦ" with "HΨ") as "[[% H] | [% H]]";
simplify_eq/=; by (awp_pure _).
iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if.
Qed.
Lemma a_if_true_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ :
awp e1 R Φ - awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof.
iIntros "HΦ".
iApply (a_if_spec _ _ (λ v, v = #true)%I).
{ iApply awp_ret. iApply wp_value. eauto. }
iIntros (? ->). iLeft. iSplit; eauto. by awp_seq.
iApply a_if_spec.
iApply awp_ret. iApply wp_value.
iLeft. iSplit; eauto. by awp_seq.
Qed.
Lemma a_if_false_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ :
awp e2 R Φ - awp (a_if (a_ret #false) (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof.
iIntros "HΦ".
iApply (a_if_spec _ _ (λ v, v = #false)%I).
{ iApply awp_ret. iApply wp_value. eauto. }
iIntros (? ->). iRight. iSplit; eauto. by awp_seq.
iApply a_if_spec.
iApply awp_ret. iApply wp_value.
iRight. iSplit; eauto. by awp_seq.
Qed.
Lemma a_seq_spec R Φ :
......@@ -145,23 +141,21 @@ Section proofs.
iModIntro. by awp_lam.
Qed.
Lemma a_load_spec R Φ Ψ e :
awp e R (λ v, l : loc, v = #l Ψ l) -
( l : loc, Ψ l - v, l U v (l U v - Φ v)) -
Lemma a_load_spec R Φ e :
awp e R (λ v, (l : loc) (w : val), v = #l l U w (l U w - Φ w)) -
awp (a_load e) R Φ.
Proof.
iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
iApply awp_bind.
iApply (awp_wand with "H"). clear v.
iIntros (v). iDestruct 1 as (l ->) "HΨ".
iIntros (v). iDestruct 1 as (l w) "(% & Hl & HΦ)". subst.
awp_lam.
iDestruct ("HΦ" with "HΨ") as (v) "[Hv HΦ]".
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
iDestruct (locked_locs_unlocked with "Hv Hσ") as %Hl.
iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hl.
assert (#l X).
{ unfold correct_locks in *. intros Hx. apply Hl.
destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
......@@ -170,22 +164,21 @@ Section proofs.
wp_apply (mset_member_spec #l env with "HX").
iIntros "Henv /=". case_decide; first by exfalso. simpl.
wp_op. iSplit; eauto. iNext. wp_seq.
rewrite mapsto_eq /mapsto_def. iDestruct "Hv" as "[Hv Hl]". wp_load.
rewrite mapsto_eq /mapsto_def. iDestruct "Hl" as "[Hv Hl]". wp_load.
iCombine "Hv Hl" as "Hv". iFrame "HR".
iSplitR "HΦ Hv".
- iExists X,σ. by iFrame.
- by iApply "HΦ".
Qed.
Lemma a_alloc_spec R Φ Ψ e :
awp e R Ψ -
( v l, Ψ v - l U v - Φ #l) -
Lemma a_alloc_spec R Φ e :
awp e R (λ v, l, l U v - Φ #l) -
awp (a_alloc e) R Φ.
Proof.
iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
iApply awp_bind.
iApply (awp_wand with "H"). clear v.
iIntros (v) "HΨ". awp_lam.
iIntros (v) "H". awp_lam.
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
......@@ -200,18 +193,18 @@ Section proofs.
by iDestruct (mapsto_valid_2 l with "Hl Hl'") as %[]. }
iDestruct "Hl" as "[Hl Hl']".
iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto.
iModIntro. iFrame "HR". iSplitR "HΦ HΨ Hl'".
iModIntro. iFrame "HR". iSplitR "H Hl'".
- iExists X,(<[l:=ULvl]>σ). iFrame. iSplit.
+ rewrite bi.big_sepM_insert; eauto. iFrame. eauto.
+ iPureIntro. by rewrite locked_locs_alloc_unlocked.
- iApply ("HΦ" with "HΨ Hl'").
- iApply ("H" with "Hl'").
Qed.
Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) :
awp e1 R Ψ1 - awp e2 R Ψ2 -
( v1 v2, Ψ1 v1 - Ψ2 v2 -
( v1 v2, Ψ1 v1 - Ψ2 v2 -
w, bin_op_eval op v1 v2 = Some w Φ w)-
awp (a_bin_op op e1 e2) R Φ.
awp (a_bin_op op e1 e2) R Φ.
Proof.
iIntros "H1 H2 HΦ".
awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam.
......
......@@ -44,9 +44,9 @@ Section factorial_spec.
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_bin_op_spec _ _
(λ v, v = #n l U #n )%I (λ v, v = #1)%I with "[-]").
+ iApply (a_load_spec _ _ (λ v, v = l)%I).
* iApply awp_ret. wp_value_head. eauto.
* iIntros (l1) "%"; subst. iExists #n. iFrame. eauto.
+ iApply a_load_spec.
iApply awp_ret. wp_value_head.
iExists _,_; iFrame; eauto.
+ iApply awp_ret. by wp_value_head.
+ iIntros (? ?) "(% & Hc) %"; subst. iExists #(n+1). by iFrame. }
iIntros (? ? ->) "[% Hl1]"; subst.
......@@ -61,51 +61,48 @@ Section factorial_spec.
iIntros "(Hk & Hc & Hr)". do 3 awp_lam.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec. iNext.
iDestruct "Hk" as %Hk.
iApply (a_if_spec _ _
(λ v, (v = #true k < n c U #k)
(v = #false k = n c U #n))%I with "[Hc]").
{ iApply (a_bin_op_spec _ _
(λ v, v = #k c U #k )%I (λ v, v = #n)%I with "[Hc]").
- iApply (a_load_spec _ _ (λ l, l = c)%I with "[] [Hc]").
+ iApply awp_ret. wp_value_head. eauto.
+ iIntros (? ->). iExists _. iFrame. eauto.
- iApply awp_ret. wp_value_head. eauto.
- iIntros (v v2) "[% Hc] %". simplify_eq/=.
rewrite /bin_op_eval /=. iExists _; iSplit; eauto.
case_bool_decide; [iLeft | iRight]; eauto.
assert (k = n) as -> by omega. eauto. }
iIntros (v) "[(% & % & Hc)|(% & % & Hc)]"; simplify_eq/=.
- iLeft. iSplit; eauto.
do 2 (awp_seq; iApply a_sequence_spec).
iApply (incr_spec with "[$Hc]").
iIntros "Hc". iModIntro. awp_seq.
iApply (a_store_spec _ _
(λ l, l = r)%I
(λ v, v = #(fact (k+1))
iApply a_if_spec.
iApply (a_bin_op_spec _ _
(λ v, v = #k c U #k )%I (λ v, v = #n)%I with "[Hc]").
- iApply a_load_spec. iApply awp_ret. wp_value_head.
iExists _,_; iFrame. eauto.
- iApply awp_ret. by wp_value_head.
- iIntros (v1 v2) "[% Hc] %"; subst.
rewrite /bin_op_eval /=. iExists _; iSplit; eauto.
case_bool_decide.
+ iLeft. iSplit; eauto.
do 2 (awp_seq; iApply a_sequence_spec).
iApply (incr_spec with "[$Hc]").
iIntros "Hc". iModIntro. awp_seq.
iApply (a_store_spec _ _
(λ l, l = r)%I
(λ v, v = #(fact (k+1))
c U #(k + 1)
r U #(fact k))%I with "[] [Hr Hc]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_bin_op_spec _ _
(λ v, v = #(fact k) r U #(fact k))%I
(λ v, v = #(k + 1) c U #(k+1))%I with "[Hr] [Hc]").
+ iApply (a_load_spec _ _ (λ v, v = r)%I).
* iApply awp_ret. wp_value_head. eauto.
* iIntros (? ->). iExists #(fact k). iFrame. eauto.
+ iApply (a_load_spec _ _ (λ v, v = c)%I).
* iApply awp_ret. wp_value_head. eauto.
* iIntros (? ->). iExists #(k+1). iFrame. eauto.
+ iIntros (? ?) "(% & Hc) (% & Hr)"; subst.
iExists #(fact (k+1)). iFrame. iSplit; last by auto.
rewrite /bin_op_eval /=.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. }
done. }
iIntros (? ? ->) "[% (Hc & Hr)]"; subst. iExists (#(fact k)); iFrame.
iIntros "Hr". iModIntro. awp_seq.
assert ( Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iApply ("IH" with "[] [$Hc] [$Hr]"). iPureIntro. lia.
- iRight. iSplit; eauto.
iApply a_seq_spec. iModIntro. by iFrame.
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_bin_op_spec _ _
(λ v, v = #(fact k) r U #(fact k))%I
(λ v, v = #(k + 1) c U #(k+1))%I with "[Hr] [Hc]").
* iApply a_load_spec.
iApply awp_ret. wp_value_head.
iExists _, _; iFrame. eauto.
* iApply a_load_spec.
iApply awp_ret. wp_value_head.
iExists _, _; iFrame. eauto.
* iIntros (? ?) "[% Hr] [% Hc]". simplify_eq.
rewrite /bin_op_eval /=.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. }
iExists #(fact (k+1)); repeat (iSplit; eauto).
by iFrame. }
iIntros (? ? ->) "(% & Hc & Hr)"; simplify_eq.
iExists _; iFrame. iIntros "Hr".
iModIntro. awp_seq.
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iApply ("IH" $! n (k+1)%nat with "[] Hc Hr"). iPureIntro. lia.
+ iRight. iSplit; eauto.
iApply a_seq_spec. iModIntro.
assert (k = n) as -> by lia. by iFrame.
Qed.
Lemma factorial_spec (n: nat) R :
......
......@@ -17,9 +17,9 @@ Section test.
iApply a_seq_spec.
iModIntro.
awp_lam.
iApply (a_load_spec _ _ (λ v, v = l)%I).
{ iApply awp_ret. iApply wp_value; eauto. }
iIntros (? ->). iExists #1. iFrame. eauto.
iApply a_load_spec.
iApply awp_ret. iApply wp_value; eauto.
iExists l, #1. iFrame. eauto.
Qed.
......@@ -54,17 +54,17 @@ Section test.
iIntros "Hl1 Hl2".
do 2 awp_lam.
iApply awp_bind.
iApply (a_alloc_spec _ _ (λ v, v = #0)%I).
{ iApply awp_ret. by iApply wp_value. }
iIntros (? r ->) "Hr". awp_lam.
iApply a_alloc_spec.
iApply awp_ret. iApply wp_value.
iIntros (r) "Hr". awp_lam.
iApply a_sequence_spec.
iApply (a_store_spec _ _ (λ l, l = r)%I
(λ v, v = v1 l1 U v1)%I with "[] [Hl1]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = l1)%I).
- iApply awp_ret. iApply wp_value; eauto.
- iIntros (? ->). iExists _; iFrame. eauto. }
{ iApply a_load_spec.
iApply awp_ret. iApply wp_value.
iExists _, _; iFrame. eauto. }
iIntros (? ? ->) "[% Hl1]"; subst.
iExists _; iFrame. iIntros "Hr". iModIntro.
awp_seq.
......@@ -73,9 +73,9 @@ Section test.
iApply (a_store_spec _ _ (λ l, l = l1)%I
(λ v, v = v2 l2 U v2)%I with "[] [Hl2]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = l2)%I).
- iApply awp_ret. iApply wp_value; eauto.
- iIntros (? ->). iExists _; iFrame. eauto. }
{ iApply a_load_spec.
iApply awp_ret. iApply wp_value.
iExists _, _; iFrame. eauto. }
iIntros (? ? ->) "[% Hl2]"; subst.
iExists _; iFrame. iIntros "Hl1". iModIntro.
awp_seq.
......@@ -84,9 +84,9 @@ Section test.
iApply (a_store_spec _ _ (λ l, l = l2)%I
(λ v, v = v1 r U v1)%I with "[] [Hr]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = r)%I).
- iApply awp_ret. iApply wp_value; eauto.
- iIntros (? ->). iExists _; iFrame. eauto. }
{ iApply a_load_spec.
iApply awp_ret. iApply wp_value.
iExists _, _; iFrame. eauto. }
iIntros (? ? ->) "[% Hr]"; subst.
iExists _; iFrame. iIntros "Hl2".
......
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