Commit fa9bc158 authored by Dan Frumin's avatar Dan Frumin
Browse files

Make parfib.v compile with the latest Iris version

parent d086103b
...@@ -40,17 +40,19 @@ Section contents. ...@@ -40,17 +40,19 @@ Section contents.
Proof. Proof.
iIntros (Φ) "_ HΦ". iIntros (Φ) "_ HΦ".
iLöb as "IH" forall (n Φ). rewrite /seqFib. iLöb as "IH" forall (n Φ). rewrite /seqFib.
wp_rec. wp_op. case_bool_decide; wp_if. wp_rec. wp_op. case_bool_decide; simplify_eq; wp_if.
{ assert (n = O) as -> by lia. { assert (n = O) as -> by lia.
assert (1 = S O) as -> by lia. assert (1 = S O) as -> by lia.
by iApply "HΦ". } by iApply "HΦ". }
wp_op. case_bool_decide; wp_if. wp_op. case_bool_decide; simplify_eq; wp_if.
{ assert (n = S O) as -> by lia. { assert (n = S O) as -> by lia.
assert (1 = S O) as -> by lia. assert (1 = S O) as -> by lia.
by iApply "HΦ". } by iApply "HΦ". }
wp_op. wp_bind ((rec: "fib" "a" := _)%V #(n - 1)). wp_op. wp_bind ((rec: "fib" "a" := _)%V #(n - 1)).
assert ( m, n = S (S m)) as [m ->]. assert ( m, n = S (S m)) as [m ->].
{ exists (n - (S (S O)))%nat. lia. } { assert (n O) by naive_solver.
assert (n S O) by naive_solver.
exists (n - (S (S O)))%nat. lia. }
assert ((S (S m) - 1) = S m) as -> by lia. assert ((S (S m) - 1) = S m) as -> by lia.
iApply "IH". iNext. iIntros (? <-). iApply "IH". iNext. iIntros (? <-).
assert (Z.of_nat (S (S m)) = m + 2) as -> by lia. assert (Z.of_nat (S (S m)) = m + 2) as -> by lia.
......
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