From 07d525a0ccc1a37ee77b90972e59b7d8a4b4a592 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 10 Feb 2016 18:02:38 +0100
Subject: [PATCH] COFE distance is no longer trivial at index 0.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
This way we avoid many one-off indexes and no longer need special cases for
index 0 in many definitions. For example, the definition of the distance
relation on option and excl has become much easier. Also, uPreds no longer need
to hold at index 0.
In order to make this change possible, we had to change the notions of
"contractive functions" and "chains" slightly.
Thanks to Aleš Bizjak and Amin Timany for suggesting this change and to help
with the proofs.
---
algebra/agree.v | 19 ++---
algebra/auth.v | 9 +-
algebra/cmra.v | 38 +++------
algebra/cofe.v | 87 +++++++++----------
algebra/cofe_solver.v | 164 ++++++++++++++++++++----------------
algebra/excl.v | 35 +++-----
algebra/fin_maps.v | 11 +--
algebra/iprod.v | 2 -
algebra/option.v | 45 +++++-----
algebra/upred.v | 86 +++++++------------
program_logic/adequacy.v | 13 +--
program_logic/lifting.v | 12 +--
program_logic/model.v | 5 +-
program_logic/ownership.v | 10 +--
program_logic/pviewshifts.v | 10 +--
program_logic/resources.v | 14 +--
program_logic/weakestpre.v | 20 ++---
program_logic/wsat.v | 26 +++---
18 files changed, 269 insertions(+), 337 deletions(-)
diff --git a/algebra/agree.v b/algebra/agree.v
index 236211c7d..3e51ad085 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -5,10 +5,9 @@ Local Hint Extern 10 (_ ≤ _) => omega.
Record agree (A : Type) : Type := Agree {
agree_car :> nat → A;
agree_is_valid : nat → Prop;
- agree_valid_0 : agree_is_valid 0;
agree_valid_S n : agree_is_valid (S n) → agree_is_valid n
}.
-Arguments Agree {_} _ _ _ _.
+Arguments Agree {_} _ _ _.
Arguments agree_car {_} _ _.
Arguments agree_is_valid {_} _ _.
@@ -27,10 +26,9 @@ Instance agree_dist : Dist (agree A) := λ n x y,
(∀ n', n' ≤ n → agree_is_valid x n' ↔ agree_is_valid y n') ∧
(∀ n', n' ≤ n → agree_is_valid x n' → x n' ≡{n'}≡ y n').
Program Instance agree_compl : Compl (agree A) := λ c,
- {| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}.
-Next Obligation. intros; apply agree_valid_0. Qed.
+ {| agree_car n := c (S n) n; agree_is_valid n := agree_is_valid (c (S n)) n |}.
Next Obligation.
- intros c n ?; apply (chain_cauchy c n (S n)), agree_valid_S; auto.
+ intros c n ?. apply (chain_cauchy c n (S (S n))), agree_valid_S; auto.
Qed.
Definition agree_cofe_mixin : CofeMixin (agree A).
Proof.
@@ -45,9 +43,8 @@ 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 x y; split; intros n'; rewrite Nat.le_0_r; intros ->; [|done].
- by split; intros; apply agree_valid_0.
- * by intros c n; split; intros; apply (chain_cauchy c).
+ * intros c n; apply and_wlog_r; intros;
+ symmetry; apply (chain_cauchy c); naive_solver.
Qed.
Canonical Structure agreeC := CofeT agree_cofe_mixin.
@@ -59,7 +56,6 @@ Proof. by intros [? Hx]; apply Hx. Qed.
Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := x;
agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ≡{n}≡ y |}.
-Next Obligation. by intros; simpl; split_ands; try apply agree_valid_0. Qed.
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
Instance agree_unit : Unit (agree A) := id.
Instance agree_minus : Minus (agree A) := λ x y, x.
@@ -100,8 +96,6 @@ Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof.
split; try (apply _ || done).
* by intros n x1 x2 Hx y1 y2 Hy.
- * intros x; split; [apply agree_valid_0|].
- by intros n'; rewrite Nat.le_0_r; intros ->.
* intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
rewrite (Hx n'); last auto.
symmetry; apply dist_le with n; try apply Hx; auto.
@@ -142,7 +136,7 @@ Arguments agreeRA : clear implicits.
Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
{| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
-Solve Obligations with auto using agree_valid_0, agree_valid_S.
+Solve Obligations with auto using agree_valid_S.
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
Proof. by destruct x. Qed.
Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
@@ -179,4 +173,3 @@ Qed.
Program Definition agreeF : iFunctor :=
{| ifunctor_car := agreeRA; ifunctor_map := @agreeC_map |}.
Solve Obligations with done.
-
diff --git a/algebra/auth.v b/algebra/auth.v
index 515be2186..7860affe8 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -46,7 +46,6 @@ Proof.
+ by intros ?? [??]; split; symmetry.
+ intros ??? [??] [??]; split; etransitivity; eauto.
* by intros ? [??] [??] [??]; split; apply dist_S.
- * by split.
* intros c n; split. apply (conv_compl (chain_map authoritative c) n).
apply (conv_compl (chain_map own c) n).
Qed.
@@ -71,7 +70,7 @@ Instance auth_validN : ValidN (auth A) := λ n x,
match authoritative x with
| Excl a => own x ≼{n} a ∧ ✓{n} a
| ExclUnit => ✓{n} (own x)
- | ExclBot => n = 0
+ | ExclBot => False
end.
Global Arguments auth_validN _ !_ /.
Instance auth_unit : Unit (auth A) := λ x,
@@ -103,10 +102,9 @@ Proof.
* by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
* by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
* intros n [x a] [y b] [Hx Ha]; simpl in *;
- destruct Hx as [[][]| | |]; intros ?; cofe_subst; auto.
+ destruct Hx; intros ?; cofe_subst; auto.
* by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
- * by intros [[] ?]; simpl.
* intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
* by split; simpl; rewrite associative.
* by split; simpl; rewrite commutative.
@@ -150,7 +148,7 @@ Lemma auth_both_op a b : Auth (Excl a) b ≡ ◠a ⋅ ◯ b.
Proof. by rewrite /op /auth_op /= left_id. Qed.
Lemma auth_update a a' b b' :
- (∀ n af, ✓{S n} a → a ≡{S n}≡ a' ⋅ af → b ≡{S n}≡ b' ⋅ af ∧ ✓{S n} 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 *.
@@ -216,4 +214,3 @@ Next Obligation.
intros Σ A B C f g x. rewrite /= -auth_map_compose.
apply auth_map_ext=>y; apply ifunctor_map_compose.
Qed.
-
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 36fb32bc9..36c3ff1e2 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -40,7 +40,6 @@ Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
mixin_cmra_validN_ne n : Proper (dist n ==> impl) (✓{n});
mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
(* valid *)
- mixin_cmra_validN_0 x : ✓{0} x;
mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
(* monoid *)
mixin_cmra_associative : Associative (≡) (⋅);
@@ -99,8 +98,6 @@ Section cmra_mixin.
Global Instance cmra_minus_ne n :
Proper (dist n ==> dist n ==> dist n) (@minus A _).
Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed.
- Lemma cmra_validN_0 x : ✓{0} x.
- Proof. apply (mixin_cmra_validN_0 _ (cmra_mixin A)). Qed.
Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x.
Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
Global Instance cmra_associative : Associative (≡) (@op A _).
@@ -123,8 +120,6 @@ Section cmra_mixin.
Proof. apply (cmra_extend_mixin A). Qed.
End cmra_mixin.
-Hint Extern 0 (✓{0} _) => apply cmra_validN_0.
-
(** * CMRAs with a global identity element *)
(** We use the notation ∅ because for most instances (maps, sets, etc) the
`empty' element is the global identity. *)
@@ -142,11 +137,11 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
(** * Frame preserving updates *)
Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
- ✓{S n} (x ⋅ z) → ∃ y, P y ∧ ✓{S n} (y ⋅ 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,
- ✓{S n} (x ⋅ z) → ✓{S n} (y ⋅ z).
+ ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
Infix "~~>" := cmra_update (at level 70).
Instance: Params (@cmra_update) 1.
@@ -251,8 +246,6 @@ 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.
Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.
-Lemma cmra_includedN_0 x y : x ≼{0} y.
-Proof. by exists (unit x). Qed.
Lemma cmra_includedN_S x y n : 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.
@@ -290,19 +283,19 @@ Proof.
Qed.
(** ** Timeless *)
-Lemma cmra_timeless_included_l x y : Timeless x → ✓{1} y → x ≼{1} y → x ≼ y.
+Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y.
Proof.
intros ?? [x' ?].
- destruct (cmra_extend_op 1 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
+ destruct (cmra_extend_op 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
by exists z'; rewrite Hy (timeless x z).
Qed.
-Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{1} y → x ≼{n} y.
+Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{0} y → x ≼{n} y.
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
Lemma cmra_op_timeless x1 x2 :
✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
Proof.
intros ??? z Hz.
- destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
+ destruct (cmra_extend_op 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
{ by rewrite -?Hz. }
by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Qed.
@@ -370,8 +363,6 @@ Section identity_updates.
End identity_updates.
End cmra.
-Hint Extern 0 (_ ≼{0} _) => apply cmra_includedN_0.
-
(** * Properties about monotone functions *)
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
Proof. by split. Qed.
@@ -444,22 +435,16 @@ Section discrete.
Context {A : cofeT} `{∀ x : A, Timeless x}.
Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
- Instance discrete_validN : ValidN A := λ n x,
- match n with 0 => True | S n => ✓ x end.
+ Instance discrete_validN : ValidN A := λ n x, ✓ x.
Definition discrete_cmra_mixin : CMRAMixin A.
Proof.
- destruct ra; split; unfold Proper, respectful, includedN;
- repeat match goal with
- | |- ∀ n : nat, _ => intros [|?]
- end; try setoid_rewrite <-(timeless_S _ _ _ _); try done.
- by intros x y ?; exists x.
+ by destruct ra; split; unfold Proper, respectful, includedN;
+ try setoid_rewrite <-(timeless_iff _ _ _ _).
Qed.
Definition discrete_extend_mixin : CMRAExtendMixin A.
Proof.
- intros [|n] x y1 y2 ??.
- * by exists (unit x, x); rewrite /= ra_unit_l.
- * exists (y1,y2); split_ands; auto.
- apply (timeless _), dist_le with (S n); auto with lia.
+ intros n x y1 y2 ??; exists (y1,y2); split_ands; auto.
+ apply (timeless _), dist_le with n; auto with lia.
Qed.
Definition discreteRA : cmraT :=
CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
@@ -512,7 +497,6 @@ Section prod.
* by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
* by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
- * by split.
* by intros n x [??]; split; apply cmra_validN_S.
* split; simpl; apply (associative _).
* split; simpl; apply (commutative _).
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 520cda1e5..646c4d541 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -23,7 +23,7 @@ Tactic Notation "cofe_subst" :=
Record chain (A : Type) `{Dist A} := {
chain_car :> nat → A;
- chain_cauchy n i : n ≤ i → chain_car n ≡{n}≡ chain_car i
+ chain_cauchy n i : n < i → chain_car i ≡{n}≡ chain_car (S n)
}.
Arguments chain_car {_ _} _ _.
Arguments chain_cauchy {_ _} _ _ _ _.
@@ -33,11 +33,10 @@ 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_dist_0 x y : x ≡{0}≡ y;
- mixin_conv_compl (c : chain A) n : compl c ≡{n}≡ c n
+ mixin_conv_compl (c : chain A) n : compl c ≡{n}≡ c (S n)
}.
Class Contractive `{Dist A, Dist B} (f : A -> B) :=
- contractive n : Proper (dist n ==> dist (S n)) f.
+ contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y.
(** Bundeled version *)
Structure cofeT := CofeT {
@@ -66,14 +65,10 @@ 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 dist_0 x y : x ≡{0}≡ y.
- Proof. apply (mixin_dist_0 _ (cofe_mixin A)). Qed.
- Lemma conv_compl (c : chain A) n : compl c ≡{n}≡ c n.
+ Lemma conv_compl (c : chain A) n : compl c ≡{n}≡ c (S n).
Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
End cofe_mixin.
-Hint Extern 0 (_ ≡{0}≡ _) => apply dist_0.
-
(** General properties *)
Section cofe.
Context {A : cofeT}.
@@ -109,13 +104,12 @@ Section cofe.
unfold Proper, respectful; setoid_rewrite equiv_dist.
by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Qed.
- Lemma compl_ne (c1 c2: chain A) n : c1 n ≡{n}≡ c2 n → compl c1 ≡{n}≡ compl c2.
- Proof. intros. by rewrite (conv_compl c1 n) (conv_compl c2 n). Qed.
- Lemma compl_ext (c1 c2 : chain A) : (∀ i, c1 i ≡ c2 i) → compl c1 ≡ compl c2.
- Proof. setoid_rewrite equiv_dist; naive_solver eauto using compl_ne. Qed.
+ Lemma contractive_S {B : cofeT} {f : A → B} `{!Contractive f} n x y :
+ x ≡{n}≡ y → f x ≡{S n}≡ f y.
+ Proof. eauto using contractive, dist_le with omega. Qed.
Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n :
Proper (dist n ==> dist n) f | 100.
- Proof. by intros x1 x2 ?; apply dist_S, contractive. Qed.
+ Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} :
Proper ((≡) ==> (≡)) f | 100 := _.
End cofe.
@@ -127,20 +121,21 @@ Program Definition chain_map `{Dist A, Dist B} (f : A → B)
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 ≡{1}≡ y → x ≡ y.
+Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
Arguments timeless {_} _ {_} _ _.
-Lemma timeless_S {A : cofeT} (x y : A) n : Timeless x → x ≡ y ↔ x ≡{S n}≡ y.
+Lemma timeless_iff {A : cofeT} (x y : A) n : Timeless x → x ≡ y ↔ x ≡{n}≡ y.
Proof.
split; intros; [by apply equiv_dist|].
- apply (timeless _), dist_le with (S n); auto with lia.
+ apply (timeless _), dist_le with n; auto with lia.
Qed.
(** Fixpoint *)
Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
- `{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}.
+ `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Next Obligation.
- intros A ? f ? n; induction n as [|n IH]; intros i ?; first done.
- destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia.
+ intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; try omega.
+ * apply contractive; auto with omega.
+ * apply contractive_S, IH; auto with omega.
Qed.
Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A)
`{!Contractive f} : A := compl (fixpoint_chain f).
@@ -149,17 +144,16 @@ Section fixpoint.
Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}.
Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
Proof.
- apply equiv_dist; intros n; unfold fixpoint.
- rewrite (conv_compl (fixpoint_chain f) n).
- by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia.
+ apply equiv_dist=>n; rewrite /fixpoint (conv_compl (fixpoint_chain f) n) //.
+ induction n as [|n IH]; simpl; eauto using contractive, dist_le with omega.
Qed.
Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
(∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
Proof.
- intros Hfg; unfold fixpoint.
- rewrite (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n).
- induction n as [|n IH]; simpl in *; first done.
- rewrite Hfg; apply contractive, IH; auto using dist_S.
+ intros Hfg. rewrite /fixpoint
+ (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n) /=.
+ induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
+ rewrite Hfg; apply contractive_S, IH; auto using dist_S.
Qed.
Lemma fixpoint_proper (g : A → A) `{!Contractive g} :
(∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g.
@@ -188,9 +182,8 @@ 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.
- rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hx.
- apply (chain_cauchy c); lia.
+ intros c n x y Hx. by rewrite (conv_compl (fun_chain c x) n)
+ (conv_compl (fun_chain c y) n) /= Hx.
Qed.
Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
Proof.
@@ -202,9 +195,8 @@ Section cofe_mor.
+ by intros f g ? x.
+ by intros f g h ?? x; transitivity (g x).
* by intros n f g ? x; apply dist_S.
- * by intros f g x.
* intros c n x; simpl.
- rewrite (conv_compl (fun_chain c x) n); apply (chain_cauchy c); lia.
+ by rewrite (conv_compl (fun_chain c x) n) /=.
Qed.
Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.
@@ -262,7 +254,6 @@ Section product.
rewrite !equiv_dist; naive_solver.
* apply _.
* by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
- * by split.
* intros c n; split. apply (conv_compl (chain_map fst c) n).
apply (conv_compl (chain_map snd c) n).
Qed.
@@ -288,17 +279,16 @@ Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
(** Discrete cofe *)
Section discrete_cofe.
Context `{Equiv A, @Equivalence A (≡)}.
- Instance discrete_dist : Dist A := λ n x y,
- match n with 0 => True | S n => x ≡ y end.
+ Instance discrete_dist : Dist A := λ n x y, x ≡ y.
Instance discrete_compl : Compl A := λ c, c 1.
Definition discrete_cofe_mixin : CofeMixin A.
Proof.
split.
- * intros x y; split; [by intros ? []|intros Hn; apply (Hn 1)].
- * intros [|n]; [done|apply _].
- * by intros [|n].
+ * intros x y; split; [done|intros Hn; apply (Hn 0)].
+ * done.
* done.
- * intros c [|n]; [done|apply (chain_cauchy c 1 (S n)); lia].
+ * intros c n. rewrite /compl /discrete_compl /=.
+ symmetry; apply (chain_cauchy c 0 (S n)); omega.
Qed.
Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
Global Instance discrete_timeless (x : A) : Timeless (x : discreteC).
@@ -314,11 +304,11 @@ Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
(** Later *)
-Inductive later (A : Type) : Type := Later { later_car : A }.
+Inductive later (A : Type) : Type := Next { later_car : A }.
Add Printing Constructor later.
-Arguments Later {_} _.
+Arguments Next {_} _.
Arguments later_car {_} _.
-Lemma later_eta {A} (x : later A) : Later (later_car x) = x.
+Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
Proof. by destruct x. Qed.
Section later.
@@ -329,7 +319,7 @@ Section later.
Program Definition later_chain (c : chain (later A)) : chain A :=
{| chain_car n := later_car (c (S n)) |}.
Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
- Instance later_compl : Compl (later A) := λ c, Later (compl (later_chain c)).
+ Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
Definition later_cofe_mixin : CofeMixin (later A).
Proof.
split.
@@ -340,20 +330,19 @@ 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.
- * done.
* intros c [|n]; [done|by apply (conv_compl (later_chain c) n)].
Qed.
Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
- Global Instance Later_contractive : Contractive (@Later A).
- Proof. by intros n ??. Qed.
- Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Later A).
+ Global Instance Next_contractive : Contractive (@Next A).
+ Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
+ Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Next A).
Proof. by intros x y. Qed.
End later.
Arguments laterC : clear implicits.
Definition later_map {A B} (f : A → B) (x : later A) : later B :=
- Later (f (later_car x)).
+ Next (f (later_car x)).
Instance later_map_ne {A B : cofeT} (f : A → B) n :
Proper (dist (pred n) ==> dist (pred n)) f →
Proper (dist n ==> dist n) (later_map f) | 0.
@@ -366,4 +355,4 @@ Proof. by destruct x. Qed.
Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
CofeMor (later_map f).
Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
-Proof. intros n f g Hf n'; apply Hf. Qed.
+Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index f03becc08..1a56cc65e 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -28,33 +28,44 @@ Lemma map_ext {A1 A2 B1 B2 : cofeT}
(∀ x, f x ≡ f' x) → (∀ y, g y ≡ g' y) → x ≡ x' →
map (f,g) x ≡ map (f',g') x'.
Proof. by rewrite -!cofe_mor_ext; intros -> -> ->. Qed.
+Lemma map_ne {A1 A2 B1 B2 : cofeT}
+ (f : A2 -n> A1) (f' : A2 -n> A1) (g : B1 -n> B2) (g' : B1 -n> B2) n x :
+ (∀ x, f x ≡{n}≡ f' x) → (∀ y, g y ≡{n}≡ g' y) →
+ map (f,g) x ≡{n}≡ map (f',g') x.
+Proof.
+ intros. by apply map_contractive=> i ?; apply dist_le with n; last lia.
+Qed.
Fixpoint A (k : nat) : cofeT :=
match k with 0 => unitC | S k => F (A k) (A k) end.
-Fixpoint f {k} : A k -n> A (S k) :=
- match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g,f) end
-with g {k} : A (S k) -n> A k :=
- match k with 0 => CofeMor (λ _, ()) | S k => map (f,g) end.
-Definition f_S k (x : A (S k)) : f x = map (g,f) x := eq_refl.
-Definition g_S k (x : A (S (S k))) : g x = map (f,g) x := eq_refl.
-Lemma gf {k} (x : A k) : g (f x) ≡ x.
+Fixpoint f (k : nat) : A k -n> A (S k) :=
+ match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
+with g (k : nat) : A (S k) -n> A k :=
+ match k with 0 => CofeMor (λ _, ()) | S k => map (f k,g k) end.
+Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
+Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
+Arguments A : simpl never.
+Arguments f : simpl never.
+Arguments g : simpl never.
+
+Lemma gf {k} (x : A k) : g k (f k x) ≡ x.
Proof.
induction k as [|k IH]; simpl in *; [by destruct x|].
rewrite -map_comp -{2}(map_id _ _ x); by apply map_ext.
Qed.
-Lemma fg {n k} (x : A (S k)) : n ≤ k → f (g x) ≡{n}≡ x.
+Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x.
Proof.
- intros Hnk; apply dist_le with k; auto; clear Hnk.
- induction k as [|k IH]; simpl; [apply dist_0|].
- rewrite -{2}(map_id _ _ x) -map_comp; by apply map_contractive.
+ induction k as [|k IH]; simpl.
+ * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp.
+ apply map_contractive=> i ?; omega.
+ * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp.
+ apply map_contractive=> i ?; apply dist_le with k; [|omega].
+ split=> x' /=; apply IH.
Qed.
-Arguments A _ : simpl never.
-Arguments f {_} : simpl never.
-Arguments g {_} : simpl never.
Record tower := {
tower_car k :> A k;
- g_tower k : g (tower_car (S k)) ≡ tower_car k
+ g_tower k : g k (tower_car (S k)) ≡ tower_car k
}.
Instance tower_equiv : Equiv tower := λ X Y, ∀ k, X k ≡ Y k.
Instance tower_dist : Dist tower := λ n X Y, ∀ k, X k ≡{n}≡ Y k.
@@ -64,9 +75,9 @@ Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
Program Instance tower_compl : Compl tower := λ c,
{| tower_car n := compl (tower_chain c n) |}.
Next Obligation.
- intros c k; apply equiv_dist; intros n.
- rewrite (conv_compl (tower_chain c k) n).
- by rewrite (conv_compl (tower_chain c (S k)) n) /= (g_tower (c n) k).
+ 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).
Qed.
Definition tower_cofe_mixin : CofeMixin tower.
Proof.
@@ -79,24 +90,23 @@ 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 X Y k; apply dist_0.
* intros c n k; rewrite /= (conv_compl (tower_chain c k) n).
apply (chain_cauchy c); lia.
Qed.
Definition T : cofeT := CofeT tower_cofe_mixin.
Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
- match i with 0 => cid | S i => f â—Ž ff i end.
+ match i with 0 => cid | S i => f (i + k) â—Ž ff i end.
Fixpoint gg {k} (i : nat) : A (i + k) -n> A k :=
- match i with 0 => cid | S i => gg i â—Ž g end.
+ match i with 0 => cid | S i => gg i â—Ž g (i + k) end.
Lemma ggff {k i} (x : A k) : gg i (ff i x) ≡ x.
Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
-Lemma f_tower {n k} (X : tower) : n ≤ k → f (X k) ≡{n}≡ X (S k).
-Proof. intros. by rewrite -(fg (X (S k))) // -(g_tower X). Qed.
-Lemma ff_tower {n} k i (X : tower) : n ≤ k → ff i (X k) ≡{n}≡ X (i + k).
+Lemma f_tower k (X : tower) : f (S k) (X (S k)) ≡{k}≡ X (S (S k)).
+Proof. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
+Lemma ff_tower k i (X : tower) : ff i (X (S k)) ≡{k}≡ X (i + S k).
Proof.
intros; induction i as [|i IH]; simpl; [done|].
- by rewrite IH (f_tower X); last lia.
+ by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last omega.
Qed.
Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k.
Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
@@ -113,10 +123,10 @@ Lemma coerce_proper {i j} (x y : A i) (H1 H2 : i = j) :
x = y → coerce H1 x = coerce H2 y.
Proof. by destruct H1; rewrite !coerce_id. Qed.
Lemma g_coerce {k j} (H : S k = S j) (x : A (S k)) :
- g (coerce H x) = coerce (Nat.succ_inj _ _ H) (g x).
+ g j (coerce H x) = coerce (Nat.succ_inj _ _ H) (g k x).
Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma coerce_f {k j} (H : S k = S j) (x : A k) :
- coerce H (f x) = f (coerce (Nat.succ_inj _ _ H) x).
+ coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x).
Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
@@ -133,14 +143,15 @@ Proof.
[by rewrite coerce_id|by rewrite coerce_f IH].
Qed.
-Definition embed' {k} (i : nat) : A k -n> A i :=
+Definition embed_coerce {k} (i : nat) : A k -n> A i :=
match le_lt_dec i k with
| left H => gg (k-i) â—Ž coerce (eq_sym (Nat.sub_add _ _ H))
| right H => coerce (Nat.sub_add k i (Nat.lt_le_incl _ _ H)) â—Ž ff (i-k)
end.
-Lemma g_embed' {k i} (x : A k) : g (embed' (S i) x) ≡ embed' i x.
+Lemma g_embed_coerce {k i} (x : A k) :
+ g i (embed_coerce (S i) x) ≡ embed_coerce i x.
Proof.
- unfold embed'; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
+ unfold embed_coerce; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
* symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl.
* exfalso; lia.
* assert (i = k) by lia; subst.
@@ -150,16 +161,16 @@ Proof.
rewrite (ff_ff _ H) /= -{2}(gf (ff (i - k) x)) g_coerce.
by erewrite coerce_proper by done.
Qed.
-Program Definition embed_inf (k : nat) (x : A k) : T :=
- {| tower_car n := embed' n x |}.
-Next Obligation. intros k x i. apply g_embed'. Qed.
-Instance embed_inf_ne k n : Proper (dist n ==> dist n) (embed_inf k).
+Program Definition embed (k : nat) (x : A k) : T :=
+ {| tower_car n := embed_coerce n x |}.
+Next Obligation. intros k x i. apply g_embed_coerce. Qed.
+Instance: Params (@embed) 1.
+Instance embed_ne k n : Proper (dist n ==> dist n) (embed k).
Proof. by intros x y Hxy i; rewrite /= Hxy. Qed.
-Definition embed (k : nat) : A k -n> T := CofeMor (embed_inf k).
-Lemma embed_f k (x : A k) : embed (S k) (f x) ≡ embed k x.
+Definition embed' (k : nat) : A k -n> T := CofeMor (embed k).
+Lemma embed_f k (x : A k) : embed (S k) (f k x) ≡ embed k x.
Proof.
- rewrite equiv_dist; intros n i.
- unfold embed_inf, embed; simpl; unfold embed'.
+ rewrite equiv_dist=> n i; rewrite /embed /= /embed_coerce.
destruct (le_lt_dec i (S k)), (le_lt_dec i k); simpl.
* assert (H : S k = S (k - i) + (0 + i)) by lia; rewrite (gg_gg _ H) /=.
by erewrite g_coerce, gf, coerce_proper by done.
@@ -170,33 +181,39 @@ Proof.
* assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H) /=.
by erewrite coerce_proper by done.
Qed.
-Lemma embed_tower j n (X : T) : n ≤ j → embed j (X j) ≡{n}≡ X.
+Lemma embed_tower k (X : T) : embed (S k) (X (S k)) ≡{k}≡ X.
Proof.
- move=> Hn i; rewrite /= /embed'; destruct (le_lt_dec i j) as [H|H]; simpl.
- * rewrite -(gg_tower i (j - i) X).
+ intros i; rewrite /= /embed_coerce.
+ destruct (le_lt_dec i (S k)) as [H|H]; simpl.
+ * rewrite -(gg_tower i (S k - i) X).
apply (_ : Proper (_ ==> _) (gg _)); by destruct (eq_sym _).
- * rewrite (ff_tower j (i-j) X); last lia. by destruct (Nat.sub_add _ _ _).
+ * rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
Qed.
Program Definition unfold_chain (X : T) : chain (F T T) :=
- {| chain_car n := map (project n,embed n) (f (X n)) |}.
+ {| chain_car n := map (project n,embed' n) (X (S n)) |}.
Next Obligation.
intros X n i Hi.
assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
- induction k as [|k Hk]; simpl; [done|].
- rewrite Hk (f_tower X); last lia; rewrite f_S -map_comp.
- apply dist_S, map_contractive.
- split; intros Y; symmetry; apply equiv_dist; [apply g_tower|apply embed_f].
+ induction k as [|k IH]; simpl.
+ { rewrite -f_tower f_S -map_comp.
+ apply map_ne=> Y /=. by rewrite g_tower. by rewrite embed_f. }
+ rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
+ rewrite f_S -map_comp.
+ apply map_ne=> Y /=. by rewrite g_tower. by rewrite embed_f.
Qed.
Definition unfold (X : T) : F T T := compl (unfold_chain X).
Instance unfold_ne : Proper (dist n ==> dist n) unfold.
-Proof. by intros n X Y HXY; apply compl_ne; rewrite /= (HXY n). Qed.
+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))).
+Qed.
Program Definition fold (X : F T T) : T :=
- {| tower_car n := g (map (embed n,project n) X) |}.
+ {| tower_car n := g n (map (embed' n,project n) X) |}.
Next Obligation.
- intros X k; apply (_ : Proper ((≡) ==> (≡)) g).
- rewrite -(map_comp _ _ _ _ _ _ (embed (S k)) f (project (S k)) g).
+ intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).
+ rewrite g_S -map_comp.
apply map_ext; [apply embed_f|intros Y; apply g_tower|done].
Qed.
Instance fold_ne : Proper (dist n ==> dist n) fold.
@@ -205,30 +222,33 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
Theorem result : solution F.
Proof.
apply (Solution F T (CofeMor unfold) (CofeMor fold)).
- * move=> X.
- assert (map_ff_gg : ∀ i k (x : A (S i + k)) (H : S i + k = i + S k),
- map (ff i, gg i) x ≡ gg i (coerce H x)).
- { intros i; induction i as [|i IH]; intros k x H; simpl.
- { by rewrite coerce_id map_id. }
- rewrite map_comp g_coerce; apply IH. }
+ * move=> X /=.
rewrite equiv_dist; intros n k; unfold unfold, fold; simpl.
- rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) g).
+ 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 (chain_cauchy (unfold_chain X) n (n + k)) /=; last lia.
- rewrite (f_tower X); last lia; rewrite -map_comp.
- apply dist_S. apply map_contractive; split; intros x; simpl; unfold embed'.
- * destruct (le_lt_dec _ _); simpl.
- { assert (n = 0) by lia; subst. apply dist_0. }
- by rewrite (ff_ff _ (eq_refl (n + (0 + k)))).
- * destruct (le_lt_dec _ _); [|exfalso; lia]; simpl.
- by rewrite (gg_gg _ (eq_refl (0 + (n + k)))). }
- assert (H: S n + k = n + S k) by lia; rewrite (map_ff_gg _ _ _ H).
+ 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 map_ne; fold A=> Y.
+ + rewrite /embed' /= /embed_coerce.
+ destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
+ by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
+ + rewrite /embed' /= /embed_coerce.
+ destruct (le_lt_dec _ _); simpl; [|exfalso; lia].
+ by rewrite (gg_gg _ (eq_refl (0 + (S n + k)))) /= gf. }
+ assert (∀ i k (x : A (S i + k)) (H : S i + k = i + S k),
+ map (ff i, gg i) x ≡ gg i (coerce H x)) as map_ff_gg.
+ { intros i; induction i as [|i IH]; intros k' x H; simpl.
+ { by rewrite coerce_id map_id. }
+ rewrite map_comp g_coerce; apply IH. }
+ assert (H: S n + k = n + S k) by lia.
+ rewrite (map_ff_gg _ _ _ H).
apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
- * move=>X; rewrite equiv_dist=> n.
- rewrite /(unfold) /= /(unfold) (conv_compl (unfold_chain (fold X)) n) /=.
- rewrite (fg (map (embed _,project n) X)); last lia.
- rewrite -map_comp -{2}(map_id _ _ X).
- apply dist_S, map_contractive; split; intros Y i; apply embed_tower; lia.
+ * intros X; rewrite equiv_dist=> n /=.
+ rewrite /unfold /= (conv_compl (unfold_chain (fold X)) n) /=.
+ rewrite g_S -!map_comp -{2}(map_id _ _ X); apply map_ne=> Y /=.
+ + apply dist_le with n; last omega.
+ rewrite f_tower. apply dist_S. by rewrite embed_tower.
+ + etransitivity; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
Qed.
End solver. End solver.
diff --git a/algebra/excl.v b/algebra/excl.v
index cc0a05498..83f4c3039 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -23,7 +23,6 @@ Inductive excl_equiv : Equiv (excl A) :=
| ExclBot_equiv : ExclBot ≡ ExclBot.
Existing Instance excl_equiv.
Inductive excl_dist `{Dist A} : Dist (excl A) :=
- | excl_dist_0 (x y : excl A) : x ≡{0}≡ y
| Excl_dist (x y : A) n : x ≡{n}≡ y → Excl x ≡{n}≡ Excl y
| ExclUnit_dist n : ExclUnit ≡{n}≡ ExclUnit
| ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
@@ -40,11 +39,9 @@ Program Definition excl_chain
(c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A :=
{| chain_car n := match c n return _ with Excl y => y | _ => x end |}.
Next Obligation.
- intros c x ? n i ?; simpl; destruct (c 1) eqn:?; simplify_equality'.
- destruct (decide (i = 0)) as [->|].
- { by replace n with 0 by lia. }
- feed inversion (chain_cauchy c 1 i); auto with lia congruence.
- feed inversion (chain_cauchy c n i); simpl; auto with lia congruence.
+ intros c x ? n [|i] ?; [omega|]; simpl.
+ destruct (c 1) eqn:?; simplify_equality'.
+ by feed inversion (chain_cauchy c n (S i)).
Qed.
Instance excl_compl : Compl (excl A) := λ c,
match Some_dec (maybe Excl (c 1)) with
@@ -61,17 +58,15 @@ Proof.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
* by inversion_clear 1; constructor; apply dist_S.
- * constructor.
* intros c n; unfold compl, excl_compl.
- destruct (decide (n = 0)) as [->|]; [constructor|].
destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|].
{ assert (c 1 = Excl x) by (by destruct (c 1); simplify_equality').
- assert (∃ y, c n = Excl y) as [y Hy].
- { feed inversion (chain_cauchy c 1 n); try congruence; eauto with lia. }
+ 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); simpl; rewrite Hy. }
- feed inversion (chain_cauchy c 1 n); auto with lia; constructor.
- destruct (c 1); simplify_equality'.
+ by rewrite (conv_compl (excl_chain c x Hx) n) /= Hy. }
+ feed inversion (chain_cauchy c 0 (S n)); first lia;
+ constructor; destruct (c 1); simplify_equality'.
Qed.
Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
@@ -89,7 +84,7 @@ Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
(* CMRA *)
Instance excl_validN : ValidN (excl A) := λ n x,
- match x with Excl _ | ExclUnit => True | ExclBot => n = 0 end.
+ match x with Excl _ | ExclUnit => True | ExclBot => False end.
Global Instance excl_empty : Empty (excl A) := ExclUnit.
Instance excl_unit : Unit (excl A) := λ _, ∅.
Instance excl_op : Op (excl A) := λ x y,
@@ -109,9 +104,8 @@ Proof.
split.
* by intros n []; destruct 1; constructor.
* constructor.
- * by destruct 1 as [? []| | |]; intros ?.
+ * by destruct 1; intros ?.
* by destruct 1; inversion_clear 1; constructor.
- * by intros [].
* intros n [?| |]; simpl; auto with lia.
* by intros [?| |] [?| |] [?| |]; constructor.
* by intros [?| |] [?| |]; constructor.
@@ -123,7 +117,7 @@ Proof.
Qed.
Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A).
Proof.
- intros [|n] x y1 y2 ? Hx; [by exists (x,∅); destruct x|].
+ intros n x y1 y2 ? Hx.
by exists match y1, y2 with
| Excl a1, Excl a2 => (Excl a1, Excl a2)
| ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot)
@@ -134,13 +128,13 @@ Canonical Structure exclRA : cmraT :=
CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
Global Instance excl_cmra_identity : CMRAIdentity exclRA.
Proof. split. done. by intros []. apply _. Qed.
-Lemma excl_validN_inv_l n x y : ✓{S n} (Excl x ⋅ y) → y = ∅.
+Lemma excl_validN_inv_l n x y : ✓{n} (Excl x ⋅ y) → y = ∅.
Proof. by destruct y. Qed.
-Lemma excl_validN_inv_r n x y : ✓{S n} (x ⋅ Excl y) → x = ∅.
+Lemma excl_validN_inv_r n x y : ✓{n} (x ⋅ Excl y) → x = ∅.
Proof. by destruct x. Qed.
Lemma Excl_includedN n x y : ✓{n} y → Excl x ≼{n} y ↔ y ≡{n}≡ Excl x.
Proof.
- intros Hvalid; split; [destruct n as [|n]; [done|]|by intros ->].
+ intros Hvalid; split; [|by intros ->].
by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
Qed.
@@ -187,4 +181,3 @@ Program Definition exclF : iFunctor :=
{| ifunctor_car := exclRA; ifunctor_map := @exclC_map |}.
Next Obligation. by intros A x; rewrite /= excl_map_id. Qed.
Next Obligation. by intros A B C f g x; rewrite /= excl_map_compose. Qed.
-
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index cf9683087..2b6cb4c1c 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -23,11 +23,9 @@ Proof.
+ by intros m1 m2 ? k.
+ by intros m1 m2 m3 ?? k; transitivity (m2 !! k).
* by intros n m1 m2 ? k; apply dist_S.
- * by intros m1 m2 k.
- * intros c n k; unfold compl, map_compl; rewrite lookup_imap.
- destruct (decide (n = 0)) as [->|]; [constructor|].
- feed inversion (λ H, chain_cauchy c 1 n H k); simpl; auto with lia.
- by rewrite conv_compl; simpl; apply reflexive_eq.
+ * intros c n 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.
Canonical Structure mapC : cofeT := CofeT map_cofe_mixin.
@@ -60,7 +58,7 @@ Qed.
Global Instance map_lookup_timeless m i : Timeless m → Timeless (m !! i).
Proof.
intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
- assert (m ≡{1}≡ <[i:=x]> m)
+ assert (m ≡{0}≡ <[i:=x]> m)
by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
Qed.
@@ -116,7 +114,6 @@ Proof.
* by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i).
* by intros n m1 m2 Hm ? i; rewrite -(Hm i).
* by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i).
- * by intros m i.
* intros n m Hm i; apply cmra_validN_S, Hm.
* by intros m1 m2 m3 i; rewrite !lookup_op associative.
* by intros m1 m2 i; rewrite !lookup_op commutative.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index c10b0f782..5d0da6da5 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -37,7 +37,6 @@ 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.
- * by intros f g x.
* intros c n x.
rewrite /compl /iprod_compl (conv_compl (iprod_chain c x) n).
apply (chain_cauchy c); lia.
@@ -141,7 +140,6 @@ Section iprod_cmra.
* by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x).
* by intros n f1 f2 Hf ? x; rewrite -(Hf x).
* by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_minus (Hf i) (Hg i).
- * by intros f x.
* intros n f Hf x; apply cmra_validN_S, Hf.
* by intros f1 f2 f3 x; rewrite iprod_lookup_op associative.
* by intros f1 f2 x; rewrite iprod_lookup_op commutative.
diff --git a/algebra/option.v b/algebra/option.v
index ec1acec1b..2339aa2c7 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -5,7 +5,6 @@ Require Import algebra.functor.
Section cofe.
Context {A : cofeT}.
Inductive option_dist : Dist (option A) :=
- | option_0_dist (x y : option A) : x ≡{0}≡ y
| Some_dist n x y : x ≡{n}≡ y → Some x ≡{n}≡ Some y
| None_dist n : None ≡{n}≡ None.
Existing Instance option_dist.
@@ -13,10 +12,9 @@ Program Definition option_chain
(c : chain (option A)) (x : A) (H : c 1 = Some x) : chain A :=
{| chain_car n := from_option x (c n) |}.
Next Obligation.
- intros c x ? n i ?; simpl; destruct (decide (i = 0)) as [->|].
- { by replace n with 0 by lia. }
- feed inversion (chain_cauchy c 1 i); auto with lia congruence.
- feed inversion (chain_cauchy c n i); simpl; auto with lia congruence.
+ intros c x ? n [|i] ?; [omega|]; simpl.
+ destruct (c 1) eqn:?; simplify_equality'.
+ by feed inversion (chain_cauchy c n (S i)).
Qed.
Instance option_compl : Compl (option A) := λ c,
match Some_dec (c 1) with
@@ -33,20 +31,19 @@ Proof.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
* by inversion_clear 1; constructor; apply dist_S.
- * constructor.
* intros c n; unfold compl, option_compl.
- destruct (decide (n = 0)) as [->|]; [constructor|].
destruct (Some_dec (c 1)) as [[x Hx]|].
- { assert (is_Some (c n)) as [y Hy].
- { feed inversion (chain_cauchy c 1 n); try congruence; eauto with lia. }
+ { 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); simpl; rewrite Hy. }
- feed inversion (chain_cauchy c 1 n); auto with lia congruence; constructor.
+ by rewrite (conv_compl (option_chain c x Hx) n) /= Hy. }
+ feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence.
+ constructor.
Qed.
Canonical Structure optionC := CofeT option_cofe_mixin.
Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
Proof. by constructor. Qed.
-Global Instance is_Some_ne n : Proper (dist (S n) ==> iff) (@is_Some A).
+Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
Proof. inversion_clear 1; split; eauto. Qed.
Global Instance Some_dist_inj : Injective (dist n) (dist n) (@Some A).
Proof. by inversion_clear 1. Qed.
@@ -70,16 +67,15 @@ Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
Instance option_minus : Minus (option A) :=
difference_with (λ x y, Some (x ⩪ y)).
Lemma option_includedN n (mx my : option A) :
- mx ≼{n} my ↔ n = 0 ∨ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
+ mx ≼{n} my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
Proof.
split.
- * intros [mz Hmz]; destruct n as [|n]; [by left|right].
+ * intros [mz Hmz].
destruct mx as [x|]; [right|by left].
destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
cofe_subst; eauto using cmra_includedN_l.
- * intros [->|[->|(x&y&->&->&z&Hz)]];
- try (by exists my; destruct my; constructor).
+ * intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
by exists (Some z); constructor.
Qed.
Lemma None_includedN n (mx : option A) : None ≼{n} mx.
@@ -93,29 +89,26 @@ Proof.
* by intros n [x|]; destruct 1; constructor;
repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
* by destruct 1; constructor; apply (_ : Proper (dist n ==> _) _).
- * destruct 1 as [[?|] [?|]| |]; unfold validN, option_validN; simpl;
- intros ?; auto using cmra_validN_0;
- eapply (_ : Proper (dist _ ==> impl) (✓{_})); eauto.
+ * destruct 1; rewrite /validN /option_validN //=.
+ eapply (_ : Proper (dist _ ==> impl) (✓{_})); eauto.
* by destruct 1; inversion_clear 1; constructor;
repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
- * intros [x|]; unfold validN, option_validN; auto using cmra_validN_0.
* intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
* intros [x|] [y|] [z|]; constructor; rewrite ?associative; auto.
* intros [x|] [y|]; constructor; rewrite 1?commutative; auto.
* by intros [x|]; constructor; rewrite cmra_unit_l.
* by intros [x|]; constructor; rewrite cmra_unit_idempotent.
- * intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto.
- do 2 right; exists (unit x), (unit y); eauto using cmra_unit_preservingN.
+ * intros n mx my; rewrite !option_includedN;intros [->|(x&y&->&->&?)]; auto.
+ right; exists (unit x), (unit y); eauto using cmra_unit_preservingN.
* intros n [x|] [y|]; rewrite /validN /option_validN /=;
eauto using cmra_validN_op_l.
* intros n mx my; rewrite option_includedN.
- intros [->|[->|(x&y&->&->&?)]]; [done|by destruct my|].
+ intros [->|(x&y&->&->&?)]; [by destruct my|].
by constructor; apply cmra_op_minus.
Qed.
Definition option_cmra_extend_mixin : CMRAExtendMixin (option A).
Proof.
- intros n mx my1 my2; destruct (decide (n = 0)) as [->|].
- { by exists (mx, None); repeat constructor; destruct mx; constructor. }
+ intros n mx my1 my2.
destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
try (by exfalso; inversion Hx'; auto).
* destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto.
@@ -171,7 +164,7 @@ Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f}
Proof.
split.
* intros n mx my; rewrite !option_includedN.
- intros [->|[->|(x&y&->&->&?)]]; simpl; eauto 10 using @includedN_preserving.
+ intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @includedN_preserving.
* by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving.
Qed.
Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
diff --git a/algebra/upred.v b/algebra/upred.v
index f88981899..72b97739d 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -6,14 +6,12 @@ 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_0 x : uPred_holds 0 x;
uPred_weaken x1 x2 n1 n2 :
uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → uPred_holds n2 x2
}.
Arguments uPred_holds {_} _ _ _ : simpl never.
Global Opaque uPred_holds.
Local Transparent uPred_holds.
-Hint Resolve uPred_0.
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
@@ -24,12 +22,11 @@ Section cofe.
Instance uPred_dist : Dist (uPred M) := λ n P Q, ∀ x n',
n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x.
Program Instance uPred_compl : Compl (uPred M) := λ c,
- {| uPred_holds n x := c n n x |}.
+ {| 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 x; simpl. Qed.
Next Obligation.
intros c x1 x2 n1 n2 ????; simpl in *.
- apply (chain_cauchy c n2 n1); eauto using uPred_weaken.
+ apply (chain_cauchy c n2 (S n1)); eauto using uPred_weaken.
Qed.
Definition uPred_cofe_mixin : CofeMixin (uPred M).
Proof.
@@ -41,8 +38,7 @@ Section cofe.
+ 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 P Q x i; rewrite Nat.le_0_r=> ->; split; intros; apply uPred_0.
- * by intros c n x i ??; apply (chain_cauchy c i n).
+ * intros c n x i ??; symmetry; apply (chain_cauchy c i (S n)); auto.
Qed.
Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
End cofe.
@@ -65,7 +61,6 @@ Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
`{!CMRAMonotone f} (P : uPred M1) :
uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. by intros M1 M2 f ? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
-Next Obligation. intros M1 M2 f _ P x; apply uPred_0. Qed.
Next Obligation.
naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
Qed.
@@ -103,9 +98,8 @@ Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
(** logical connectives *)
Program Definition uPred_const {M} (φ : Prop) : uPred M :=
- {| uPred_holds n x := match n return _ with 0 => True | _ => φ end |}.
+ {| uPred_holds n x := φ |}.
Solve Obligations with done.
-Next Obligation. intros M P x1 x2 [|n1] [|n2]; auto with lia. Qed.
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
Program Definition uPred_and {M} (P Q : uPred M) : uPred M :=
@@ -125,19 +119,13 @@ Next Obligation.
eauto using uPred_weaken, uPred_ne.
Qed.
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
-Next Obligation. naive_solver eauto 2 with lia. Qed.
Program Definition uPred_forall {M A} (P : A → uPred M) : uPred M :=
{| uPred_holds n x := ∀ a, P a n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_exist {M A} (P : A → uPred M) : uPred M :=
- {| uPred_holds n x :=
- match n return _ with 0 => True | _ => ∃ a, P a n x end |}.
-Next Obligation. intros M A P x y [|n]; naive_solver eauto using uPred_ne. Qed.
-Next Obligation. done. Qed.
-Next Obligation.
- intros M A P x y [|n] [|n']; naive_solver eauto 2 using uPred_weaken with lia.
-Qed.
+ {| uPred_holds n x := ∃ a, P a n x |}.
+Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_eq {M} {A : cofeT} (a1 a2 : A) : uPred M :=
{| uPred_holds n x := a1 ≡{n}≡ a2 |}.
@@ -148,7 +136,6 @@ Program Definition uPred_sep {M} (P Q : uPred M) : uPred M :=
Next Obligation.
by intros M P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
Qed.
-Next Obligation. by intros M P Q x; exists x, x. Qed.
Next Obligation.
intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??.
assert (∃ x2', y ≡{n2}≡ x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
@@ -167,7 +154,6 @@ Next Obligation.
rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
by rewrite (dist_le _ _ _ n2 Hx).
Qed.
-Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Next Obligation.
intros M P Q x1 x2 n1 n2 HPQ ??? x3 n3 ???; simpl in *.
apply uPred_weaken with (x1 â‹… x3) n3;
@@ -177,14 +163,12 @@ 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. done. Qed.
Next Obligation.
- intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken, cmra_validN_S.
+ intros M P x1 x2 [|n1] [|n2]; 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. by intros; simpl. Qed.
Next Obligation.
intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
eauto using cmra_unit_preserving, cmra_unit_validN.
@@ -193,14 +177,13 @@ Qed.
Program Definition uPred_own {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 x; exists x. Qed.
Next Obligation.
intros M a x1 x n1 n2 [a' Hx1] [x2 Hx] ??.
exists (a' â‹… x2). by rewrite (associative op) -(dist_le _ _ _ _ Hx1) // Hx.
Qed.
Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
{| uPred_holds n x := ✓{n} a |}.
-Solve Obligations with naive_solver eauto 2 using cmra_validN_le, cmra_validN_0.
+Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
@@ -329,18 +312,14 @@ Global Instance forall_proper A :
Proof. by intros P1 P2 HP12 x n'; split; intros HP a; apply HP12. 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 [|n']; [|split; intros [a ?]; exists a; apply HP].
-Qed.
+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 x n'; 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|].
- apply HPQ; eauto using cmra_validN_S.
+ apply (HPQ n'); eauto using cmra_validN_S.
Qed.
Global Instance later_proper :
Proper ((≡) ==> (≡)) (@uPred_later M) := ne_proper _.
@@ -364,10 +343,7 @@ 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] ??; first done.
- apply HQR; first eapply (HQP _ (S n)); eauto.
-Qed.
+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.
Lemma False_elim P : False ⊑ P.
@@ -395,9 +371,9 @@ Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
Lemma forall_elim {A} {P : A → uPred M} a : (∀ a, P a) ⊑ P a.
Proof. intros x n ? HP; apply HP. Qed.
Lemma exist_intro {A} {P : A → uPred M} a : P a ⊑ (∃ a, P a).
-Proof. by intros x [|n] ??; [done|exists a]. Qed.
+Proof. by intros x n ??; exists a. Qed.
Lemma exist_elim {A} (P : A → uPred M) Q : (∀ a, P a ⊑ Q) → (∃ a, P a) ⊑ Q.
-Proof. by intros HPQ x [|n] ?; [|intros [a ?]; apply HPQ with a]. Qed.
+Proof. by intros HPQ x n ? [a ?]; apply HPQ with a. Qed.
Lemma eq_refl {A : cofeT} (a : A) P : P ⊑ (a ≡ a).
Proof. by intros x n ??; simpl. Qed.
Lemma eq_rewrite {A : cofeT} P (Q : A → uPred M)
@@ -408,12 +384,11 @@ Qed.
Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
True ⊑ (a ≡ b) → a ≡ b.
Proof.
- intros Hab; apply equiv_dist; intros n; apply Hab with ∅.
- * apply cmra_valid_validN, cmra_empty_valid.
- * by destruct n.
+ intros Hab; apply equiv_dist; intros n; apply Hab with ∅; last done.
+ 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 (S n)]. Qed.
+Proof. by intros HPQ x n ?; split; intros; apply HPQ with x n. Qed.
(* Derived logical stuff *)
Lemma and_elim_l' P Q R : P ⊑ R → (P ∧ Q) ⊑ R.
@@ -577,7 +552,7 @@ Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
Proof.
intros P x n Hvalid; split.
* intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
- * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite cmra_unit_l].
+ * by intros ?; exists (unit x), x; rewrite cmra_unit_l.
Qed.
Global Instance sep_commutative : Commutative (≡) (@uPred_sep M).
Proof.
@@ -702,8 +677,9 @@ Proof. intros x [|[|n]]; split; done || by exists inhabitant; simpl. Qed.
Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
Proof.
intros x n ?; split.
- * destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
- destruct (cmra_extend_op n x x1 x2)
+ * 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)
as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
* destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
@@ -823,15 +799,15 @@ Qed.
Lemma always_own (a : M) : unit a ≡ a → (□ uPred_own a)%I ≡ uPred_own a.
Proof. by intros <-; rewrite always_own_unit. Qed.
Lemma own_something : True ⊑ ∃ a, uPred_own a.
-Proof. intros x [|n] ??; [done|]. by exists x; simpl. Qed.
+Proof. intros x n ??. by exists x; simpl. Qed.
Lemma own_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_own ∅.
-Proof. intros x [|n] ??; [done|]. by exists x; rewrite (left_id _ _). Qed.
+Proof. intros x n ??; by exists x; rewrite (left_id _ _). Qed.
Lemma own_valid (a : M) : uPred_own a ⊑ ✓ a.
Proof. intros x n 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.
-Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{1} a → ✓ a ⊑ False.
-Proof. intros Ha x [|n] ??; [|apply Ha, cmra_validN_le with (S n)]; auto. 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.
Lemma valid_mono {A B : cmraT} (a : A) (b : B) :
(∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊑ ✓ b.
Proof. by intros ? x n ?; simpl; auto. Qed.
@@ -839,7 +815,7 @@ Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a))%I ≡ (✓ a : uPred M)%I
Proof. done. Qed.
(* Own and valid derived *)
-Lemma own_invalid (a : M) : ¬ ✓{1} a → uPred_own a ⊑ False.
+Lemma own_invalid (a : M) : ¬ ✓{0} a → uPred_own a ⊑ False.
Proof. by intros; rewrite own_valid valid_elim. Qed.
(* Big ops *)
@@ -873,13 +849,13 @@ Lemma uPred_big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊑ P.
Proof. induction 1; simpl; auto. Qed.
(* Timeless *)
-Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 1 x → P n x.
+Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 0 x → P n x.
Proof.
split.
- * intros HP x n ??; induction n as [|[|n]]; auto.
- by destruct (HP x (S (S n))); auto using cmra_validN_S.
- * move=> HP x [|[|n]] /=; auto; left.
- apply HP, uPred_weaken with x (S n); eauto using cmra_validN_le.
+ * 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.
Qed.
Global Instance const_timeless φ : TimelessP (■φ : uPred M)%I.
Proof. by apply timelessP_spec=> x [|n]. Qed.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 29df1e9d2..f6e81accf 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -3,8 +3,9 @@ Require Import program_logic.wsat program_logic.ownership.
Local Hint Extern 10 (_ ≤ _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
Local Hint Extern 10 (✓{_} _) =>
- repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
- solve_validN.
+ repeat match goal with
+ | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
+ end; solve_validN.
Section adequacy.
Context {Λ : language} {Σ : iFunctor}.
@@ -67,7 +68,7 @@ Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
✓m →
{{ ownP σ1 ★ ownG m }} e1 @ coPset_all {{ Q }} →
rtc step ([e1],σ1) (t2,σ2) →
- ∃ rs2 Qs', wptp 3 t2 (Q :: Qs') rs2 ∧ wsat 3 coPset_all σ2 (big_op rs2).
+ ∃ rs2 Qs', wptp 2 t2 (Q :: Qs') rs2 ∧ wsat 2 coPset_all σ2 (big_op rs2).
Proof.
intros Hv ? [k ?]%rtc_nsteps.
eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
@@ -88,7 +89,7 @@ Proof.
as (rs2&Qs&Hwptp&?); auto.
{ by rewrite -(ht_mask_weaken E coPset_all). }
inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst.
- apply wp_value_inv in Hwp; destruct (Hwp (big_op rs) 3 ∅ σ2) as [r' []]; auto.
+ apply wp_value_inv in Hwp; destruct (Hwp (big_op rs) 2 ∅ σ2) as [r' []]; auto.
by rewrite right_id_L.
Qed.
Lemma ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2 :
@@ -100,9 +101,9 @@ Proof.
intros Hv ? Hs [i ?]%elem_of_list_lookup He.
destruct (ht_adequacy_own Q e1 t2 σ1 m σ2) as (rs2&Qs&?&?); auto.
{ by rewrite -(ht_mask_weaken E coPset_all). }
- destruct (Forall3_lookup_l (λ e Q r, wp coPset_all e Q 3 r) t2
+ destruct (Forall3_lookup_l (λ e Q r, wp coPset_all e Q 2 r) t2
(Q :: Qs) rs2 i e2) as (Q'&r2&?&?&Hwp); auto.
- destruct (wp_step_inv coPset_all ∅ Q' e2 2 3 σ2 r2 (big_op (delete i rs2)));
+ destruct (wp_step_inv coPset_all ∅ Q' e2 1 2 σ2 r2 (big_op (delete i rs2)));
rewrite ?right_id_L ?big_op_delete; auto.
Qed.
Theorem ht_adequacy_safe E Q e1 t2 σ1 m σ2 :
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 3b474e67a..e72e87a05 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -3,8 +3,9 @@ Require Import program_logic.wsat program_logic.ownership.
Local Hint Extern 10 (_ ≤ _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
Local Hint Extern 10 (✓{_} _) =>
- repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
- solve_validN.
+ repeat match goal with
+ | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
+ end; solve_validN.
Section lifting.
Context {Λ : language} {Σ : iFunctor}.
@@ -45,10 +46,10 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Q e1 :
(∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
(▷ ∀ e2 ef, ■φ e2 ef → wp E e2 Q ★ wp_fork ef) ⊑ wp E e1 Q.
Proof.
- intros He Hsafe Hstep r [|n] ?; [done|]; intros Hwp; constructor; auto.
- intros rf k Ef σ1 ???; split; [done|].
+ intros He Hsafe Hstep r n ? 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; [by destruct k|].
+ destruct (Hwp e2 ef r k) as (r1&r2&Hr&?&?); auto.
exists r1,r2; split_ands; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
Qed.
@@ -106,4 +107,3 @@ Proof.
Qed.
End lifting.
-
diff --git a/program_logic/model.v b/program_logic/model.v
index ca0bbec0c..dda84c106 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -23,8 +23,9 @@ 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' [??] P.
- by apply upredC_map_ne, resC_map_ne, laterC_map_contractive.
+ * 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.
Qed.
End iProp.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 2899d3b6a..d1f3a35d9 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -1,7 +1,7 @@
Require Export program_logic.model.
Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
- uPred_own (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
+ uPred_own (Res {[ i ↦ to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
Arguments ownI {_ _} _ _%I.
Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_own (Res ∅ (Excl σ) ∅).
Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_own (Res ∅ ∅ (Some m)).
@@ -21,9 +21,9 @@ Implicit Types m : iGst Λ Σ.
(* Invariants *)
Global Instance ownI_contractive i : Contractive (@ownI Λ Σ i).
Proof.
- intros n P Q HPQ.
- apply (_: Proper (_ ==> _) iProp_unfold), Later_contractive in HPQ.
- by unfold ownI; rewrite HPQ.
+ intros n P Q HPQ. rewrite /ownI.
+ apply uPred.own_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
+ by apply Next_contractive=> j ?; rewrite (HPQ j).
Qed.
Lemma always_ownI i P : (□ ownI i P)%I ≡ ownI i P.
Proof.
@@ -65,7 +65,7 @@ Proof. rewrite /ownG; apply _. Qed.
(* inversion lemmas *)
Lemma ownI_spec r n i P :
✓{n} r →
- (ownI i P) n r ↔ wld r !! i ≡{n}≡ Some (to_agree (Later (iProp_unfold P))).
+ (ownI i P) n r ↔ wld r !! i ≡{n}≡ Some (to_agree (Next (iProp_unfold P))).
Proof.
intros [??]; rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
* intros [(P'&Hi&HP) _]; rewrite Hi.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index f76066f5f..6184683cf 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -5,19 +5,19 @@ Local Hint Extern 10 (_ ≤ _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
Local Hint Extern 10 (✓{_} _) =>
- repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
- solve_validN.
+ repeat match goal with
+ | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
+ end; solve_validN.
Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
{| uPred_holds n r1 := ∀ rf k Ef σ,
- 1 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ →
+ 0 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ →
wsat k (E1 ∪ Ef) σ (r1 ⋅ rf) →
∃ r2, P k r2 ∧ wsat k (E2 ∪ Ef) σ (r2 ⋅ rf) |}.
Next Obligation.
intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia.
Qed.
-Next Obligation. intros Λ Σ E1 E2 P r rf k Ef σ; simpl in *; lia. Qed.
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 ?(associative op); auto.
@@ -121,7 +121,7 @@ Proof.
intros ? r [|n] ? 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. }
- exists (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
+ 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 e6c145f52..77d718f57 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -38,8 +38,8 @@ Global Instance wld_proper : Proper ((≡) ==> (≡)) (@wld Λ Σ A).
Proof. by destruct 1. Qed.
Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ Σ A).
Proof. by destruct 1. Qed.
-Global Instance pst_ne' n : Proper (dist (S n) ==> (≡)) (@pst Λ Σ A).
-Proof. destruct 1; apply (timeless _), dist_le with (S n); auto with lia. Qed.
+Global Instance pst_ne' n : Proper (dist n ==> (≡)) (@pst Λ Σ A).
+Proof. destruct 1; apply (timeless _), dist_le with n; auto with lia. Qed.
Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Λ Σ A).
Proof. by destruct 1; unfold_leibniz. Qed.
Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ Σ A).
@@ -60,7 +60,6 @@ Proof.
+ by destruct 1; constructor.
+ do 2 destruct 1; constructor; etransitivity; eauto.
* by destruct 1; constructor; apply dist_S.
- * done.
* intros c n; constructor.
+ apply (conv_compl (chain_map wld c) n).
+ apply (conv_compl (chain_map pst c) n).
@@ -102,7 +101,6 @@ Proof.
* by intros n [???] ? [???] (?&?&?); split_ands'; simpl in *; cofe_subst.
* by intros n [???] ? [???] [???] ? [???];
constructor; simpl in *; cofe_subst.
- * done.
* by intros n ? (?&?&?); split_ands'; apply cmra_validN_S.
* intros ???; constructor; simpl; apply (associative _).
* intros ??; constructor; simpl; apply (commutative _).
@@ -220,9 +218,5 @@ Program Definition resF {Λ Σ} : iFunctor := {|
ifunctor_car := resRA Λ Σ;
ifunctor_map A B := resC_map
|}.
-Next Obligation.
- intros Λ Σ A x. by rewrite /= res_map_id.
-Qed.
-Next Obligation.
- intros Λ Σ A B C f g x. by rewrite /= res_map_compose.
-Qed.
+Next Obligation. intros Λ Σ A x. by rewrite /= res_map_id. Qed.
+Next Obligation. intros Λ Σ A B C f g x. by rewrite /= res_map_compose. Qed.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 3618e8753..1f03296f3 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -5,8 +5,9 @@ Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
Local Hint Extern 100 (@subseteq coPset _ _ _) => solve_elem_of.
Local Hint Extern 10 (✓{_} _) =>
- repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
- solve_validN.
+ repeat match goal with
+ | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
+ end; solve_validN.
Record wp_go {Λ Σ} (E : coPset) (Q Qfork : expr Λ → nat → iRes Λ Σ → Prop)
(k : nat) (rf : iRes Λ Σ) (e1 : expr Λ) (σ1 : state Λ) := {
@@ -24,7 +25,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset)
| wp_pre_step n r1 e1 :
to_val e1 = None →
(∀ rf k Ef σ1,
- 1 < k < n → E ∩ Ef = ∅ →
+ 0 < k < n → E ∩ Ef = ∅ →
wsat (S k) (E ∪ Ef) σ1 (r1 ⋅ rf) →
wp_go (E ∪ Ef) (wp_pre E Q)
(wp_pre coPset_all (λ _, True%I)) k rf e1 σ1) →
@@ -36,11 +37,6 @@ Next Obligation.
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 Q r; destruct (to_val e) as [v|] eqn:?.
- * by rewrite -(of_to_val e v) //; constructor.
- * constructor; auto with lia.
-Qed.
Next Obligation.
intros Λ Σ E e Q r1 r2 n1; revert Q E e r1 r2.
induction n1 as [n1 IH] using lt_wf_ind; intros Q E e r1 r1' n2.
@@ -104,7 +100,7 @@ Proof.
by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_equality.
Qed.
Lemma wp_step_inv E Ef Q e k n σ r rf :
- to_val e = None → 1 < k < n → E ∩ Ef = ∅ →
+ to_val e = None → 0 < k < n → E ∩ Ef = ∅ →
wp E e Q n r → wsat (S k) (E ∪ Ef) σ (r ⋅ rf) →
wp_go (E ∪ Ef) (λ e, wp E e Q) (λ e, wp coPset_all e (λ _, True%I)) k rf e σ.
Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
@@ -113,7 +109,7 @@ Lemma wp_value E Q v : Q v ⊑ wp E (of_val v) Q.
Proof. by constructor; apply pvs_intro. Qed.
Lemma pvs_wp E e Q : pvs E E (wp E e Q) ⊑ wp E e Q.
Proof.
- intros r [|n] ?; [done|]; intros Hvs.
+ intros r n ? 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. }
@@ -171,8 +167,8 @@ Lemma wp_frame_later_r E e Q R :
to_val e = None → (wp E e Q ★ ▷ R) ⊑ wp E e (λ v, Q v ★ R).
Proof.
intros He r' n 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|done|].
- constructor; [done|intros rf k Ef σ1 ???].
+ 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 ?(associative _);auto.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 6ec7b21a4..b187cd744 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -12,7 +12,7 @@ Record wsat_pre {Λ Σ} (n : nat) (E : coPset)
wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i);
wsat_pre_wld i P :
i ∈ E →
- wld r !! i ≡{S n}≡ Some (to_agree (Later (iProp_unfold P))) →
+ wld r !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) →
∃ r', rs !! i = Some r' ∧ P n r'
}.
Arguments wsat_pre_valid {_ _ _ _ _ _ _} _.
@@ -50,22 +50,22 @@ Proof.
intros [rs [Hval Hσ HE Hwld]] ?; exists rs; constructor; auto.
intros i P ? HiP; destruct (wld (r â‹… big_opM rs) !! i) as [P'|] eqn:HP';
[apply (injective Some) in HiP|inversion_clear HiP].
- assert (P' ≡{S n}≡ to_agree $ Later $ iProp_unfold $
+ assert (P' ≡{S n}≡ to_agree $ Next $ iProp_unfold $
iProp_fold $ later_car $ P' (S n)) as HPiso.
{ rewrite iProp_unfold_fold later_eta to_agree_car //.
apply (map_lookup_validN _ (wld (r â‹… big_opM rs)) i); rewrite ?HP'; auto. }
assert (P ≡{n'}≡ iProp_fold (later_car (P' (S n)))) as HPP'.
- { apply (injective iProp_unfold), (injective Later), (injective to_agree).
+ { apply (injective iProp_unfold), (injective Next), (injective to_agree).
by rewrite -HiP -(dist_le _ _ _ _ HPiso). }
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].
Qed.
-Lemma wsat_valid n E σ r : wsat n E σ r → ✓{n} r.
+Lemma wsat_valid n E σ r : n ≠0 → wsat n E σ r → ✓{n} r.
Proof.
- destruct n; [done|intros [rs ?]].
- eapply cmra_validN_op_l, wsat_pre_valid; eauto.
+ destruct n; first done.
+ intros _ [rs ?]; eapply cmra_validN_op_l, wsat_pre_valid; eauto.
Qed.
Lemma wsat_init k E σ mm : ✓{S k} mm → wsat (S k) E σ (Res ∅ (Excl σ) mm).
Proof.
@@ -77,7 +77,7 @@ Proof.
* intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
Qed.
Lemma wsat_open n E σ r i P :
- wld r !! i ≡{S n}≡ Some (to_agree (Later (iProp_unfold P))) → i ∉ E →
+ wld r !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E →
wsat (S n) ({[i]} ∪ E) σ r → ∃ rP, wsat (S n) E σ (rP ⋅ r) ∧ P n rP.
Proof.
intros HiP Hi [rs [Hval Hσ HE Hwld]].
@@ -92,7 +92,7 @@ Proof.
apply Hwld; [solve_elem_of +Hj|done].
Qed.
Lemma wsat_close n E σ r i P rP :
- wld rP !! i ≡{S n}≡ Some (to_agree (Later (iProp_unfold P))) → i ∉ E →
+ wld rP !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E →
wsat (S n) E σ (rP ⋅ r) → P n rP → wsat (S n) ({[i]} ∪ E) σ r.
Proof.
intros HiP HiE [rs [Hval Hσ HE Hwld]] ?.
@@ -106,7 +106,7 @@ Proof.
* intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst.
+ rewrite !lookup_wld_op_l ?HiP; auto=> HP.
apply (injective Some), (injective to_agree),
- (injective Later), (injective iProp_unfold) in HP.
+ (injective Next), (injective iProp_unfold) in HP.
exists rP; split; [rewrite lookup_insert|apply HP]; auto.
+ intros. destruct (Hwld j P') as (r'&?&?); auto.
exists r'; rewrite lookup_insert_ne; naive_solver.
@@ -117,7 +117,7 @@ Lemma wsat_update_pst n E σ1 σ1' r rf :
Proof.
intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in *.
assert (pst rf ⋅ pst (big_opM rs) = ∅) as Hpst'.
- { by apply: (excl_validN_inv_l n σ1); rewrite -Hpst_r associative. }
+ { by apply: (excl_validN_inv_l (S n) σ1); rewrite -Hpst_r associative. }
assert (σ1' = σ1) as ->.
{ apply leibniz_equiv, (timeless _), dist_le with (S n); auto.
apply (injective Excl).
@@ -130,14 +130,14 @@ 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)) n) as ([m2|]&?&Hval'); try done.
+ destruct (Hup (mf â‹… gst (rf â‹… big_opM rs)) (S n)) as ([m2|]&?&Hval'); try done.
{ by rewrite /= (associative _ mm1) -Hr associative. }
exists m2; split; [exists rs; split; split_ands'; auto|done].
Qed.
Lemma wsat_alloc n E1 E2 σ r P rP :
¬set_finite E1 → P n rP → wsat (S n) (E1 ∪ E2) σ (rP ⋅ r) →
∃ i, wsat (S n) (E1 ∪ E2) σ
- (Res {[i ↦ to_agree (Later (iProp_unfold P))]} ∅ ∅ ⋅ r) ∧
+ (Res {[i ↦ to_agree (Next (iProp_unfold P))]} ∅ ∅ ⋅ r) ∧
wld r !! i = None ∧ i ∈ E1.
Proof.
intros HE1 ? [rs [Hval Hσ HE Hwld]].
@@ -167,7 +167,7 @@ Proof.
* intros j P'; rewrite -associative Hr; destruct (decide (j=i)) as [->|].
+ rewrite /= !lookup_op Hri HrPi Hrsi right_id lookup_singleton=>? HP.
apply (injective Some), (injective to_agree),
- (injective Later), (injective iProp_unfold) in HP.
+ (injective Next), (injective iProp_unfold) in HP.
exists rP; rewrite lookup_insert; split; [|apply HP]; auto.
+ rewrite /= lookup_op lookup_singleton_ne // left_id=> ??.
destruct (Hwld j P') as [r' ?]; auto.
--
GitLab