From fa9bc15829163d256d4e5a217aeb26b7a9eb1f4b Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Mon, 30 Apr 2018 11:49:21 +0200 Subject: [PATCH] Make parfib.v compile with the latest Iris version --- theories/hocap/parfib.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/theories/hocap/parfib.v b/theories/hocap/parfib.v index 7788c88..74c4002 100644 --- a/theories/hocap/parfib.v +++ b/theories/hocap/parfib.v @@ -40,17 +40,19 @@ Section contents. Proof. iIntros (Φ) "_ HΦ". 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 (1 = S O) as -> by lia. 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 (1 = S O) as -> by lia. by iApply "HΦ". } wp_op. wp_bind ((rec: "fib" "a" := _)%V #(n - 1)). 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. iApply "IH". iNext. iIntros (? <-). assert (Z.of_nat (S (S m)) = m + 2) as -> by lia. -- GitLab