From 8fab551a797f2653b0536f6a357264899e09596f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 Nov 2020 13:24:12 +0100
Subject: [PATCH] Fix compilation with Coq 8.10 (lia is weaker).
---
theories/heap_lang/lib/array.v | 18 ++++++++++--------
1 file changed, 10 insertions(+), 8 deletions(-)
diff --git a/theories/heap_lang/lib/array.v b/theories/heap_lang/lib/array.v
index 585b0ca72..f7e2bd7bd 100644
--- a/theories/heap_lang/lib/array.v
+++ b/theories/heap_lang/lib/array.v
@@ -195,11 +195,12 @@ Section proof.
}}}.
Proof.
iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
- wp_apply (wp_array_init_loop _ _ _ 0 n (Z.to_nat n)
- with "[Hl $Hf] [HΦ]"); first lia.
+ wp_apply (wp_array_init_loop _ _ _ 0 n (Z.to_nat n) with "[Hl $Hf] [HΦ]").
+ { by rewrite /= Z2Nat.id; last lia. }
{ by rewrite loc_add_0. }
- iIntros "!>" (vs). iDestruct 1 as (?) "[Hl Hvs]". wp_pures.
- iApply ("HΦ" $! _ vs). iSplit; [iPureIntro; lia|].
+ iIntros "!>" (vs). iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
+ iApply ("HΦ" $! _ vs). iSplit.
+ { iPureIntro. by rewrite Hlen Z2Nat.id; last lia. }
rewrite loc_add_0. iFrame.
Qed.
Lemma twp_array_init stk E n f :
@@ -213,11 +214,12 @@ Section proof.
}]].
Proof.
iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
- wp_apply (twp_array_init_loop _ _ _ 0 n (Z.to_nat n)
- with "[Hl $Hf] [HΦ]"); first lia.
+ wp_apply (twp_array_init_loop _ _ _ 0 n (Z.to_nat n) with "[Hl $Hf] [HΦ]").
+ { by rewrite /= Z2Nat.id; last lia. }
{ by rewrite loc_add_0. }
- iIntros (vs). iDestruct 1 as (?) "[Hl Hvs]". wp_pures.
- iApply ("HΦ" $! _ vs). iSplit; [iPureIntro; lia|].
+ iIntros (vs). iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
+ iApply ("HΦ" $! _ vs). iSplit.
+ { iPureIntro. by rewrite Hlen Z2Nat.id; last lia. }
rewrite loc_add_0. iFrame.
Qed.
End array_init.
--
GitLab