From 775f13011aefbb232ee2f868754b24525227d8df Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 11 Dec 2018 15:05:02 +0100
Subject: [PATCH] bump iris
---
opam | 2 +-
theories/adequacy.v | 9 ++---
theories/bigop.v | 4 +-
theories/examples/abs_hashtable.v | 52 +++++++++++++-------------
theories/examples/circ_buffer.v | 2 +-
theories/examples/hashtable.v | 61 +++++++++++++++----------------
theories/examples/kvnode.v | 34 ++++++++---------
theories/infrastructure.v | 7 +---
theories/lifting.v | 10 ++---
theories/weakestpre.v | 10 ++---
10 files changed, 92 insertions(+), 99 deletions(-)
diff --git a/opam b/opam
index 61cdb5ef..88b82e36 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
depends: [
- "coq-iris" { (= "dev.2018-10-22.2.46e20e91") | (= "dev") }
+ "coq-iris" { (= "dev.2018-12-08.0.5c61abfb") | (= "dev") }
]
diff --git a/theories/adequacy.v b/theories/adequacy.v
index 52954f88..d98eca8d 100644
--- a/theories/adequacy.v
+++ b/theories/adequacy.v
@@ -13,7 +13,7 @@ Class basePreG Σ := BasePreG {
base_preG_info :> inG Σ (authR Infos);
}.
-Definition baseΣ : gFunctors := #[ownPΣ (language.state ra_lang);
+Definition baseΣ : gFunctors := #[ownPΣ (ra_lang);
GFunctor (authR Views);
GFunctor (authR Hists);
GFunctor (authR Infos)].
@@ -269,12 +269,11 @@ Proof.
apply set_unfold_2. move => m. split.
* intuition. rewrite (_ : l = mloc x); last by abstract set_solver+H1.
rewrite (_ : msg_ok _); last (apply Inv; abstract set_solver+H1).
- apply H0. abstract set_solver.
- * intuition. intros ? ?.
- move : H0.
+ apply H3. abstract set_solver.
+ * intuition. intros ? H4. move : H3.
rewrite (_ : l = mloc x); last by abstract set_solver+H1.
rewrite (_ : msg_ok _); last by (apply Inv; abstract set_solver+H1).
- etrans; last apply: H0.
+ etrans; last apply: H3.
case: (total (⊑) (mtime x0) (mtime x)); first auto.
by apply: H2.
+ intros ? ?. apply set_unfold_2. move => [[m [-> /= [FA In]]]].
diff --git a/theories/bigop.v b/theories/bigop.v
index ba58a651..cdbaf6b5 100644
--- a/theories/bigop.v
+++ b/theories/bigop.v
@@ -12,10 +12,10 @@ Proof.
rewrite /= -fmap_seq.
destruct j as [|j].
- by rewrite big_sepL_nil Pos2Qp_1 Qp_mult_1_l bi.sep_emp.
- - rewrite Nat2Pos.inj_succ; last omega.
+ - rewrite Nat2Pos.inj_succ; last lia.
rewrite Pos2Qp_succ Qp_mult_plus_distr_l Qp_mult_1_l.
rewrite fractional bi.sep_comm.
- rewrite big_sepL_fmap IHj; [auto|omega].
+ rewrite big_sepL_fmap IHj; [auto|lia].
Qed.
(* Section BigOp. *)
diff --git a/theories/examples/abs_hashtable.v b/theories/examples/abs_hashtable.v
index 3867a194..c3f55454 100644
--- a/theories/examples/abs_hashtable.v
+++ b/theories/examples/abs_hashtable.v
@@ -49,16 +49,16 @@ Proof.
induction m; simpl; auto; intros.
{ split; intro; inversion H. }
destruct (decide _).
- { subst; split; [omega|].
+ { subst; split; [lia|].
rewrite sublist_nil; split; auto. }
destruct (decide _).
- { subst; split; [omega|].
+ { subst; split; [lia|].
rewrite sublist_nil; split; auto. }
destruct (index_of' m k); simpl.
- destruct IHm as (? & ? & ?).
split; [omega|].
split; auto.
- rewrite sublist_0_cons; last omega; constructor; auto; simpl.
+ rewrite sublist_0_cons; last lia; constructor; auto; simpl.
rewrite Nat.sub_0_r; auto.
- split; intro; inversion H; subst; tauto.
Qed.
@@ -90,8 +90,8 @@ Lemma Forall_sublist_le : forall {A} (P : A -> Prop) i j l d
Proof.
intros.
destruct (decide (j <= i)); auto.
- eapply Forall_nth with (i0 := i) in Hj; [|rewrite length_sublist; omega].
- rewrite nth_sublist in Hj; try omega.
+ eapply Forall_nth with (i0 := i) in Hj; [|rewrite length_sublist; lia].
+ rewrite nth_sublist in Hj; try lia.
rewrite Nat.add_0_r in Hj; done.
Qed.
@@ -118,7 +118,7 @@ Proof.
pose proof (index_of'_spec k m).
destruct (index_of' m k).
- destruct H as (? & Hz & Hnz').
- f_equal; eapply Forall_sublist_first with (d := 0%Z); eauto; omega.
+ f_equal; eapply Forall_sublist_first with (d := 0%Z); eauto; lia.
- destruct H as (Hk' & Hz'); destruct Hk as [Hk | Hk]; [contradiction Hk' | contradiction Hz'];
rewrite <- Hk; apply nth_elem; auto.
Qed.
@@ -127,7 +127,7 @@ Lemma length_rebase : forall {A} (m : list A) i, 0 <= i < length m ->
length (rebase m i) = length m.
Proof.
intros; unfold rebase.
- rewrite app_length !length_sublist; omega.
+ rewrite app_length !length_sublist; lia.
Qed.
Lemma Forall_forall_nth : forall {A} (P : A -> Prop) l d,
@@ -136,7 +136,7 @@ Proof.
split; intros; [apply Forall_nth; auto|].
induction l; auto; simpl in *.
constructor.
- - apply (H 0); omega.
+ - apply (H 0); lia.
- apply IHl; intros.
apply (H (S i)); omega.
Qed.
@@ -152,10 +152,10 @@ Proof.
rewrite nth_sublist; try omega.
rewrite Nat.mod_small; [done | omega].
- rewrite app_nth2; last omega.
- rewrite nth_sublist; try omega.
+ rewrite nth_sublist; try lia.
rewrite Nat.add_0_r H1.
- replace (i + j) with ((i + j - length m) + 1 * length m); last omega.
- rewrite Nat.mod_add; last omega.
+ replace (i + j) with ((i + j - length m) + 1 * length m); last lia.
+ rewrite Nat.mod_add; last lia.
rewrite Nat.mod_small; last omega.
f_equal; omega.
Qed.
@@ -195,7 +195,7 @@ Proof.
unfold sublist; intros.
rewrite minus_plus.
revert dependent l.
- induction i; destruct l; simpl; intros; try omega; auto.
+ induction i; destruct l; simpl; intros; try lia; auto.
apply IHi; omega.
Qed.
@@ -209,7 +209,7 @@ Qed.
Lemma insert_over : forall {A} (l : list A) i x, length l <= i -> <[i:=x]>l = l.
Proof.
induction l; auto; simpl; intros.
- destruct i; first omega; simpl.
+ destruct i; first lia; simpl.
rewrite IHl; auto; omega.
Qed.
@@ -219,7 +219,7 @@ Proof.
induction n; simpl; intros.
{ by rewrite Nat.sub_0_r. }
destruct l; auto.
- destruct i; first omega; simpl.
+ destruct i; first lia; simpl.
apply IHn; omega.
Qed.
@@ -267,26 +267,26 @@ Proof.
- rewrite insert_app_l; last omega.
rewrite Nat.mod_small; last omega.
rewrite sublist_insert_m; try omega.
- rewrite sublist_insert_l; try omega.
+ rewrite sublist_insert_l; try lia.
rewrite Nat.add_sub; done.
- rewrite insert_app_r_alt; last omega.
rewrite Hlen.
replace ((i + j) mod length m) with (i - (length m - j)).
rewrite sublist_insert_r; try omega.
- rewrite sublist_insert_m; try omega.
+ rewrite sublist_insert_m; try lia.
rewrite Nat.sub_0_r; done.
{ rewrite <- (Nat.mod_small (_ - _) (length m)); last omega.
- rewrite <- (Nat.mod_add (_ - _) 1); last omega.
- simpl; f_equal; omega. }
+ rewrite <- (Nat.mod_add (_ - _) 1); last lia.
+ simpl; f_equal; lia. }
Qed.
Corollary rebase_insert' : forall {A} (m : list A) (i j : nat) x, i < length m -> j < length m ->
rebase (<[i:=x]>m) j = <[Z.to_nat ((i - j) mod length m) := x]>(rebase m j).
Proof.
intros; rewrite <- rebase_insert; try done.
- rewrite <- (Nat2Z.id (_ mod _)), mod_Zmod; last omega.
+ rewrite <- (Nat2Z.id (_ mod _)), mod_Zmod; last lia.
rewrite Nat2Z.inj_add Z2Nat.id; last by apply Z_mod_lt; omega.
- rewrite Zplus_mod_idemp_l Z.sub_simpl_r -mod_Zmod; last omega.
+ rewrite Zplus_mod_idemp_l Z.sub_simpl_r -mod_Zmod; last lia.
rewrite Nat2Z.id Nat.mod_small; done.
{ apply Nat2Z.inj_lt.
rewrite Z2Nat.id; apply Z_mod_lt; omega. }
@@ -308,7 +308,7 @@ Qed.
Lemma insert_in : forall {A} (l : list A) i x, i < length l -> x ∈ <[i:=x]>l.
Proof.
- induction l; simpl; intros; first omega.
+ induction l; simpl; intros; first lia.
destruct i; simpl; constructor.
apply IHl; omega.
Qed.
@@ -323,15 +323,15 @@ Proof.
- rewrite insert_length in Hk'.
destruct Hk as (? & Hk & ?), Hk' as (? & Hz & Hall).
destruct (decide (i < n0)).
- { rewrite sublist_insert_m in Hall; try omega.
+ { rewrite sublist_insert_m in Hall; try lia.
eapply Forall_forall in Hall as []; first done.
apply insert_in.
- rewrite length_sublist; omega. }
- rewrite sublist_insert_l in Hall; try omega.
+ rewrite length_sublist; lia. }
+ rewrite sublist_insert_l in Hall; try lia.
rewrite nth_insert in Hz; last done.
- apply f_equal; destruct (decide _); subst; eapply Forall_sublist_first; eauto; simpl; try omega.
+ apply f_equal; destruct (decide _); subst; eapply Forall_sublist_first; eauto; simpl; try lia.
+ destruct Hi as [-> | ->]; tauto.
- + simpl; destruct Hk as [-> | ->]; tauto.
+ + simpl; move : Hk => [-> | ->]; tauto.
+ destruct Hz as [-> | ->]; tauto.
+ destruct Hk as [-> | ->]; tauto.
- destruct Hk' as [Hk']; contradiction Hk'; apply insert_in; done.
diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index 7eb1ee6b..435571db 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -226,7 +226,7 @@ Section CircBuffer.
rewrite (_ : Z.to_nat (n + b) = S $ S $ Z.to_nat n); last first.
{ rewrite Z2Nat.inj_add; [|omega|omega].
- rewrite (_: Z.to_nat 2 = 2%nat); last auto. omega. }
+ rewrite (_: Z.to_nat 2 = 2%nat); last auto. lia. }
rewrite 2!big_sepL_cons -/seq.
iDestruct "oLs" as "(owi & ori & oLs)".
diff --git a/theories/examples/hashtable.v b/theories/examples/hashtable.v
index a1dbf11c..e8007239 100644
--- a/theories/examples/hashtable.v
+++ b/theories/examples/hashtable.v
@@ -39,7 +39,7 @@ Proof.
destruct (elem_of_list_split _ _ e) as (li1 & li2 & ?); subst.
apply NoDup_remove in Hunique as [].
rewrite !app_length (IHl (li1 ++ li2)%list); auto.
- rewrite app_length; simpl; omega.
+ rewrite app_length; simpl; lia.
* rewrite Forall_forall; intros j Hin.
eapply Forall_forall in Hli;
last by rewrite elem_of_app; apply elem_of_app in Hin as [|]; eauto; repeat constructor.
@@ -47,7 +47,7 @@ Proof.
pose proof (lookup_lt_Some _ _ _ Hi) as Hlt.
rewrite lookup_app_l in Hi; eauto.
rewrite app_length in Hlt; simpl in Hlt.
- destruct (decide (j = length l)); [subst; done | omega].
+ destruct (decide (j = length l)); [subst; done | lia].
* intros ?? Hout Hi.
pose proof (lookup_lt_Some _ _ _ Hi) as Hlt.
apply (Hrest i).
@@ -63,7 +63,7 @@ Proof.
destruct (decide (j = length l));
first by rewrite list_lookup_middle in Hi; last done; inversion Hi; subst.
rewrite lookup_app_l in Hi; eauto.
- rewrite app_length in Hlt; simpl in Hlt; omega.
+ rewrite app_length in Hlt; simpl in Hlt; lia.
* intros ?? Hout Hi.
pose proof (lookup_lt_Some _ _ _ Hi) as Hlt.
apply (Hrest i); auto.
@@ -377,7 +377,7 @@ Section proof.
wp_op.
destruct (size - Z.to_nat i)%nat eqn: Hi.
{ apply Z2Nat.inj_lt in H; try omega.
- rewrite Nat2Z.id in H; omega. }
+ rewrite Nat2Z.id in H; lia. }
simpl replicate; rewrite big_sepL_cons.
iDestruct "Hrest" as "[Hi Hrest]".
rewrite Z.add_0_l.
@@ -397,10 +397,9 @@ Section proof.
iSplit.
{ iPureIntro; rewrite !app_length; simpl; omega. }
iSplitL "Hrest"; [|iSplitL "HA"].
- + replace (size - (Z.to_nat i + 1))%nat with n by omega.
+ + replace (size - (Z.to_nat i + 1))%nat with n by lia.
iApply (big_sepL_proper with "Hrest"); intros; simpl.
- rewrite Zpos_P_of_succ_nat.
- unfold Z.succ; rewrite <- Z.add_assoc, (Z.add_comm i 1); done.
+ rewrite (_: k + (i + 1) = S k + i); [done|lia].
+ iSplit; last eauto.
iApply (big_sepL_proper with "HA"); intros ? (?, ?) ?%lookup_replicate_1; simpl.
unfold hashtable_entry_A.
@@ -645,7 +644,7 @@ Section proof.
{ rewrite map_insert Hi1.
replace size with (length (map fst T)).
rewrite rebase_insert; try omega.
- rewrite sublist_insert_l; auto; omega. }
+ rewrite sublist_insert_l; auto; lia. }
{ rewrite map_insert nth_insert.
rewrite decide_left; auto.
rewrite map_length HlenT; auto. } }
@@ -699,10 +698,10 @@ Section proof.
rewrite map_insert Hi1.
replace size with (length (map fst T)).
rewrite rebase_insert; try omega.
- rewrite sublist_insert_m; try omega.
- rewrite Nat.sub_0_r sublist_split; last omega.
+ rewrite sublist_insert_m; try lia.
+ rewrite Nat.sub_0_r sublist_split; last lia.
rewrite (sublist_len_1 _ _ 0); last omega.
- rewrite insert_app_r_alt; rewrite length_sublist; try omega.
+ rewrite insert_app_r_alt; rewrite length_sublist; try lia.
rewrite Nat.sub_0_r Nat.sub_diag; simpl.
rewrite Forall_app; split; first done; repeat constructor; auto.
* iApply big_sepL_insert; first done.
@@ -734,7 +733,7 @@ Section proof.
- by rewrite lookup_insert_same; rewrite ?map_length; try omega.
- specialize (Hwf _ _ Hj eq_refl).
rewrite lookup_insert_diff; simpl; rewrite ?map_length; try congruence.
- split; congruence.
+ split; [congruence|lia].
Qed.
Definition past_snaps lgk k (T : list (Z * gmap nat Z)) i : vProp Σ :=
@@ -746,9 +745,9 @@ Section proof.
intros.
destruct (decide (x < y)%nat); first by left; apply Nat.mod_small; omega.
right.
- replace x with ((x - y) + 1 * y)%nat at 1; last omega.
+ replace x with ((x - y) + 1 * y)%nat at 1; last lia.
rewrite Nat.mod_add; last done.
- rewrite Nat.mod_small; omega.
+ rewrite Nat.mod_small; lia.
Qed.
Lemma mod_plus_inv : forall a b c d, (c ≠0 -> (a + b) mod c = (d + b) mod c -> a mod c = d mod c)%nat.
@@ -759,7 +758,7 @@ Section proof.
pose proof (Nat.mod_upper_bound a c Hc).
pose proof (Nat.mod_upper_bound b c Hc).
pose proof (Nat.mod_upper_bound d c Hc).
- destruct (mod_smallish (a mod c + b mod c) c), (mod_smallish (d mod c + b mod c) c); omega.
+ destruct (mod_smallish (a mod c + b mod c) c), (mod_smallish (d mod c + b mod c) c); lia.
Qed.
Lemma entries_lookup : forall k i i1 T0 lgk lgv T (Hk : k ≠0) (Hi : (i < size)%nat)
@@ -781,7 +780,7 @@ Section proof.
pose proof (lookup_lt_Some _ _ _ Hjth) as Hj.
apply nth_lookup_Some with (d := 0) in Hjth.
pose proof (hash_range k).
- rewrite length_sublist in Hj; try (rewrite length_rebase map_length; omega).
+ rewrite length_sublist in Hj; try (rewrite length_rebase map_length; lia).
rewrite nth_sublist in Hjth; last omega.
rewrite nth_rebase in Hjth; try (rewrite map_length; omega).
unfold past_snaps.
@@ -842,7 +841,7 @@ Section proof.
destruct (decide _); auto.
rewrite Hi1 in e; apply mod_plus_inv in e; last done.
match goal with H : seq _ _ !! _ = Some _ |- _ => apply lookup_seq_inv in H as []; subst end.
- rewrite !Nat.mod_small in e; omega.
+ rewrite !Nat.mod_small in e; lia.
- simpl.
rewrite nth_insert; last by rewrite map_length.
rewrite Hi1 decide_left -Hi1; auto.
@@ -948,7 +947,7 @@ Section proof.
{ rewrite map_insert Hi1.
replace size with (length (map fst T)).
rewrite rebase_insert; try omega.
- rewrite sublist_insert_l; auto; omega. }
+ rewrite sublist_insert_l; auto; lia. }
{ rewrite map_insert nth_insert.
rewrite decide_left; auto.
rewrite map_length HlenT; auto. } }
@@ -1028,7 +1027,7 @@ Section proof.
{ rewrite map_insert Hi1.
replace size with (length (map fst T)).
rewrite rebase_insert; try omega.
- rewrite sublist_insert_l; auto; omega. }
+ rewrite sublist_insert_l; auto; lia. }
{ rewrite map_insert nth_insert.
rewrite decide_left; auto.
rewrite map_length HlenT; auto. } }
@@ -1108,7 +1107,7 @@ Section proof.
{ rewrite map_insert Hi1.
replace size with (length (map fst T)).
rewrite rebase_insert; try omega.
- rewrite sublist_insert_l; auto; omega. }
+ rewrite sublist_insert_l; auto; lia. }
{ rewrite map_insert nth_insert.
rewrite decide_left; auto.
rewrite map_length HlenT; auto. } }
@@ -1148,10 +1147,10 @@ Section proof.
rewrite map_insert Hi1.
replace size with (length (map fst T)).
rewrite rebase_insert; try omega.
- rewrite sublist_insert_m; try omega.
- rewrite Nat.sub_0_r sublist_split; last omega.
+ rewrite sublist_insert_m; try lia.
+ rewrite Nat.sub_0_r sublist_split; last lia.
rewrite (sublist_len_1 _ _ 0); last omega.
- rewrite insert_app_r_alt; rewrite length_sublist; try omega.
+ rewrite insert_app_r_alt; rewrite length_sublist; try lia.
rewrite Nat.sub_0_r Nat.sub_diag; simpl.
rewrite Forall_app; split; first done; repeat constructor; auto.
-- iApply big_sepL_insert; first done.
@@ -1178,10 +1177,10 @@ Section proof.
rewrite map_insert Hi1.
replace size with (length (map fst T)).
rewrite rebase_insert; try omega.
- rewrite sublist_insert_m; try omega.
- rewrite Nat.sub_0_r sublist_split; last omega.
+ rewrite sublist_insert_m; try lia.
+ rewrite Nat.sub_0_r sublist_split; last lia.
rewrite (sublist_len_1 _ _ 0); last omega.
- rewrite insert_app_r_alt; rewrite length_sublist; try omega.
+ rewrite insert_app_r_alt; rewrite length_sublist; try lia.
rewrite Nat.sub_0_r Nat.sub_diag; simpl.
rewrite Forall_app; split; first done; repeat constructor; auto.
+ iApply big_sepL_insert; first done.
@@ -1273,7 +1272,7 @@ Section proof.
match goal with H : value_of s' 0 |- _ => destruct H as (j & ? & Hlast) end.
set (lv' := <[(j+1)%nat := v]>s').
assert (map_subseteq s' lv').
- { simpl in *; apply insert_subseteq, Hlast; omega. }
+ { simpl in *; apply insert_subseteq, Hlast; lia. }
iDestruct "HH" as (HTa) "(% & Hexcl & HH)".
destruct H8 as (? & Hwf & HHTa).
destruct (lookup_lt_is_Some_2 HTa i) as [(k1, lv1) Hpi'].
@@ -1480,7 +1479,7 @@ Section proof.
+ rewrite lookup_app_l; auto.
eapply lookup_lt_Some; eauto.
+ pose proof (lookup_lt_Some _ _ _ Ht) as Hlen; rewrite app_length in Hlen; simpl in Hlen.
- rewrite lookup_app_l in Ht; auto; omega.
+ rewrite lookup_app_l in Ht; auto; lia.
Qed.
Lemma add_fails : forall k v b l H H' (HH : apply_hist H l H') (Hadd : HAdd k v b ∈ l)
@@ -1596,7 +1595,7 @@ Section proof.
- apply lookup_difference_Some in Hl as [Hl Ht].
apply H, lookup_app_Some in Hl as [|[? Hl]]; auto.
destruct (t - length l)%nat eqn: Hminus; inversion Hl.
- assert (t = length l) by omega; subst; rewrite lookup_insert in Ht; done.
+ assert (t = length l) by lia; subst; rewrite lookup_insert in Ht; done.
- rewrite lookup_difference_Some.
pose proof (lookup_lt_Some _ _ _ Hl); rewrite lookup_insert_ne; last omega; split; auto.
rewrite H lookup_app_l; done.
@@ -2004,7 +2003,7 @@ Section proof.
Lemma drop_lookup: forall {A} i l (d : A), (i < length l)%nat ->
drop i l = nth i l d :: drop (S i) l.
Proof.
- induction i; destruct l; simpl; auto; intros; try omega.
+ induction i; destruct l; simpl; auto; intros; try lia.
apply IHi; omega.
Qed.
@@ -2194,7 +2193,7 @@ Section proof.
rewrite Z2Nat.inj_add; try omega.
rewrite Nat.add_1_r; simpl; iFrame.
iExists (lr ++ (h, b1, b2, b3) :: nil)%list.
- rewrite app_length; simpl; iSplit; first by iPureIntro; omega.
+ rewrite app_length; simpl; iSplit; first by iPureIntro; lia.
rewrite big_sepL_app; simpl; iFrame.
iSplitR "Htotal".
* iSplit; last auto.
diff --git a/theories/examples/kvnode.v b/theories/examples/kvnode.v
index d3355c64..30b54b70 100644
--- a/theories/examples/kvnode.v
+++ b/theories/examples/kvnode.v
@@ -309,7 +309,7 @@ Section proof.
- rewrite lookup_insert_ne; last done.
rewrite Hin.
split; intros []; split; auto; try omega.
- destruct (decide (n' = n + 1)%nat); last omega.
+ destruct (decide (n' = n + 1)%nat); last lia.
subst; rewrite Nat.even_add Heven in H; done.
Qed.
@@ -320,11 +320,11 @@ Section proof.
intros; destruct (decide (n' = O)).
+ subst; rewrite lookup_insert; split; eauto.
+ rewrite lookup_insert_ne; last done.
- rewrite lookup_empty; split; intros []; [done | omega].
+ rewrite lookup_empty; split; intros []; [done | lia].
- assert (n = (n - 2) + 2)%nat as Heq.
{ rewrite Nat.sub_add; first done.
destruct n; first done.
- destruct n; [done | omega]. }
+ destruct n; [done | lia]. }
rewrite {1 3}Heq.
eapply log_latest_insert, IHg.
rewrite Heq Nat.even_add in H.
@@ -366,7 +366,7 @@ Section proof.
destruct (decide (i < length l)); [rewrite app_nth1 | rewrite app_nth2]; try omega;
destruct (decide _); auto; try omega.
- subst; rewrite minus_diag; auto.
- - rewrite !nth_overflow; auto; simpl; omega.
+ - rewrite !nth_overflow; auto; simpl; lia.
Qed.
Lemma map_nth_app {A} m1 n m2 i (d : A) (Hm1: map_size m1 n)
@@ -393,7 +393,7 @@ Section proof.
Proof.
intros; induction vals using rev_ind; simpl; iIntros "H".
{ iExists (make_log v nil); iFrame; iPureIntro.
- split; last by (split; [apply make_log_latest | intros; omega]).
+ split; last by (split; [apply make_log_latest | intros; lia]).
intros ???%make_log_lookup; subst; auto. }
rewrite big_sepL_app; simpl.
iDestruct "H" as "(H & Hi & _)".
@@ -419,7 +419,7 @@ Section proof.
intros; erewrite map_nth_app; eauto.
rewrite Nat.add_0_r in H4.
destruct (decide _); first by subst.
- apply H2; omega.
+ apply H2; lia.
- rewrite big_sepL_app; simpl.
erewrite Nat.add_0_r, map_nth_app; eauto.
rewrite decide_True; last done; iFrame.
@@ -531,7 +531,7 @@ Section proof.
repeat wp_op.
wp_bind ([_]_at)%E.
destruct (8 - Z.to_nat i)%nat eqn: Hi.
- { apply Z2Nat.inj_lt in H2; [change (Z.to_nat 8) with 8%nat in H2| |]; omega. }
+ { apply Z2Nat.inj_lt in H2; [change (Z.to_nat 8) with 8%nat in H2| |]; lia. }
rewrite !big_sepL_cons.
iDestruct "Hdata" as "[Hdi Hdata]"; iDestruct "Hrest" as "[Hi Hrest]".
rewrite Z2Nat.id; last omega.
@@ -570,7 +570,7 @@ Section proof.
by rewrite Nat2Z.inj_add. }
rewrite big_sepL_app; simpl.
change (Z.to_nat 1) with 1%nat.
- replace (8 - (length vals + 1))%nat with n1 by (rewrite H3 Nat2Z.id in Hi; omega).
+ replace (8 - (length vals + 1))%nat with n1 by (rewrite H3 Nat2Z.id in Hi; lia).
rewrite Nat.add_0_r Nat.add_1_r; iFrame.
iExists (Nat.max v' vi); rewrite -Nat.sub_max_distr_r.
iSplit.
@@ -597,7 +597,7 @@ Section proof.
- iNext; iIntros "H"; iDestruct "H" as (i) "(% & % & H)".
assert (i = 8) by omega; subst.
iDestruct "H" as (vals) "(% & out & _ & H)".
- assert (length vals = 8)%nat as Hlen by omega.
+ assert (length vals = 8)%nat as Hlen by lia.
iDestruct "H" as (v') "(% & #kV' & Hvals & _)".
match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
wp_seq; clear Hclosed.
@@ -627,8 +627,8 @@ Section proof.
iPureIntro; destruct H8 as (? & ? & Hlatest & ?); split; eauto.
pose proof (log_latest_even _ _ _ Hlatest) as Heven'.
destruct (decide (x = v1)); first by subst.
- subst; rewrite Nat.even_sub in Heven; last omega.
- assert (x = v') by omega; subst.
+ subst; rewrite Nat.even_sub in Heven; last lia.
+ assert (x = v') by lia; subst.
rewrite Heven' in Heven; done. }
destruct H6 as (Hsize & Hlatest & Hincl).
iMod (node_state_ord _ _ v1 v1 with "[#] [#]") as "%"; first auto.
@@ -656,7 +656,7 @@ Section proof.
{ rewrite Hsize1; omega. }
eapply lookup_weaken_inv; [| apply Hincl; eauto |];
rewrite lookup_fmap; [erewrite HL1 | erewrite HL']; simpl; erewrite nth_lookup_Some; eauto.
- * lapply (Hincl O); last omega; intro X.
+ * lapply (Hincl O); last lia; intro X.
specialize (X i); rewrite !lookup_fmap HL1 HL' in X; done.
+ eapply lookup_weaken; last eauto.
destruct Hlatest; done.
@@ -764,7 +764,7 @@ Section proof.
destruct HL as [_ Hlast].
destruct (Hlast (v + 2)%nat) as [Hnone _].
destruct (L !! (v + 2)%nat) eqn: H2; last done.
- destruct Hnone; [eauto | omega]. }
+ destruct Hnone; [eauto | lia]. }
pose proof (log_latest_insert _ _ _ vals HL) as HL'.
wp_bind (for_loop _ _ _ _).
iApply (wp_for_simple with "[] [data in]").
@@ -786,7 +786,7 @@ Section proof.
iNext; iIntros (?) "[% Hi]"; subst.
iPoseProof ("Hin" with "Hi") as "Hin".
destruct (8 - Z.to_nat i)%nat eqn: Hi.
- { apply Z2Nat.inj_lt in H; [change (Z.to_nat 8) with 8%nat in H| |]; omega. }
+ { apply Z2Nat.inj_lt in H; [change (Z.to_nat 8) with 8%nat in H| |]; lia. }
rewrite big_sepL_cons.
iDestruct "Hrest" as "[Hi Hrest]".
rewrite Z2Nat.id; last omega.
@@ -799,14 +799,14 @@ Section proof.
unfold dataP, dataP'.
eapply fmap_nth_log_latest in HL'.
erewrite map_nth_insert, nth_lookup_Some in HL' by eauto.
- iSplit; iNext; iExists (v + 2)%nat; replace (v + 2 - 1)%nat with (v + 1)%nat by omega; auto. }
+ iSplit; iNext; iExists (v + 2)%nat; replace (v + 2 - 1)%nat with (v + 1)%nat by lia; auto. }
iNext; iIntros "[_ Hi]".
iApply "Hpost".
iSplit; first by iPureIntro; omega.
rewrite Z2Nat.inj_add; try omega.
rewrite -take_take_drop big_sepL_app.
change (Z.to_nat 1) with 1%nat.
- replace (8 - (Z.to_nat i + 1))%nat with n0 by omega.
+ replace (8 - (Z.to_nat i + 1))%nat with n0 by lia.
rewrite !Nat.add_1_r; iFrame.
erewrite take_1_drop by eauto; simpl.
rewrite take_length Nat.add_0_r Min.min_l; last omega.
@@ -820,7 +820,7 @@ Section proof.
repeat wp_op.
iMod ("Hshift" with "HP") as (L1) "[oL' Hclose]".
iApply (GPS_SW_ExWrite (s := (v + 1)%nat) (versionP n g) (v + 2)%nat emp%I (fun _ => |={base_mask,⊤}=> Φ #())%I
- with "[-]"); [hnf; omega | done | done | | by iNext; iIntros "[_ ?]"].
+ with "[-]"); [hnf; lia | done | done | | by iNext; iIntros "[_ ?]"].
iFrame "#"; iFrame.
iNext; iIntros (?) "(_ & vP & kV)".
iPoseProof (@own_master_eq _ _ _ _ _ (hist_join (list.listC ZC)) with "oL oL'") as "%"; subst L1.
diff --git a/theories/infrastructure.v b/theories/infrastructure.v
index 03413dae..45c146ea 100644
--- a/theories/infrastructure.v
+++ b/theories/infrastructure.v
@@ -13,7 +13,7 @@ Proof.
induction n; [done|].
rewrite seq_set_S_union_L /=.
rewrite size_union.
- + rewrite IHn size_singleton. omega.
+ + rewrite IHn size_singleton. lia.
+ apply disjoint_singleton_l.
move => /elem_of_seq_set [_ ?]. omega.
Qed.
@@ -27,7 +27,7 @@ Qed.
Lemma seq_elem_of t n (Lt : (t < n)%nat): t ∈ seq 0 n.
Proof.
- induction n; first omega.
+ induction n; first lia.
rewrite seq_S elem_of_app. apply lt_n_Sm_le, le_lt_or_eq in Lt as [Lt|Eq].
- left. by apply IHn.
- right. rewrite Eq. left.
@@ -980,9 +980,6 @@ Instance gset_SimpleCollection `{Countable K} : SimpleCollection K (gset K) := _
Instance gset_Collection `{Countable K} : Collection K (gset K) := _.
-
-
-
Program Definition Pos2Qp (n: positive) : Qp := mk_Qp (Zpos n) _.
Next Obligation. intros n. rewrite /Qcanon.Qclt /QArith_base.Qlt /=. lia. Qed.
diff --git a/theories/lifting.v b/theories/lifting.v
index 0be8e257..26e71279 100644
--- a/theories/lifting.v
+++ b/theories/lifting.v
@@ -153,8 +153,8 @@ Lemma wp_rec E π f x erec e1 e2 Φ :
base.Closed (f :b: x :b: []) erec →
▷ WP (subst' x e2 (subst' f e1 erec), π) @ E {{ Φ }} ⊢ WP (App e1 e2, π) @ E {{ Φ }}.
Proof.
- intros -> [v2 ?] ?. rewrite -(ownP_lift_pure_det_head_step (App _ _, π)
- (subst' x e2 (subst' f (Rec f x erec) erec), π) []); eauto.
+ intros -> [v2 ?] ?. rewrite -(ownP_lift_pure_det_head_step_no_fork (App _ _, π)
+ (subst' x e2 (subst' f (Rec f x erec) erec), π)); eauto.
- by repeat econstructor.
- intros; by inv_head_step.
Qed.
@@ -185,8 +185,7 @@ Qed.
Lemma wp_if_true E π e1 e2 Φ :
▷ WP (e1, π) @ E {{ Φ }} ⊢ WP (If (Lit $ lit_of_bool true) e1 e2, π) @ E {{ Φ }}.
Proof.
- rewrite -(ownP_lift_pure_det_head_step (If _ _ _, _) (e1, _) []) //; intros.
- - rewrite big_sepL_nil. iIntros "$".
+ rewrite -(ownP_lift_pure_det_head_step_no_fork (If _ _ _, _) (e1, _)) //; intros.
- by repeat econstructor.
- inversion H; [inversion BaseStep|by inversion ExprStep]; subst; intuition.
Qed.
@@ -194,8 +193,7 @@ Qed.
Lemma wp_if_false E π e1 e2 Φ :
▷ WP (e2, π) @ E {{ Φ }} ⊢ WP (If (Lit $ lit_of_bool false) e1 e2, π) @ E {{ Φ }}.
Proof.
- rewrite -(ownP_lift_pure_det_head_step (If _ _ _, _) (e2, _) []) //; intros.
- - rewrite big_sepL_nil. iIntros "$".
+ rewrite -(ownP_lift_pure_det_head_step_no_fork (If _ _ _, _) (e2, _)) //; intros.
- by repeat econstructor.
- inversion H; [inversion BaseStep|by inversion ExprStep]; subst; intuition.
Qed.
diff --git a/theories/weakestpre.v b/theories/weakestpre.v
index 0afb35d8..0ac76de9 100644
--- a/theories/weakestpre.v
+++ b/theories/weakestpre.v
@@ -145,7 +145,7 @@ Proof.
iApply (fupd_mask_mono E1 _); first done.
iExact "H". (* TODO why does `done` not work? *)
}
- iIntros (σ1 κ κs) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
+ iIntros (σ1 κ κs n) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
iMod ("H" with "[$]") as "[$ H]".
iModIntro. iIntros (e2 σ2 efs Hstep).
iMod ("H" with "[//]") as "H". iIntros "!> !>". iMod "H" as "($ & H & $)"; auto.
@@ -174,8 +174,8 @@ Proof.
iIntros (V ? ?).
rewrite !bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
destruct (ra_lang.to_val ((e, V))) as [v|] eqn:?; [by iMod "H"|].
- iIntros "S" (σ1 κ κs) "Hσ1". iMod ("H" with "S") as "H".
- iApply ("H" $! σ1 κ κs with "Hσ1").
+ iIntros "S" (σ1 κ κs n) "Hσ1". iMod ("H" with "S") as "H".
+ iApply ("H" $! σ1 κ κs n with "Hσ1").
Qed.
Lemma wp_fupd E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed.
@@ -202,8 +202,8 @@ Proof.
rewrite /to_val /= /ra_lang.to_val /=.
iIntros (-> ?) "H". iIntros (V'' HV'' π) "S".
iSpecialize ("H" with "[//]").
- iIntros (σ1 κ κs) "Hσ". iMod "HR". iSpecialize ("H" with "S").
- iMod ("H" $! σ1 κ κs with "[$]") as "[$ H]".
+ iIntros (σ1 κ κs n) "Hσ". iMod "HR". iSpecialize ("H" with "S").
+ iMod ("H" $! σ1 κ κs n with "[$]") as "[$ H]".
iModIntro; iIntros (e2 σ2 efs Hstep).
iMod ("H" $! e2 σ2 efs with "[% //]") as "H".
iIntros "!> !>". iMod "H" as "($ & H & $)".
--
GitLab