From 035f0b2994256c1b238b22d8661a8e7386d63973 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 18 Feb 2016 12:30:18 +0100
Subject: [PATCH] Put step-indexes first.
---
algebra/agree.v | 20 +--
algebra/auth.v | 6 +-
algebra/cmra.v | 56 ++++-----
algebra/cofe.v | 30 ++---
algebra/cofe_solver.v | 14 +--
algebra/excl.v | 10 +-
algebra/fin_maps.v | 16 +--
algebra/iprod.v | 12 +-
algebra/option.v | 12 +-
algebra/upred.v | 235 ++++++++++++++++++------------------
program_logic/adequacy.v | 4 +-
program_logic/lifting.v | 8 +-
program_logic/model.v | 5 +-
program_logic/pviewshifts.v | 38 +++---
program_logic/resources.v | 10 +-
program_logic/weakestpre.v | 29 +++--
program_logic/wsat.v | 4 +-
17 files changed, 251 insertions(+), 258 deletions(-)
diff --git a/algebra/agree.v b/algebra/agree.v
index b21e24653..d2d187668 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -16,7 +16,7 @@ Context {A : cofeT}.
Instance agree_validN : ValidN (agree A) := λ n x,
agree_is_valid x n ∧ ∀ n', n' ≤ n → x n' ≡{n'}≡ x n.
-Lemma agree_valid_le (x : agree A) n n' :
+Lemma agree_valid_le n n' (x : agree A) :
agree_is_valid x n → n' ≤ n → agree_is_valid x n'.
Proof. induction 2; eauto using agree_valid_S. Qed.
Instance agree_equiv : Equiv (agree A) := λ x y,
@@ -43,14 +43,14 @@ Proof.
* transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz.
* transitivity (y n'). by apply Hxy. by apply Hyz, Hxy.
- intros n x y Hxy; split; intros; apply Hxy; auto.
- - intros c n; apply and_wlog_r; intros;
+ - intros n c; apply and_wlog_r; intros;
symmetry; apply (chain_cauchy c); naive_solver.
Qed.
Canonical Structure agreeC := CofeT agree_cofe_mixin.
-Lemma agree_car_ne (x y : agree A) n : ✓{n} x → x ≡{n}≡ y → x n ≡{n}≡ y n.
+Lemma agree_car_ne n (x y : agree A) : ✓{n} x → x ≡{n}≡ y → x n ≡{n}≡ y n.
Proof. by intros [??] Hxy; apply Hxy. Qed.
-Lemma agree_cauchy (x : agree A) n i : ✓{n} x → i ≤ n → x i ≡{i}≡ x n.
+Lemma agree_cauchy n (x : agree A) i : ✓{n} x → i ≤ n → x i ≡{i}≡ x n.
Proof. by intros [? Hx]; apply Hx. Qed.
Program Instance agree_op : Op (agree A) := λ x y,
@@ -87,7 +87,7 @@ Proof.
repeat match goal with H : agree_is_valid _ _ |- _ => clear H end;
by cofe_subst; rewrite !agree_idemp.
Qed.
-Lemma agree_includedN (x y : agree A) n : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y.
+Lemma agree_includedN n (x y : agree A) : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y.
Proof.
split; [|by intros ?; exists y].
by intros [z Hz]; rewrite Hz assoc agree_idemp.
@@ -100,12 +100,12 @@ Proof.
rewrite (Hx n'); last auto.
symmetry; apply dist_le with n; try apply Hx; auto.
- intros x; apply agree_idemp.
- - by intros x y n [(?&?&?) ?].
- - by intros x y n; rewrite agree_includedN.
+ - by intros n x y [(?&?&?) ?].
+ - by intros n x y; rewrite agree_includedN.
Qed.
-Lemma agree_op_inv (x1 x2 : agree A) n : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2.
+Lemma agree_op_inv n (x1 x2 : agree A) : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2.
Proof. intros Hxy; apply Hxy. Qed.
-Lemma agree_valid_includedN (x y : agree A) n : ✓{n} y → x ≼{n} y → x ≡{n}≡ y.
+Lemma agree_valid_includedN n (x y : agree A) : ✓{n} y → x ≼{n} y → x ≡{n}≡ y.
Proof.
move=> Hval [z Hy]; move: Hval; rewrite Hy.
by move=> /agree_op_inv->; rewrite agree_idemp.
@@ -161,7 +161,7 @@ Section agree_map.
Global Instance agree_map_monotone : CMRAMonotone (agree_map f).
Proof.
split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]].
- intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy.
+ intros n x y; rewrite !agree_includedN; intros Hy; rewrite Hy.
split; last done; split; simpl; last tauto.
by intros (?&?&Hxy); repeat split; intros;
try apply Hxy; try apply Hf; eauto using @agree_valid_le.
diff --git a/algebra/auth.v b/algebra/auth.v
index 11fcc65e7..9c78a1fd9 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -46,8 +46,8 @@ Proof.
+ by intros ?? [??]; split; symmetry.
+ intros ??? [??] [??]; split; etransitivity; eauto.
- by intros ? [??] [??] [??]; split; apply dist_S.
- - intros c n; split. apply (conv_compl (chain_map authoritative c) n).
- apply (conv_compl (chain_map own c) n).
+ - intros n c; split. apply (conv_compl n (chain_map authoritative c)).
+ apply (conv_compl n (chain_map own c)).
Qed.
Canonical Structure authC := CofeT auth_cofe_mixin.
Global Instance auth_timeless (x : auth A) :
@@ -163,7 +163,7 @@ Lemma auth_update a a' b b' :
(∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b) →
â— a â‹… â—¯ a' ~~> â— b â‹… â—¯ b'.
Proof.
- move=> Hab [[?| |] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
+ move=> Hab n [[?| |] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
destruct (Hab n (bf1 â‹… bf2)) as [Ha' ?]; auto.
{ by rewrite Ha left_id assoc. }
split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done].
diff --git a/algebra/cmra.v b/algebra/cmra.v
index a441ce98a..93126eecc 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -147,11 +147,11 @@ Class LocalUpdate {A : cmraT} (Lv : A → Prop) (L : A → A) := {
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.
(** * Frame preserving updates *)
-Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
+Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n z,
✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
Instance: Params (@cmra_updateP) 1.
Infix "~~>:" := cmra_updateP (at level 70).
-Definition cmra_update {A : cmraT} (x y : A) := ∀ z n,
+Definition cmra_update {A : cmraT} (x y : A) := ∀ n z,
✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
Infix "~~>" := cmra_update (at level 70).
Instance: Params (@cmra_update) 1.
@@ -202,23 +202,23 @@ Qed.
Global Instance cmra_update_proper :
Proper ((≡) ==> (≡) ==> iff) (@cmra_update A).
Proof.
- intros x1 x2 Hx y1 y2 Hy; split=>? z n; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
+ intros x1 x2 Hx y1 y2 Hy; split=>? n z; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
Qed.
Global Instance cmra_updateP_proper :
Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
- intros x1 x2 Hx P1 P2 HP; split=>Hup z n;
+ intros x1 x2 Hx P1 P2 HP; split=>Hup n z;
[rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
Qed.
(** ** Validity *)
Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
Proof. done. Qed.
-Lemma cmra_validN_le x n n' : ✓{n} x → n' ≤ n → ✓{n'} x.
+Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x.
Proof. induction 2; eauto using cmra_validN_S. Qed.
Lemma cmra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed.
-Lemma cmra_validN_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y.
+Lemma cmra_validN_op_r n x y : ✓{n} (x ⋅ y) → ✓{n} y.
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
Lemma cmra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.
@@ -228,7 +228,7 @@ Lemma cmra_unit_r x : x ⋅ unit x ≡ x.
Proof. by rewrite (comm _ x) cmra_unit_l. Qed.
Lemma cmra_unit_unit x : unit x ⋅ unit x ≡ unit x.
Proof. by rewrite -{2}(cmra_unit_idemp x) cmra_unit_r. Qed.
-Lemma cmra_unit_validN x n : ✓{n} x → ✓{n} unit x.
+Lemma cmra_unit_validN n x : ✓{n} x → ✓{n} unit x.
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
Lemma cmra_unit_valid x : ✓ x → ✓ unit x.
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
@@ -237,7 +237,7 @@ Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
Lemma cmra_included_includedN x y : x ≼ y ↔ ∀ n, x ≼{n} y.
Proof.
split; [by intros [z Hz] n; exists z; rewrite Hz|].
- intros Hxy; exists (y ⩪ x); apply equiv_dist; intros n.
+ intros Hxy; exists (y ⩪ x); apply equiv_dist=> n.
symmetry; apply cmra_op_minus, Hxy.
Qed.
Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
@@ -252,14 +252,14 @@ Proof.
split; red; intros until 0; rewrite !cmra_included_includedN; first done.
intros; etransitivity; eauto.
Qed.
-Lemma cmra_validN_includedN x y n : ✓{n} y → x ≼{n} y → ✓{n} x.
+Lemma cmra_validN_includedN n x y : ✓{n} y → x ≼{n} y → ✓{n} x.
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
-Lemma cmra_validN_included x y n : ✓{n} y → x ≼ y → ✓{n} x.
+Lemma cmra_validN_included n x y : ✓{n} y → x ≼ y → ✓{n} x.
Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.
-Lemma cmra_includedN_S x y n : x ≼{S n} y → x ≼{n} y.
+Lemma cmra_includedN_S n x y : x ≼{S n} y → x ≼{n} y.
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
-Lemma cmra_includedN_le x y n n' : x ≼{n} y → n' ≤ n → x ≼{n'} y.
+Lemma cmra_includedN_le n n' x y : x ≼{n} y → n' ≤ n → x ≼{n'} y.
Proof. induction 2; auto using cmra_includedN_S. Qed.
Lemma cmra_includedN_l n x y : x ≼{n} x ⋅ y.
@@ -284,7 +284,7 @@ Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
-Lemma cmra_included_dist_l x1 x2 x1' n :
+Lemma cmra_included_dist_l n x1 x2 x1' :
x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2.
Proof.
intros [z Hx2] Hx1; exists (x1' â‹… z); split; auto using cmra_included_l.
@@ -318,7 +318,7 @@ Qed.
(** ** RAs with an empty element *)
Section identity.
Context `{Empty A, !CMRAIdentity A}.
- Lemma cmra_empty_leastN n x : ∅ ≼{n} x.
+ Lemma cmra_empty_leastN n x : ∅ ≼{n} x.
Proof. by exists x; rewrite left_id. Qed.
Lemma cmra_empty_least x : ∅ ≼ x.
Proof. by exists x; rewrite left_id. Qed.
@@ -350,14 +350,14 @@ Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =).
Proof.
split.
- by intros Hx z ?; exists y; split; [done|apply (Hx z)].
- - by intros Hx z n ?; destruct (Hx z n) as (?&<-&?).
+ - by intros Hx n z ?; destruct (Hx n z) as (?&<-&?).
Qed.
Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P.
-Proof. by intros ? z n ?; exists x. Qed.
+Proof. by intros ? n z ?; exists x. Qed.
Lemma cmra_updateP_compose (P Q : A → Prop) x :
x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q.
Proof.
- intros Hx Hy z n ?. destruct (Hx z n) as (y&?&?); auto. by apply (Hy y).
+ intros Hx Hy n z ?. destruct (Hx n z) as (y&?&?); auto. by apply (Hy y).
Qed.
Lemma cmra_updateP_compose_l (Q : A → Prop) x y : x ~~> y → y ~~>: Q → x ~~>: Q.
Proof.
@@ -370,9 +370,9 @@ Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q.
Proof.
- intros Hx1 Hx2 Hy z n ?.
- destruct (Hx1 (x2 â‹… z) n) as (y1&?&?); first by rewrite assoc.
- destruct (Hx2 (y1 â‹… z) n) as (y2&?&?);
+ intros Hx1 Hx2 Hy n z ?.
+ destruct (Hx1 n (x2 â‹… z)) as (y1&?&?); first by rewrite assoc.
+ destruct (Hx2 n (y1 â‹… z)) as (y2&?&?);
first by rewrite assoc (comm _ x2) -assoc.
exists (y1 â‹… y2); split; last rewrite (comm _ y1) -assoc; auto.
Qed.
@@ -389,7 +389,7 @@ Proof. intro. auto. Qed.
Section identity_updates.
Context `{Empty A, !CMRAIdentity A}.
Lemma cmra_update_empty x : x ~~> ∅.
- Proof. intros z n; rewrite left_id; apply cmra_validN_op_r. Qed.
+ Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
Lemma cmra_update_empty_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y.
Proof. split; [intros; transitivity ∅|]; auto using cmra_update_empty. Qed.
End identity_updates.
@@ -472,7 +472,7 @@ Section discrete.
Definition discrete_cmra_mixin : CMRAMixin A.
Proof.
by destruct ra; split; unfold Proper, respectful, includedN;
- try setoid_rewrite <-(timeless_iff _ _ _ _).
+ try setoid_rewrite <-(timeless_iff _ _).
Qed.
Definition discrete_extend_mixin : CMRAExtendMixin A.
Proof.
@@ -483,10 +483,10 @@ Section discrete.
CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
Lemma discrete_updateP (x : discreteRA) (P : A → Prop) :
(∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P.
- Proof. intros Hvalid z n; apply Hvalid. Qed.
+ Proof. intros Hvalid n z; apply Hvalid. Qed.
Lemma discrete_update (x y : discreteRA) :
(∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y.
- Proof. intros Hvalid z n; apply Hvalid. Qed.
+ Proof. intros Hvalid n z; apply Hvalid. Qed.
Lemma discrete_valid (x : discreteRA) : v x → validN_valid x.
Proof. move=>Hx n. exact Hx. Qed.
End discrete.
@@ -540,7 +540,7 @@ Section prod.
- intros n x y; rewrite !prod_includedN.
by intros [??]; split; apply cmra_unit_preservingN.
- intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
- - intros x y n; rewrite prod_includedN; intros [??].
+ - intros n x y; rewrite prod_includedN; intros [??].
by split; apply cmra_op_minus.
Qed.
Definition prod_cmra_extend_mixin : CMRAExtendMixin (A * B).
@@ -561,12 +561,12 @@ Section prod.
- by intros ? [??]; split; apply (timeless _).
Qed.
Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
- Proof. intros ?? z n [??]; split; simpl in *; auto. Qed.
+ Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q.
Proof.
- intros Hx1 Hx2 HP z n [??]; simpl in *.
- destruct (Hx1 (z.1) n) as (a&?&?), (Hx2 (z.2) n) as (b&?&?); auto.
+ intros Hx1 Hx2 HP n z [??]; simpl in *.
+ destruct (Hx1 n (z.1)) as (a&?&?), (Hx2 n (z.2)) as (b&?&?); auto.
exists (a,b); repeat split; auto.
Qed.
Lemma prod_updateP' P1 P2 x :
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 1d008a7eb..4bdb3007b 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -54,7 +54,7 @@ Record CofeMixin A `{Equiv A, Compl A} := {
mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
mixin_dist_equivalence n : Equivalence (dist n);
mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y;
- mixin_conv_compl (c : chain A) n : compl c ≡{n}≡ c (S n)
+ mixin_conv_compl n c : compl c ≡{n}≡ c (S n)
}.
Class Contractive `{Dist A, Dist B} (f : A -> B) :=
contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y.
@@ -86,7 +86,7 @@ Section cofe_mixin.
Proof. apply (mixin_dist_equivalence _ (cofe_mixin A)). Qed.
Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y.
Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
- Lemma conv_compl (c : chain A) n : compl c ≡{n}≡ c (S n).
+ Lemma conv_compl n (c : chain A) : compl c ≡{n}≡ c (S n).
Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
End cofe_mixin.
@@ -113,7 +113,7 @@ Section cofe.
Qed.
Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x).
Proof. by apply dist_proper. Qed.
- Lemma dist_le (x y : A) n n' : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y.
+ Lemma dist_le n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y.
Proof. induction 2; eauto using dist_S. Qed.
Instance ne_proper {B : cofeT} (f : A → B)
`{!∀ n, Proper (dist n ==> dist n) f} : Proper ((≡) ==> (≡)) f | 100.
@@ -147,7 +147,7 @@ Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
(** Timeless elements *)
Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
Arguments timeless {_} _ {_} _ _.
-Lemma timeless_iff {A : cofeT} (x y : A) n : Timeless x → x ≡ y ↔ x ≡{n}≡ y.
+Lemma timeless_iff {A : cofeT} n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y.
Proof.
split; intros; [by apply equiv_dist|].
apply (timeless _), dist_le with n; auto with lia.
@@ -168,14 +168,14 @@ Section fixpoint.
Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}.
Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
Proof.
- apply equiv_dist=>n; rewrite /fixpoint (conv_compl (fixpoint_chain f) n) //.
+ apply equiv_dist=>n; rewrite /fixpoint (conv_compl n (fixpoint_chain f)) //.
induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Qed.
Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
(∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
Proof.
intros Hfg. rewrite /fixpoint
- (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n) /=.
+ (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
rewrite Hfg; apply contractive_S, IH; auto using dist_S.
Qed.
@@ -206,21 +206,21 @@ Section cofe_mor.
Program Instance cofe_mor_compl : Compl (cofeMor A B) := λ c,
{| cofe_mor_car x := compl (fun_chain c x) |}.
Next Obligation.
- intros c n x y Hx. by rewrite (conv_compl (fun_chain c x) n)
- (conv_compl (fun_chain c y) n) /= Hx.
+ intros c n x y Hx. by rewrite (conv_compl n (fun_chain c x))
+ (conv_compl n (fun_chain c y)) /= Hx.
Qed.
Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
Proof.
split.
- intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
- intros Hfg k; apply equiv_dist; intros n; apply Hfg.
+ intros Hfg k; apply equiv_dist=> n; apply Hfg.
- intros n; split.
+ by intros f x.
+ by intros f g ? x.
+ by intros f g h ?? x; transitivity (g x).
- by intros n f g ? x; apply dist_S.
- - intros c n x; simpl.
- by rewrite (conv_compl (fun_chain c x) n) /=.
+ - intros n c x; simpl.
+ by rewrite (conv_compl n (fun_chain c x)) /=.
Qed.
Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.
@@ -278,8 +278,8 @@ Section product.
rewrite !equiv_dist; naive_solver.
- apply _.
- by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
- - intros c n; split. apply (conv_compl (chain_map fst c) n).
- apply (conv_compl (chain_map snd c) n).
+ - intros n c; split. apply (conv_compl n (chain_map fst c)).
+ apply (conv_compl n (chain_map snd c)).
Qed.
Canonical Structure prodC : cofeT := CofeT prod_cofe_mixin.
Global Instance pair_timeless (x : A) (y : B) :
@@ -311,7 +311,7 @@ Section discrete_cofe.
- intros x y; split; [done|intros Hn; apply (Hn 0)].
- done.
- done.
- - intros c n. rewrite /compl /discrete_compl /=.
+ - intros n c. rewrite /compl /discrete_compl /=.
symmetry; apply (chain_cauchy c 0 (S n)); omega.
Qed.
Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
@@ -354,7 +354,7 @@ Section later.
+ by intros [x] [y].
+ by intros [x] [y] [z] ??; transitivity y.
- intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
- - intros c [|n]; [done|by apply (conv_compl (later_chain c) n)].
+ - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
Qed.
Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
Global Instance Next_contractive : Contractive (@Next A).
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 6874a99fa..dac844a64 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -60,8 +60,8 @@ Program Instance tower_compl : Compl tower := λ c,
{| tower_car n := compl (tower_chain c n) |}.
Next Obligation.
intros c k; apply equiv_dist=> n.
- by rewrite (conv_compl (tower_chain c k) n)
- (conv_compl (tower_chain c (S k)) n) /= (g_tower (c (S n)) k).
+ by rewrite (conv_compl n (tower_chain c k))
+ (conv_compl n (tower_chain c (S k))) /= (g_tower (c (S n)) k).
Qed.
Definition tower_cofe_mixin : CofeMixin tower.
Proof.
@@ -74,7 +74,7 @@ Proof.
+ by intros X Y Z ?? n; transitivity (Y n).
- intros k X Y HXY n; apply dist_S.
by rewrite -(g_tower X) (HXY (S n)) g_tower.
- - intros c n k; rewrite /= (conv_compl (tower_chain c k) n).
+ - intros n c k; rewrite /= (conv_compl n (tower_chain c k)).
apply (chain_cauchy c); lia.
Qed.
Definition T : cofeT := CofeT tower_cofe_mixin.
@@ -189,8 +189,8 @@ Qed.
Definition unfold (X : T) : F T T := compl (unfold_chain X).
Instance unfold_ne : Proper (dist n ==> dist n) unfold.
Proof.
- intros n X Y HXY. by rewrite /unfold (conv_compl (unfold_chain X) n)
- (conv_compl (unfold_chain Y) n) /= (HXY (S (S n))).
+ intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
+ (conv_compl n (unfold_chain Y)) /= (HXY (S (S n))).
Qed.
Program Definition fold (X : F T T) : T :=
@@ -210,7 +210,7 @@ Proof.
rewrite equiv_dist; intros n k; unfold unfold, fold; simpl.
rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
transitivity (map (ff n, gg n) (X (S (n + k)))).
- { rewrite /unfold (conv_compl (unfold_chain X) n).
+ { rewrite /unfold (conv_compl n (unfold_chain X)).
rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
rewrite f_S -!map_comp; apply (contractive_ne map); split=> Y.
@@ -229,7 +229,7 @@ Proof.
rewrite (map_ff_gg _ _ _ H).
apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
- intros X; rewrite equiv_dist=> n /=.
- rewrite /unfold /= (conv_compl (unfold_chain (fold X)) n) /=.
+ rewrite /unfold /= (conv_compl n (unfold_chain (fold X))) /=.
rewrite g_S -!map_comp -{2}(map_id _ _ X).
apply (contractive_ne map); split => Y /=.
+ apply dist_le with n; last omega.
diff --git a/algebra/excl.v b/algebra/excl.v
index 31a9fd774..c340c7245 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -27,7 +27,7 @@ Inductive excl_dist `{Dist A} : Dist (excl A) :=
| ExclUnit_dist n : ExclUnit ≡{n}≡ ExclUnit
| ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
Existing Instance excl_dist.
-Global Instance Excl_ne : Proper (dist n ==> dist n) (@Excl A).
+Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A).
Proof. by constructor. Qed.
Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A).
Proof. by constructor. Qed.
@@ -58,13 +58,13 @@ Proof.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
- by inversion_clear 1; constructor; apply dist_S.
- - intros c n; unfold compl, excl_compl.
+ - intros n c; unfold compl, excl_compl.
destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|].
{ assert (c 1 = Excl x) by (by destruct (c 1); simplify_eq/=).
assert (∃ y, c (S n) = Excl y) as [y Hy].
{ feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. }
rewrite Hy; constructor.
- by rewrite (conv_compl (excl_chain c x Hx) n) /= Hy. }
+ by rewrite (conv_compl n (excl_chain c x Hx)) /= Hy. }
feed inversion (chain_cauchy c 0 (S n)); first lia;
constructor; destruct (c 1); simplify_eq/=.
Qed.
@@ -161,9 +161,9 @@ Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.
(** Updates *)
Lemma excl_update (x : A) y : ✓ y → Excl x ~~> y.
-Proof. by destruct y; intros ? [?| |]. Qed.
+Proof. destruct y; by intros ?? [?| |]. Qed.
Lemma excl_updateP (P : excl A → Prop) x y : ✓ y → P y → Excl x ~~>: P.
-Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed.
+Proof. intros ?? n z ?; exists y. by destruct y, z as [?| |]. Qed.
End excl.
Arguments exclC : clear implicits.
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 92248e87f..7485fd19f 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -24,7 +24,7 @@ Proof.
+ by intros m1 m2 ? k.
+ by intros m1 m2 m3 ?? k; transitivity (m2 !! k).
- by intros n m1 m2 ? k; apply dist_S.
- - intros c n k; rewrite /compl /map_compl lookup_imap.
+ - intros n c k; rewrite /compl /map_compl lookup_imap.
feed inversion (λ H, chain_cauchy c 0 (S n) H k); simpl; auto with lia.
by rewrite conv_compl /=; apply reflexive_eq.
Qed.
@@ -61,7 +61,7 @@ Proof.
[by constructor|by apply lookup_ne].
Qed.
-Global Instance map_timeless `{∀ a : A, Timeless a} (m : gmap K A) : Timeless m.
+Global Instance map_timeless `{∀ a : A, Timeless a} m : Timeless m.
Proof. by intros m' ? i; apply (timeless _). Qed.
Instance map_empty_timeless : Timeless (∅ : gmap K A).
@@ -140,7 +140,7 @@ Proof.
by rewrite !lookup_unit; apply cmra_unit_preservingN.
- intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- - intros x y n; rewrite map_includedN_spec=> ? i.
+ - intros n x y; rewrite map_includedN_spec=> ? i.
by rewrite lookup_op lookup_minus cmra_op_minus.
Qed.
Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A).
@@ -248,8 +248,8 @@ Qed.
Lemma map_insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q.
Proof.
- intros Hx%option_updateP' HP mf n Hm.
- destruct (Hx (mf !! i) n) as ([y|]&?&?); try done.
+ intros Hx%option_updateP' HP n mf Hm.
+ destruct (Hx n (mf !! i)) as ([y|]&?&?); try done.
{ by generalize (Hm i); rewrite lookup_op; simplify_map_eq. }
exists (<[i:=y]> m); split; first by auto.
intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm.
@@ -276,8 +276,8 @@ Lemma map_singleton_updateP_empty `{Empty A, !CMRAIdentity A}
(P : A → Prop) (Q : gmap K A → Prop) i :
∅ ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
Proof.
- intros Hx HQ gf n Hg.
- destruct (Hx (from_option ∅ (gf !! i)) n) as (y&?&Hy).
+ intros Hx HQ n gf Hg.
+ destruct (Hx n (from_option ∅ (gf !! i))) as (y&?&Hy).
{ move:(Hg i). rewrite !left_id.
case _: (gf !! i); simpl; auto using cmra_empty_valid. }
exists {[ i := y ]}; split; first by auto.
@@ -296,7 +296,7 @@ Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma map_updateP_alloc_strong (Q : gmap K A → Prop) (I : gset K) m x :
✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
Proof.
- intros ? HQ mf n Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))).
+ intros ? HQ n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))).
assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]].
{ rewrite -not_elem_of_union -map_dom_op -not_elem_of_union; apply is_fresh. }
exists (<[i:=x]>m); split.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 3d9fd3d85..b43d242b1 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -37,8 +37,8 @@ Section iprod_cofe.
+ by intros f g ? x.
+ by intros f g h ?? x; transitivity (g x).
- intros n f g Hfg x; apply dist_S, Hfg.
- - intros c n x.
- rewrite /compl /iprod_compl (conv_compl (iprod_chain c x) n).
+ - intros n c x.
+ rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)).
apply (chain_cauchy c); lia.
Qed.
Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin.
@@ -55,7 +55,7 @@ Section iprod_cofe.
(** Properties of iprod_insert. *)
Context `{∀ x x' : A, Decision (x = x')}.
- Global Instance iprod_insert_ne x n :
+ Global Instance iprod_insert_ne n x :
Proper (dist n ==> dist n ==> dist n) (iprod_insert x).
Proof.
intros y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert.
@@ -94,7 +94,7 @@ Section iprod_cofe.
(** Properties of iprod_singletom. *)
Context `{∀ x : A, Empty (B x)}.
- Global Instance iprod_singleton_ne x n :
+ Global Instance iprod_singleton_ne n x :
Proper (dist n ==> dist n) (iprod_singleton x).
Proof. by intros y1 y2 Hy; rewrite /iprod_singleton Hy. Qed.
Global Instance iprod_singleton_proper x :
@@ -182,7 +182,7 @@ Section iprod_cmra.
y1 ~~>: P → (∀ y2, P y2 → Q (iprod_insert x y2 g)) →
iprod_insert x y1 g ~~>: Q.
Proof.
- intros Hy1 HP gf n Hg. destruct (Hy1 (gf x) n) as (y2&?&?).
+ intros Hy1 HP n gf Hg. destruct (Hy1 n (gf x)) as (y2&?&?).
{ move: (Hg x). by rewrite iprod_lookup_op iprod_lookup_insert. }
exists (iprod_insert x y2 g); split; [auto|].
intros x'; destruct (decide (x' = x)) as [->|];
@@ -242,7 +242,7 @@ Section iprod_cmra.
Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) :
∅ ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ∅ ~~>: Q.
Proof.
- intros Hx HQ gf n Hg. destruct (Hx (gf x) n) as (y2&?&?); first apply Hg.
+ intros Hx HQ n gf Hg. destruct (Hx n (gf x)) as (y2&?&?); first apply Hg.
exists (iprod_singleton x y2); split; [by apply HQ|].
intros x'; destruct (decide (x' = x)) as [->|].
- by rewrite iprod_lookup_op iprod_lookup_singleton.
diff --git a/algebra/option.v b/algebra/option.v
index eef547354..3882532bd 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -31,12 +31,12 @@ Proof.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
- by inversion_clear 1; constructor; apply dist_S.
- - intros c n; unfold compl, option_compl.
+ - intros n c; unfold compl, option_compl.
destruct (Some_dec (c 1)) as [[x Hx]|].
{ assert (is_Some (c (S n))) as [y Hy].
{ feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. }
rewrite Hy; constructor.
- by rewrite (conv_compl (option_chain c x Hx) n) /= Hy. }
+ by rewrite (conv_compl n (option_chain c x Hx)) /= Hy. }
feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence.
constructor.
Qed.
@@ -147,9 +147,9 @@ Proof. by destruct x. Qed.
Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q.
Proof.
- intros Hx Hy [y|] n ?.
- { destruct (Hx y n) as (y'&?&?); auto. exists (Some y'); auto. }
- destruct (Hx (unit x) n) as (y'&?&?); rewrite ?cmra_unit_r; auto.
+ intros Hx Hy n [y|] ?.
+ { destruct (Hx n y) as (y'&?&?); auto. exists (Some y'); auto. }
+ destruct (Hx n (unit x)) as (y'&?&?); rewrite ?cmra_unit_r; auto.
by exists (Some y'); split; [auto|apply cmra_validN_op_l with (unit x)].
Qed.
Lemma option_updateP' (P : A → Prop) x :
@@ -161,7 +161,7 @@ Proof.
Qed.
Lemma option_update_None `{Empty A, !CMRAIdentity A} : ∅ ~~> Some ∅.
Proof.
- intros [x|] n ?; rewrite /op /cmra_op /validN /cmra_validN /= ?left_id;
+ intros n [x|] ?; rewrite /op /cmra_op /validN /cmra_validN /= ?left_id;
auto using cmra_empty_valid.
Qed.
End cmra.
diff --git a/algebra/upred.v b/algebra/upred.v
index de250643a..4a0c0817b 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -5,8 +5,8 @@ Local Hint Extern 10 (_ ≤ _) => omega.
Record uPred (M : cmraT) : Type := IProp {
uPred_holds :> nat → M → Prop;
- uPred_ne x1 x2 n : uPred_holds n x1 → x1 ≡{n}≡ x2 → uPred_holds n x2;
- uPred_weaken x1 x2 n1 n2 :
+ uPred_ne n x1 x2 : uPred_holds n x1 → x1 ≡{n}≡ x2 → uPred_holds n x2;
+ uPred_weaken n1 n2 x1 x2 :
uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → uPred_holds n2 x2
}.
Arguments uPred_holds {_} _ _ _ : simpl never.
@@ -21,28 +21,28 @@ Arguments uPred_holds {_} _%I _ _.
Section cofe.
Context {M : cmraT}.
- Instance uPred_equiv : Equiv (uPred M) := λ P Q, ∀ x n,
+ Instance uPred_equiv : Equiv (uPred M) := λ P Q, ∀ n x,
✓{n} x → P n x ↔ Q n x.
- Instance uPred_dist : Dist (uPred M) := λ n P Q, ∀ x n',
+ Instance uPred_dist : Dist (uPred M) := λ n P Q, ∀ n' x,
n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x.
Program Instance uPred_compl : Compl (uPred M) := λ c,
{| uPred_holds n x := c (S n) n x |}.
- Next Obligation. by intros c x y n ??; simpl in *; apply uPred_ne with x. Qed.
+ Next Obligation. by intros c n x y ??; simpl in *; apply uPred_ne with x. Qed.
Next Obligation.
- intros c x1 x2 n1 n2 ????; simpl in *.
+ intros c n1 n2 x1 x2 ????; simpl in *.
apply (chain_cauchy c n2 (S n1)); eauto using uPred_weaken.
Qed.
Definition uPred_cofe_mixin : CofeMixin (uPred M).
Proof.
split.
- intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
- intros HPQ x n ?; apply HPQ with n; auto.
+ intros HPQ n x ?; apply HPQ with n; auto.
- intros n; split.
+ by intros P x i.
+ by intros P Q HPQ x i ??; symmetry; apply HPQ.
- + by intros P Q Q' HP HQ x i ??; transitivity (Q i x);[apply HP|apply HQ].
- - intros n P Q HPQ x i ??; apply HPQ; auto.
- - intros c n x i ??; symmetry; apply (chain_cauchy c i (S n)); auto.
+ + by intros P Q Q' HP HQ i x ??; transitivity (Q i x);[apply HP|apply HQ].
+ - intros n P Q HPQ i x ??; apply HPQ; auto.
+ - intros n c i x ??; symmetry; apply (chain_cauchy c i (S n)); auto.
Qed.
Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
End cofe.
@@ -56,7 +56,7 @@ Proof. by intros x1 x2 Hx; apply uPred_ne', equiv_dist. Qed.
Lemma uPred_holds_ne {M} (P1 P2 : uPred M) n x :
P1 ≡{n}≡ P2 → ✓{n} x → P1 n x → P2 n x.
Proof. intros HP ?; apply HP; auto. Qed.
-Lemma uPred_weaken' {M} (P : uPred M) x1 x2 n1 n2 :
+Lemma uPred_weaken' {M} (P : uPred M) n1 n2 x1 x2 :
x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → P n1 x1 → P n2 x2.
Proof. eauto using uPred_weaken. Qed.
@@ -69,34 +69,32 @@ Next Obligation.
naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
Qed.
Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
- `{!CMRAMonotone f} :
- Proper (dist n ==> dist n) (uPred_map f).
+ `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
Proof.
- by intros n x1 x2 Hx y n'; split; apply Hx; auto using validN_preserving.
+ by intros x1 x2 Hx n' y; split; apply Hx; auto using validN_preserving.
Qed.
Lemma uPred_map_id {M : cmraT} (P : uPred M): uPred_map cid P ≡ P.
-Proof. by intros x n ?. Qed.
+Proof. by intros n x ?. Qed.
Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
- `{!CMRAMonotone f} `{!CMRAMonotone g}
- (P : uPred M3):
+ `{!CMRAMonotone f, !CMRAMonotone g} (P : uPred M3):
uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
-Proof. by intros x n Hx. Qed.
+Proof. by intros n x Hx. Qed.
Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
- `{!CMRAMonotone f} `{!CMRAMonotone g}:
- (∀ x, f x ≡ g x) -> ∀ x, uPred_map f x ≡ uPred_map g x.
-Proof. move=> H x P n Hx /=. by rewrite /uPred_holds /= H. Qed.
+ `{!CMRAMonotone f, !CMRAMonotone g} :
+ (∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
+Proof. move=> Hfg x P n Hx /=. by rewrite /uPred_holds /= Hfg. Qed.
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
`{!CMRAMonotone f, !CMRAMonotone g} n :
f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g.
Proof.
- by intros Hfg P y n' ??;
+ by intros Hfg P n' y ??;
rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Qed.
(** logical entailement *)
-Definition uPred_entails {M} (P Q : uPred M) := ∀ x n, ✓{n} x → P n x → Q n x.
+Definition uPred_entails {M} (P Q : uPred M) := ∀ n x, ✓{n} x → P n x → Q n x.
Hint Extern 0 (uPred_entails _ _) => reflexivity.
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
@@ -113,16 +111,16 @@ Program Definition uPred_or {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := P n x ∨ Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_impl {M} (P Q : uPred M) : uPred M :=
- {| uPred_holds n x := ∀ x' n',
+ {| uPred_holds n x := ∀ n' x',
x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}.
Next Obligation.
- intros M P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
- destruct (cmra_included_dist_l x1 x2 x1' n1) as (x2'&?&Hx2); auto.
+ intros M P Q n1 x1' x1 HPQ Hx1 n2 x2 ????.
+ destruct (cmra_included_dist_l n1 x1 x2 x1') as (x2'&?&Hx2); auto.
assert (x2' ≡{n2}≡ x2) as Hx2' by (by apply dist_le with n1).
assert (✓{n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
eauto using uPred_weaken, uPred_ne.
Qed.
-Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
+Next Obligation. intros M P Q [|n] x1 x2; auto with lia. Qed.
Program Definition uPred_forall {M A} (Ψ : A → uPred M) : uPred M :=
{| uPred_holds n x := ∀ a, Ψ a n x |}.
@@ -138,51 +136,51 @@ Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
Program Definition uPred_sep {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
Next Obligation.
- by intros M P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
+ by intros M P Q n x y (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
Qed.
Next Obligation.
- intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??.
+ intros M P Q n1 n2 x y (x1&x2&Hx&?&?) Hxy ??.
assert (∃ x2', y ≡{n2}≡ x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
{ destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using cmra_included_l.
apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. }
clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
- - apply uPred_weaken with x1 n1; eauto using cmra_validN_op_l.
- - apply uPred_weaken with x2 n1; eauto using cmra_validN_op_r.
+ - apply uPred_weaken with n1 x1; eauto using cmra_validN_op_l.
+ - apply uPred_weaken with n1 x2; eauto using cmra_validN_op_r.
Qed.
Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
- {| uPred_holds n x := ∀ x' n',
+ {| uPred_holds n x := ∀ n' x',
n' ≤ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
Next Obligation.
- intros M P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *.
+ intros M P Q n1 x1 x2 HPQ Hx n2 x3 ???; simpl in *.
rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
- by rewrite (dist_le _ _ _ n2 Hx).
+ by rewrite (dist_le _ _ _ _ Hx).
Qed.
Next Obligation.
- intros M P Q x1 x2 n1 n2 HPQ ??? x3 n3 ???; simpl in *.
- apply uPred_weaken with (x1 â‹… x3) n3;
+ intros M P Q n1 n2 x1 x2 HPQ ??? n3 x3 ???; simpl in *.
+ apply uPred_weaken with n3 (x1 â‹… x3);
eauto using cmra_validN_included, cmra_preserving_r.
Qed.
Program Definition uPred_later {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
-Next Obligation. intros M P ?? [|n]; eauto using uPred_ne,(dist_le (A:=M)). Qed.
+Next Obligation. intros M P [|n] ??; eauto using uPred_ne,(dist_le (A:=M)). Qed.
Next Obligation.
- intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken,cmra_validN_S; try lia.
+ intros M P [|n1] [|n2] x1 x2; eauto using uPred_weaken,cmra_validN_S; try lia.
Qed.
Program Definition uPred_always {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (unit x) |}.
Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
Next Obligation.
- intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
+ intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (unit x1);
eauto using cmra_unit_preserving, cmra_unit_validN.
Qed.
Program Definition uPred_ownM {M : cmraT} (a : M) : uPred M :=
{| uPred_holds n x := a ≼{n} x |}.
-Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite -Hx. Qed.
+Next Obligation. by intros M a n x1 x2 [a' ?] Hx; exists a'; rewrite -Hx. Qed.
Next Obligation.
- intros M a x1 x n1 n2 [a' Hx1] [x2 Hx] ??.
+ intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] ??.
exists (a' â‹… x2). by rewrite (assoc op) -(dist_le _ _ _ _ Hx1) // Hx.
Qed.
Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
@@ -251,7 +249,7 @@ Qed.
(** Non-expansiveness and setoid morphisms *)
Global Instance const_proper : Proper (iff ==> (≡)) (@uPred_const M).
-Proof. by intros φ1 φ2 Hφ ? [|n] ?; try apply Hφ. Qed.
+Proof. by intros φ1 φ2 Hφ [|n] ??; try apply Hφ. Qed.
Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
Proof.
intros P P' HP Q Q' HQ; split; intros [??]; split; by apply HP || by apply HQ.
@@ -274,7 +272,7 @@ Global Instance impl_proper :
Proper ((≡) ==> (≡) ==> (≡)) (@uPred_impl M) := ne_proper_2 _.
Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
Proof.
- intros P P' HP Q Q' HQ x n' ??; split; intros (x1&x2&?&?&?); cofe_subst x;
+ intros P P' HP Q Q' HQ n' x ??; split; intros (x1&x2&?&?&?); cofe_subst x;
exists x1, x2; split_ands; try (apply HP || apply HQ);
eauto using cmra_validN_op_l, cmra_validN_op_r.
Qed.
@@ -283,7 +281,7 @@ Global Instance sep_proper :
Global Instance wand_ne n :
Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
Proof.
- intros P P' HP Q Q' HQ x n' ??; split; intros HPQ x' n'' ???;
+ intros P P' HP Q Q' HQ n' x ??; split; intros HPQ n'' x' ???;
apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Qed.
Global Instance wand_proper :
@@ -291,7 +289,7 @@ Global Instance wand_proper :
Global Instance eq_ne (A : cofeT) n :
Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
Proof.
- intros x x' Hx y y' Hy z n'; split; intros; simpl in *.
+ intros x x' Hx y y' Hy n' z; split; intros; simpl in *.
- by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
- by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
Qed.
@@ -299,30 +297,30 @@ Global Instance eq_proper (A : cofeT) :
Proper ((≡) ==> (≡) ==> (≡)) (@uPred_eq M A) := ne_proper_2 _.
Global Instance forall_ne A :
Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
-Proof. by intros n Ψ1 Ψ2 HΨ x n'; split; intros HP a; apply HΨ. Qed.
+Proof. by intros n Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed.
Global Instance forall_proper A :
Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_forall M A).
-Proof. by intros Ψ1 Ψ2 HΨ x n'; split; intros HP a; apply HΨ. Qed.
+Proof. by intros Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed.
Global Instance exists_ne A :
Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
Proof. by intros n P1 P2 HP x; split; intros [a ?]; exists a; apply HP. Qed.
Global Instance exist_proper A :
Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_exist M A).
-Proof. by intros P1 P2 HP x n'; split; intros [a ?]; exists a; apply HP. Qed.
+Proof. by intros P1 P2 HP n' x; split; intros [a ?]; exists a; apply HP. Qed.
Global Instance later_contractive : Contractive (@uPred_later M).
Proof.
- intros n P Q HPQ x [|n'] ??; simpl; [done|].
+ intros n P Q HPQ [|n'] x ??; simpl; [done|].
apply (HPQ n'); eauto using cmra_validN_S.
Qed.
Global Instance later_proper :
Proper ((≡) ==> (≡)) (@uPred_later M) := ne_proper _.
Global Instance always_ne n: Proper (dist n ==> dist n) (@uPred_always M).
-Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_validN. Qed.
+Proof. intros P1 P2 HP n' x; split; apply HP; eauto using cmra_unit_validN. Qed.
Global Instance always_proper :
Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _.
Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
Proof.
- by intros a1 a2 Ha x n'; split; intros [a' ?]; exists a'; simpl; first
+ by intros a1 a2 Ha n' x; split; intros [a' ?]; exists a'; simpl; first
[rewrite -(dist_le _ _ _ _ Ha); last lia
|rewrite (dist_le _ _ _ _ Ha); last lia].
Qed.
@@ -336,43 +334,41 @@ Global Instance iff_proper :
Lemma const_intro φ P : φ → P ⊑ ■φ.
Proof. by intros ???. Qed.
Lemma const_elim φ Q R : Q ⊑ ■φ → (φ → Q ⊑ R) → Q ⊑ R.
-Proof. intros HQP HQR x n ??; apply HQR; first eapply (HQP _ n); eauto. Qed.
-Lemma True_intro P : P ⊑ True.
-Proof. by apply const_intro. Qed.
+Proof. intros HQP HQR n x ??; apply HQR; first eapply (HQP n); eauto. Qed.
Lemma False_elim P : False ⊑ P.
-Proof. by intros x n ?. Qed.
+Proof. by intros n x ?. Qed.
Lemma and_elim_l P Q : (P ∧ Q) ⊑ P.
-Proof. by intros x n ? [??]. Qed.
+Proof. by intros n x ? [??]. Qed.
Lemma and_elim_r P Q : (P ∧ Q) ⊑ Q.
-Proof. by intros x n ? [??]. Qed.
+Proof. by intros n x ? [??]. Qed.
Lemma and_intro P Q R : P ⊑ Q → P ⊑ R → P ⊑ (Q ∧ R).
-Proof. intros HQ HR x n ??; split; auto. Qed.
+Proof. intros HQ HR n x ??; split; auto. Qed.
Lemma or_intro_l P Q : P ⊑ (P ∨ Q).
-Proof. intros x n ??; left; auto. Qed.
+Proof. intros n x ??; left; auto. Qed.
Lemma or_intro_r P Q : Q ⊑ (P ∨ Q).
-Proof. intros x n ??; right; auto. Qed.
+Proof. intros n x ??; right; auto. Qed.
Lemma or_elim P Q R : P ⊑ R → Q ⊑ R → (P ∨ Q) ⊑ R.
-Proof. intros HP HQ x n ? [?|?]. by apply HP. by apply HQ. Qed.
+Proof. intros HP HQ n x ? [?|?]. by apply HP. by apply HQ. Qed.
Lemma impl_intro_r P Q R : (P ∧ Q) ⊑ R → P ⊑ (Q → R).
Proof.
- intros HQ x n ?? x' n' ????; apply HQ; naive_solver eauto using uPred_weaken.
+ intros HQ; repeat intro; apply HQ; naive_solver eauto using uPred_weaken.
Qed.
Lemma impl_elim P Q R : P ⊑ (Q → R) → P ⊑ Q → P ⊑ R.
-Proof. by intros HP HP' x n ??; apply HP with x n, HP'. Qed.
+Proof. by intros HP HP' n x ??; apply HP with n x, HP'. Qed.
Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊑ Ψ a) → P ⊑ (∀ a, Ψ a).
-Proof. by intros HPΨ x n ?? a; apply HPΨ. Qed.
+Proof. by intros HPΨ n x ?? a; apply HPΨ. Qed.
Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊑ Ψ a.
-Proof. intros x n ? HP; apply HP. Qed.
+Proof. intros n x ? HP; apply HP. Qed.
Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊑ (∃ a, Ψ a).
-Proof. by intros x n ??; exists a. Qed.
+Proof. by intros n x ??; exists a. Qed.
Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊑ Q) → (∃ a, Φ a) ⊑ Q.
-Proof. by intros HΦΨ x n ? [a ?]; apply HΦΨ with a. Qed.
+Proof. by intros HΦΨ n x ? [a ?]; apply HΦΨ with a. Qed.
Lemma eq_refl {A : cofeT} (a : A) P : P ⊑ (a ≡ a).
-Proof. by intros x n ??; simpl. Qed.
+Proof. by intros n x ??; simpl. Qed.
Lemma eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P
`{HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : P ⊑ (a ≡ b) → P ⊑ Ψ a → P ⊑ Ψ b.
Proof.
- intros Hab Ha x n ??; apply HΨ with n a; auto. by symmetry; apply Hab with x.
+ intros Hab Ha n x ??; apply HΨ with n a; auto. by symmetry; apply Hab with x.
Qed.
Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
True ⊑ (a ≡ b) → a ≡ b.
@@ -381,9 +377,11 @@ Proof.
apply cmra_valid_validN, cmra_empty_valid.
Qed.
Lemma iff_equiv P Q : True ⊑ (P ↔ Q) → P ≡ Q.
-Proof. by intros HPQ x n ?; split; intros; apply HPQ with x n. Qed.
+Proof. by intros HPQ n x ?; split; intros; apply HPQ with n x. Qed.
(* Derived logical stuff *)
+Lemma True_intro P : P ⊑ True.
+Proof. by apply const_intro. Qed.
Lemma and_elim_l' P Q R : P ⊑ R → (P ∧ Q) ⊑ R.
Proof. by rewrite and_elim_l. Qed.
Lemma and_elim_r' P Q R : Q ⊑ R → (P ∧ Q) ⊑ R.
@@ -548,23 +546,23 @@ Qed.
(* BI connectives *)
Lemma sep_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ★ P') ⊑ (Q ★ Q').
Proof.
- intros HQ HQ' x n' ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
+ intros HQ HQ' n' x ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
Qed.
Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
Proof.
- intros P x n Hvalid; split.
+ intros P n x Hvalid; split.
- intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
- by intros ?; exists (unit x), x; rewrite cmra_unit_l.
Qed.
Global Instance sep_comm : Comm (≡) (@uPred_sep M).
Proof.
- by intros P Q x n ?; split;
+ by intros P Q n x ?; split;
intros (x1&x2&?&?&?); exists x2, x1; rewrite (comm op).
Qed.
Global Instance sep_assoc : Assoc (≡) (@uPred_sep M).
Proof.
- intros P Q R x n ?; split.
+ intros P Q R n x ?; split.
- intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 â‹… y1), y2; split_ands; auto.
+ by rewrite -(assoc op) -Hy -Hx.
+ by exists x1, y1.
@@ -574,12 +572,12 @@ Proof.
Qed.
Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
Proof.
- intros HPQR x n ?? x' n' ???; apply HPQR; auto.
+ intros HPQR n x ?? n' x' ???; apply HPQR; auto.
exists x, x'; split_ands; auto.
- eapply uPred_weaken with x n; eauto using cmra_validN_op_l.
+ eapply uPred_weaken with n x; eauto using cmra_validN_op_l.
Qed.
Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊑ Q.
-Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
+Proof. by intros n x ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
(* Derived BI Stuff *)
Hint Resolve sep_mono.
@@ -667,33 +665,33 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
(* Later *)
Lemma later_mono P Q : P ⊑ Q → ▷ P ⊑ ▷ Q.
-Proof. intros HP x [|n] ??; [done|apply HP; eauto using cmra_validN_S]. Qed.
+Proof. intros HP [|n] x ??; [done|apply HP; eauto using cmra_validN_S]. Qed.
Lemma later_intro P : P ⊑ ▷ P.
Proof.
- intros x [|n] ??; simpl in *; [done|].
- apply uPred_weaken with x (S n); eauto using cmra_validN_S.
+ intros [|n] x ??; simpl in *; [done|].
+ apply uPred_weaken with (S n) x; eauto using cmra_validN_S.
Qed.
Lemma löb P : (▷ P → P) ⊑ P.
Proof.
- intros x n ? HP; induction n as [|n IH]; [by apply HP|].
- apply HP, IH, uPred_weaken with x (S n); eauto using cmra_validN_S.
+ intros n x ? HP; induction n as [|n IH]; [by apply HP|].
+ apply HP, IH, uPred_weaken with (S n) x; eauto using cmra_validN_S.
Qed.
Lemma later_True' : True ⊑ (▷ True : uPred M).
-Proof. by intros x [|n]. Qed.
+Proof. by intros [|n] x. Qed.
Lemma later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I.
-Proof. by intros x [|n]; split. Qed.
+Proof. by intros [|n] x; split. Qed.
Lemma later_or P Q : (▷ (P ∨ Q))%I ≡ (▷ P ∨ ▷ Q)%I.
-Proof. intros x [|n]; simpl; tauto. Qed.
+Proof. intros [|n] x; simpl; tauto. Qed.
Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a)%I ≡ (∀ a, ▷ Φ a)%I.
-Proof. by intros x [|n]. Qed.
+Proof. by intros [|n] x. Qed.
Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊑ (▷ ∃ a, Φ a).
-Proof. by intros x [|[|n]]. Qed.
+Proof. by intros [|[|n]] x. Qed.
Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
(▷ ∃ a, Φ a)%I ≡ (∃ a, ▷ Φ a)%I.
-Proof. intros x [|[|n]]; split; done || by exists inhabitant; simpl. Qed.
+Proof. intros [|[|n]] x; split; done || by exists inhabitant; simpl. Qed.
Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
Proof.
- intros x n ?; split.
+ intros n x ?; split.
- destruct n as [|n]; simpl.
{ by exists x, (unit x); rewrite cmra_unit_r. }
intros (x1&x2&Hx&?&?); destruct (cmra_extend_op n x x1 x2)
@@ -730,13 +728,10 @@ Qed.
Lemma always_const φ : (□ ■φ : uPred M)%I ≡ (■φ)%I.
Proof. done. Qed.
Lemma always_elim P : □ P ⊑ P.
-Proof.
- intros x n ??; apply uPred_weaken with (unit x) n;
- eauto using cmra_included_unit.
-Qed.
+Proof. intros n x ?; simpl; eauto using uPred_weaken, cmra_included_unit. Qed.
Lemma always_intro' P Q : □ P ⊑ Q → □ P ⊑ □ Q.
Proof.
- intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
+ intros HPQ n x ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
by rewrite cmra_unit_idemp.
Qed.
Lemma always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
@@ -749,11 +744,11 @@ Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a)%I ≡ (∃ a,
Proof. done. Qed.
Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊑ □ (P ★ Q).
Proof.
- intros x n ? [??]; exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
+ intros n x ? [??]; exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
Qed.
Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊑ (□ P ★ Q).
Proof.
- intros x n ? [??]; exists (unit x), x; simpl in *.
+ intros n x ? [??]; exists (unit x), x; simpl in *.
by rewrite cmra_unit_l cmra_unit_idemp.
Qed.
Lemma always_later P : (□ ▷ P)%I ≡ (▷ □ P)%I.
@@ -804,7 +799,7 @@ Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
Lemma ownM_op (a1 a2 : M) :
uPred_ownM (a1 ⋅ a2) ≡ (uPred_ownM a1 ★ uPred_ownM a2)%I.
Proof.
- intros x n ?; split.
+ intros n x ?; split.
- intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
split. by exists (unit a1); rewrite cmra_unit_r. by exists z.
- intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
@@ -813,34 +808,34 @@ Proof.
Qed.
Lemma always_ownM_unit (a : M) : (□ uPred_ownM (unit a))%I ≡ uPred_ownM (unit a).
Proof.
- intros x n; split; [by apply always_elim|intros [a' Hx]]; simpl.
+ intros n x; split; [by apply always_elim|intros [a' Hx]]; simpl.
rewrite -(cmra_unit_idemp a) Hx.
apply cmra_unit_preservingN, cmra_includedN_l.
Qed.
Lemma always_ownM (a : M) : unit a ≡ a → (□ uPred_ownM a)%I ≡ uPred_ownM a.
Proof. by intros <-; rewrite always_ownM_unit. Qed.
Lemma ownM_something : True ⊑ ∃ a, uPred_ownM a.
-Proof. intros x n ??. by exists x; simpl. Qed.
+Proof. intros n x ??. by exists x; simpl. Qed.
Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_ownM ∅.
-Proof. intros x n ??; by exists x; rewrite left_id. Qed.
+Proof. intros n x ??; by exists x; rewrite left_id. Qed.
(* Valid *)
Lemma ownM_valid (a : M) : uPred_ownM a ⊑ ✓ a.
-Proof. intros x n Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
+Proof. intros n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊑ ✓ a.
-Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
+Proof. by intros ? n x ? _; simpl; apply cmra_valid_validN. Qed.
Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊑ False.
-Proof. intros Ha x n ??; apply Ha, cmra_validN_le with n; auto. Qed.
+Proof. intros Ha n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a))%I ≡ (✓ a : uPred M)%I.
Proof. done. Qed.
Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊑ ✓ a.
-Proof. intros r n _; apply cmra_validN_op_l. Qed.
+Proof. intros n x _; apply cmra_validN_op_l. Qed.
(* Own and valid derived *)
Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
Proof. by intros; rewrite ownM_valid valid_elim. Qed.
Global Instance ownM_mono : Proper (flip (≼) ==> (⊑)) (@uPred_ownM M).
-Proof. move=>a b [c H]. rewrite H ownM_op. eauto. Qed.
+Proof. intros x y [z ->]. rewrite ownM_op. eauto. Qed.
(* Products *)
Lemma prod_equivI {A B : cofeT} (x y : A * B) :
@@ -863,16 +858,16 @@ Lemma discrete_validI {A : cofeT} `{∀ x : A, Timeless x}
Proof. done. Qed.
(* Timeless *)
-Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 0 x → P n x.
+Lemma timelessP_spec P : TimelessP P ↔ ∀ n x, ✓{n} x → P 0 x → P n x.
Proof.
split.
- - intros HP x n ??; induction n as [|n]; auto.
- by destruct (HP x (S n)); auto using cmra_validN_S.
- - move=> HP x [|n] /=; auto; left.
- apply HP, uPred_weaken with x n; eauto using cmra_validN_le.
+ - intros HP n x ??; induction n as [|n]; auto.
+ by destruct (HP (S n) x); auto using cmra_validN_S.
+ - move=> HP [|n] x /=; auto; left.
+ apply HP, uPred_weaken with n x; eauto using cmra_validN_le.
Qed.
Global Instance const_timeless φ : TimelessP (■φ : uPred M)%I.
-Proof. by apply timelessP_spec=> x [|n]. Qed.
+Proof. by apply timelessP_spec=> -[|n] x. Qed.
Global Instance and_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∧ Q).
Proof. by intros ??; rewrite /TimelessP later_and or_and_r; apply and_mono. Qed.
Global Instance or_timeless P Q : TimelessP P → TimelessP Q → TimelessP (P ∨ Q).
@@ -881,8 +876,8 @@ Proof.
Qed.
Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
Proof.
- rewrite !timelessP_spec=> HP x [|n] ? HPQ x' [|n'] ????; auto.
- apply HP, HPQ, uPred_weaken with x' (S n'); eauto using cmra_validN_le.
+ rewrite !timelessP_spec=> HP [|n] x ? HPQ [|n'] x' ????; auto.
+ apply HP, HPQ, uPred_weaken with (S n') x'; eauto using cmra_validN_le.
Qed.
Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ★ Q).
Proof.
@@ -893,17 +888,17 @@ Proof.
Qed.
Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q).
Proof.
- rewrite !timelessP_spec=> HP x [|n] ? HPQ x' [|n'] ???; auto.
- apply HP, HPQ, uPred_weaken with x' (S n');
+ rewrite !timelessP_spec=> HP [|n] x ? HPQ [|n'] x' ???; auto.
+ apply HP, HPQ, uPred_weaken with (S n') x';
eauto 3 using cmra_validN_le, cmra_validN_op_r.
Qed.
Global Instance forall_timeless {A} (Ψ : A → uPred M) :
(∀ x, TimelessP (Ψ x)) → TimelessP (∀ x, Ψ x).
-Proof. by setoid_rewrite timelessP_spec=> HΨ x n ?? a; apply HΨ. Qed.
+Proof. by setoid_rewrite timelessP_spec=> HΨ n x ?? a; apply HΨ. Qed.
Global Instance exist_timeless {A} (Ψ : A → uPred M) :
(∀ x, TimelessP (Ψ x)) → TimelessP (∃ x, Ψ x).
Proof.
- by setoid_rewrite timelessP_spec=> HΨ x [|n] ?;
+ by setoid_rewrite timelessP_spec=> HΨ [|n] x ?;
[|intros [a ?]; exists a; apply HΨ].
Qed.
Global Instance always_timeless P : TimelessP P → TimelessP (□ P).
@@ -913,17 +908,17 @@ Proof.
Qed.
Global Instance eq_timeless {A : cofeT} (a b : A) :
Timeless a → TimelessP (a ≡ b : uPred M)%I.
-Proof. by intro; apply timelessP_spec=> x n ??; apply equiv_dist, timeless. Qed.
+Proof. by intro; apply timelessP_spec=> n x ??; apply equiv_dist, timeless. Qed.
Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
Proof.
- intros ?; apply timelessP_spec=> x n ??; apply cmra_included_includedN,
+ intros ?; apply timelessP_spec=> n x ??; apply cmra_included_includedN,
cmra_timeless_included_l; eauto using cmra_validN_le.
Qed.
Lemma timeless_eq {A : cofeT} (a b : A) :
Timeless a → (a ≡ b)%I ≡ (■(a ≡ b) : uPred M)%I.
Proof.
intros ?. apply (anti_symm (⊑)).
- - move=>x n ? EQ /=. eapply timeless_iff; last exact EQ. apply _.
+ - move=>n x ? ? /=. by apply (timeless_iff n a).
- eapply const_elim; first done. move=>->. apply eq_refl.
Qed.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 886b66dc4..d7f0609df 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -49,7 +49,7 @@ Proof.
- apply (IH (Φs1 ++ Φ :: Φs2) (rs1 ++ r2 ⋅ r2' :: rs2)).
{ rewrite /option_list right_id_L.
apply Forall3_app, Forall3_cons; eauto using wptp_le.
- apply uPred_weaken with r2 (k + n); eauto using cmra_included_l. }
+ apply uPred_weaken with (k + n) r2; eauto using cmra_included_l. }
by rewrite -Permutation_middle /= big_op_app.
Qed.
Lemma ht_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
@@ -62,7 +62,7 @@ Proof.
intros Hht ????; apply (nsteps_wptp [Φ] k n ([e1],σ1) (t2,σ2) [r1]);
rewrite /big_op ?right_id; auto.
constructor; last constructor.
- apply Hht with r1 (k + n); eauto using cmra_included_unit.
+ apply Hht with (k + n) r1; eauto using cmra_included_unit.
eapply uPred.const_intro; eauto.
Qed.
Lemma ht_adequacy_own Φ e1 t2 σ1 m σ2 :
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index c9b24371a..79e6b0b9b 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -27,14 +27,14 @@ Lemma wp_lift_step E1 E2
(■φ e2 σ2 ef ∧ ownP σ2) -★ pvs E1 E2 (wp E2 e2 Φ ★ wp_fork ef))
⊑ wp E2 e1 Φ.
Proof.
- intros ? He Hsafe Hstep r n ? Hvs; constructor; auto.
+ intros ? He Hsafe Hstep n r ? Hvs; constructor; auto.
intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1')
as (r'&(r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'.
destruct (wsat_update_pst k (E1 ∪ Ef) σ1 σ1' r1 (r2 ⋅ rf)) as [-> Hws'].
{ by apply ownP_spec; auto. }
{ by rewrite assoc. }
constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)].
- destruct (λ H1 H2 H3, Hwp e2 σ2 ef (update_pst σ2 r1) k H1 H2 H3 rf k Ef σ2)
+ destruct (λ H1 H2 H3, Hwp e2 σ2 ef k (update_pst σ2 r1) H1 H2 H3 rf k Ef σ2)
as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
{ split. destruct k; try eapply Hstep; eauto. apply ownP_spec; auto. }
{ rewrite (comm _ r2) -assoc; eauto using wsat_le. }
@@ -47,10 +47,10 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
(∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
(▷ ∀ e2 ef, ■φ e2 ef → wp E e2 Φ ★ wp_fork ef) ⊑ wp E e1 Φ.
Proof.
- intros He Hsafe Hstep r n ? Hwp; constructor; auto.
+ intros He Hsafe Hstep n r ? Hwp; constructor; auto.
intros rf k Ef σ1 ???; split; [done|]. destruct n as [|n]; first lia.
intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
- destruct (Hwp e2 ef r k) as (r1&r2&Hr&?&?); auto.
+ destruct (Hwp e2 ef k r) as (r1&r2&Hr&?&?); auto.
exists r1,r2; split_ands; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
Qed.
diff --git a/program_logic/model.v b/program_logic/model.v
index 037d39b32..711b5bac8 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -24,9 +24,8 @@ Proof.
rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
by rewrite -later_map_compose.
- - intros A1 A2 B1 B2 n f f' Hf P [???].
- apply upredC_map_ne, resC_map_ne, laterC_map_contractive.
- by intros i ?; apply Hf.
+ - intros A1 A2 B1 B2 n f f' Hf P n' [???].
+ apply upredC_map_ne, resC_map_ne, laterC_map_contractive=>i. by apply Hf.
Qed.
End iProp.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 9fb421ddd..6619abfb1 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -22,7 +22,7 @@ Next Obligation.
intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
destruct (HP (r3⋅rf) k Ef σ) as (r'&?&Hws'); rewrite ?(assoc op); auto.
exists (r' â‹… r3); rewrite -assoc; split; last done.
- apply uPred_weaken with r' k; eauto using cmra_included_l.
+ apply uPred_weaken with k r'; eauto using cmra_included_l.
Qed.
Arguments pvs {_ _} _ _ _%I : simpl never.
Instance: Params (@pvs) 4.
@@ -44,63 +44,63 @@ Proof. apply ne_proper, _. Qed.
Lemma pvs_intro E P : P ⊑ pvs E E P.
Proof.
- intros r n ? HP rf k Ef σ ???; exists r; split; last done.
- apply uPred_weaken with r n; eauto.
+ intros n r ? HP rf k Ef σ ???; exists r; split; last done.
+ apply uPred_weaken with n r; eauto.
Qed.
Lemma pvs_mono E1 E2 P Q : P ⊑ Q → pvs E1 E2 P ⊑ pvs E1 E2 Q.
Proof.
- intros HPQ r n ? HP rf k Ef σ ???.
+ intros HPQ n r ? HP rf k Ef σ ???.
destruct (HP rf k Ef σ) as (r2&?&?); eauto; exists r2; eauto.
Qed.
Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊑ pvs E E P.
Proof.
- rewrite uPred.timelessP_spec=> HP r [|n] ? HP' rf k Ef σ ???; first lia.
+ rewrite uPred.timelessP_spec=> HP [|n] r ? HP' rf k Ef σ ???; first lia.
exists r; split; last done.
- apply HP, uPred_weaken with r n; eauto using cmra_validN_le.
+ apply HP, uPred_weaken with n r; eauto using cmra_validN_le.
Qed.
Lemma pvs_trans E1 E2 E3 P :
E2 ⊆ E1 ∪ E3 → pvs E1 E2 (pvs E2 E3 P) ⊑ pvs E1 E3 P.
Proof.
- intros ? r1 n ? HP1 rf k Ef σ ???.
+ intros ? n r1 ? HP1 rf k Ef σ ???.
destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto.
Qed.
Lemma pvs_mask_frame E1 E2 Ef P :
Ef ∩ (E1 ∪ E2) = ∅ → pvs E1 E2 P ⊑ pvs (E1 ∪ Ef) (E2 ∪ Ef) P.
Proof.
- intros ? r n ? HP rf k Ef' σ ???.
+ intros ? n r ? HP rf k Ef' σ ???.
destruct (HP rf k (Ef∪Ef') σ) as (r'&?&?); rewrite ?(assoc_L _); eauto.
by exists r'; rewrite -(assoc_L _).
Qed.
Lemma pvs_frame_r E1 E2 P Q : (pvs E1 E2 P ★ Q) ⊑ pvs E1 E2 (P ★ Q).
Proof.
- intros r n ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
+ intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
destruct (HP (r2 ⋅ rf) k Ef σ) as (r'&?&?); eauto.
{ by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. }
exists (r' â‹… r2); split; last by rewrite -assoc.
- exists r', r2; split_ands; auto; apply uPred_weaken with r2 n; auto.
+ exists r', r2; split_ands; auto; apply uPred_weaken with n r2; auto.
Qed.
Lemma pvs_openI i P : ownI i P ⊑ pvs {[ i ]} ∅ (▷ P).
Proof.
- intros r [|n] ? Hinv rf [|k] Ef σ ???; try lia.
+ intros [|n] r ? Hinv rf [|k] Ef σ ???; try lia.
apply ownI_spec in Hinv; last auto.
destruct (wsat_open k Ef σ (r ⋅ rf) i P) as (rP&?&?); auto.
{ rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
exists (rP â‹… r); split; last by rewrite (left_id_L _ _) -assoc.
- eapply uPred_weaken with rP (S k); eauto using cmra_included_l.
+ eapply uPred_weaken with (S k) rP; eauto using cmra_included_l.
Qed.
Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊑ pvs ∅ {[ i ]} True.
Proof.
- intros r [|n] ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ∅; split; [done|].
+ intros [|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ∅; split; [done|].
rewrite left_id; apply wsat_close with P r.
- - apply ownI_spec, uPred_weaken with r (S n); auto.
+ - apply ownI_spec, uPred_weaken with (S n) r; auto.
- set_solver +HE.
- by rewrite -(left_id_L ∅ (∪) Ef).
- - apply uPred_weaken with r n; auto.
+ - apply uPred_weaken with n r; auto.
Qed.
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■P m' ∧ ownG m').
Proof.
- intros Hup%option_updateP' r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
+ intros Hup%option_updateP' [|n] r ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
destruct (wsat_update_gst k (E ∪ Ef) σ r rf (Some m) P) as (m'&?&?); eauto.
{ apply cmra_includedN_le with (S n); auto. }
by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
@@ -109,7 +109,7 @@ Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
E (P : iGst Λ Σ → Prop) :
∅ ~~>: P → True ⊑ pvs E E (∃ m', ■P m' ∧ ownG m').
Proof.
- intros Hup r [|n] ? _ rf [|k] Ef σ ???; try lia.
+ intros Hup [|n] r ? _ rf [|k] Ef σ ???; try lia.
destruct (wsat_update_gst k (E ∪ Ef) σ r rf ∅ P) as (m'&?&?); eauto.
{ apply cmra_empty_leastN. }
{ apply cmra_updateP_compose_l with (Some ∅), option_updateP with P;
@@ -118,9 +118,9 @@ Proof.
Qed.
Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■(i ∈ E) ∧ ownI i P).
Proof.
- intros ? r [|n] ? HP rf [|k] Ef σ ???; try lia.
+ intros ? [|n] r ? HP rf [|k] Ef σ ???; try lia.
destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
- { apply uPred_weaken with r n; eauto. }
+ { apply uPred_weaken with n r; eauto. }
exists (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
by split; [by exists i; split; rewrite /uPred_holds /=|].
Qed.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index c64a46062..10cd773e1 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -61,10 +61,10 @@ Proof.
+ by destruct 1; constructor.
+ do 2 destruct 1; constructor; etransitivity; eauto.
- by destruct 1; constructor; apply dist_S.
- - intros c n; constructor.
- + apply (conv_compl (chain_map wld c) n).
- + apply (conv_compl (chain_map pst c) n).
- + apply (conv_compl (chain_map gst c) n).
+ - intros n c; constructor.
+ + apply (conv_compl n (chain_map wld c)).
+ + apply (conv_compl n (chain_map pst c)).
+ + apply (conv_compl n (chain_map gst c)).
Qed.
Canonical Structure resC : cofeT := CofeT res_cofe_mixin.
Global Instance res_timeless r :
@@ -151,7 +151,7 @@ Lemma lookup_wld_op_l n r1 r2 i P :
Proof.
move=>/wld_validN /(_ i) Hval Hi1P; move: Hi1P Hval; rewrite lookup_op.
destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?right_id // =>-> ?.
- by constructor; rewrite (agree_op_inv P P') // agree_idemp.
+ by constructor; rewrite (agree_op_inv _ P P') // agree_idemp.
Qed.
Lemma lookup_wld_op_r n r1 r2 i P :
✓{n} (r1⋅r2) → wld r2 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 19aabc83c..452970393 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -33,13 +33,13 @@ CoInductive wp_pre {Λ Σ} (E : coPset)
Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ)
(Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}.
Next Obligation.
- intros Λ Σ E e Φ r1 r2 n Hwp Hr.
+ intros Λ Σ E e Φ n r1 r2 Hwp Hr.
destruct Hwp as [|n r1 e2 ? Hgo]; constructor; rewrite -?Hr; auto.
intros rf k Ef σ1 ?; rewrite -(dist_le _ _ _ _ Hr); naive_solver.
Qed.
Next Obligation.
- intros Λ Σ E e Φ r1 r2 n1; revert Φ E e r1 r2.
- induction n1 as [n1 IH] using lt_wf_ind; intros Φ E e r1 r1' n2.
+ intros Λ Σ E e Φ n1 n2 r1 r2; revert Φ E e n2 r1 r2.
+ induction n1 as [n1 IH] using lt_wf_ind; intros Φ E e n2 r1 r1'.
destruct 1 as [|n1 r1 e1 ? Hgo].
- constructor; eauto using uPred_weaken.
- intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???].
@@ -63,9 +63,9 @@ Global Instance wp_ne E e n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
Proof.
cut (∀ Φ Ψ, (∀ v, Φ v ≡{n}≡ Ψ v) →
- ∀ r n', n' ≤ n → ✓{n'} r → wp E e Φ n' r → wp E e Ψ n' r).
+ ∀ n' r, n' ≤ n → ✓{n'} r → wp E e Φ n' r → wp E e Ψ n' r).
{ by intros help Φ Ψ HΦΨ; split; apply help. }
- intros Φ Ψ HΦΨ r n'; revert e r.
+ intros Φ Ψ HΦΨ n' r; revert e r.
induction n' as [n' IH] using lt_wf_ind=> e r.
destruct 3 as [n' r v HpvsQ|n' r e1 ? Hgo].
{ constructor. by eapply pvs_ne, HpvsQ; eauto. }
@@ -83,7 +83,7 @@ Qed.
Lemma wp_mask_frame_mono E1 E2 e Φ Ψ :
E1 ⊆ E2 → (∀ v, Φ v ⊑ Ψ v) → wp E1 e Φ ⊑ wp E2 e Ψ.
Proof.
- intros HE HΦ r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r.
+ intros HE HΦ n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r.
destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo].
{ constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. }
constructor; [done|]=> rf k Ef σ1 ???.
@@ -109,7 +109,7 @@ Lemma wp_value' E Φ v : Φ v ⊑ wp E (of_val v) Φ.
Proof. by constructor; apply pvs_intro. Qed.
Lemma pvs_wp E e Φ : pvs E E (wp E e Φ) ⊑ wp E e Φ.
Proof.
- intros r n ? Hvs.
+ intros n r ? Hvs.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
{ constructor; eapply pvs_trans', pvs_mono, Hvs; eauto.
intros ???; apply wp_value_inv. }
@@ -119,7 +119,7 @@ Proof.
Qed.
Lemma wp_pvs E e Φ : wp E e (λ v, pvs E E (Φ v)) ⊑ wp E e Φ.
Proof.
- intros r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
+ intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
{ constructor; apply pvs_trans', (wp_value_inv _ (pvs E E ∘ Φ)); auto. }
constructor; [done|]=> rf k Ef σ1 ???.
@@ -131,7 +131,7 @@ Qed.
Lemma wp_atomic E1 E2 e Φ :
E2 ⊆ E1 → atomic e → pvs E1 E2 (wp E2 e (λ v, pvs E2 E1 (Φ v))) ⊑ wp E1 e Φ.
Proof.
- intros ? He r n ? Hvs; constructor; eauto using atomic_not_val.
+ intros ? He n r ? Hvs; constructor; eauto using atomic_not_val.
intros rf k Ef σ1 ???.
destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
destruct (wp_step_inv E2 Ef (pvs E2 E1 ∘ Φ) e k (S k) σ1 r' rf)
@@ -148,7 +148,7 @@ Proof.
Qed.
Lemma wp_frame_r E e Φ R : (wp E e Φ ★ R) ⊑ wp E e (λ v, Φ v ★ R).
Proof.
- intros r' n Hvalid (r&rR&Hr&Hwp&?); revert Hvalid.
+ intros n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid.
rewrite Hr; clear Hr; revert e r Hwp.
induction n as [n IH] using lt_wf_ind; intros e r1.
destruct 1 as [|n r e ? Hgo]=>?.
@@ -166,22 +166,21 @@ Qed.
Lemma wp_frame_later_r E e Φ R :
to_val e = None → (wp E e Φ ★ ▷ R) ⊑ wp E e (λ v, Φ v ★ R).
Proof.
- intros He r' n Hvalid (r&rR&Hr&Hwp&?); revert Hvalid; rewrite Hr; clear Hr.
+ intros He n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid; rewrite Hr; clear Hr.
destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
constructor; [done|]=>rf k Ef σ1 ???; destruct n as [|n]; first omega.
destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep];rewrite ?assoc;auto.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
exists (r2 â‹… rR), r2'; split_ands; auto.
- - by rewrite -(assoc _ r2)
- (comm _ rR) !assoc -(assoc _ _ rR).
+ - by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR).
- apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
- eapply uPred_weaken with rR n; eauto.
+ eapply uPred_weaken with n rR; eauto.
Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
wp E e (λ v, wp E (K (of_val v)) Φ) ⊑ wp E (K e) Φ.
Proof.
- intros r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?.
+ intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?.
destruct 1 as [|n r e ? Hgo]; [by apply pvs_wp|].
constructor; auto using fill_not_val=> rf k Ef σ1 ???.
destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 91ec36a58..5795b16e2 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -61,7 +61,7 @@ Proof.
destruct (Hwld i (iProp_fold (later_car (P' (S n))))) as (r'&?&?); auto.
{ by rewrite HP' -HPiso. }
assert (✓{S n} r') by (apply (big_opM_lookup_valid _ rs i); auto).
- exists r'; split; [done|apply HPP', uPred_weaken with r' n; auto].
+ exists r'; split; [done|apply HPP', uPred_weaken with n r'; auto].
Qed.
Lemma wsat_valid n E σ r : n ≠0 → wsat n E σ r → ✓{n} r.
Proof.
@@ -130,7 +130,7 @@ Lemma wsat_update_gst n E σ r rf mm1 (P : iGst Λ Σ → Prop) :
wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
Proof.
intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
- destruct (Hup (mf â‹… gst (rf â‹… big_opM rs)) (S n)) as ([m2|]&?&Hval'); try done.
+ destruct (Hup (S n) (mf â‹… gst (rf â‹… big_opM rs))) as ([m2|]&?&Hval'); try done.
{ by rewrite /= (assoc _ mm1) -Hr assoc. }
exists m2; split; [exists rs; split; split_ands'; auto|done].
Qed.
--
GitLab