Commit 66710e16 authored by Dan Frumin's avatar Dan Frumin

Simplify the factorial proof a bit

parent 90285dac
......@@ -71,8 +71,8 @@ Section proofs.
AsVal e1 ->
AsVal e2 ->
awp e R Ψ -
( v, Ψ v - (v = #true awp (e1 #()) R Φ)
(v = #false awp (e2 #()) R Φ)) -
( v, Ψ 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 HΦ".
......
......@@ -34,9 +34,8 @@ Section factorial_spec.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma incr_spec (l : loc) (n : Z) R Φ :
l U #n - (l L #(n+1) - Φ #(n+1)) -
l U #n - (l L #(n+1) - Φ #(n+1)) -
awp (incr #l) R Φ.
Proof.
iIntros "Hl HΦ".
awp_lam.
......@@ -54,28 +53,29 @@ Section factorial_spec.
iExists _; iFrame.
Qed.
Lemma factorial_body_spec (n: nat) (c r: loc) R :
k: nat, (k <= n c U #k r U #(fact k)) -
awp (factorial_body #n #c #r) R
(λ _, c U #n r U #(fact n))%I.
Lemma factorial_body_spec (n k : nat) (c r: loc) R :
(k <= n c U #k r U #(fact k)) -
awp (factorial_body #n #c #r) R
(λ _, c U #n r U #(fact n))%I.
Proof.
iIntros (k) "(Hk & Hc & Hr)". do 3 awp_lam.
iIntros "(Hk & Hc & Hr)". do 3 awp_lam.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec. iNext.
iAssert (k < n k = n)%I with "[Hk]" as "Hk".
{ iRevert "Hk"; iIntros "%"; iPureIntro; by lia. }
iDestruct "Hk" as "[Hk | Hk]".
- iApply (a_if_spec _ _
((λ v, (v = #true k < n c U #k))%I) with "[Hk Hc]").
+ iApply (a_bin_op_spec _ _
(λ v, v = #k c U #k )%I (λ v, v = #n)%I with "[Hc] [] [Hk]").
* iApply (a_load_spec _ _ (λ v, v = c)%I).
** iApply awp_ret. wp_value_head. eauto.
** iIntros (l) "%"; subst. iExists #k. iFrame. eauto.
* iApply awp_ret. by wp_value_head.
* iIntros (? ?) "(% & Hc) %"; subst. iExists #true.
iFrame "Hc". admit.
+ iIntros (v) "(% & % & Hc)"; subst.
iLeft. iSplit; first by eauto.
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.
......@@ -90,30 +90,23 @@ Section factorial_spec.
(λ 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 (l1) "%"; subst. iExists #(fact k). iFrame. eauto.
* iIntros (? ->). iExists #(fact k). iFrame. eauto.
+ iApply (a_load_spec _ _ (λ v, v = c)%I).
* iApply awp_ret. wp_value_head. eauto.
* iIntros (l1) "%"; subst. iExists #(k+1). iFrame. eauto.
* iIntros (? ->). iExists #(k+1). iFrame. eauto.
+ iIntros (? ?) "(% & Hc) (% & Hr)"; subst.
iExists #(fact (k+1)). iFrame. iSplit; last by auto. admit. }
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)) by lia. rewrite- H3; clear H3.
assert ( Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iApply ("IH" with "[] [$Hc] [$Hr]"). iPureIntro. lia.
- iApply (a_if_spec _ _
((λ v, (v = #false k = n c U #k))%I) with "[Hk Hc]").
iApply (a_bin_op_spec _ _
(λ v, v = #k c U #k )%I (λ v, v = #n)%I with "[Hc] [] [Hk]").
* iApply (a_load_spec _ _ (λ v, v = c)%I).
** iApply awp_ret. wp_value_head. eauto.
** iIntros (l) "%"; subst. iExists #k. iFrame. eauto.
* iApply awp_ret. by wp_value_head.
* iIntros (? ?) "(% & Hc) %"; subst. iExists #false.
iFrame "Hc". admit.
* iIntros (v) "(% & % & Hc)"; subst.
iRight. iSplit; first by eauto.
iApply a_seq_spec. iModIntro. by iFrame.
Admitted.
- iRight. iSplit; eauto.
iApply a_seq_spec. iModIntro. by iFrame.
Qed.
Lemma factorial_spec (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
......@@ -125,8 +118,8 @@ Section factorial_spec.
{ iApply awp_ret. by iApply wp_value. }
iIntros (? c ->) "Hc". awp_lam.
iApply a_sequence_spec.
iApply ((awp_wand _ (λ _, c U #n r U #(fact n))%I) with "[Hr Hc]").
- iApply (factorial_body_spec n c r R 0). iFrame. iPureIntro. lia.
iApply (awp_wand _ (λ _, c U #n r U #(fact n))%I with "[Hr Hc]").
- iApply (factorial_body_spec n 0 c r R). iFrame. iPureIntro. lia.
- iIntros (?) "[Hc Hr]". iModIntro. awp_seq.
iApply (a_load_spec _ _ (λ v, v = r)%I).
+ iApply awp_ret. iApply wp_value; eauto.
......
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