From 8c96ad4e7e90e599ef318048935faf23f94dfe4b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Feb 2016 22:48:51 +0100
Subject: [PATCH] Shorter names for common math notions.
Also do some minor clean up.
---
algebra/agree.v | 22 ++---
algebra/auth.v | 12 +--
algebra/cmra.v | 64 ++++++-------
algebra/cmra_big_op.v | 10 +--
algebra/cmra_tactics.v | 2 +-
algebra/cofe.v | 2 +-
algebra/dra.v | 18 ++--
algebra/excl.v | 4 +-
algebra/fin_maps.v | 6 +-
algebra/iprod.v | 6 +-
algebra/option.v | 8 +-
algebra/sts.v | 2 +-
algebra/upred.v | 136 ++++++++++++++--------------
heap_lang/heap_lang.v | 10 +--
heap_lang/lifting.v | 2 +-
heap_lang/tests.v | 2 +-
prelude/base.v | 164 ++++++++++++++++------------------
prelude/countable.v | 20 ++---
prelude/decidable.v | 2 +-
prelude/error.v | 4 +-
prelude/fin_collections.v | 2 +-
prelude/fin_maps.v | 60 ++++++-------
prelude/finite.v | 58 ++++++------
prelude/gmap.v | 2 +-
prelude/list.v | 136 ++++++++++++++--------------
prelude/numbers.v | 26 +++---
prelude/option.v | 10 +--
prelude/orders.v | 72 +++++++--------
prelude/pmap.v | 32 +++----
prelude/pretty.v | 2 +-
prelude/strings.v | 2 +-
prelude/tactics.v | 4 +-
prelude/vector.v | 4 +-
program_logic/adequacy.v | 6 +-
program_logic/auth.v | 18 ++--
program_logic/hoare.v | 18 ++--
program_logic/hoare_lifting.v | 26 +++---
program_logic/invariants.v | 14 +--
program_logic/language.v | 4 +-
program_logic/lifting.v | 8 +-
program_logic/model.v | 4 +-
program_logic/ownership.v | 4 +-
program_logic/pviewshifts.v | 24 ++---
program_logic/resources.v | 14 +--
program_logic/viewshifts.v | 12 +--
program_logic/weakestpre.v | 28 +++---
program_logic/wsat.v | 38 ++++----
47 files changed, 554 insertions(+), 570 deletions(-)
diff --git a/algebra/agree.v b/algebra/agree.v
index 3e51ad085..e85de4ec8 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -59,9 +59,9 @@ Program Instance agree_op : Op (agree A) := λ x y,
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.
-Instance: Commutative (≡) (@op (agree A) _).
+Instance: Comm (≡) (@op (agree A) _).
Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
-Definition agree_idempotent (x : agree A) : x ⋅ x ≡ x.
+Definition agree_idemp (x : agree A) : x ⋅ x ≡ x.
Proof. split; naive_solver. Qed.
Instance: ∀ n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n).
Proof.
@@ -79,18 +79,18 @@ Proof.
eauto using agree_valid_le.
Qed.
Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
-Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(commutative _ _ y2) Hx. Qed.
+Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
Instance: Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
-Instance: Associative (≡) (@op (agree A) _).
+Instance: Assoc (≡) (@op (agree A) _).
Proof.
intros x y z; split; simpl; intuition;
repeat match goal with H : agree_is_valid _ _ |- _ => clear H end;
- by cofe_subst; rewrite !agree_idempotent.
+ by cofe_subst; rewrite !agree_idemp.
Qed.
Lemma agree_includedN (x y : agree A) n : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y.
Proof.
split; [|by intros ?; exists y].
- by intros [z Hz]; rewrite Hz (associative _) agree_idempotent.
+ by intros [z Hz]; rewrite Hz assoc agree_idemp.
Qed.
Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof.
@@ -99,7 +99,7 @@ Proof.
* 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.
- * intros x; apply agree_idempotent.
+ * intros x; apply agree_idemp.
* by intros x y n [(?&?&?) ?].
* by intros x y n; rewrite agree_includedN.
Qed.
@@ -108,13 +108,13 @@ Proof. intros Hxy; apply Hxy. Qed.
Lemma agree_valid_includedN (x y : agree A) n : ✓{n} y → x ≼{n} y → x ≡{n}≡ y.
Proof.
move=> Hval [z Hy]; move: Hval; rewrite Hy.
- by move=> /agree_op_inv->; rewrite agree_idempotent.
+ by move=> /agree_op_inv->; rewrite agree_idemp.
Qed.
Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A).
Proof.
intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
- * by rewrite agree_idempotent.
- * by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idempotent.
+ * by rewrite agree_idemp.
+ * by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
Qed.
Canonical Structure agreeRA : cmraT :=
CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin.
@@ -125,7 +125,7 @@ Solve Obligations with done.
Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree.
Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
-Global Instance to_agree_inj n : Injective (dist n) (dist n) (to_agree).
+Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree).
Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
diff --git a/algebra/auth.v b/algebra/auth.v
index 924b06c6b..d21944475 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -106,10 +106,10 @@ Proof.
* by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
* intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
- * by split; simpl; rewrite associative.
- * by split; simpl; rewrite commutative.
+ * by split; simpl; rewrite assoc.
+ * by split; simpl; rewrite comm.
* by split; simpl; rewrite ?cmra_unit_l.
- * by split; simpl; rewrite ?cmra_unit_idempotent.
+ * by split; simpl; rewrite ?cmra_unit_idemp.
* intros n ??; rewrite! auth_includedN; intros [??].
by split; simpl; apply cmra_unit_preservingN.
* assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
@@ -153,8 +153,8 @@ Lemma auth_update a a' b b' :
Proof.
move=> Hab [[?| |] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
destruct (Hab n (bf1 â‹… bf2)) as [Ha' ?]; auto.
- { by rewrite Ha left_id associative. }
- split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done].
+ { by rewrite Ha left_id assoc. }
+ split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done].
Qed.
Lemma auth_local_update L `{!LocalUpdate Lv L} a a' :
@@ -170,7 +170,7 @@ Lemma auth_update_op_l a a' b :
Proof. by intros; apply (auth_local_update _). Qed.
Lemma auth_update_op_r a a' b :
✓ (a ⋅ b) → ◠a ⋅ ◯ a' ~~> ◠(a ⋅ b) ⋅ ◯ (a' ⋅ b).
-Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed.
+Proof. rewrite -!(comm _ b); apply auth_update_op_l. Qed.
(* This does not seem to follow from auth_local_update.
The trouble is that given ✓ (L a ⋅ a'), Lv a
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 94672a03c..94a13c0c1 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -43,10 +43,10 @@ Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
(* valid *)
mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
(* monoid *)
- mixin_cmra_associative : Associative (≡) (⋅);
- mixin_cmra_commutative : Commutative (≡) (⋅);
+ mixin_cmra_assoc : Assoc (≡) (⋅);
+ mixin_cmra_comm : Comm (≡) (⋅);
mixin_cmra_unit_l x : unit x ⋅ x ≡ x;
- mixin_cmra_unit_idempotent x : unit (unit x) ≡ unit x;
+ mixin_cmra_unit_idemp x : unit (unit x) ≡ unit x;
mixin_cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y;
mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y
@@ -101,14 +101,14 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_minus_ne _ (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 _).
- Proof. apply (mixin_cmra_associative _ (cmra_mixin A)). Qed.
- Global Instance cmra_commutative : Commutative (≡) (@op A _).
- Proof. apply (mixin_cmra_commutative _ (cmra_mixin A)). Qed.
+ Global Instance cmra_assoc : Assoc (≡) (@op A _).
+ Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed.
+ Global Instance cmra_comm : Comm (≡) (@op A _).
+ Proof. apply (mixin_cmra_comm _ (cmra_mixin A)). Qed.
Lemma cmra_unit_l x : unit x ⋅ x ≡ x.
Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed.
- Lemma cmra_unit_idempotent x : unit (unit x) ≡ unit x.
- Proof. apply (mixin_cmra_unit_idempotent _ (cmra_mixin A)). Qed.
+ Lemma cmra_unit_idemp x : unit (unit x) ≡ unit x.
+ Proof. apply (mixin_cmra_unit_idemp _ (cmra_mixin A)). Qed.
Lemma cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y.
Proof. apply (mixin_cmra_unit_preservingN _ (cmra_mixin A)). Qed.
Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
@@ -166,7 +166,7 @@ Proof. apply (ne_proper _). Qed.
Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
Proof.
intros x1 x2 Hx y1 y2 Hy.
- by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
+ by rewrite Hy (comm _ x1) Hx (comm _ y2).
Qed.
Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
Proof. apply (ne_proper_2 _). Qed.
@@ -217,15 +217,15 @@ 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.
-Proof. rewrite (commutative _ x); apply cmra_validN_op_l. Qed.
+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.
(** ** Units *)
Lemma cmra_unit_r x : x ⋅ unit x ≡ x.
-Proof. by rewrite (commutative _ x) cmra_unit_l. Qed.
+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_idempotent x) cmra_unit_r. Qed.
+Proof. by rewrite -{2}(cmra_unit_idemp x) cmra_unit_r. Qed.
Lemma cmra_unit_validN x n : ✓{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.
@@ -243,7 +243,7 @@ Proof.
split.
* by intros x; exists (unit x); rewrite cmra_unit_r.
* intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
- by rewrite (associative _) -Hy -Hz.
+ by rewrite assoc -Hy -Hz.
Qed.
Global Instance cmra_included_preorder: PreOrder (@included A _ _).
Proof.
@@ -265,22 +265,22 @@ Proof. by exists y. Qed.
Lemma cmra_included_l x y : x ≼ x ⋅ y.
Proof. by exists y. Qed.
Lemma cmra_includedN_r n x y : y ≼{n} x ⋅ y.
-Proof. rewrite (commutative op); apply cmra_includedN_l. Qed.
+Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
Lemma cmra_included_r x y : y ≼ x ⋅ y.
-Proof. rewrite (commutative op); apply cmra_included_l. Qed.
+Proof. rewrite (comm op); apply cmra_included_l. Qed.
Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y.
Proof. rewrite !cmra_included_includedN; eauto using cmra_unit_preservingN. Qed.
Lemma cmra_included_unit x : unit x ≼ x.
Proof. by exists x; rewrite cmra_unit_l. Qed.
Lemma cmra_preservingN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
-Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
+Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
-Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
+Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
Lemma cmra_preservingN_r n x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z.
-Proof. by intros; rewrite -!(commutative _ z); apply cmra_preservingN_l. Qed.
+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 -!(commutative _ z); apply cmra_preserving_l. Qed.
+Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
Lemma cmra_included_dist_l x1 x2 x1' n :
x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2.
@@ -321,7 +321,7 @@ Section identity.
Lemma cmra_empty_least x : ∅ ≼ x.
Proof. by exists x; rewrite left_id. Qed.
Global Instance cmra_empty_right_id : RightId (≡) ∅ (⋅).
- Proof. by intros x; rewrite (commutative op) left_id. Qed.
+ Proof. by intros x; rewrite (comm op) left_id. Qed.
Lemma cmra_unit_empty : unit ∅ ≡ ∅.
Proof. by rewrite -{2}(cmra_unit_l ∅) right_id. Qed.
End identity.
@@ -336,7 +336,7 @@ Lemma local_update L `{!LocalUpdate Lv L} x y :
Proof. by rewrite equiv_dist=>?? n; apply (local_updateN L). Qed.
Global Instance local_update_op x : LocalUpdate (λ _, True) (op x).
-Proof. split. apply _. by intros n y1 y2 _ _; rewrite associative. Qed.
+Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.
(** ** Updates *)
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
@@ -366,10 +366,10 @@ 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 associative.
+ destruct (Hx1 (x2 â‹… z) n) as (y1&?&?); first by rewrite assoc.
destruct (Hx2 (y1 â‹… z) n) as (y2&?&?);
- first by rewrite associative (commutative _ x2) -associative.
- exists (y1 â‹… y2); split; last rewrite (commutative _ y1) -associative; auto.
+ first by rewrite assoc (comm _ x2) -assoc.
+ exists (y1 â‹… y2); split; last rewrite (comm _ y1) -assoc; auto.
Qed.
Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 :
x1 ~~>: P1 → x2 ~~>: P2 → x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2.
@@ -448,10 +448,10 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
ra_validN_ne :> Proper ((≡) ==> impl) valid;
ra_minus_ne :> Proper ((≡) ==> (≡) ==> (≡)) minus;
(* monoid *)
- ra_associative :> Associative (≡) (⋅);
- ra_commutative :> Commutative (≡) (⋅);
+ ra_assoc :> Assoc (≡) (⋅);
+ ra_comm :> Comm (≡) (⋅);
ra_unit_l x : unit x ⋅ x ≡ x;
- ra_unit_idempotent x : unit (unit x) ≡ unit x;
+ ra_unit_idemp x : unit (unit x) ≡ unit x;
ra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x;
ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
@@ -524,10 +524,10 @@ Section prod.
* by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
* by intros n x [??]; split; apply cmra_validN_S.
- * split; simpl; apply (associative _).
- * split; simpl; apply (commutative _).
- * split; simpl; apply cmra_unit_l.
- * split; simpl; apply cmra_unit_idempotent.
+ * by split; rewrite /= assoc.
+ * by split; rewrite /= comm.
+ * by split; rewrite /= cmra_unit_l.
+ * by split; rewrite /= cmra_unit_idemp.
* 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.
diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index a6f9ee8af..58dfbeaab 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -22,21 +22,21 @@ Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
Proof.
induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
* by rewrite IH.
- * by rewrite !(associative _) (commutative _ x).
+ * by rewrite !assoc (comm _ x).
* by transitivity (big_op xs2).
Qed.
Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
Proof.
- induction xs as [|x xs IH]; simpl; first by rewrite ?(left_id _ _).
- by rewrite IH (associative _).
+ induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
+ by rewrite IH assoc.
Qed.
Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys.
Proof.
induction 1 as [|x xs ys|x y xs|x xs ys|xs ys zs]; rewrite //=.
* by apply cmra_preserving_l.
- * by rewrite !associative (commutative _ y).
+ * by rewrite !assoc (comm _ y).
* by transitivity (big_op ys); last apply cmra_included_r.
* by transitivity (big_op ys).
Qed.
@@ -58,7 +58,7 @@ Qed.
Lemma big_opM_singleton i x : big_opM ({[i ↦ x]} : M A) ≡ x.
Proof.
rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
- by rewrite big_opM_empty (right_id _ _).
+ by rewrite big_opM_empty right_id.
Qed.
Global Instance big_opM_proper : Proper ((≡) ==> (≡)) (big_opM : M A → _).
Proof.
diff --git a/algebra/cmra_tactics.v b/algebra/cmra_tactics.v
index 27b6efb85..a9eb5bb43 100644
--- a/algebra/cmra_tactics.v
+++ b/algebra/cmra_tactics.v
@@ -25,7 +25,7 @@ Module ra_reflection. Section ra_reflection.
eval Σ e ≡ big_op ((λ n, from_option ∅ (Σ !! n)) <$> flatten e).
Proof.
by induction e as [| |e1 IH1 e2 IH2];
- rewrite /= ?(right_id _ _) ?fmap_app ?big_op_app ?IH1 ?IH2.
+ rewrite /= ?right_id ?fmap_app ?big_op_app ?IH1 ?IH2.
Qed.
Lemma flatten_correct Σ e1 e2 :
flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index ae0a93f7c..550c2fc5a 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -337,7 +337,7 @@ Section later.
Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
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).
+ Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
Proof. by intros x y. Qed.
End later.
diff --git a/algebra/dra.v b/algebra/dra.v
index 093fc8f68..625978f63 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -46,14 +46,14 @@ Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
dra_unit_valid x : ✓ x → ✓ unit x;
dra_minus_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ⩪ x);
(* monoid *)
- dra_associative :> Associative (≡) (⋅);
+ dra_assoc :> Assoc (≡) (⋅);
dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
dra_disjoint_move_l x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
dra_symmetric :> Symmetric (@disjoint A _);
- dra_commutative x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
+ dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
dra_unit_disjoint_l x : ✓ x → unit x ⊥ x;
dra_unit_l x : ✓ x → unit x ⋅ x ≡ x;
- dra_unit_idempotent x : ✓ x → unit (unit x) ≡ unit x;
+ dra_unit_idemp x : ✓ x → unit (unit x) ≡ unit x;
dra_unit_preserving x y : ✓ x → ✓ y → x ≼ y → unit x ≼ unit y;
dra_disjoint_minus x y : ✓ x → ✓ y → x ≼ y → x ⊥ y ⩪ x;
dra_op_minus x y : ✓ x → ✓ y → x ≼ y → x ⋅ y ⩪ x ≡ y
@@ -73,12 +73,12 @@ Qed.
Lemma dra_disjoint_rl x y z : ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⊥ y.
Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed.
Lemma dra_disjoint_lr x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z.
-Proof. intros ????. rewrite dra_commutative //. by apply dra_disjoint_ll. Qed.
+Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
Lemma dra_disjoint_move_r x y z :
✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z.
Proof.
- intros; symmetry; rewrite dra_commutative; eauto using dra_disjoint_rl.
- apply dra_disjoint_move_l; auto; by rewrite dra_commutative.
+ intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
+ apply dra_disjoint_move_l; auto; by rewrite dra_comm.
Qed.
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Hint Unfold dra_included.
@@ -114,11 +114,11 @@ Proof.
+ exists z. by rewrite Hx ?Hy; tauto.
* intros [x px ?] [y py ?] [z pz ?]; split; simpl;
[intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
- |intros; apply (associative _)].
- * intros [x px ?] [y py ?]; split; naive_solver eauto using dra_commutative.
+ |by intros; rewrite assoc].
+ * intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
* intros [x px ?]; split;
naive_solver eauto using dra_unit_l, dra_unit_disjoint_l.
- * intros [x px ?]; split; naive_solver eauto using dra_unit_idempotent.
+ * intros [x px ?]; split; naive_solver eauto using dra_unit_idemp.
* intros x y Hxy; exists (unit y ⩪ unit x).
destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *.
assert (py → unit x ≼ unit y)
diff --git a/algebra/excl.v b/algebra/excl.v
index db3d83f2f..cf50b1f71 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -31,9 +31,9 @@ Global Instance Excl_ne : Proper (dist n ==> dist n) (@Excl A).
Proof. by constructor. Qed.
Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A).
Proof. by constructor. Qed.
-Global Instance Excl_inj : Injective (≡) (≡) (@Excl A).
+Global Instance Excl_inj : Inj (≡) (≡) (@Excl A).
Proof. by inversion_clear 1. Qed.
-Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A).
+Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
Proof. by inversion_clear 1. Qed.
Program Definition excl_chain
(c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A :=
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 121be983e..f6410f94e 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -121,10 +121,10 @@ Proof.
* 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).
* 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.
+ * by intros m1 m2 m3 i; rewrite !lookup_op assoc.
+ * by intros m1 m2 i; rewrite !lookup_op comm.
* by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l.
- * by intros m i; rewrite !lookup_unit cmra_unit_idempotent.
+ * by intros m i; rewrite !lookup_unit cmra_unit_idemp.
* intros n x y; rewrite !map_includedN_spec; intros Hm i.
by rewrite !lookup_unit; apply cmra_unit_preservingN.
* intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 89d1919e3..ff77fd0aa 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -141,10 +141,10 @@ Section iprod_cmra.
* 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).
* 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.
+ * by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc.
+ * by intros f1 f2 x; rewrite iprod_lookup_op comm.
* by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l.
- * by intros f x; rewrite iprod_lookup_unit cmra_unit_idempotent.
+ * by intros f x; rewrite iprod_lookup_unit cmra_unit_idemp.
* intros n f1 f2; rewrite !iprod_includedN_spec=> Hf x.
by rewrite iprod_lookup_unit; apply cmra_unit_preservingN, Hf.
* intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
diff --git a/algebra/option.v b/algebra/option.v
index cb0eec68e..11c3228fd 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -45,7 +45,7 @@ Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
Proof. by constructor. Qed.
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).
+Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
Proof. by inversion_clear 1. Qed.
Global Instance None_timeless : Timeless (@None A).
Proof. inversion_clear 1; constructor. Qed.
@@ -92,10 +92,10 @@ Proof.
* by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
* by destruct 1; inversion_clear 1; constructor; cofe_subst.
* 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.
+ * intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
+ * intros [x|] [y|]; constructor; rewrite 1?comm; auto.
* by intros [x|]; constructor; rewrite cmra_unit_l.
- * by intros [x|]; constructor; rewrite cmra_unit_idempotent.
+ * by intros [x|]; constructor; rewrite cmra_unit_idemp.
* 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 /=;
diff --git a/algebra/sts.v b/algebra/sts.v
index 4e699e1d3..af06fd1ee 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -151,7 +151,7 @@ Proof.
* intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst;
rewrite ?disjoint_union_difference; auto using closed_up with sts.
eapply closed_up_set; eauto 2 using closed_disjoint with sts.
- * intros [] [] []; constructor; rewrite ?(associative _); auto with sts.
+ * intros [] [] []; constructor; rewrite ?assoc; auto with sts.
* destruct 4; inversion_clear 1; constructor; auto with sts.
* destruct 4; inversion_clear 1; constructor; auto with sts.
* destruct 1; constructor; auto with sts.
diff --git a/algebra/upred.v b/algebra/upred.v
index e54f52b13..64c01202f 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -140,7 +140,7 @@ 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&?).
{ destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using cmra_included_l.
- apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
+ 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.
@@ -179,7 +179,7 @@ Program Definition uPred_ownM {M : cmraT} (a : M) : uPred M :=
Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite -Hx. 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.
+ exists (a' â‹… x2). by rewrite (assoc op) -(dist_le _ _ _ _ Hx1) // Hx.
Qed.
Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
{| uPred_holds n x := ✓{n} a |}.
@@ -245,11 +245,11 @@ Arguments uPred_holds {_} !_ _ _ /.
Global Instance: PreOrder (@uPred_entails M).
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
-Global Instance: AntiSymmetric (≡) (@uPred_entails M).
+Global Instance: AntiSymm (≡) (@uPred_entails M).
Proof. intros P Q HPQ HQP; split; auto. Qed.
Lemma equiv_spec P Q : P ≡ Q ↔ P ⊑ Q ∧ Q ⊑ P.
Proof.
- split; [|by intros [??]; apply (anti_symmetric (⊑))].
+ split; [|by intros [??]; apply (anti_symm (⊑))].
intros HPQ; split; intros x i; apply HPQ.
Qed.
Global Instance entails_proper :
@@ -434,7 +434,7 @@ Proof. intros; apply const_elim with φ; eauto. Qed.
Lemma const_elim_r φ Q R : (φ → Q ⊑ R) → (Q ∧ ■φ) ⊑ R.
Proof. intros; apply const_elim with φ; eauto. Qed.
Lemma const_equiv (φ : Prop) : φ → (■φ : uPred M)%I ≡ True%I.
-Proof. intros; apply (anti_symmetric _); auto using const_intro. Qed.
+Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊑ (a ≡ b).
Proof. intros ->; apply eq_refl. Qed.
Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊑ (b ≡ a).
@@ -484,57 +484,57 @@ Global Instance exist_mono' A :
Proper (pointwise_relation _ (⊑) ==> (⊑)) (@uPred_exist M A).
Proof. intros P1 P2; apply exist_mono. Qed.
-Global Instance and_idem : Idempotent (≡) (@uPred_and M).
-Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed.
-Global Instance or_idem : Idempotent (≡) (@uPred_or M).
-Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed.
-Global Instance and_comm : Commutative (≡) (@uPred_and M).
-Proof. intros P Q; apply (anti_symmetric (⊑)); auto. Qed.
+Global Instance and_idem : IdemP (≡) (@uPred_and M).
+Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
+Global Instance or_idem : IdemP (≡) (@uPred_or M).
+Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
+Global Instance and_comm : Comm (≡) (@uPred_and M).
+Proof. intros P Q; apply (anti_symm (⊑)); auto. Qed.
Global Instance True_and : LeftId (≡) True%I (@uPred_and M).
-Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed.
+Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
Global Instance and_True : RightId (≡) True%I (@uPred_and M).
-Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed.
+Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
Global Instance False_and : LeftAbsorb (≡) False%I (@uPred_and M).
-Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed.
+Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
Global Instance and_False : RightAbsorb (≡) False%I (@uPred_and M).
-Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed.
+Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
Global Instance True_or : LeftAbsorb (≡) True%I (@uPred_or M).
-Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed.
+Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
Global Instance or_True : RightAbsorb (≡) True%I (@uPred_or M).
-Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed.
+Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
Global Instance False_or : LeftId (≡) False%I (@uPred_or M).
-Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed.
+Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
Global Instance or_False : RightId (≡) False%I (@uPred_or M).
-Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed.
-Global Instance and_assoc : Associative (≡) (@uPred_and M).
-Proof. intros P Q R; apply (anti_symmetric (⊑)); auto. Qed.
-Global Instance or_comm : Commutative (≡) (@uPred_or M).
-Proof. intros P Q; apply (anti_symmetric (⊑)); auto. Qed.
-Global Instance or_assoc : Associative (≡) (@uPred_or M).
-Proof. intros P Q R; apply (anti_symmetric (⊑)); auto. Qed.
+Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
+Global Instance and_assoc : Assoc (≡) (@uPred_and M).
+Proof. intros P Q R; apply (anti_symm (⊑)); auto. Qed.
+Global Instance or_comm : Comm (≡) (@uPred_or M).
+Proof. intros P Q; apply (anti_symm (⊑)); auto. Qed.
+Global Instance or_assoc : Assoc (≡) (@uPred_or M).
+Proof. intros P Q R; apply (anti_symm (⊑)); auto. Qed.
Global Instance True_impl : LeftId (≡) True%I (@uPred_impl M).
Proof.
- intros P; apply (anti_symmetric (⊑)).
+ intros P; apply (anti_symm (⊑)).
* by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r.
* by apply impl_intro_l; rewrite left_id.
Qed.
Lemma or_and_l P Q R : (P ∨ Q ∧ R)%I ≡ ((P ∨ Q) ∧ (P ∨ R))%I.
Proof.
- apply (anti_symmetric (⊑)); first auto.
+ apply (anti_symm (⊑)); first auto.
do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
Qed.
Lemma or_and_r P Q R : (P ∧ Q ∨ R)%I ≡ ((P ∨ R) ∧ (Q ∨ R))%I.
-Proof. by rewrite -!(commutative _ R) or_and_l. Qed.
+Proof. by rewrite -!(comm _ R) or_and_l. Qed.
Lemma and_or_l P Q R : (P ∧ (Q ∨ R))%I ≡ (P ∧ Q ∨ P ∧ R)%I.
Proof.
- apply (anti_symmetric (⊑)); last auto.
+ apply (anti_symm (⊑)); last auto.
apply impl_elim_r', or_elim; apply impl_intro_l; auto.
Qed.
Lemma and_or_r P Q R : ((P ∨ Q) ∧ R)%I ≡ (P ∧ R ∨ Q ∧ R)%I.
-Proof. by rewrite -!(commutative _ R) and_or_l. Qed.
+Proof. by rewrite -!(comm _ R) and_or_l. Qed.
Lemma and_exist_l {A} P (Q : A → uPred M) : (P ∧ ∃ a, Q a)%I ≡ (∃ a, P ∧ Q a)%I.
Proof.
- apply (anti_symmetric (⊑)).
+ apply (anti_symm (⊑)).
- apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
by rewrite -(exist_intro a).
- apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
@@ -542,8 +542,8 @@ Proof.
Qed.
Lemma and_exist_r {A} P (Q : A → uPred M) : ((∃ a, Q a) ∧ P)%I ≡ (∃ a, Q a ∧ P)%I.
Proof.
- rewrite -(commutative _ P) and_exist_l.
- apply exist_proper=>a. by rewrite commutative.
+ rewrite -(comm _ P) and_exist_l.
+ apply exist_proper=>a. by rewrite comm.
Qed.
(* BI connectives *)
@@ -558,19 +558,19 @@ Proof.
* 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_commutative : Commutative (≡) (@uPred_sep M).
+Global Instance sep_comm : Comm (≡) (@uPred_sep M).
Proof.
by intros P Q x n ?; split;
- intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
+ intros (x1&x2&?&?&?); exists x2, x1; rewrite (comm op).
Qed.
-Global Instance sep_associative : Associative (≡) (@uPred_sep M).
+Global Instance sep_assoc : Assoc (≡) (@uPred_sep M).
Proof.
intros P Q R x n ?; split.
* intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 â‹… y1), y2; split_ands; auto.
- + by rewrite -(associative op) -Hy -Hx.
+ + by rewrite -(assoc op) -Hy -Hx.
+ by exists x1, y1.
* intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 â‹… x2); split_ands; auto.
- + by rewrite (associative op) -Hy -Hx.
+ + by rewrite (assoc op) -Hy -Hx.
+ by exists y2, x2.
Qed.
Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
@@ -595,11 +595,11 @@ Global Instance wand_mono' : Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@uPred_wan
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
Global Instance sep_True : RightId (≡) True%I (@uPred_sep M).
-Proof. by intros P; rewrite (commutative _) (left_id _ _). Qed.
+Proof. by intros P; rewrite comm left_id. Qed.
Lemma sep_elim_l P Q : (P ★ Q) ⊑ P.
-Proof. by rewrite (True_intro Q) (right_id _ _). Qed.
+Proof. by rewrite (True_intro Q) right_id. Qed.
Lemma sep_elim_r P Q : (P ★ Q) ⊑ Q.
-Proof. by rewrite (commutative (★))%I; apply sep_elim_l. Qed.
+Proof. by rewrite (comm (★))%I; apply sep_elim_l. Qed.
Lemma sep_elim_l' P Q R : P ⊑ R → (P ★ Q) ⊑ R.
Proof. intros ->; apply sep_elim_l. Qed.
Lemma sep_elim_r' P Q R : Q ⊑ R → (P ★ Q) ⊑ R.
@@ -610,9 +610,9 @@ Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
Lemma sep_intro_True_r P Q R : R ⊑ P → True ⊑ Q → R ⊑ (P ★ Q).
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
Lemma wand_intro_l P Q R : (Q ★ P) ⊑ R → P ⊑ (Q -★ R).
-Proof. rewrite (commutative _); apply wand_intro_r. Qed.
+Proof. rewrite comm; apply wand_intro_r. Qed.
Lemma wand_elim_r P Q : (P ★ (P -★ Q)) ⊑ Q.
-Proof. rewrite (commutative _ P); apply wand_elim_l. Qed.
+Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
Lemma wand_elim_l' P Q R : P ⊑ (Q -★ R) → (P ★ Q) ⊑ R.
Proof. intros ->; apply wand_elim_l. Qed.
Lemma wand_elim_r' P Q R : Q ⊑ (P -★ R) → (P ★ Q) ⊑ R.
@@ -627,9 +627,9 @@ Lemma const_elim_sep_r φ Q R : (φ → Q ⊑ R) → (Q ★ ■φ) ⊑ R.
Proof. intros; apply const_elim with φ; eauto. Qed.
Global Instance sep_False : LeftAbsorb (≡) False%I (@uPred_sep M).
-Proof. intros P; apply (anti_symmetric _); auto. Qed.
+Proof. intros P; apply (anti_symm _); auto. Qed.
Global Instance False_sep : RightAbsorb (≡) False%I (@uPred_sep M).
-Proof. intros P; apply (anti_symmetric _); auto. Qed.
+Proof. intros P; apply (anti_symm _); auto. Qed.
Lemma sep_and_l P Q R : (P ★ (Q ∧ R)) ⊑ ((P ★ Q) ∧ (P ★ R)).
Proof. auto. Qed.
@@ -637,22 +637,22 @@ Lemma sep_and_r P Q R : ((P ∧ Q) ★ R) ⊑ ((P ★ R) ∧ (Q ★ R)).
Proof. auto. Qed.
Lemma sep_or_l P Q R : (P ★ (Q ∨ R))%I ≡ ((P ★ Q) ∨ (P ★ R))%I.
Proof.
- apply (anti_symmetric (⊑)); last by eauto 8.
+ apply (anti_symm (⊑)); last by eauto 8.
apply wand_elim_r', or_elim; apply wand_intro_l.
- by apply or_intro_l.
- by apply or_intro_r.
Qed.
Lemma sep_or_r P Q R : ((P ∨ Q) ★ R)%I ≡ ((P ★ R) ∨ (Q ★ R))%I.
-Proof. by rewrite -!(commutative _ R) sep_or_l. Qed.
+Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
Lemma sep_exist_l {A} P (Q : A → uPred M) : (P ★ ∃ a, Q a)%I ≡ (∃ a, P ★ Q a)%I.
Proof.
- intros; apply (anti_symmetric (⊑)).
+ intros; apply (anti_symm (⊑)).
- apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
by rewrite -(exist_intro a).
- apply exist_elim=> a; apply sep_mono; auto using exist_intro.
Qed.
Lemma sep_exist_r {A} (P: A → uPred M) Q: ((∃ a, P a) ★ Q)%I ≡ (∃ a, P a ★ Q)%I.
-Proof. setoid_rewrite (commutative _ _ Q); apply sep_exist_l. Qed.
+Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
Lemma sep_forall_l {A} P (Q : A → uPred M) : (P ★ ∀ a, Q a) ⊑ (∀ a, P ★ Q a).
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Lemma sep_forall_r {A} (P : A → uPred M) Q : ((∀ a, P a) ★ Q) ⊑ (∀ a, P a ★ Q).
@@ -724,7 +724,7 @@ Qed.
Lemma always_intro P Q : □ P ⊑ Q → □ P ⊑ □ Q.
Proof.
intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
- by rewrite cmra_unit_idempotent.
+ by rewrite cmra_unit_idemp.
Qed.
Lemma always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
Proof. done. Qed.
@@ -741,7 +741,7 @@ Qed.
Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊑ (□ P ★ Q).
Proof.
intros x n ? [??]; exists (unit x), x; simpl in *.
- by rewrite cmra_unit_l cmra_unit_idempotent.
+ by rewrite cmra_unit_l cmra_unit_idemp.
Qed.
Lemma always_later P : (□ ▷ P)%I ≡ (▷ □ P)%I.
Proof. done. Qed.
@@ -759,26 +759,26 @@ Proof.
Qed.
Lemma always_eq {A:cofeT} (a b : A) : (□ (a ≡ b))%I ≡ (a ≡ b : uPred M)%I.
Proof.
- apply (anti_symmetric (⊑)); auto using always_elim.
+ apply (anti_symm (⊑)); auto using always_elim.
apply (eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
{ intros n; solve_proper. }
rewrite -(eq_refl _ True) always_const; auto.
Qed.
Lemma always_and_sep P Q : (□ (P ∧ Q))%I ≡ (□ (P ★ Q))%I.
-Proof. apply (anti_symmetric (⊑)); auto using always_and_sep_1. Qed.
+Proof. apply (anti_symm (⊑)); auto using always_and_sep_1. Qed.
Lemma always_and_sep_l P Q : (□ P ∧ Q)%I ≡ (□ P ★ Q)%I.
-Proof. apply (anti_symmetric (⊑)); auto using always_and_sep_l_1. Qed.
+Proof. apply (anti_symm (⊑)); auto using always_and_sep_l_1. Qed.
Lemma always_and_sep_r P Q : (P ∧ □ Q)%I ≡ (P ★ □ Q)%I.
-Proof. by rewrite !(commutative _ P) always_and_sep_l. Qed.
+Proof. by rewrite !(comm _ P) always_and_sep_l. Qed.
Lemma always_sep P Q : (□ (P ★ Q))%I ≡ (□ P ★ □ Q)%I.
Proof. by rewrite -always_and_sep -always_and_sep_l always_and. Qed.
Lemma always_wand P Q : □ (P -★ Q) ⊑ (□ P -★ □ Q).
Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
Lemma always_sep_dup P : (□ P)%I ≡ (□ P ★ □ P)%I.
-Proof. by rewrite -always_sep -always_and_sep (idempotent _). Qed.
+Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.
Lemma always_wand_impl P Q : (□ (P -★ Q))%I ≡ (□ (P → Q))%I.
Proof.
- apply (anti_symmetric (⊑)); [|by rewrite -impl_wand].
+ apply (anti_symm (⊑)); [|by rewrite -impl_wand].
apply always_intro, impl_intro_r.
by rewrite always_and_sep_l always_elim wand_elim_l.
Qed.
@@ -792,16 +792,16 @@ Lemma ownM_op (a1 a2 : M) :
uPred_ownM (a1 ⋅ a2) ≡ (uPred_ownM a1 ★ uPred_ownM a2)%I.
Proof.
intros x n ?; split.
- * intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (associative op)|].
+ * 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).
- by rewrite (associative op _ z1) -(commutative op z1) (associative op z1)
- -(associative op _ a2) (commutative op z1) -Hy1 -Hy2.
+ by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
+ -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
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.
- rewrite -(cmra_unit_idempotent a) Hx.
+ 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.
@@ -809,7 +809,7 @@ 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.
Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_ownM ∅.
-Proof. intros x n ??; by exists x; rewrite (left_id _ _). Qed.
+Proof. intros x n ??; by exists x; rewrite left_id. Qed.
Lemma ownM_valid (a : M) : uPred_ownM 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.
@@ -835,20 +835,20 @@ Global Instance big_and_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_and M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
* by rewrite IH.
- * by rewrite !associative (commutative _ P).
+ * by rewrite !assoc (comm _ P).
* etransitivity; eauto.
Qed.
Global Instance big_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_sep M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
* by rewrite IH.
- * by rewrite !associative (commutative _ P).
+ * by rewrite !assoc (comm _ P).
* etransitivity; eauto.
Qed.
Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I.
-Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?associative ?IH. Qed.
+Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I.
-Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?associative ?IH. Qed.
+Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_and Ps : (Π★ Ps) ⊑ (Π∧ Ps).
Proof. by induction Ps as [|P Ps IH]; simpl; auto. Qed.
Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊑ P.
@@ -883,7 +883,7 @@ Proof.
intros; rewrite /TimelessP later_sep (timelessP P) (timelessP Q).
apply wand_elim_l', or_elim; apply wand_intro_r; auto.
apply wand_elim_r', or_elim; apply wand_intro_r; auto.
- rewrite ?(commutative _ Q); auto.
+ rewrite ?(comm _ Q); auto.
Qed.
Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q).
Proof.
@@ -963,7 +963,7 @@ Proof. unfold ASL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed.
(* Derived lemmas for always stable *)
Lemma always_always P `{!AlwaysStable P} : (□ P)%I ≡ P.
-Proof. apply (anti_symmetric (⊑)); auto using always_elim. Qed.
+Proof. apply (anti_symm (⊑)); auto using always_elim. Qed.
Lemma always_intro' P Q `{!AlwaysStable P} : P ⊑ Q → P ⊑ □ Q.
Proof. rewrite -(always_always P); apply always_intro. Qed.
Lemma always_and_sep_l' P Q `{!AlwaysStable P} : (P ∧ Q)%I ≡ (P ★ Q)%I.
diff --git a/heap_lang/heap_lang.v b/heap_lang/heap_lang.v
index 1b428cda2..eba609456 100644
--- a/heap_lang/heap_lang.v
+++ b/heap_lang/heap_lang.v
@@ -242,13 +242,13 @@ Proof.
revert v; induction e; intros; simplify_option_equality; auto with f_equal.
Qed.
-Instance: Injective (=) (=) of_val.
-Proof. by intros ?? Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
+Instance: Inj (=) (=) of_val.
+Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
-Instance fill_item_inj Ki : Injective (=) (=) (fill_item Ki).
+Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_equality'; auto with f_equal. Qed.
-Instance ectx_fill_inj K : Injective (=) (=) (fill K).
+Instance ectx_fill_inj K : Inj (=) (=) (fill K).
Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
Lemma fill_app K1 K2 e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
@@ -348,7 +348,7 @@ Proof.
* intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
destruct (heap_lang.step_by_val
K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
- rewrite heap_lang.fill_app in Heq1; apply (injective _) in Heq1.
+ rewrite heap_lang.fill_app in Heq1; apply (inj _) in Heq1.
exists (heap_lang.fill K' e2''); rewrite heap_lang.fill_app; split; auto.
econstructor; eauto.
Qed.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 8c078f9b9..c52e34a7e 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -99,7 +99,7 @@ Proof.
apply sep_mono, later_mono; first done.
apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
apply wand_intro_l.
- rewrite always_and_sep_l' -associative -always_and_sep_l'.
+ rewrite always_and_sep_l' -assoc -always_and_sep_l'.
apply const_elim_l=>-[l [-> [-> [-> ?]]]].
by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
Qed.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 01a987d57..b86a28823 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -68,7 +68,7 @@ Module LiftingTests.
rewrite /FindPred.
rewrite -(wp_bindi (AppLCtx _)) -wp_let //=.
revert n1. apply löb_all_1=>n1.
- rewrite (commutative uPred_and (â– _)%I) associative; apply const_elim_r=>?.
+ rewrite (comm uPred_and (â– _)%I) assoc; apply const_elim_r=>?.
rewrite -wp_value' //.
rewrite -wp_rec' // =>-/=.
(* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
diff --git a/prelude/base.v b/prelude/base.v
index 82a05497e..3f30a1122 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -514,71 +514,71 @@ Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch.
(** ** Common properties *)
(** These operational type classes allow us to refer to common mathematical
properties in a generic way. For example, for injectivity of [(k ++)] it
-allows us to write [injective (k ++)] instead of [app_inv_head k]. *)
-Class Injective {A B} (R : relation A) (S : relation B) (f : A → B) : Prop :=
- injective: ∀ x y, S (f x) (f y) → R x y.
-Class Injective2 {A B C} (R1 : relation A) (R2 : relation B)
+allows us to write [inj (k ++)] instead of [app_inv_head k]. *)
+Class Inj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop :=
+ inj x y : S (f x) (f y) → R x y.
+Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
(S : relation C) (f : A → B → C) : Prop :=
- injective2: ∀ x1 x2 y1 y2, S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2.
+ inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2.
Class Cancel {A B} (S : relation B) (f : A → B) (g : B → A) : Prop :=
- cancel: ∀ x, S (f (g x)) x.
-Class Surjective {A B} (R : relation B) (f : A → B) :=
- surjective : ∀ y, ∃ x, R (f x) y.
-Class Idempotent {A} (R : relation A) (f : A → A → A) : Prop :=
- idempotent: ∀ x, R (f x x) x.
-Class Commutative {A B} (R : relation A) (f : B → B → A) : Prop :=
- commutative: ∀ x y, R (f x y) (f y x).
+ cancel : ∀ x, S (f (g x)) x.
+Class Surj {A B} (R : relation B) (f : A → B) :=
+ surj y : ∃ x, R (f x) y.
+Class IdemP {A} (R : relation A) (f : A → A → A) : Prop :=
+ idemp x : R (f x x) x.
+Class Comm {A B} (R : relation A) (f : B → B → A) : Prop :=
+ comm x y : R (f x y) (f y x).
Class LeftId {A} (R : relation A) (i : A) (f : A → A → A) : Prop :=
- left_id: ∀ x, R (f i x) x.
+ left_id x : R (f i x) x.
Class RightId {A} (R : relation A) (i : A) (f : A → A → A) : Prop :=
- right_id: ∀ x, R (f x i) x.
-Class Associative {A} (R : relation A) (f : A → A → A) : Prop :=
- associative: ∀ x y z, R (f x (f y z)) (f (f x y) z).
+ right_id x : R (f x i) x.
+Class Assoc {A} (R : relation A) (f : A → A → A) : Prop :=
+ assoc x y z : R (f x (f y z)) (f (f x y) z).
Class LeftAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop :=
- left_absorb: ∀ x, R (f i x) i.
+ left_absorb x : R (f i x) i.
Class RightAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop :=
- right_absorb: ∀ x, R (f x i) i.
-Class AntiSymmetric {A} (R S : relation A) : Prop :=
- anti_symmetric: ∀ x y, S x y → S y x → R x y.
+ right_absorb x : R (f x i) i.
+Class AntiSymm {A} (R S : relation A) : Prop :=
+ anti_symm x y : S x y → S y x → R x y.
Class Total {A} (R : relation A) := total x y : R x y ∨ R y x.
Class Trichotomy {A} (R : relation A) :=
- trichotomy : ∀ x y, R x y ∨ x = y ∨ R y x.
+ trichotomy x y : R x y ∨ x = y ∨ R y x.
Class TrichotomyT {A} (R : relation A) :=
- trichotomyT : ∀ x y, {R x y} + {x = y} + {R y x}.
+ trichotomyT x y : {R x y} + {x = y} + {R y x}.
Arguments irreflexivity {_} _ {_} _ _.
-Arguments injective {_ _ _ _} _ {_} _ _ _.
-Arguments injective2 {_ _ _ _ _ _} _ {_} _ _ _ _ _.
+Arguments inj {_ _ _ _} _ {_} _ _ _.
+Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _.
Arguments cancel {_ _ _} _ _ {_} _.
-Arguments surjective {_ _ _} _ {_} _.
-Arguments idempotent {_ _} _ {_} _.
-Arguments commutative {_ _ _} _ {_} _ _.
+Arguments surj {_ _ _} _ {_} _.
+Arguments idemp {_ _} _ {_} _.
+Arguments comm {_ _ _} _ {_} _ _.
Arguments left_id {_ _} _ _ {_} _.
Arguments right_id {_ _} _ _ {_} _.
-Arguments associative {_ _} _ {_} _ _ _.
+Arguments assoc {_ _} _ {_} _ _ _.
Arguments left_absorb {_ _} _ _ {_} _.
Arguments right_absorb {_ _} _ _ {_} _.
-Arguments anti_symmetric {_ _} _ {_} _ _ _ _.
+Arguments anti_symm {_ _} _ {_} _ _ _ _.
Arguments total {_} _ {_} _ _.
Arguments trichotomy {_} _ {_} _ _.
Arguments trichotomyT {_} _ {_} _ _.
-Instance id_injective {A} : Injective (=) (=) (@id A).
+Instance id_inj {A} : Inj (=) (=) (@id A).
Proof. intros ??; auto. Qed.
(** The following lemmas are specific versions of the projections of the above
type classes for Leibniz equality. These lemmas allow us to enforce Coq not to
use the setoid rewriting mechanism. *)
-Lemma idempotent_L {A} (f : A → A → A) `{!Idempotent (=) f} x : f x x = x.
+Lemma idemp_L {A} (f : A → A → A) `{!IdemP (=) f} x : f x x = x.
Proof. auto. Qed.
-Lemma commutative_L {A B} (f : B → B → A) `{!Commutative (=) f} x y :
+Lemma comm_L {A B} (f : B → B → A) `{!Comm (=) f} x y :
f x y = f y x.
Proof. auto. Qed.
Lemma left_id_L {A} (i : A) (f : A → A → A) `{!LeftId (=) i f} x : f i x = x.
Proof. auto. Qed.
Lemma right_id_L {A} (i : A) (f : A → A → A) `{!RightId (=) i f} x : f x i = x.
Proof. auto. Qed.
-Lemma associative_L {A} (f : A → A → A) `{!Associative (=) f} x y z :
+Lemma assoc_L {A} (f : A → A → A) `{!Assoc (=) f} x y z :
f x (f y z) = f (f x y) z.
Proof. auto. Qed.
Lemma left_absorb_L {A} (i : A) (f : A → A → A) `{!LeftAbsorb (=) i f} x :
@@ -593,7 +593,7 @@ Proof. auto. Qed.
relation [R] instead of [⊆] to support multiple orders on the same type. *)
Class PartialOrder {A} (R : relation A) : Prop := {
partial_order_pre :> PreOrder R;
- partial_order_anti_symmetric :> AntiSymmetric (=) R
+ partial_order_anti_symm :> AntiSymm (=) R
}.
Class TotalOrder {A} (R : relation A) : Prop := {
total_order_partial :> PartialOrder R;
@@ -746,31 +746,17 @@ Proof. intuition. Qed.
Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y ↔ R y x.
Proof. intuition. Qed.
-(** ** Pointwise relations *)
-(** These instances are in Coq trunk since revision 15455, but are not in Coq
-8.4 yet. *)
-Instance pointwise_reflexive {A} `{R : relation B} :
- Reflexive R → Reflexive (pointwise_relation A R) | 9.
-Proof. firstorder. Qed.
-Instance pointwise_symmetric {A} `{R : relation B} :
- Symmetric R → Symmetric (pointwise_relation A R) | 9.
-Proof. firstorder. Qed.
-Instance pointwise_transitive {A} `{R : relation B} :
- Transitive R → Transitive (pointwise_relation A R) | 9.
-Proof. firstorder. Qed.
-
(** ** Unit *)
Instance unit_equiv : Equiv unit := λ _ _, True.
Instance unit_equivalence : Equivalence (@equiv unit _).
Proof. repeat split. Qed.
(** ** Products *)
-Instance prod_map_injective {A A' B B'} (f : A → A') (g : B → B') :
- Injective (=) (=) f → Injective (=) (=) g →
- Injective (=) (=) (prod_map f g).
+Instance prod_map_inj {A A' B B'} (f : A → A') (g : B → B') :
+ Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (prod_map f g).
Proof.
intros ?? [??] [??] ?; simpl in *; f_equal;
- [apply (injective f)|apply (injective g)]; congruence.
+ [apply (inj f)|apply (inj g)]; congruence.
Qed.
Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
@@ -815,17 +801,17 @@ Lemma and_wlog_l (P Q : Prop) : (Q → P) → Q → (P ∧ Q).
Proof. tauto. Qed.
Lemma and_wlog_r (P Q : Prop) : P → (P → Q) → (P ∧ Q).
Proof. tauto. Qed.
-Instance: ∀ A B (x : B), Commutative (=) (λ _ _ : A, x).
+Instance: ∀ A B (x : B), Comm (=) (λ _ _ : A, x).
Proof. red. trivial. Qed.
-Instance: ∀ A (x : A), Associative (=) (λ _ _ : A, x).
+Instance: ∀ A (x : A), Assoc (=) (λ _ _ : A, x).
Proof. red. trivial. Qed.
-Instance: ∀ A, Associative (=) (λ x _ : A, x).
+Instance: ∀ A, Assoc (=) (λ x _ : A, x).
Proof. red. trivial. Qed.
-Instance: ∀ A, Associative (=) (λ _ x : A, x).
+Instance: ∀ A, Assoc (=) (λ _ x : A, x).
Proof. red. trivial. Qed.
-Instance: ∀ A, Idempotent (=) (λ x _ : A, x).
+Instance: ∀ A, IdemP (=) (λ x _ : A, x).
Proof. red. trivial. Qed.
-Instance: ∀ A, Idempotent (=) (λ _ x : A, x).
+Instance: ∀ A, IdemP (=) (λ _ x : A, x).
Proof. red. trivial. Qed.
Instance left_id_propholds {A} (R : relation A) i f :
@@ -841,7 +827,7 @@ Instance right_absorb_propholds {A} (R : relation A) i f :
RightAbsorb R i f → ∀ x, PropHolds (R (f x i) i).
Proof. red. trivial. Qed.
Instance idem_propholds {A} (R : relation A) f :
- Idempotent R f → ∀ x, PropHolds (R (f x x) x).
+ IdemP R f → ∀ x, PropHolds (R (f x x) x).
Proof. red. trivial. Qed.
Instance: ∀ `{R1 : relation A, R2 : relation B} (x : B),
@@ -849,47 +835,47 @@ Instance: ∀ `{R1 : relation A, R2 : relation B} (x : B),
Proof. intros A R1 B R2 x ? y1 y2; reflexivity. Qed.
Instance: @PreOrder A (=).
Proof. split; repeat intro; congruence. Qed.
-Lemma injective_iff {A B} {R : relation A} {S : relation B} (f : A → B)
- `{!Injective R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y) ↔ R x y.
+Lemma inj_iff {A B} {R : relation A} {S : relation B} (f : A → B)
+ `{!Inj R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y) ↔ R x y.
Proof. firstorder. Qed.
-Instance: Injective (=) (=) (@inl A B).
+Instance: Inj (=) (=) (@inl A B).
Proof. injection 1; auto. Qed.
-Instance: Injective (=) (=) (@inr A B).
+Instance: Inj (=) (=) (@inr A B).
Proof. injection 1; auto. Qed.
-Instance: Injective2 (=) (=) (=) (@pair A B).
+Instance: Inj2 (=) (=) (=) (@pair A B).
Proof. injection 1; auto. Qed.
-Instance: ∀ `{Injective2 A B C R1 R2 R3 f} y, Injective R1 R3 (λ x, f x y).
-Proof. repeat intro; edestruct (injective2 f); eauto. Qed.
-Instance: ∀ `{Injective2 A B C R1 R2 R3 f} x, Injective R2 R3 (f x).
-Proof. repeat intro; edestruct (injective2 f); eauto. Qed.
+Instance: ∀ `{Inj2 A B C R1 R2 R3 f} y, Inj R1 R3 (λ x, f x y).
+Proof. repeat intro; edestruct (inj2 f); eauto. Qed.
+Instance: ∀ `{Inj2 A B C R1 R2 R3 f} x, Inj R2 R3 (f x).
+Proof. repeat intro; edestruct (inj2 f); eauto. Qed.
-Lemma cancel_injective `{Cancel A B R1 f g}
- `{!Equivalence R1} `{!Proper (R2 ==> R1) f} : Injective R1 R2 g.
+Lemma cancel_inj `{Cancel A B R1 f g}
+ `{!Equivalence R1} `{!Proper (R2 ==> R1) f} : Inj R1 R2 g.
Proof.
intros x y E. rewrite <-(cancel f g x), <-(cancel f g y), E. reflexivity.
Qed.
-Lemma cancel_surjective `{Cancel A B R1 f g} : Surjective R1 f.
+Lemma cancel_surj `{Cancel A B R1 f g} : Surj R1 f.
Proof. intros y. exists (g y). auto. Qed.
Lemma impl_transitive (P Q R : Prop) : (P → Q) → (Q → R) → (P → R).
Proof. tauto. Qed.
-Instance: Commutative (↔) (@eq A).
+Instance: Comm (↔) (@eq A).
Proof. red; intuition. Qed.
-Instance: Commutative (↔) (λ x y, @eq A y x).
+Instance: Comm (↔) (λ x y, @eq A y x).
Proof. red; intuition. Qed.
-Instance: Commutative (↔) (↔).
+Instance: Comm (↔) (↔).
Proof. red; intuition. Qed.
-Instance: Commutative (↔) (∧).
+Instance: Comm (↔) (∧).
Proof. red; intuition. Qed.
-Instance: Associative (↔) (∧).
+Instance: Assoc (↔) (∧).
Proof. red; intuition. Qed.
-Instance: Idempotent (↔) (∧).
+Instance: IdemP (↔) (∧).
Proof. red; intuition. Qed.
-Instance: Commutative (↔) (∨).
+Instance: Comm (↔) (∨).
Proof. red; intuition. Qed.
-Instance: Associative (↔) (∨).
+Instance: Assoc (↔) (∨).
Proof. red; intuition. Qed.
-Instance: Idempotent (↔) (∨).
+Instance: IdemP (↔) (∨).
Proof. red; intuition. Qed.
Instance: LeftId (↔) True (∧).
Proof. red; intuition. Qed.
@@ -911,26 +897,26 @@ Instance: LeftId (↔) True impl.
Proof. unfold impl. red; intuition. Qed.
Instance: RightAbsorb (↔) True impl.
Proof. unfold impl. red; intuition. Qed.
-Lemma not_injective `{Injective A B R R' f} x y : ¬R x y → ¬R' (f x) (f y).
+Lemma not_inj `{Inj A B R R' f} x y : ¬R x y → ¬R' (f x) (f y).
Proof. intuition. Qed.
-Instance injective_compose {A B C} R1 R2 R3 (f : A → B) (g : B → C) :
- Injective R1 R2 f → Injective R2 R3 g → Injective R1 R3 (g ∘ f).
+Instance inj_compose {A B C} R1 R2 R3 (f : A → B) (g : B → C) :
+ Inj R1 R2 f → Inj R2 R3 g → Inj R1 R3 (g ∘ f).
Proof. red; intuition. Qed.
-Instance surjective_compose {A B C} R (f : A → B) (g : B → C) :
- Surjective (=) f → Surjective R g → Surjective R (g ∘ f).
+Instance surj_compose {A B C} R (f : A → B) (g : B → C) :
+ Surj (=) f → Surj R g → Surj R (g ∘ f).
Proof.
- intros ?? x. unfold compose. destruct (surjective g x) as [y ?].
- destruct (surjective f y) as [z ?]. exists z. congruence.
+ intros ?? x. unfold compose. destruct (surj g x) as [y ?].
+ destruct (surj f y) as [z ?]. exists z. congruence.
Qed.
Section sig_map.
Context `{P : A → Prop} `{Q : B → Prop} (f : A → B) (Hf : ∀ x, P x → Q (f x)).
Definition sig_map (x : sig P) : sig Q := f (`x) ↾ Hf _ (proj2_sig x).
- Global Instance sig_map_injective:
- (∀ x, ProofIrrel (P x)) → Injective (=) (=) f → Injective (=) (=) sig_map.
+ Global Instance sig_map_inj:
+ (∀ x, ProofIrrel (P x)) → Inj (=) (=) f → Inj (=) (=) sig_map.
Proof.
intros ?? [x Hx] [y Hy]. injection 1. intros Hxy.
- apply (injective f) in Hxy; subst. rewrite (proof_irrel _ Hy). auto.
+ apply (inj f) in Hxy; subst. rewrite (proof_irrel _ Hy). auto.
Qed.
End sig_map.
Arguments sig_map _ _ _ _ _ _ !_ /.
diff --git a/prelude/countable.v b/prelude/countable.v
index ab860ddf6..1635bac29 100644
--- a/prelude/countable.v
+++ b/prelude/countable.v
@@ -15,13 +15,13 @@ Definition encode_nat `{Countable A} (x : A) : nat :=
pred (Pos.to_nat (encode x)).
Definition decode_nat `{Countable A} (i : nat) : option A :=
decode (Pos.of_nat (S i)).
-Instance encode_injective `{Countable A} : Injective (=) (=) encode.
+Instance encode_inj `{Countable A} : Inj (=) (=) encode.
Proof.
- intros x y Hxy; apply (injective Some).
+ intros x y Hxy; apply (inj Some).
by rewrite <-(decode_encode x), Hxy, decode_encode.
Qed.
-Instance encode_nat_injective `{Countable A} : Injective (=) (=) encode_nat.
-Proof. unfold encode_nat; intros x y Hxy; apply (injective encode); lia. Qed.
+Instance encode_nat_inj `{Countable A} : Inj (=) (=) encode_nat.
+Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
Lemma decode_encode_nat `{Countable A} x : decode_nat (encode_nat x) = Some x.
Proof.
pose proof (Pos2Nat.is_pos (encode x)).
@@ -70,11 +70,11 @@ Section choice.
Definition choice (HA : ∃ x, P x) : { x | P x } := _↾choose_correct HA.
End choice.
-Lemma surjective_cancel `{Countable A} `{∀ x y : B, Decision (x = y)}
- (f : A → B) `{!Surjective (=) f} : { g : B → A & Cancel (=) f g }.
+Lemma surj_cancel `{Countable A} `{∀ x y : B, Decision (x = y)}
+ (f : A → B) `{!Surj (=) f} : { g : B → A & Cancel (=) f g }.
Proof.
- exists (λ y, choose (λ x, f x = y) (surjective f y)).
- intros y. by rewrite (choose_correct (λ x, f x = y) (surjective f y)).
+ exists (λ y, choose (λ x, f x = y) (surj f y)).
+ intros y. by rewrite (choose_correct (λ x, f x = y) (surj f y)).
Qed.
(** * Instances *)
@@ -197,7 +197,7 @@ Lemma list_encode_app' `{Countable A} (l1 l2 : list A) acc :
Proof.
revert acc; induction l1; simpl; auto.
induction l2 as [|x l IH]; intros acc; simpl; [by rewrite ?(left_id_L _ _)|].
- by rewrite !(IH (Nat.iter _ _ _)), (associative_L _), x0_iter_x1.
+ by rewrite !(IH (Nat.iter _ _ _)), (assoc_L _), x0_iter_x1.
Qed.
Program Instance list_countable `{Countable A} : Countable (list A) :=
{| encode := list_encode 1; decode := list_decode [] 0 |}.
@@ -211,7 +211,7 @@ Next Obligation.
{ by intros help l; rewrite help, (right_id_L _ _). }
induction l as [|x l IH] using @rev_ind; intros acc; [done|].
rewrite list_encode_app'; simpl; rewrite <-x0_iter_x1, decode_iter; simpl.
- by rewrite decode_encode_nat; simpl; rewrite IH, <-(associative_L _).
+ by rewrite decode_encode_nat; simpl; rewrite IH, <-(assoc_L _).
Qed.
Lemma list_encode_app `{Countable A} (l1 l2 : list A) :
encode (l1 ++ l2)%list = encode l1 ++ encode l2.
diff --git a/prelude/decidable.v b/prelude/decidable.v
index 184372c8b..817357de2 100644
--- a/prelude/decidable.v
+++ b/prelude/decidable.v
@@ -12,7 +12,7 @@ Proof. firstorder. Qed.
Lemma Is_true_reflect (b : bool) : reflect b b.
Proof. destruct b. by left. right. intros []. Qed.
-Instance: Injective (=) (↔) Is_true.
+Instance: Inj (=) (↔) Is_true.
Proof. intros [] []; simpl; intuition. Qed.
(** We introduce [decide_rel] to avoid inefficienct computation due to eager
diff --git a/prelude/error.v b/prelude/error.v
index 0eb6c33f5..b2eb18522 100644
--- a/prelude/error.v
+++ b/prelude/error.v
@@ -47,7 +47,7 @@ Lemma error_fmap_bind {S E A B C} (f : A → B) (g : B → error S E C) x s :
((f <$> x) ≫= g) s = (x ≫= g ∘ f) s.
Proof. by compute; destruct (x s) as [|[??]]. Qed.
-Lemma error_associative {S E A B C} (f : A → error S E B) (g : B → error S E C) x s :
+Lemma error_assoc {S E A B C} (f : A → error S E B) (g : B → error S E C) x s :
((x ≫= f) ≫= g) s = (a ↠x; f a ≫= g) s.
Proof. by compute; destruct (x s) as [|[??]]. Qed.
Lemma error_of_option_bind {S E A B} (f : A → option B) o e :
@@ -114,7 +114,7 @@ Tactic Notation "error_proceed" :=
| H : (gets _ ≫= _) _ = _ |- _ => rewrite error_left_gets in H
| H : (modify _ ≫= _) _ = _ |- _ => rewrite error_left_modify in H
| H : ((_ <$> _) ≫= _) _ = _ |- _ => rewrite error_fmap_bind in H
- | H : ((_ ≫= _) ≫= _) _ = _ |- _ => rewrite error_associative in H
+ | H : ((_ ≫= _) ≫= _) _ = _ |- _ => rewrite error_assoc in H
| H : (error_guard _ _ _) _ = _ |- _ =>
let H' := fresh in apply error_guard_ret in H; destruct H as [H' H]
| _ => progress simplify_equality'
diff --git a/prelude/fin_collections.v b/prelude/fin_collections.v
index 2f7a573d0..7fe252900 100644
--- a/prelude/fin_collections.v
+++ b/prelude/fin_collections.v
@@ -108,7 +108,7 @@ Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
Proof.
rewrite <-size_union by solve_elem_of.
setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by solve_elem_of.
- rewrite <-union_difference, (commutative (∪)); solve_elem_of.
+ rewrite <-union_difference, (comm (∪)); solve_elem_of.
Qed.
Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 09c65cdad..9ed4f6986 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -820,28 +820,28 @@ Proof.
intros ??. apply map_eq. intros.
by rewrite !(lookup_merge f), lookup_empty, (right_id_L None f).
Qed.
-Lemma merge_commutative m1 m2 :
+Lemma merge_comm m1 m2 :
(∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
merge f m1 m2 = merge f m2 m1.
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance: Commutative (=) f → Commutative (=) (merge f).
+Global Instance: Comm (=) f → Comm (=) (merge f).
Proof.
- intros ???. apply merge_commutative. intros. by apply (commutative f).
+ intros ???. apply merge_comm. intros. by apply (comm f).
Qed.
-Lemma merge_associative m1 m2 m3 :
+Lemma merge_assoc m1 m2 m3 :
(∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance: Associative (=) f → Associative (=) (merge f).
+Global Instance: Assoc (=) f → Assoc (=) (merge f).
Proof.
- intros ????. apply merge_associative. intros. by apply (associative_L f).
+ intros ????. apply merge_assoc. intros. by apply (assoc_L f).
Qed.
-Lemma merge_idempotent m1 :
+Lemma merge_idemp m1 :
(∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → merge f m1 m1 = m1.
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance: Idempotent (=) f → Idempotent (=) (merge f).
-Proof. intros ??. apply merge_idempotent. intros. by apply (idempotent f). Qed.
+Global Instance: IdemP (=) f → IdemP (=) (merge f).
+Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed.
End merge.
Section more_merge.
@@ -1033,19 +1033,19 @@ Global Instance: LeftId (@eq (M A)) ∅ (union_with f).
Proof. unfold union_with, map_union_with. apply _. Qed.
Global Instance: RightId (@eq (M A)) ∅ (union_with f).
Proof. unfold union_with, map_union_with. apply _. Qed.
-Lemma union_with_commutative m1 m2 :
+Lemma union_with_comm m1 m2 :
(∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) →
union_with f m1 m2 = union_with f m2 m1.
Proof.
- intros. apply (merge_commutative _). intros i.
+ intros. apply (merge_comm _). intros i.
destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
Qed.
-Global Instance: Commutative (=) f → Commutative (@eq (M A)) (union_with f).
-Proof. intros ???. apply union_with_commutative. eauto. Qed.
-Lemma union_with_idempotent m :
+Global Instance: Comm (=) f → Comm (@eq (M A)) (union_with f).
+Proof. intros ???. apply union_with_comm. eauto. Qed.
+Lemma union_with_idemp m :
(∀ i x, m !! i = Some x → f x x = Some x) → union_with f m m = m.
Proof.
- intros. apply (merge_idempotent _). intros i.
+ intros. apply (merge_idemp _). intros i.
destruct (m !! i) eqn:?; simpl; eauto.
Qed.
Lemma alter_union_with (g : A → A) m1 m2 i :
@@ -1100,14 +1100,14 @@ End union_with.
(** ** Properties of the [union] operation *)
Global Instance: LeftId (@eq (M A)) ∅ (∪) := _.
Global Instance: RightId (@eq (M A)) ∅ (∪) := _.
-Global Instance: Associative (@eq (M A)) (∪).
+Global Instance: Assoc (@eq (M A)) (∪).
Proof.
intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with.
- apply (merge_associative _). intros i.
+ apply (merge_assoc _). intros i.
by destruct (m1 !! i), (m2 !! i), (m3 !! i).
Qed.
-Global Instance: Idempotent (@eq (M A)) (∪).
-Proof. intros A ?. by apply union_with_idempotent. Qed.
+Global Instance: IdemP (@eq (M A)) (∪).
+Proof. intros A ?. by apply union_with_idemp. Qed.
Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x :
(m1 ∪ m2) !! i = Some x ↔
m1 !! i = Some x ∨ (m1 !! i = None ∧ m2 !! i = Some x).
@@ -1140,9 +1140,9 @@ Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
m1 ⊥ₘ m2 → m2 !! i = Some x → (m1 ∪ m2) !! i = Some x.
Proof. intro. rewrite lookup_union_Some; intuition. Qed.
-Lemma map_union_commutative {A} (m1 m2 : M A) : m1 ⊥ₘ m2 → m1 ∪ m2 = m2 ∪ m1.
+Lemma map_union_comm {A} (m1 m2 : M A) : m1 ⊥ₘ m2 → m1 ∪ m2 = m2 ∪ m1.
Proof.
- intros Hdisjoint. apply (merge_commutative (union_with (λ x _, Some x))).
+ intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))).
intros i. specialize (Hdisjoint i).
destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed.
@@ -1160,7 +1160,7 @@ Proof.
Qed.
Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 ⊥ₘ m2 → m2 ⊆ m1 ∪ m2.
Proof.
- intros. rewrite map_union_commutative by done. by apply map_union_subseteq_l.
+ intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
Qed.
Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m1 ⊆ m2 ∪ m3.
Proof. intros. transitivity m2; auto using map_union_subseteq_l. Qed.
@@ -1175,7 +1175,7 @@ Qed.
Lemma map_union_preserving_r {A} (m1 m2 m3 : M A) :
m2 ⊥ₘ m3 → m1 ⊆ m2 → m1 ∪ m3 ⊆ m2 ∪ m3.
Proof.
- intros. rewrite !(map_union_commutative _ m3)
+ intros. rewrite !(map_union_comm _ m3)
by eauto using map_disjoint_weaken_l.
by apply map_union_preserving_l.
Qed.
@@ -1189,19 +1189,19 @@ Qed.
Lemma map_union_reflecting_r {A} (m1 m2 m3 : M A) :
m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m1 ∪ m3 ⊆ m2 ∪ m3 → m1 ⊆ m2.
Proof.
- intros ??. rewrite !(map_union_commutative _ m3) by done.
+ intros ??. rewrite !(map_union_comm _ m3) by done.
by apply map_union_reflecting_l.
Qed.
Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) :
m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m3 ∪ m1 = m3 ∪ m2 → m1 = m2.
Proof.
- intros. apply (anti_symmetric (⊆));
+ intros. apply (anti_symm (⊆));
apply map_union_reflecting_l with m3; auto using (reflexive_eq (R:=(⊆))).
Qed.
Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) :
m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m1 ∪ m3 = m2 ∪ m3 → m1 = m2.
Proof.
- intros. apply (anti_symmetric (⊆));
+ intros. apply (anti_symm (⊆));
apply map_union_reflecting_r with m3; auto using (reflexive_eq (R:=(⊆))).
Qed.
Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) :
@@ -1231,7 +1231,7 @@ Qed.
Lemma insert_union_singleton_r {A} (m : M A) i x :
m !! i = None → <[i:=x]>m = m ∪ {[i ↦ x]}.
Proof.
- intro. rewrite insert_union_singleton_l, map_union_commutative; [done |].
+ intro. rewrite insert_union_singleton_l, map_union_comm; [done |].
by apply map_disjoint_singleton_l.
Qed.
Lemma map_disjoint_insert_l {A} (m1 m2 : M A) i x :
@@ -1254,12 +1254,12 @@ Lemma map_disjoint_insert_r_2 {A} (m1 m2 : M A) i x :
Proof. by rewrite map_disjoint_insert_r. Qed.
Lemma insert_union_l {A} (m1 m2 : M A) i x :
<[i:=x]>(m1 ∪ m2) = <[i:=x]>m1 ∪ m2.
-Proof. by rewrite !insert_union_singleton_l, (associative_L (∪)). Qed.
+Proof. by rewrite !insert_union_singleton_l, (assoc_L (∪)). Qed.
Lemma insert_union_r {A} (m1 m2 : M A) i x :
m1 !! i = None → <[i:=x]>(m1 ∪ m2) = m1 ∪ <[i:=x]>m2.
Proof.
- intro. rewrite !insert_union_singleton_l, !(associative_L (∪)).
- rewrite (map_union_commutative m1); [done |].
+ intro. rewrite !insert_union_singleton_l, !(assoc_L (∪)).
+ rewrite (map_union_comm m1); [done |].
by apply map_disjoint_singleton_r.
Qed.
Lemma foldr_insert_union {A} (m : M A) l :
diff --git a/prelude/finite.v b/prelude/finite.v
index 76006bf3a..a529a1a04 100644
--- a/prelude/finite.v
+++ b/prelude/finite.v
@@ -71,27 +71,27 @@ Proof.
unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
constructor; exact x.
Qed.
-Lemma finite_injective_contains `{finA: Finite A} `{finB: Finite B} (f: A → B)
- `{!Injective (=) (=) f} : f <$> enum A `contains` enum B.
+Lemma finite_inj_contains `{finA: Finite A} `{finB: Finite B} (f: A → B)
+ `{!Inj (=) (=) f} : f <$> enum A `contains` enum B.
Proof.
intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2.
Qed.
-Lemma finite_injective_Permutation `{Finite A} `{Finite B} (f : A → B)
- `{!Injective (=) (=) f} : card A = card B → f <$> enum A ≡ₚ enum B.
+Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B)
+ `{!Inj (=) (=) f} : card A = card B → f <$> enum A ≡ₚ enum B.
Proof.
intros. apply contains_Permutation_length_eq.
* by rewrite fmap_length.
- * by apply finite_injective_contains.
+ * by apply finite_inj_contains.
Qed.
-Lemma finite_injective_surjective `{Finite A} `{Finite B} (f : A → B)
- `{!Injective (=) (=) f} : card A = card B → Surjective (=) f.
+Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B)
+ `{!Inj (=) (=) f} : card A = card B → Surj (=) f.
Proof.
intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto.
- rewrite finite_injective_Permutation; auto using elem_of_enum.
+ rewrite finite_inj_Permutation; auto using elem_of_enum.
Qed.
-Lemma finite_surjective A `{Finite A} B `{Finite B} :
- 0 < card A ≤ card B → ∃ g : B → A, Surjective (=) g.
+Lemma finite_surj A `{Finite A} B `{Finite B} :
+ 0 < card A ≤ card B → ∃ g : B → A, Surj (=) g.
Proof.
intros [??]. destruct (finite_inhabited A) as [x']; auto with lia.
exists (λ y : B, from_option x' (decode_nat (encode_nat y))).
@@ -99,38 +99,38 @@ Proof.
{ pose proof (encode_lt_card x); lia. }
exists y. by rewrite Hy2, decode_encode_nat.
Qed.
-Lemma finite_injective A `{Finite A} B `{Finite B} :
- card A ≤ card B ↔ ∃ f : A → B, Injective (=) (=) f.
+Lemma finite_inj A `{Finite A} B `{Finite B} :
+ card A ≤ card B ↔ ∃ f : A → B, Inj (=) (=) f.
Proof.
split.
* intros. destruct (decide (card A = 0)) as [HA|?].
{ exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
- destruct (finite_surjective A B) as (g&?); auto with lia.
- destruct (surjective_cancel g) as (f&?). exists f. apply cancel_injective.
+ destruct (finite_surj A B) as (g&?); auto with lia.
+ destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
* intros [f ?]. unfold card. rewrite <-(fmap_length f).
- by apply contains_length, (finite_injective_contains f).
+ by apply contains_length, (finite_inj_contains f).
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
- card A = card B ↔ ∃ f : A → B, Injective (=) (=) f ∧ Surjective (=) f.
+ card A = card B ↔ ∃ f : A → B, Inj (=) (=) f ∧ Surj (=) f.
Proof.
split.
- * intros; destruct (proj1 (finite_injective A B)) as [f ?]; auto with lia.
- exists f; auto using (finite_injective_surjective f).
- * intros (f&?&?). apply (anti_symmetric (≤)); apply finite_injective.
+ * intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
+ exists f; auto using (finite_inj_surj f).
+ * intros (f&?&?). apply (anti_symm (≤)); apply finite_inj.
+ by exists f.
- + destruct (surjective_cancel f) as (g&?); eauto using cancel_injective.
+ + destruct (surj_cancel f) as (g&?); eauto using cancel_inj.
Qed.
-Lemma injective_card `{Finite A} `{Finite B} (f : A → B)
- `{!Injective (=) (=) f} : card A ≤ card B.
-Proof. apply finite_injective. eauto. Qed.
-Lemma surjective_card `{Finite A} `{Finite B} (f : A → B)
- `{!Surjective (=) f} : card B ≤ card A.
+Lemma inj_card `{Finite A} `{Finite B} (f : A → B)
+ `{!Inj (=) (=) f} : card A ≤ card B.
+Proof. apply finite_inj. eauto. Qed.
+Lemma surj_card `{Finite A} `{Finite B} (f : A → B)
+ `{!Surj (=) f} : card B ≤ card A.
Proof.
- destruct (surjective_cancel f) as (g&?).
- apply injective_card with g, cancel_injective.
+ destruct (surj_cancel f) as (g&?).
+ apply inj_card with g, cancel_inj.
Qed.
Lemma bijective_card `{Finite A} `{Finite B} (f : A → B)
- `{!Injective (=) (=) f} `{!Surjective (=) f} : card A = card B.
+ `{!Inj (=) (=) f} `{!Surj (=) f} : card A = card B.
Proof. apply finite_bijective. eauto. Qed.
(** Decidability of quantification over finite types *)
@@ -180,7 +180,7 @@ End enc_finite.
Section bijective_finite.
Context `{Finite A, ∀ x y : B, Decision (x = y)} (f : A → B) (g : B → A).
- Context `{!Injective (=) (=) f, !Cancel (=) f g}.
+ Context `{!Inj (=) (=) f, !Cancel (=) f g}.
Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
diff --git a/prelude/gmap.v b/prelude/gmap.v
index 1c2cd5ec7..a3466c307 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -89,7 +89,7 @@ Proof.
* done.
* intros A f [m Hm] i; apply (lookup_partial_alter f m).
* intros A f [m Hm] i j Hs; apply (lookup_partial_alter_ne f m).
- by contradict Hs; apply (injective encode).
+ by contradict Hs; apply (inj encode).
* intros A B f [m Hm] i; apply (lookup_fmap f m).
* intros A [m Hm]; unfold map_to_list; simpl.
apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm.
diff --git a/prelude/list.v b/prelude/list.v
index ef167dc39..d0e0eafb0 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -339,13 +339,13 @@ Tactic Notation "discriminate_list_equality" :=
(** The tactic [simplify_list_equality] simplifies hypotheses involving
equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies
lookups in singleton lists. *)
-Lemma app_injective_1 {A} (l1 k1 l2 k2 : list A) :
+Lemma app_inj_1 {A} (l1 k1 l2 k2 : list A) :
length l1 = length k1 → l1 ++ l2 = k1 ++ k2 → l1 = k1 ∧ l2 = k2.
Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed.
-Lemma app_injective_2 {A} (l1 k1 l2 k2 : list A) :
+Lemma app_inj_2 {A} (l1 k1 l2 k2 : list A) :
length l2 = length k2 → l1 ++ l2 = k1 ++ k2 → l1 = k1 ∧ l2 = k2.
Proof.
- intros ? Hl. apply app_injective_1; auto.
+ intros ? Hl. apply app_inj_1; auto.
apply (f_equal length) in Hl. rewrite !app_length in Hl. lia.
Qed.
Ltac simplify_list_equality :=
@@ -353,8 +353,8 @@ Ltac simplify_list_equality :=
| _ => progress simplify_equality'
| H : _ ++ _ = _ ++ _ |- _ => first
[ apply app_inv_head in H | apply app_inv_tail in H
- | apply app_injective_1 in H; [destruct H|done]
- | apply app_injective_2 in H; [destruct H|done] ]
+ | apply app_inj_1 in H; [destruct H|done]
+ | apply app_inj_2 in H; [destruct H|done] ]
| H : [?x] !! ?i = Some ?y |- _ =>
destruct i; [change (Some x = Some y) in H | discriminate]
end.
@@ -386,13 +386,13 @@ Section setoid.
Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
End setoid.
-Global Instance: Injective2 (=) (=) (=) (@cons A).
+Global Instance: Inj2 (=) (=) (=) (@cons A).
Proof. by injection 1. Qed.
-Global Instance: ∀ k, Injective (=) (=) (k ++).
+Global Instance: ∀ k, Inj (=) (=) (k ++).
Proof. intros ???. apply app_inv_head. Qed.
-Global Instance: ∀ k, Injective (=) (=) (++ k).
+Global Instance: ∀ k, Inj (=) (=) (++ k).
Proof. intros ???. apply app_inv_tail. Qed.
-Global Instance: Associative (=) (@app A).
+Global Instance: Assoc (=) (@app A).
Proof. intros ???. apply app_assoc. Qed.
Global Instance: LeftId (=) [] (@app A).
Proof. done. Qed.
@@ -698,7 +698,7 @@ Proof.
induction l as [|x l IH]; intros Hl; constructor.
* rewrite elem_of_list_lookup. intros [i ?].
by feed pose proof (Hl (S i) 0 x); auto.
- * apply IH. intros i j x' ??. by apply (injective S), (Hl (S i) (S j) x').
+ * apply IH. intros i j x' ??. by apply (inj S), (Hl (S i) (S j) x').
Qed.
Section no_dup_dec.
@@ -849,7 +849,7 @@ Proof.
split; auto using elem_of_reverse_2.
intros. rewrite <-(reverse_involutive l). by apply elem_of_reverse_2.
Qed.
-Global Instance: Injective (=) (=) (@reverse A).
+Global Instance: Inj (=) (=) (@reverse A).
Proof.
intros l1 l2 Hl.
by rewrite <-(reverse_involutive l1), <-(reverse_involutive l2), Hl.
@@ -885,7 +885,7 @@ Proof. induction l; f_equal'; auto. Qed.
Lemma take_app_alt l k n : n = length l → take n (l ++ k) = l.
Proof. intros ->. by apply take_app. Qed.
Lemma take_app3_alt l1 l2 l3 n : n = length l1 → take n ((l1 ++ l2) ++ l3) = l1.
-Proof. intros ->. by rewrite <-(associative_L (++)), take_app. Qed.
+Proof. intros ->. by rewrite <-(assoc_L (++)), take_app. Qed.
Lemma take_app_le l k n : n ≤ length l → take n (l ++ k) = take n l.
Proof. revert n. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
Lemma take_plus_app l k n m :
@@ -898,7 +898,7 @@ Lemma take_ge l n : length l ≤ n → take n l = l.
Proof. revert n. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
Lemma take_take l n m : take n (take m l) = take (min n m) l.
Proof. revert n m. induction l; intros [|?] [|?]; f_equal'; auto. Qed.
-Lemma take_idempotent l n : take n (take n l) = take n l.
+Lemma take_idemp l n : take n (take n l) = take n l.
Proof. by rewrite take_take, Min.min_idempotent. Qed.
Lemma take_length l n : length (take n l) = min n (length l).
Proof. revert n. induction l; intros [|?]; f_equal'; done. Qed.
@@ -949,7 +949,7 @@ Lemma drop_app_alt l k n : n = length l → drop n (l ++ k) = k.
Proof. intros ->. by apply drop_app. Qed.
Lemma drop_app3_alt l1 l2 l3 n :
n = length l1 → drop n ((l1 ++ l2) ++ l3) = l2 ++ l3.
-Proof. intros ->. by rewrite <-(associative_L (++)), drop_app. Qed.
+Proof. intros ->. by rewrite <-(assoc_L (++)), drop_app. Qed.
Lemma drop_app_ge l k n :
length l ≤ n → drop n (l ++ k) = drop (n - length l) k.
Proof.
@@ -1076,7 +1076,7 @@ Proof. intros ->. by rewrite resize_app_le, resize_all. Qed.
Lemma resize_app_ge l1 l2 n x :
length l1 ≤ n → resize n x (l1 ++ l2) = l1 ++ resize (n - length l1) x l2.
Proof.
- intros. rewrite !resize_spec, take_app_ge, (associative_L (++)) by done.
+ intros. rewrite !resize_spec, take_app_ge, (assoc_L (++)) by done.
do 2 f_equal. rewrite app_length. lia.
Qed.
Lemma resize_length l n x : length (resize n x l) = n.
@@ -1089,7 +1089,7 @@ Proof.
* intros. by rewrite !resize_nil, resize_replicate.
* intros [|?] [|?] ?; f_equal'; auto with lia.
Qed.
-Lemma resize_idempotent l n x : resize n x (resize n x l) = resize n x l.
+Lemma resize_idemp l n x : resize n x (resize n x l) = resize n x l.
Proof. by rewrite resize_resize. Qed.
Lemma resize_take_le l n m x : n ≤ m → resize n x (take m l) = resize n x l.
Proof. revert n m. induction l; intros [|?][|?] ?; f_equal'; auto with lia. Qed.
@@ -1265,7 +1265,7 @@ Lemma sublist_alter_compose f g l i n k :
sublist_alter (f ∘ g) i n l = sublist_alter f i n (sublist_alter g i n l).
Proof.
unfold sublist_alter, sublist_lookup. intros Hk ??; simplify_option_equality.
- by rewrite !take_app_alt, drop_app_alt, !(associative_L (++)), drop_app_alt,
+ by rewrite !take_app_alt, drop_app_alt, !(assoc_L (++)), drop_app_alt,
take_app_alt by (rewrite ?app_length, ?take_length, ?Hk; lia).
Qed.
@@ -1344,22 +1344,22 @@ Definition Permutation_singleton_inj := @Permutation_length_1 A.
Global Existing Instance Permutation_app'.
Global Instance: Proper ((≡ₚ) ==> (=)) (@length A).
Proof. induction 1; simpl; auto with lia. Qed.
-Global Instance: Commutative (≡ₚ) (@app A).
+Global Instance: Comm (≡ₚ) (@app A).
Proof.
intros l1. induction l1 as [|x l1 IH]; intros l2; simpl.
* by rewrite (right_id_L [] (++)).
* rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
Qed.
-Global Instance: ∀ x : A, Injective (≡ₚ) (≡ₚ) (x ::).
+Global Instance: ∀ x : A, Inj (≡ₚ) (≡ₚ) (x ::).
Proof. red. eauto using Permutation_cons_inv. Qed.
-Global Instance: ∀ k : list A, Injective (≡ₚ) (≡ₚ) (k ++).
+Global Instance: ∀ k : list A, Inj (≡ₚ) (≡ₚ) (k ++).
Proof.
red. induction k as [|x k IH]; intros l1 l2; simpl; auto.
- intros. by apply IH, (injective (x ::)).
+ intros. by apply IH, (inj (x ::)).
Qed.
-Global Instance: ∀ k : list A, Injective (≡ₚ) (≡ₚ) (++ k).
+Global Instance: ∀ k : list A, Inj (≡ₚ) (≡ₚ) (++ k).
Proof.
- intros k l1 l2. rewrite !(commutative (++) _ k). by apply (injective (k ++)).
+ intros k l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++)).
Qed.
Lemma replicate_Permutation n x l : replicate n x ≡ₚ l → replicate n x = l.
Proof.
@@ -1370,7 +1370,7 @@ Qed.
Lemma reverse_Permutation l : reverse l ≡ₚ l.
Proof.
induction l as [|x l IH]; [done|].
- by rewrite reverse_cons, (commutative (++)), IH.
+ by rewrite reverse_cons, (comm (++)), IH.
Qed.
Lemma delete_Permutation l i x : l !! i = Some x → l ≡ₚ x :: delete i l.
Proof.
@@ -1383,7 +1383,7 @@ Global Instance: PreOrder (@prefix_of A).
Proof.
split.
* intros ?. eexists []. by rewrite (right_id_L [] (++)).
- * intros ???[k1->] [k2->]. exists (k1 ++ k2). by rewrite (associative_L (++)).
+ * intros ???[k1->] [k2->]. exists (k1 ++ k2). by rewrite (assoc_L (++)).
Qed.
Lemma prefix_of_nil l : [] `prefix_of` l.
Proof. by exists l. Qed.
@@ -1400,14 +1400,14 @@ Lemma prefix_of_cons_inv_2 x y l1 l2 :
x :: l1 `prefix_of` y :: l2 → l1 `prefix_of` l2.
Proof. intros [k ?]; simplify_equality'. by exists k. Qed.
Lemma prefix_of_app k l1 l2 : l1 `prefix_of` l2 → k ++ l1 `prefix_of` k ++ l2.
-Proof. intros [k' ->]. exists k'. by rewrite (associative_L (++)). Qed.
+Proof. intros [k' ->]. exists k'. by rewrite (assoc_L (++)). Qed.
Lemma prefix_of_app_alt k1 k2 l1 l2 :
k1 = k2 → l1 `prefix_of` l2 → k1 ++ l1 `prefix_of` k2 ++ l2.
Proof. intros ->. apply prefix_of_app. Qed.
Lemma prefix_of_app_l l1 l2 l3 : l1 ++ l3 `prefix_of` l2 → l1 `prefix_of` l2.
-Proof. intros [k ->]. exists (l3 ++ k). by rewrite (associative_L (++)). Qed.
+Proof. intros [k ->]. exists (l3 ++ k). by rewrite (assoc_L (++)). Qed.
Lemma prefix_of_app_r l1 l2 l3 : l1 `prefix_of` l2 → l1 `prefix_of` l2 ++ l3.
-Proof. intros [k ->]. exists (k ++ l3). by rewrite (associative_L (++)). Qed.
+Proof. intros [k ->]. exists (k ++ l3). by rewrite (assoc_L (++)). Qed.
Lemma prefix_of_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
Proof. intros [? ->]. rewrite app_length. lia. Qed.
Lemma prefix_of_snoc_not l x : ¬l ++ [x] `prefix_of` l.
@@ -1416,7 +1416,7 @@ Global Instance: PreOrder (@suffix_of A).
Proof.
split.
* intros ?. by eexists [].
- * intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (associative_L (++)).
+ * intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)).
Qed.
Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2,
Decision (l1 `prefix_of` l2) := fix go l1 l2 :=
@@ -1513,41 +1513,41 @@ Lemma suffix_of_cons_nil_inv x l : ¬x :: l `suffix_of` [].
Proof. by intros [[] ?]. Qed.
Lemma suffix_of_snoc l1 l2 x :
l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [x].
-Proof. intros [k ->]. exists k. by rewrite (associative_L (++)). Qed.
+Proof. intros [k ->]. exists k. by rewrite (assoc_L (++)). Qed.
Lemma suffix_of_snoc_alt x y l1 l2 :
x = y → l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [y].
Proof. intros ->. apply suffix_of_snoc. Qed.
Lemma suffix_of_app l1 l2 k : l1 `suffix_of` l2 → l1 ++ k `suffix_of` l2 ++ k.
-Proof. intros [k' ->]. exists k'. by rewrite (associative_L (++)). Qed.
+Proof. intros [k' ->]. exists k'. by rewrite (assoc_L (++)). Qed.
Lemma suffix_of_app_alt l1 l2 k1 k2 :
k1 = k2 → l1 `suffix_of` l2 → l1 ++ k1 `suffix_of` l2 ++ k2.
Proof. intros ->. apply suffix_of_app. Qed.
Lemma suffix_of_snoc_inv_1 x y l1 l2 :
l1 ++ [x] `suffix_of` l2 ++ [y] → x = y.
Proof.
- intros [k' E]. rewrite (associative_L (++)) in E.
+ intros [k' E]. rewrite (assoc_L (++)) in E.
by simplify_list_equality.
Qed.
Lemma suffix_of_snoc_inv_2 x y l1 l2 :
l1 ++ [x] `suffix_of` l2 ++ [y] → l1 `suffix_of` l2.
Proof.
- intros [k' E]. exists k'. rewrite (associative_L (++)) in E.
+ intros [k' E]. exists k'. rewrite (assoc_L (++)) in E.
by simplify_list_equality.
Qed.
Lemma suffix_of_app_inv l1 l2 k :
l1 ++ k `suffix_of` l2 ++ k → l1 `suffix_of` l2.
Proof.
- intros [k' E]. exists k'. rewrite (associative_L (++)) in E.
+ intros [k' E]. exists k'. rewrite (assoc_L (++)) in E.
by simplify_list_equality.
Qed.
Lemma suffix_of_cons_l l1 l2 x : x :: l1 `suffix_of` l2 → l1 `suffix_of` l2.
-Proof. intros [k ->]. exists (k ++ [x]). by rewrite <-(associative_L (++)). Qed.
+Proof. intros [k ->]. exists (k ++ [x]). by rewrite <-(assoc_L (++)). Qed.
Lemma suffix_of_app_l l1 l2 l3 : l3 ++ l1 `suffix_of` l2 → l1 `suffix_of` l2.
-Proof. intros [k ->]. exists (k ++ l3). by rewrite <-(associative_L (++)). Qed.
+Proof. intros [k ->]. exists (k ++ l3). by rewrite <-(assoc_L (++)). Qed.
Lemma suffix_of_cons_r l1 l2 x : l1 `suffix_of` l2 → l1 `suffix_of` x :: l2.
Proof. intros [k ->]. by exists (x :: k). Qed.
Lemma suffix_of_app_r l1 l2 l3 : l1 `suffix_of` l2 → l1 `suffix_of` l3 ++ l2.
-Proof. intros [k ->]. exists (l3 ++ k). by rewrite (associative_L (++)). Qed.
+Proof. intros [k ->]. exists (l3 ++ k). by rewrite (assoc_L (++)). Qed.
Lemma suffix_of_cons_inv l1 l2 x y :
x :: l1 `suffix_of` y :: l2 → x :: l1 = y :: l2 ∨ x :: l1 `suffix_of` l2.
Proof.
@@ -1682,7 +1682,7 @@ Proof.
{ eexists [], k. by repeat constructor. }
rewrite sublist_cons_l. intros (k1 & k2 &?&?); subst.
destruct (IH l2 k2) as (h1 & h2 &?&?&?); trivial; subst.
- exists (k1 ++ x :: h1), h2. rewrite <-(associative_L (++)).
+ exists (k1 ++ x :: h1), h2. rewrite <-(assoc_L (++)).
auto using sublist_inserts_l, sublist_skip.
* intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
@@ -1698,10 +1698,10 @@ Proof.
revert l1 l2. induction k as [|y k IH]; intros l1 l2.
{ by rewrite !(right_id_L [] (++)). }
intros. feed pose proof (IH (l1 ++ [y]) (l2 ++ [y])) as Hl12.
- { by rewrite <-!(associative_L (++)). }
+ { by rewrite <-!(assoc_L (++)). }
rewrite sublist_app_l in Hl12. destruct Hl12 as (k1&k2&E&?&Hk2).
destruct k2 as [|z k2] using rev_ind; [inversion Hk2|].
- rewrite (associative_L (++)) in E; simplify_list_equality.
+ rewrite (assoc_L (++)) in E; simplify_list_equality.
eauto using sublist_inserts_r.
Qed.
Global Instance: PartialOrder (@sublist A).
@@ -1737,7 +1737,7 @@ Proof.
induction Hl12 as [|x l1 l2 _ IH|x l1 l2 _ IH]; intros k.
* by eexists [].
* destruct (IH (k ++ [x])) as [is His]. exists is.
- by rewrite <-!(associative_L (++)) in His.
+ by rewrite <-!(assoc_L (++)) in His.
* destruct (IH k) as [is His]. exists (is ++ [length k]).
rewrite fold_right_app. simpl. by rewrite delete_middle.
Qed.
@@ -1809,7 +1809,7 @@ Proof.
* exists k. by rewrite Hk.
* eexists []. rewrite (right_id_L [] (++)). by constructor.
* exists (x :: k). by rewrite Hk, Permutation_middle.
- * exists (k ++ k'). by rewrite Hk', Hk, (associative_L (++)).
+ * exists (k ++ k'). by rewrite Hk', Hk, (assoc_L (++)).
Qed.
Lemma contains_Permutation_length_le l1 l2 :
length l2 ≤ length l1 → l1 `contains` l2 → l1 ≡ₚ l2.
@@ -1829,7 +1829,7 @@ Proof.
* transitivity l2. by apply Permutation_contains.
transitivity k2. done. by apply Permutation_contains.
Qed.
-Global Instance: AntiSymmetric (≡ₚ) (@contains A).
+Global Instance: AntiSymm (≡ₚ) (@contains A).
Proof. red. auto using contains_Permutation_length_le, contains_length. Qed.
Lemma contains_take l i : take i l `contains` l.
Proof. auto using sublist_take, sublist_contains. Qed.
@@ -1863,11 +1863,11 @@ Qed.
Lemma contains_inserts_l k l1 l2 : l1 `contains` l2 → l1 `contains` k ++ l2.
Proof. induction k; try constructor; auto. Qed.
Lemma contains_inserts_r k l1 l2 : l1 `contains` l2 → l1 `contains` l2 ++ k.
-Proof. rewrite (commutative (++)). apply contains_inserts_l. Qed.
+Proof. rewrite (comm (++)). apply contains_inserts_l. Qed.
Lemma contains_skips_l k l1 l2 : l1 `contains` l2 → k ++ l1 `contains` k ++ l2.
Proof. induction k; try constructor; auto. Qed.
Lemma contains_skips_r k l1 l2 : l1 `contains` l2 → l1 ++ k `contains` l2 ++ k.
-Proof. rewrite !(commutative (++) _ k). apply contains_skips_l. Qed.
+Proof. rewrite !(comm (++) _ k). apply contains_skips_l. Qed.
Lemma contains_app l1 l2 k1 k2 :
l1 `contains` l2 → k1 `contains` k2 → l1 ++ k1 `contains` l2 ++ k2.
Proof.
@@ -1925,10 +1925,10 @@ Proof.
revert l1 l2. induction k as [|y k IH]; intros l1 l2.
{ by rewrite !(right_id_L [] (++)). }
intros. feed pose proof (IH (l1 ++ [y]) (l2 ++ [y])) as Hl12.
- { by rewrite <-!(associative_L (++)). }
+ { by rewrite <-!(assoc_L (++)). }
rewrite contains_app_l in Hl12. destruct Hl12 as (k1&k2&E1&?&Hk2).
rewrite contains_cons_l in Hk2. destruct Hk2 as (k2'&E2&?).
- rewrite E2, (Permutation_cons_append k2'), (associative_L (++)) in E1.
+ rewrite E2, (Permutation_cons_append k2'), (assoc_L (++)) in E1.
apply Permutation_app_inv_r in E1. rewrite E1. eauto using contains_inserts_r.
Qed.
Lemma contains_cons_middle x l k1 k2 :
@@ -1937,7 +1937,7 @@ Proof. rewrite <-Permutation_middle. by apply contains_skip. Qed.
Lemma contains_app_middle l1 l2 k1 k2 :
l2 `contains` k1 ++ k2 → l1 ++ l2 `contains` k1 ++ l1 ++ k2.
Proof.
- rewrite !(associative (++)), (commutative (++) k1 l1), <-(associative_L (++)).
+ rewrite !(assoc (++)), (comm (++) k1 l1), <-(assoc_L (++)).
by apply contains_skips_l.
Qed.
Lemma contains_middle l k1 k2 : l `contains` k1 ++ l ++ k2.
@@ -1964,7 +1964,7 @@ Proof.
Qed.
Lemma NoDup_Permutation l k : NoDup l → NoDup k → (∀ x, x ∈ l ↔ x ∈ k) → l ≡ₚ k.
Proof.
- intros. apply (anti_symmetric contains); apply NoDup_contains; naive_solver.
+ intros. apply (anti_symm contains); apply NoDup_contains; naive_solver.
Qed.
Section contains_dec.
@@ -2506,7 +2506,7 @@ Section Forall2_order.
Proof. split; apply _. Qed.
Global Instance: PreOrder R → PreOrder (Forall2 R).
Proof. split; apply _. Qed.
- Global Instance: AntiSymmetric (=) R → AntiSymmetric (=) (Forall2 R).
+ Global Instance: AntiSymm (=) R → AntiSymm (=) (Forall2 R).
Proof. induction 2; inversion_clear 1; f_equal; auto. Qed.
Global Instance: Proper (R ==> Forall2 R ==> Forall2 R) (::).
Proof. by constructor. Qed.
@@ -2620,7 +2620,7 @@ Section fmap.
Lemma list_fmap_ext (g : A → B) (l1 l2 : list A) :
(∀ x, f x = g x) → l1 = l2 → fmap f l1 = fmap g l2.
Proof. intros ? <-. induction l1; f_equal'; auto. Qed.
- Global Instance: Injective (=) (=) f → Injective (=) (=) (fmap f).
+ Global Instance: Inj (=) (=) f → Inj (=) (=) (fmap f).
Proof.
intros ? l1. induction l1 as [|x l1 IH]; [by intros [|??]|].
intros [|??]; intros; f_equal'; simplify_equality; auto.
@@ -2694,12 +2694,12 @@ Section fmap.
induction l; simpl; inversion_clear 1; constructor; auto.
rewrite elem_of_list_fmap in *. naive_solver.
Qed.
- Lemma NoDup_fmap_2 `{!Injective (=) (=) f} l : NoDup l → NoDup (f <$> l).
+ Lemma NoDup_fmap_2 `{!Inj (=) (=) f} l : NoDup l → NoDup (f <$> l).
Proof.
induction 1; simpl; constructor; trivial. rewrite elem_of_list_fmap.
- intros [y [Hxy ?]]. apply (injective f) in Hxy. by subst.
+ intros [y [Hxy ?]]. apply (inj f) in Hxy. by subst.
Qed.
- Lemma NoDup_fmap `{!Injective (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
+ Lemma NoDup_fmap `{!Inj (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
Global Instance fmap_sublist: Proper (sublist ==> sublist) (fmap f).
Proof. induction 1; simpl; econstructor; eauto. Qed.
@@ -2774,7 +2774,7 @@ Section bind.
Proof.
induction 1; csimpl; auto.
* by apply contains_app.
- * by rewrite !(associative_L (++)), (commutative (++) (f _)).
+ * by rewrite !(assoc_L (++)), (comm (++) (f _)).
* by apply contains_inserts_l.
* etransitivity; eauto.
Qed.
@@ -2782,7 +2782,7 @@ Section bind.
Proof.
induction 1; csimpl; auto.
* by f_equiv.
- * by rewrite !(associative_L (++)), (commutative (++) (f _)).
+ * by rewrite !(assoc_L (++)), (comm (++) (f _)).
* etransitivity; eauto.
Qed.
Lemma bind_cons x l : (x :: l) ≫= f = f x ++ l ≫= f.
@@ -2790,7 +2790,7 @@ Section bind.
Lemma bind_singleton x : [x] ≫= f = f x.
Proof. csimpl. by rewrite (right_id_L _ (++)). Qed.
Lemma bind_app l1 l2 : (l1 ++ l2) ≫= f = (l1 ≫= f) ++ (l2 ≫= f).
- Proof. by induction l1; csimpl; rewrite <-?(associative_L (++)); f_equal. Qed.
+ Proof. by induction l1; csimpl; rewrite <-?(assoc_L (++)); f_equal. Qed.
Lemma elem_of_list_bind (x : B) (l : list A) :
x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
Proof.
@@ -2944,7 +2944,7 @@ Section permutations.
revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl.
{ rewrite !elem_of_list_singleton. intros ? ->. exists [x1].
change (interleave x2 [x1]) with ([[x2; x1]] ++ [[x1; x2]]).
- by rewrite (commutative (++)), elem_of_list_singleton. }
+ by rewrite (comm (++)), elem_of_list_singleton. }
rewrite elem_of_cons, elem_of_list_fmap.
intros Hl1 [? | [l2' [??]]]; simplify_equality'.
* rewrite !elem_of_cons, elem_of_list_fmap in Hl1.
@@ -3069,7 +3069,7 @@ Section zip_with.
destruct (IH l k) as (l1&k1&l2&k2&->&->&->&->&?); [done |].
exists (x :: l1), (y :: k1), l2, k2; simpl; auto with congruence.
Qed.
- Lemma zip_with_inj `{!Injective2 (=) (=) (=) f} l1 l2 k1 k2 :
+ Lemma zip_with_inj `{!Inj2 (=) (=) (=) f} l1 l2 k1 k2 :
length l1 = length k1 → length l2 = length k2 →
zip_with f l1 k1 = zip_with f l2 k2 → l1 = l2 ∧ k1 = k2.
Proof.
@@ -3198,9 +3198,9 @@ Proof.
* revert l. induction k as [|z k IH]; simpl; intros l; inversion_clear 1.
{ by eexists [], k, z. }
destruct (IH (z :: l)) as (k'&k''&y&->&->); [done |].
- eexists (z :: k'), k'', y. by rewrite reverse_cons, <-(associative_L (++)).
+ eexists (z :: k'), k'', y. by rewrite reverse_cons, <-(assoc_L (++)).
* intros (k'&k''&y&->&->). revert l. induction k' as [|z k' IH]; [by left|].
- intros l; right. by rewrite reverse_cons, <-!(associative_L (++)).
+ intros l; right. by rewrite reverse_cons, <-!(assoc_L (++)).
Qed.
Section zipped_list_ind.
Context {A} (P : list A → list A → Prop).
@@ -3214,7 +3214,7 @@ Lemma zipped_Forall_app {A} (P : list A → list A → A → Prop) l k k' :
zipped_Forall P l (k ++ k') → zipped_Forall P (reverse k ++ l) k'.
Proof.
revert l. induction k as [|x k IH]; simpl; [done |].
- inversion_clear 1. rewrite reverse_cons, <-(associative_L (++)). by apply IH.
+ inversion_clear 1. rewrite reverse_cons, <-(assoc_L (++)). by apply IH.
Qed.
(** * Relection over lists *)
@@ -3339,8 +3339,8 @@ Ltac simplify_list_equality ::= repeat
| H : [] = _ <$> _ |- _ => symmetry in H; apply fmap_nil_inv in H
| H : zip_with _ _ _ = [] |- _ => apply zip_with_nil_inv in H; destruct H
| H : [] = zip_with _ _ _ |- _ => symmetry in H
- | |- context [(_ ++ _) ++ _] => rewrite <-(associative_L (++))
- | H : context [(_ ++ _) ++ _] |- _ => rewrite <-(associative_L (++)) in H
+ | |- context [(_ ++ _) ++ _] => rewrite <-(assoc_L (++))
+ | H : context [(_ ++ _) ++ _] |- _ => rewrite <-(assoc_L (++)) in H
| H : context [_ <$> (_ ++ _)] |- _ => rewrite fmap_app in H
| |- context [_ <$> (_ ++ _)] => rewrite fmap_app
| |- context [_ ++ []] => rewrite (right_id_L [] (++))
@@ -3350,11 +3350,11 @@ Ltac simplify_list_equality ::= repeat
| |- context [drop _ (_ <$> _)] => rewrite <-fmap_drop
| H : context [drop _ (_ <$> _)] |- _ => rewrite <-fmap_drop in H
| H : _ ++ _ = _ ++ _ |- _ =>
- repeat (rewrite <-app_comm_cons in H || rewrite <-(associative_L (++)) in H);
- apply app_injective_1 in H; [destruct H|solve_length]
+ repeat (rewrite <-app_comm_cons in H || rewrite <-(assoc_L (++)) in H);
+ apply app_inj_1 in H; [destruct H|solve_length]
| H : _ ++ _ = _ ++ _ |- _ =>
- repeat (rewrite app_comm_cons in H || rewrite (associative_L (++)) in H);
- apply app_injective_2 in H; [destruct H|solve_length]
+ repeat (rewrite app_comm_cons in H || rewrite (assoc_L (++)) in H);
+ apply app_inj_2 in H; [destruct H|solve_length]
| |- context [zip_with _ (_ ++ _) (_ ++ _)] =>
rewrite zip_with_app by solve_length
| |- context [take _ (_ ++ _)] => rewrite take_app_alt by solve_length
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 65b9621e9..e2e728b3f 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -35,7 +35,7 @@ Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
Instance nat_le_dec: ∀ x y : nat, Decision (x ≤ y) := le_dec.
Instance nat_lt_dec: ∀ x y : nat, Decision (x < y) := lt_dec.
Instance nat_inhabited: Inhabited nat := populate 0%nat.
-Instance: Injective (=) (=) S.
+Instance: Inj (=) (=) S.
Proof. by injection 1. Qed.
Instance: PartialOrder (≤).
Proof. repeat split; repeat intro; auto with lia. Qed.
@@ -110,9 +110,9 @@ Instance positive_inhabited: Inhabited positive := populate 1.
Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
Instance maybe_x1 : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
-Instance: Injective (=) (=) (~0).
+Instance: Inj (=) (=) (~0).
Proof. by injection 1. Qed.
-Instance: Injective (=) (=) (~1).
+Instance: Inj (=) (=) (~1).
Proof. by injection 1. Qed.
(** Since [positive] represents lists of bits, we define list operations
@@ -141,9 +141,9 @@ Global Instance: LeftId (=) 1 (++).
Proof. intros p. by induction p; intros; f_equal'. Qed.
Global Instance: RightId (=) 1 (++).
Proof. done. Qed.
-Global Instance: Associative (=) (++).
+Global Instance: Assoc (=) (++).
Proof. intros ?? p. by induction p; intros; f_equal'. Qed.
-Global Instance: ∀ p : positive, Injective (=) (=) (++ p).
+Global Instance: ∀ p : positive, Inj (=) (=) (++ p).
Proof. intros p ???. induction p; simplify_equality; auto. Qed.
Lemma Preverse_go_app p1 p2 p3 :
@@ -184,7 +184,7 @@ Infix "`mod`" := N.modulo (at level 35) : N_scope.
Arguments N.add _ _ : simpl never.
-Instance: Injective (=) (=) Npos.
+Instance: Inj (=) (=) Npos.
Proof. by injection 1. Qed.
Instance N_eq_dec: ∀ x y : N, Decision (x = y) := N.eq_dec.
@@ -220,9 +220,9 @@ Infix "`rem`" := Z.rem (at level 35) : Z_scope.
Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope.
-Instance: Injective (=) (=) Zpos.
+Instance: Inj (=) (=) Zpos.
Proof. by injection 1. Qed.
-Instance: Injective (=) (=) Zneg.
+Instance: Inj (=) (=) Zneg.
Proof. by injection 1. Qed.
Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
@@ -371,18 +371,18 @@ Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y ↔ z + x < z + y.
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed.
Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y ↔ x + z < y + z.
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
-Instance: Injective (=) (=) Qcopp.
+Instance: Inj (=) (=) Qcopp.
Proof.
intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
Qed.
-Instance: ∀ z, Injective (=) (=) (Qcplus z).
+Instance: ∀ z, Inj (=) (=) (Qcplus z).
Proof.
- intros z x y H. by apply (anti_symmetric (≤));
+ intros z x y H. by apply (anti_symm (≤));
rewrite (Qcplus_le_mono_l _ _ z), H.
Qed.
-Instance: ∀ z, Injective (=) (=) (λ x, x + z).
+Instance: ∀ z, Inj (=) (=) (λ x, x + z).
Proof.
- intros z x y H. by apply (anti_symmetric (≤));
+ intros z x y H. by apply (anti_symm (≤));
rewrite (Qcplus_le_mono_r _ _ z), H.
Qed.
Lemma Qcplus_pos_nonneg (x y : Qc) : 0 < x → 0 ≤ y → 0 < x + y.
diff --git a/prelude/option.v b/prelude/option.v
index 4a28e666c..f6e217602 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -16,7 +16,7 @@ Lemma Some_ne_None {A} (a : A) : Some a ≠None.
Proof. congruence. Qed.
Lemma eq_None_ne_Some {A} (x : option A) a : x = None → x ≠Some a.
Proof. congruence. Qed.
-Instance Some_inj {A} : Injective (=) (=) (@Some A).
+Instance Some_inj {A} : Inj (=) (=) (@Some A).
Proof. congruence. Qed.
(** The non dependent elimination principle on the option type. *)
@@ -232,14 +232,14 @@ Section option_union_intersection_difference.
Proof. by intros [?|]. Qed.
Global Instance: RightId (=) None (union_with f).
Proof. by intros [?|]. Qed.
- Global Instance: Commutative (=) f → Commutative (=) (union_with f).
- Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
+ Global Instance: Comm (=) f → Comm (=) (union_with f).
+ Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
Global Instance: LeftAbsorb (=) None (intersection_with f).
Proof. by intros [?|]. Qed.
Global Instance: RightAbsorb (=) None (intersection_with f).
Proof. by intros [?|]. Qed.
- Global Instance: Commutative (=) f → Commutative (=) (intersection_with f).
- Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
+ Global Instance: Comm (=) f → Comm (=) (intersection_with f).
+ Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
Global Instance: RightId (=) None (difference_with f).
Proof. by intros [?|]. Qed.
End option_union_intersection_difference.
diff --git a/prelude/orders.v b/prelude/orders.v
index 0dd57462b..220376482 100644
--- a/prelude/orders.v
+++ b/prelude/orders.v
@@ -17,8 +17,8 @@ Section orders.
Lemma reflexive_eq `{!Reflexive R} X Y : X = Y → X ⊆ Y.
Proof. by intros <-. Qed.
- Lemma anti_symmetric_iff `{!PartialOrder R} X Y : X = Y ↔ R X Y ∧ R Y X.
- Proof. split. by intros ->. by intros [??]; apply (anti_symmetric _). Qed.
+ Lemma anti_symm_iff `{!PartialOrder R} X Y : X = Y ↔ R X Y ∧ R Y X.
+ Proof. split. by intros ->. by intros [??]; apply (anti_symm _). Qed.
Lemma strict_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ Y ⊈ X.
Proof. done. Qed.
Lemma strict_include X Y : X ⊂ Y → X ⊆ Y.
@@ -46,17 +46,17 @@ Section orders.
Qed.
Global Instance preorder_subset_dec_slow `{∀ X Y, Decision (X ⊆ Y)}
(X Y : A) : Decision (X ⊂ Y) | 100 := _.
- Lemma strict_spec_alt `{!AntiSymmetric (=) R} X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠Y.
+ Lemma strict_spec_alt `{!AntiSymm (=) R} X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠Y.
Proof.
split.
* intros [? HYX]. split. done. by intros <-.
- * intros [? HXY]. split. done. by contradict HXY; apply (anti_symmetric R).
+ * intros [? HXY]. split. done. by contradict HXY; apply (anti_symm R).
Qed.
Lemma po_eq_dec `{!PartialOrder R, ∀ X Y, Decision (X ⊆ Y)} (X Y : A) :
Decision (X = Y).
Proof.
refine (cast_if_and (decide (X ⊆ Y)) (decide (Y ⊆ X)));
- abstract (rewrite anti_symmetric_iff; tauto).
+ abstract (rewrite anti_symm_iff; tauto).
Defined.
Lemma total_not `{!Total R} X Y : X ⊈ Y → Y ⊆ X.
Proof. intros. destruct (total R X Y); tauto. Qed.
@@ -77,7 +77,7 @@ Section strict_orders.
Lemma irreflexive_eq `{!Irreflexive R} X Y : X = Y → ¬X ⊂ Y.
Proof. intros ->. apply (irreflexivity R). Qed.
- Lemma strict_anti_symmetric `{!StrictOrder R} X Y :
+ Lemma strict_anti_symm `{!StrictOrder R} X Y :
X ⊂ Y → Y ⊂ X → False.
Proof. intros. apply (irreflexivity R X). by transitivity Y. Qed.
Global Instance trichotomyT_dec `{!TrichotomyT R, !StrictOrder R} X Y :
@@ -85,7 +85,7 @@ Section strict_orders.
match trichotomyT R X Y with
| inleft (left H) => left H
| inleft (right H) => right (irreflexive_eq _ _ H)
- | inright H => right (strict_anti_symmetric _ _ H)
+ | inright H => right (strict_anti_symm _ _ H)
end.
Global Instance trichotomyT_trichotomy `{!TrichotomyT R} : Trichotomy R.
Proof. intros X Y. destruct (trichotomyT R X Y) as [[|]|]; tauto. Qed.
@@ -98,7 +98,7 @@ Ltac simplify_order := repeat
| H1 : ?R ?x ?y |- _ =>
match goal with
| H2 : R y x |- _ =>
- assert (x = y) by (by apply (anti_symmetric R)); clear H1 H2
+ assert (x = y) by (by apply (anti_symm R)); clear H1 H2
| H2 : R y ?z |- _ =>
unless (R x z) by done;
assert (R x z) by (by transitivity y)
@@ -150,7 +150,7 @@ Section sorted.
Lemma Sorted_StronglySorted `{!Transitive R} l :
Sorted R l → StronglySorted R l.
Proof. by apply Sorted.Sorted_StronglySorted. Qed.
- Lemma StronglySorted_unique `{!AntiSymmetric (=) R} l1 l2 :
+ Lemma StronglySorted_unique `{!AntiSymm (=) R} l1 l2 :
StronglySorted R l1 → StronglySorted R l2 → l1 ≡ₚ l2 → l1 = l2.
Proof.
intros Hl1; revert l2. induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hl2 E.
@@ -162,9 +162,9 @@ Section sorted.
assert (x2 ∈ x1 :: l1) as Hx2' by (by rewrite E; left).
assert (x1 ∈ x2 :: l2) as Hx1' by (by rewrite <-E; left).
inversion Hx1'; inversion Hx2'; simplify_equality; auto. }
- f_equal. by apply IH, (injective (x2 ::)).
+ f_equal. by apply IH, (inj (x2 ::)).
Qed.
- Lemma Sorted_unique `{!Transitive R, !AntiSymmetric (=) R} l1 l2 :
+ Lemma Sorted_unique `{!Transitive R, !AntiSymm (=) R} l1 l2 :
Sorted R l1 → Sorted R l2 → l1 ≡ₚ l2 → l1 = l2.
Proof. auto using StronglySorted_unique, Sorted_StronglySorted. Qed.
@@ -272,7 +272,7 @@ Section merge_sort_correct.
l ++ merge_stack_flatten st.
Proof.
revert l. induction st as [|[l'|] st IH]; intros l; simpl; auto.
- by rewrite IH, merge_Permutation, (associative_L _), (commutative (++) l).
+ by rewrite IH, merge_Permutation, (assoc_L _), (comm (++) l).
Qed.
Lemma Sorted_merge_stack st :
merge_stack_Sorted st → Sorted R (merge_stack R st).
@@ -364,7 +364,7 @@ Hint Extern 0 (@Equivalence _ (≡)) =>
Section partial_order.
Context `{SubsetEq A, !PartialOrder (@subseteq A _)}.
Global Instance: LeibnizEquiv A.
- Proof. intros ?? [??]; by apply (anti_symmetric (⊆)). Qed.
+ Proof. intros ?? [??]; by apply (anti_symm (⊆)). Qed.
End partial_order.
(** * Join semi lattices *)
@@ -393,15 +393,15 @@ Section join_semi_lattice.
unfold equiv, preorder_equiv.
split; apply union_preserving; simpl in *; tauto.
Qed.
- Global Instance: Idempotent ((≡) : relation A) (∪).
+ Global Instance: IdemP ((≡) : relation A) (∪).
Proof. split; eauto. Qed.
Global Instance: LeftId ((≡) : relation A) ∅ (∪).
Proof. split; eauto. Qed.
Global Instance: RightId ((≡) : relation A) ∅ (∪).
Proof. split; eauto. Qed.
- Global Instance: Commutative ((≡) : relation A) (∪).
+ Global Instance: Comm ((≡) : relation A) (∪).
Proof. split; auto. Qed.
- Global Instance: Associative ((≡) : relation A) (∪).
+ Global Instance: Assoc ((≡) : relation A) (∪).
Proof. split; auto. Qed.
Lemma subseteq_union X Y : X ⊆ Y ↔ X ∪ Y ≡ Y.
Proof. repeat split; eauto. intros HXY. rewrite <-HXY. auto. Qed.
@@ -422,13 +422,13 @@ Section join_semi_lattice.
Lemma union_list_app Xs1 Xs2 : ⋃ (Xs1 ++ Xs2) ≡ ⋃ Xs1 ∪ ⋃ Xs2.
Proof.
induction Xs1 as [|X Xs1 IH]; simpl; [by rewrite (left_id ∅ _)|].
- by rewrite IH, (associative _).
+ by rewrite IH, (assoc _).
Qed.
Lemma union_list_reverse Xs : ⋃ (reverse Xs) ≡ ⋃ Xs.
Proof.
induction Xs as [|X Xs IH]; simpl; [done |].
by rewrite reverse_cons, union_list_app,
- union_list_singleton, (commutative _), IH.
+ union_list_singleton, (comm _), IH.
Qed.
Lemma union_list_preserving Xs Ys : Xs ⊆* Ys → ⋃ Xs ⊆ ⋃ Ys.
Proof. induction 1; simpl; auto using union_preserving. Qed.
@@ -448,16 +448,16 @@ Section join_semi_lattice.
Section leibniz.
Context `{!LeibnizEquiv A}.
- Global Instance: Idempotent (=) (∪).
- Proof. intros ?. unfold_leibniz. apply (idempotent _). Qed.
+ Global Instance: IdemP (=) (∪).
+ Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
Global Instance: LeftId (=) ∅ (∪).
Proof. intros ?. unfold_leibniz. apply (left_id _ _). Qed.
Global Instance: RightId (=) ∅ (∪).
Proof. intros ?. unfold_leibniz. apply (right_id _ _). Qed.
- Global Instance: Commutative (=) (∪).
- Proof. intros ??. unfold_leibniz. apply (commutative _). Qed.
- Global Instance: Associative (=) (∪).
- Proof. intros ???. unfold_leibniz. apply (associative _). Qed.
+ Global Instance: Comm (=) (∪).
+ Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
+ Global Instance: Assoc (=) (∪).
+ Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
Lemma subseteq_union_L X Y : X ⊆ Y ↔ X ∪ Y = Y.
Proof. unfold_leibniz. apply subseteq_union. Qed.
Lemma subseteq_union_1_L X Y : X ⊆ Y → X ∪ Y = Y.
@@ -519,11 +519,11 @@ Section meet_semi_lattice.
unfold equiv, preorder_equiv. split;
apply intersection_preserving; simpl in *; tauto.
Qed.
- Global Instance: Idempotent ((≡) : relation A) (∩).
+ Global Instance: IdemP ((≡) : relation A) (∩).
Proof. split; eauto. Qed.
- Global Instance: Commutative ((≡) : relation A) (∩).
+ Global Instance: Comm ((≡) : relation A) (∩).
Proof. split; auto. Qed.
- Global Instance: Associative ((≡) : relation A) (∩).
+ Global Instance: Assoc ((≡) : relation A) (∩).
Proof. split; auto. Qed.
Lemma subseteq_intersection X Y : X ⊆ Y ↔ X ∩ Y ≡ X.
Proof. repeat split; eauto. intros HXY. rewrite <-HXY. auto. Qed.
@@ -534,12 +534,12 @@ Section meet_semi_lattice.
Section leibniz.
Context `{!LeibnizEquiv A}.
- Global Instance: Idempotent (=) (∩).
- Proof. intros ?. unfold_leibniz. apply (idempotent _). Qed.
- Global Instance: Commutative (=) (∩).
- Proof. intros ??. unfold_leibniz. apply (commutative _). Qed.
- Global Instance: Associative (=) (∩).
- Proof. intros ???. unfold_leibniz. apply (associative _). Qed.
+ Global Instance: IdemP (=) (∩).
+ Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
+ Global Instance: Comm (=) (∩).
+ Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
+ Global Instance: Assoc (=) (∩).
+ Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
Lemma subseteq_intersection_L X Y : X ⊆ Y ↔ X ∩ Y = X.
Proof. unfold_leibniz. apply subseteq_intersection. Qed.
Lemma subseteq_intersection_1_L X Y : X ⊆ Y → X ∩ Y = X.
@@ -556,7 +556,7 @@ Section lattice.
Global Instance: LeftAbsorb ((≡) : relation A) ∅ (∩).
Proof. split. by apply intersection_subseteq_l. by apply subseteq_empty. Qed.
Global Instance: RightAbsorb ((≡) : relation A) ∅ (∩).
- Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed.
+ Proof. intros ?. by rewrite (comm _), (left_absorb _ _). Qed.
Lemma union_intersection_l (X Y Z : A) : X ∪ (Y ∩ Z) ≡ (X ∪ Y) ∩ (X ∪ Z).
Proof.
split; [apply union_least|apply lattice_distr].
@@ -566,7 +566,7 @@ Section lattice.
* apply union_subseteq_r_transitive, intersection_subseteq_r.
Qed.
Lemma union_intersection_r (X Y Z : A) : (X ∩ Y) ∪ Z ≡ (X ∪ Z) ∩ (Y ∪ Z).
- Proof. by rewrite !(commutative _ _ Z), union_intersection_l. Qed.
+ Proof. by rewrite !(comm _ _ Z), union_intersection_l. Qed.
Lemma intersection_union_l (X Y Z : A) : X ∩ (Y ∪ Z) ≡ (X ∩ Y) ∪ (X ∩ Z).
Proof.
split.
@@ -582,7 +582,7 @@ Section lattice.
+ apply intersection_subseteq_r_transitive, union_subseteq_r.
Qed.
Lemma intersection_union_r (X Y Z : A) : (X ∪ Y) ∩ Z ≡ (X ∩ Z) ∪ (Y ∩ Z).
- Proof. by rewrite !(commutative _ _ Z), intersection_union_l. Qed.
+ Proof. by rewrite !(comm _ _ Z), intersection_union_l. Qed.
Section leibniz.
Context `{!LeibnizEquiv A}.
diff --git a/prelude/pmap.v b/prelude/pmap.v
index ec91cd490..00cd7e874 100644
--- a/prelude/pmap.v
+++ b/prelude/pmap.v
@@ -178,14 +178,14 @@ Proof.
* rewrite elem_of_cons. intros [?|?]; simplify_equality.
{ left; exists 1. by rewrite (left_id_L 1 (++))%positive. }
destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
- { left; exists (i' ~ 0). by rewrite Preverse_xO, (associative_L _). }
+ { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
- left; exists (i' ~ 1). by rewrite Preverse_xI, (associative_L _).
+ left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _).
* intros.
destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
- { left; exists (i' ~ 0). by rewrite Preverse_xO, (associative_L _). }
+ { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
- left; exists (i' ~ 1). by rewrite Preverse_xI, (associative_L _). }
+ left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _). }
revert t j i acc. assert (∀ t j i acc,
(i, x) ∈ acc → (i, x) ∈ Pto_list_raw j t acc) as help.
{ intros t; induction t as [|[y|] l IHl r IHr]; intros j i acc;
@@ -195,15 +195,15 @@ Proof.
* done.
* rewrite elem_of_cons. destruct i as [i|i|]; simplify_equality'.
+ right. apply help. specialize (IHr (j~1) i).
- rewrite Preverse_xI, (associative_L _) in IHr. by apply IHr.
+ rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
+ right. specialize (IHl (j~0) i).
- rewrite Preverse_xO, (associative_L _) in IHl. by apply IHl.
+ rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
+ left. by rewrite (left_id_L 1 (++))%positive.
* destruct i as [i|i|]; simplify_equality'.
+ apply help. specialize (IHr (j~1) i).
- rewrite Preverse_xI, (associative_L _) in IHr. by apply IHr.
+ rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
+ specialize (IHl (j~0) i).
- rewrite Preverse_xO, (associative_L _) in IHl. by apply IHl.
+ rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
Qed.
Lemma Pto_list_nodup {A} j (t : Pmap_raw A) acc :
(∀ i x, (i ++ Preverse j, x) ∈ acc → t !! i = None) →
@@ -222,18 +222,18 @@ Proof.
discriminate (Hin Hj). }
apply IHl.
{ intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
- + rewrite Preverse_xO, Preverse_xI, !(associative_L _) in Hi.
- by apply (injective (++ _)) in Hi.
- + apply (Hin (i~0) x). by rewrite Preverse_xO, (associative_L _) in Hi. }
+ + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
+ by apply (inj (++ _)) in Hi.
+ + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
apply IHr; auto. intros i x Hi.
- apply (Hin (i~1) x). by rewrite Preverse_xI, (associative_L _) in Hi.
+ apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
* apply IHl.
{ intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
- + rewrite Preverse_xO, Preverse_xI, !(associative_L _) in Hi.
- by apply (injective (++ _)) in Hi.
- + apply (Hin (i~0) x). by rewrite Preverse_xO, (associative_L _) in Hi. }
+ + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
+ by apply (inj (++ _)) in Hi.
+ + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
apply IHr; auto. intros i x Hi.
- apply (Hin (i~1) x). by rewrite Preverse_xI, (associative_L _) in Hi.
+ apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
Qed.
Lemma Pomap_lookup {A B} (f : A → option B) t i :
Pomap_raw f t !! i = t !! i ≫= f.
diff --git a/prelude/pretty.v b/prelude/pretty.v
index dbd0311de..b246ec428 100644
--- a/prelude/pretty.v
+++ b/prelude/pretty.v
@@ -36,7 +36,7 @@ Proof.
by destruct (decide (0 < x)%N); auto using pretty_N_go_help_irrel.
Qed.
Instance pretty_N : Pretty N := λ x, pretty_N_go x ""%string.
-Instance pretty_N_injective : Injective (@eq N) (=) pretty.
+Instance pretty_N_inj : Inj (@eq N) (=) pretty.
Proof.
assert (∀ x y, x < 10 → y < 10 →
pretty_N_char x = pretty_N_char y → x = y)%N.
diff --git a/prelude/strings.v b/prelude/strings.v
index fd41ea2de..f2074f248 100644
--- a/prelude/strings.v
+++ b/prelude/strings.v
@@ -13,7 +13,7 @@ Arguments String.append _ _ : simpl never.
Instance assci_eq_dec : ∀ a1 a2, Decision (a1 = a2) := ascii_dec.
Instance string_eq_dec (s1 s2 : string) : Decision (s1 = s2).
Proof. solve_decision. Defined.
-Instance: Injective (=) (=) (String.append s1).
+Instance: Inj (=) (=) (String.append s1).
Proof. intros s1 ???. induction s1; simplify_equality'; f_equal'; auto. Qed.
(* Reverse *)
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 8a0551fb8..357f4fbde 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -186,8 +186,8 @@ Ltac simplify_equality := repeat
| H : ?x = _ |- _ => subst x
| H : _ = ?x |- _ => subst x
| H : _ = _ |- _ => discriminate H
- | H : ?f _ = ?f _ |- _ => apply (injective f) in H
- | H : ?f _ _ = ?f _ _ |- _ => apply (injective2 f) in H; destruct H
+ | H : ?f _ = ?f _ |- _ => apply (inj f) in H
+ | H : ?f _ _ = ?f _ _ |- _ => apply (inj2 f) in H; destruct H
(* before [injection'] to circumvent bug #2939 in some situations *)
| H : ?f _ = ?f _ |- _ => injection' H
| H : ?f _ _ = ?f _ _ |- _ => injection' H
diff --git a/prelude/vector.v b/prelude/vector.v
index da77f8fd9..4b11efe4a 100644
--- a/prelude/vector.v
+++ b/prelude/vector.v
@@ -69,9 +69,9 @@ Ltac inv_fin i :=
revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
end.
-Instance: Injective (=) (=) (@FS n).
+Instance: Inj (=) (=) (@FS n).
Proof. intros n i j. apply Fin.FS_inj. Qed.
-Instance: Injective (=) (=) (@fin_to_nat n).
+Instance: Inj (=) (=) (@fin_to_nat n).
Proof.
intros n i. induction i; intros j; inv_fin j; intros; f_equal'; auto with lia.
Qed.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index f6e81accf..c0a1c6b13 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -41,10 +41,10 @@ Proof.
(rs1 ++ r2 :: rs2 ++ [r2'])) as (rs'&Qs'&?&?).
{ apply Forall3_app, Forall3_cons,
Forall3_app, Forall3_cons, Forall3_nil; eauto using wptp_le. }
- { by rewrite -Permutation_middle /= (associative (++))
- (commutative (++)) /= associative big_op_app. }
+ { by rewrite -Permutation_middle /= (assoc (++))
+ (comm (++)) /= assoc big_op_app. }
exists rs', ([λ _, True%I] ++ Qs'); split; auto.
- by rewrite (associative _ _ _ Qs') -(associative _ Qs1).
+ by rewrite (assoc _ _ _ Qs') -(assoc _ Qs1).
* apply (IH (Qs1 ++ Q :: Qs2) (rs1 ++ r2 â‹… r2' :: rs2)).
{ rewrite /option_list right_id_L.
apply Forall3_app, Forall3_cons; eauto using wptp_le.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index b4dff6309..a063d70d8 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -37,7 +37,7 @@ Section auth.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
transitivity (▷auth_inv γ ★ auth_own γ a)%I.
{ rewrite /auth_inv -later_intro -(exist_intro a).
- rewrite [(_ ★ φ _)%I]commutative -associative. apply sep_mono; first done.
+ rewrite [(_ ★ φ _)%I]comm -assoc. apply sep_mono; first done.
rewrite /auth_own -own_op auth_both_op. done. }
rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
by rewrite always_and_sep_l'.
@@ -50,7 +50,7 @@ Section auth.
Proof.
rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
rewrite later_sep [(â–·own _ _ _)%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
- rewrite /auth_own [(_ ★ ▷φ _)%I]commutative -associative -own_op.
+ rewrite /auth_own [(_ ★ ▷φ _)%I]comm -assoc -own_op.
rewrite own_valid_r auth_valid !sep_exist_l /=. apply exist_elim=>a'.
rewrite [∅ ⋅ _]left_id -(exist_intro a').
apply (eq_rewrite b (a â‹… a')
@@ -66,7 +66,7 @@ Section auth.
⊑ pvs E E (▷auth_inv γ ★ auth_own γ (L a)).
Proof.
intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a â‹… a')).
- rewrite later_sep [(_ ★ ▷φ _)%I]commutative -associative.
+ rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
rewrite -pvs_frame_l. apply sep_mono; first done.
rewrite -later_intro -own_op.
by apply own_update, (auth_local_update_l L).
@@ -85,14 +85,14 @@ Section auth.
rewrite /auth_ctx=>HN.
rewrite -inv_fsa; last eassumption.
apply sep_mono; first done. apply wand_intro_l.
- rewrite associative auth_opened !pvs_frame_r !sep_exist_r.
+ rewrite assoc auth_opened !pvs_frame_r !sep_exist_r.
apply fsa_strip_pvs; first done. apply exist_elim=>a'.
- rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]commutative.
- rewrite -[((_ ★ ▷_) ★ _)%I]associative wand_elim_r fsa_frame_l.
- apply fsa_mono_pvs; first done. intros x. rewrite commutative -!associative.
+ rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]comm.
+ rewrite -[((_ ★ ▷_) ★ _)%I]assoc wand_elim_r fsa_frame_l.
+ apply fsa_mono_pvs; first done. intros x. rewrite comm -!assoc.
apply const_elim_sep_l=>-[HL Hv].
- rewrite associative [(_ ★ (_ -★ _))%I]commutative -associative.
+ rewrite assoc [(_ ★ (_ -★ _))%I]comm -assoc.
rewrite auth_closing //; []. erewrite pvs_frame_l. apply pvs_mono.
- by rewrite associative [(_ ★ ▷_)%I]commutative -associative wand_elim_l.
+ by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l.
Qed.
End auth.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index dbda42db2..59619a203 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -40,8 +40,8 @@ Lemma ht_vs E P P' Q Q' e :
⊑ {{ P }} e @ E {{ Q }}.
Proof.
apply (always_intro' _ _), impl_intro_l.
- rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
- rewrite associative pvs_impl_r pvs_always_r wp_always_r.
+ rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
+ rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
rewrite -(pvs_wp E e Q) -(wp_pvs E e Q); apply pvs_mono, wp_mono=> v.
by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
Qed.
@@ -51,8 +51,8 @@ Lemma ht_atomic E1 E2 P P' Q Q' e :
⊑ {{ P }} e @ E1 {{ Q }}.
Proof.
intros ??; apply (always_intro' _ _), impl_intro_l.
- rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
- rewrite (associative _) pvs_impl_r pvs_always_r wp_always_r.
+ rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
+ rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
Qed.
@@ -61,7 +61,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Q Q' e :
⊑ {{ P }} K e @ E {{ Q' }}.
Proof.
intros; apply (always_intro' _ _), impl_intro_l.
- rewrite (associative _ P) {1}/ht always_elim impl_elim_r.
+ rewrite (assoc _ P) {1}/ht always_elim impl_elim_r.
rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
by rewrite (forall_elim v) /ht always_elim impl_elim_r.
Qed.
@@ -72,25 +72,25 @@ Lemma ht_frame_l E P Q R e :
{{ P }} e @ E {{ Q }} ⊑ {{ R ★ P }} e @ E {{ λ v, R ★ Q v }}.
Proof.
apply always_intro, impl_intro_l.
- rewrite always_and_sep_r -(associative _) (sep_and P) always_elim impl_elim_r.
+ rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
by rewrite wp_frame_l.
Qed.
Lemma ht_frame_r E P Q R e :
{{ P }} e @ E {{ Q }} ⊑ {{ P ★ R }} e @ E {{ λ v, Q v ★ R }}.
-Proof. setoid_rewrite (commutative _ _ R); apply ht_frame_l. Qed.
+Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
Lemma ht_frame_later_l E P R e Q :
to_val e = None →
{{ P }} e @ E {{ Q }} ⊑ {{ ▷ R ★ P }} e @ E {{ λ v, R ★ Q v }}.
Proof.
intros; apply always_intro, impl_intro_l.
- rewrite always_and_sep_r -(associative _) (sep_and P) always_elim impl_elim_r.
+ rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
by rewrite wp_frame_later_l //; apply wp_mono=>v; rewrite pvs_frame_l.
Qed.
Lemma ht_frame_later_r E P R e Q :
to_val e = None →
{{ P }} e @ E {{ Q }} ⊑ {{ P ★ ▷ R }} e @ E {{ λ v, Q v ★ R }}.
Proof.
- rewrite (commutative _ _ (â–· R)%I); setoid_rewrite (commutative _ _ R).
+ rewrite (comm _ _ (â–· R)%I); setoid_rewrite (comm _ _ R).
apply ht_frame_later_l.
Qed.
End hoare.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index 17d14715a..fd876ea96 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -27,19 +27,19 @@ Lemma ht_lift_step E1 E2
⊑ {{ P }} e1 @ E2 {{ R }}.
Proof.
intros ?? Hsafe Hstep; apply (always_intro' _ _), impl_intro_l.
- rewrite (associative _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
+ rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono.
- rewrite always_and_sep_r' -associative; apply sep_mono; first done.
+ rewrite always_and_sep_r' -assoc; apply sep_mono; first done.
rewrite (later_intro (∀ _, _)) -later_sep; apply later_mono.
apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef).
apply wand_intro_l; rewrite !always_and_sep_l'.
- rewrite (associative _ _ P') -(associative _ _ _ P') associative.
+ rewrite (assoc _ _ P') -(assoc _ _ _ P') assoc.
rewrite {1}/vs -always_wand_impl always_elim wand_elim_r.
rewrite pvs_frame_r; apply pvs_mono.
- rewrite (commutative _ (Q1 _ _ _)) -associative (associative _ (Q1 _ _ _)).
+ rewrite (comm _ (Q1 _ _ _)) -assoc (assoc _ (Q1 _ _ _)).
rewrite {1}/ht -always_wand_impl always_elim wand_elim_r.
- rewrite associative (commutative _ _ (wp _ _ _)) -associative.
+ rewrite assoc (comm _ _ (wp _ _ _)) -assoc.
apply sep_mono; first done.
destruct ef as [e'|]; simpl; [|by apply const_intro].
rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
@@ -63,7 +63,7 @@ Proof.
apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
apply and_intro; [|apply and_intro; [|done]].
* rewrite -vs_impl; apply (always_intro' _ _),impl_intro_l;rewrite and_elim_l.
- rewrite !associative; apply sep_mono; last done.
+ rewrite !assoc; apply sep_mono; last done.
rewrite -!always_and_sep_l' -!always_and_sep_r'; apply const_elim_l=>-[??].
by repeat apply and_intro; try apply const_intro.
* apply (always_intro' _ _), impl_intro_l; rewrite and_elim_l.
@@ -88,12 +88,12 @@ Proof.
apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l.
rewrite (forall_elim e2) (forall_elim ef).
rewrite always_and_sep_l' !always_and_sep_r' {1}(always_sep_dup' (â– _)).
- rewrite {1}(associative _ (_ ★ _)%I) -(associative _ (■_)%I).
- rewrite (associative _ (â– _)%I P) -{1}(commutative _ P) -(associative _ P).
- rewrite (associative _ (■_)%I) associative -(associative _ (■_ ★ P))%I.
- rewrite (commutative _ (■_ ★ P'))%I associative.
+ rewrite {1}(assoc _ (_ ★ _)%I) -(assoc _ (■_)%I).
+ rewrite (assoc _ (â– _)%I P) -{1}(comm _ P) -(assoc _ P).
+ rewrite (assoc _ (■_)%I) assoc -(assoc _ (■_ ★ P))%I.
+ rewrite (comm _ (■_ ★ P'))%I assoc.
rewrite {1}/ht -always_wand_impl always_elim wand_elim_r.
- rewrite -associative; apply sep_mono; first done.
+ rewrite -assoc; apply sep_mono; first done.
destruct ef as [e'|]; simpl; [|by apply const_intro].
rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
by apply const_intro.
@@ -111,11 +111,11 @@ Proof.
rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
apply forall_intro=>e2'; apply forall_intro=>ef'; apply and_mono.
* apply (always_intro' _ _), impl_intro_l.
- rewrite -always_and_sep_l' -associative; apply const_elim_l=>-[??]; subst.
+ rewrite -always_and_sep_l' -assoc; apply const_elim_l=>-[??]; subst.
by rewrite /ht always_elim impl_elim_r.
* destruct ef' as [e'|]; simpl; [|by apply const_intro].
apply (always_intro' _ _), impl_intro_l.
- rewrite -always_and_sep_l' -associative; apply const_elim_l=>-[??]; subst.
+ rewrite -always_and_sep_l' -assoc; apply const_elim_l=>-[??]; subst.
by rewrite /= /ht always_elim impl_elim_r.
Qed.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index f5a2f0994..99961ffb9 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -15,7 +15,7 @@ Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
encode x :: N.
Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
-Instance ndot_injective `{Countable A} : Injective2 (=) (=) (=) (@ndot A _ _).
+Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed.
Lemma nclose_nnil : nclose nnil = coPset_all.
Proof. by apply (sig_eq_pi _). Qed.
@@ -25,7 +25,7 @@ Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x) ⊆ nclose N.
Proof.
intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|].
- by exists (q ++ q')%positive; rewrite <-(associative_L _); f_equal.
+ by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
Qed.
Lemma ndot_nclose `{Countable A} N x : encode (ndot N x) ∈ nclose N.
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
@@ -34,9 +34,9 @@ Lemma nclose_disjoint `{Countable A} N (x y : A) :
Proof.
intros Hxy; apply elem_of_equiv_empty_L=> p; unfold nclose, ndot.
rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]].
- apply Hxy, (injective encode), (injective encode_nat); revert Hq.
+ apply Hxy, (inj encode), (inj encode_nat); revert Hq.
rewrite !(list_encode_cons (encode _)).
- rewrite !(associative_L _) (injective_iff (++ _)%positive) /=.
+ rewrite !(assoc_L _) (inj_iff (++ _)%positive) /=.
generalize (encode_nat (encode y)).
induction (encode_nat (encode x)); intros [|?] ?; f_equal'; naive_solver.
Qed.
@@ -72,16 +72,16 @@ Lemma inv_fsa {A : Type} {FSA} (FSAs : FrameShiftAssertion (A:=A) FSA)
Proof.
move=>HN.
rewrite /inv sep_exist_r. apply exist_elim=>i.
- rewrite always_and_sep_l' -associative. apply const_elim_sep_l=>HiN.
+ rewrite always_and_sep_l' -assoc. apply const_elim_sep_l=>HiN.
rewrite -(fsa_trans3 E (E ∖ {[encode i]})) //; last by solve_elem_of+.
(* Add this to the local context, so that solve_elem_of finds it. *)
assert ({[encode i]} ⊆ nclose N) by eauto.
rewrite (always_sep_dup' (ownI _ _)).
rewrite {1}pvs_openI !pvs_frame_r.
apply pvs_mask_frame_mono ; [solve_elem_of..|].
- rewrite (commutative _ (â–·_)%I) -associative wand_elim_r fsa_frame_l.
+ rewrite (comm _ (â–·_)%I) -assoc wand_elim_r fsa_frame_l.
apply fsa_mask_frame_mono; [solve_elem_of..|]. intros a.
- rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id.
+ rewrite assoc -always_and_sep_l' pvs_closeI pvs_frame_r left_id.
apply pvs_mask_frame'; solve_elem_of.
Qed.
diff --git a/program_logic/language.v b/program_logic/language.v
index 783ac2a73..4b24374ca 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -48,8 +48,8 @@ Section language.
Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
Lemma atomic_of_val v : ¬atomic (of_val v).
Proof. by intros Hat%atomic_not_val; rewrite to_of_val in Hat. Qed.
- Global Instance: Injective (=) (=) (@of_val Λ).
- Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
+ Global Instance: Inj (=) (=) (@of_val Λ).
+ Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
End language.
Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index e72e87a05..91a19e33c 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -31,12 +31,12 @@ Proof.
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 (associative _). }
+ { 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)
as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
{ split. destruct k; try eapply Hstep; eauto. apply ownP_spec; auto. }
- { rewrite (commutative _ r2) -(associative _); eauto using wsat_le. }
+ { rewrite (comm _ r2) -assoc; eauto using wsat_le. }
by exists r1', r2'; split_ands; [| |by intros ? ->].
Qed.
@@ -71,7 +71,7 @@ Proof.
rewrite -pvs_intro. apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'.
apply forall_intro=>ef; apply wand_intro_l.
- rewrite always_and_sep_l' -associative -always_and_sep_l'.
+ rewrite always_and_sep_l' -assoc -always_and_sep_l'.
apply const_elim_l=>-[v2' [Hv ?]] /=.
rewrite -pvs_intro.
rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //.
@@ -90,7 +90,7 @@ Proof.
apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'.
apply wand_intro_l.
- rewrite always_and_sep_l' -associative -always_and_sep_l'.
+ rewrite always_and_sep_l' -assoc -always_and_sep_l'.
apply const_elim_l=>-[-> [-> ->]] /=. by rewrite wand_elim_r.
Qed.
diff --git a/program_logic/model.v b/program_logic/model.v
index dda84c106..42bddbdd2 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -46,8 +46,8 @@ Lemma iProp_unfold_fold {Λ Σ} (P : iPreProp Λ Σ) :
Proof. apply solution_fold_unfold. Qed.
Bind Scope uPred_scope with iProp.
-Instance iProp_fold_inj n Λ Σ : Injective (dist n) (dist n) (@iProp_fold Λ Σ).
+Instance iProp_fold_inj n Λ Σ : Inj (dist n) (dist n) (@iProp_fold Λ Σ).
Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
Instance iProp_unfold_inj n Λ Σ :
- Injective (dist n) (dist n) (@iProp_unfold Λ Σ).
+ Inj (dist n) (dist n) (@iProp_unfold Λ Σ).
Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 2f7de641b..dff05bd9d 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -49,11 +49,11 @@ Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
Proof. by intros m m' Hm; unfold ownG; rewrite Hm. Qed.
Global Instance ownG_proper : Proper ((≡) ==> (≡)) (@ownG Λ Σ) := ne_proper _.
Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ≡ (ownG m1 ★ ownG m2)%I.
-Proof. by rewrite /ownG -uPred.ownM_op Res_op !(left_id _ _). Qed.
+Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
Lemma always_ownG_unit m : (□ ownG (unit m))%I ≡ ownG (unit m).
Proof.
apply uPred.always_ownM.
- by rewrite Res_unit !cmra_unit_empty -{2}(cmra_unit_idempotent m).
+ by rewrite Res_unit !cmra_unit_empty -{2}(cmra_unit_idemp m).
Qed.
Lemma ownG_valid m : (ownG m) ⊑ (✓ m).
Proof. by rewrite /ownG uPred.ownM_valid; apply uPred.valid_mono=> n [? []]. Qed.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 663090b3b..2f576280c 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -20,8 +20,8 @@ Next Obligation.
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.
- exists (r' â‹… r3); rewrite -(associative _); split; last done.
+ 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.
Qed.
Arguments pvs {_ _} _ _ _%I : simpl never.
@@ -68,15 +68,15 @@ 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' σ ???.
- destruct (HP rf k (Ef∪Ef') σ) as (r'&?&?); rewrite ?(associative_L _); eauto.
- by exists r'; rewrite -(associative_L _).
+ 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 σ ???.
destruct (HP (r2 ⋅ rf) k Ef σ) as (r'&?&?); eauto.
- { by rewrite (associative _) -(dist_le _ _ _ _ Hr); last lia. }
- exists (r' â‹… r2); split; last by rewrite -(associative _).
+ { 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.
Qed.
Lemma pvs_openI i P : ownI i P ⊑ pvs {[ i ]} ∅ (▷ P).
@@ -85,13 +85,13 @@ Proof.
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 _ _) -(associative _).
+ exists (rP â‹… r); split; last by rewrite (left_id_L _ _) -assoc.
eapply uPred_weaken with rP (S k); 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|].
- rewrite (left_id _ _); apply wsat_close with P r.
+ rewrite left_id; apply wsat_close with P r.
* apply ownI_spec, uPred_weaken with r (S n); auto.
* solve_elem_of +HE.
* by rewrite -(left_id_L ∅ (∪) Ef).
@@ -135,7 +135,7 @@ Proof. apply pvs_trans; solve_elem_of. Qed.
Lemma pvs_strip_pvs E P Q : P ⊑ pvs E E Q → pvs E E P ⊑ pvs E E Q.
Proof. move=>->. by rewrite pvs_trans'. Qed.
Lemma pvs_frame_l E1 E2 P Q : (P ★ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ★ Q).
-Proof. rewrite !(commutative _ P); apply pvs_frame_r. Qed.
+Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :
(P ∧ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ∧ Q).
Proof. by rewrite !always_and_sep_l' pvs_frame_l. Qed.
@@ -145,7 +145,7 @@ Proof. by rewrite !always_and_sep_r' pvs_frame_r. Qed.
Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ pvs E1 E2 P) ⊑ pvs E1 E2 Q.
Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P ∧ □ (P → Q)) ⊑ pvs E1 E2 Q.
-Proof. by rewrite (commutative _) pvs_impl_l. Qed.
+Proof. by rewrite comm pvs_impl_l. Qed.
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → pvs E1' E2' P ⊑ pvs E1 E2 P.
@@ -206,8 +206,8 @@ Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
Lemma fsa_frame_l E P Q :
(P ★ FSA E Q) ⊑ FSA E (λ a, P ★ Q a).
Proof.
- rewrite commutative fsa_frame_r. apply fsa_mono=>a.
- by rewrite commutative.
+ rewrite comm fsa_frame_r. apply fsa_mono=>a.
+ by rewrite comm.
Qed.
Lemma fsa_strip_pvs E P Q : P ⊑ FSA E Q → pvs E E P ⊑ FSA E Q.
Proof.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index d704106d5..ee5ad3d63 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -102,10 +102,10 @@ Proof.
* by intros n [???] ? [???] [???] ? [???];
constructor; simpl in *; cofe_subst.
* by intros n ? (?&?&?); split_ands'; apply cmra_validN_S.
- * intros ???; constructor; simpl; apply (associative _).
- * intros ??; constructor; simpl; apply (commutative _).
- * intros ?; constructor; simpl; apply cmra_unit_l.
- * intros ?; constructor; simpl; apply cmra_unit_idempotent.
+ * by intros ???; constructor; rewrite /= assoc.
+ * by intros ??; constructor; rewrite /= comm.
+ * by intros ?; constructor; rewrite /= cmra_unit_l.
+ * by intros ?; constructor; rewrite /= cmra_unit_idemp.
* intros n r1 r2; rewrite !res_includedN.
by intros (?&?&?); split_ands'; apply cmra_unit_preservingN.
* intros n r1 r2 (?&?&?);
@@ -127,7 +127,7 @@ Global Instance res_cmra_identity : CMRAIdentity resRA.
Proof.
split.
* intros n; split_ands'; apply cmra_empty_valid.
- * by split; rewrite /= (left_id _ _).
+ * by split; rewrite /= left_id.
* apply _.
Qed.
@@ -150,12 +150,12 @@ 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_idempotent.
+ 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.
Proof.
- rewrite (commutative _ r1) (commutative _ (wld r1)); apply lookup_wld_op_l.
+ rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l.
Qed.
Global Instance Res_timeless eσ m : Timeless m → Timeless (Res ∅ eσ m).
Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 53db3c226..d666a056f 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -24,7 +24,7 @@ Implicit Types P Q R : iProp Λ Σ.
Lemma vs_alt E1 E2 P Q : (P ⊑ pvs E1 E2 Q) → P ={E1,E2}=> Q.
Proof.
intros; rewrite -{1}always_const; apply always_intro, impl_intro_l.
- by rewrite always_const (right_id _ _).
+ by rewrite always_const right_id.
Qed.
Global Instance vs_ne E1 E2 n :
@@ -51,7 +51,7 @@ Lemma vs_transitive E1 E2 E3 P Q R :
E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R)) ⊑ (P ={E1,E3}=> R).
Proof.
intros; rewrite -always_and; apply always_intro, impl_intro_l.
- rewrite always_and (associative _) (always_elim (P → _)) impl_elim_r.
+ rewrite always_and assoc (always_elim (P → _)) impl_elim_r.
by rewrite pvs_impl_r; apply pvs_trans.
Qed.
@@ -69,12 +69,12 @@ Qed.
Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) ⊑ (R ★ P ={E1,E2}=> R ★ Q).
Proof.
apply always_intro, impl_intro_l.
- rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -(associative _).
+ rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -assoc.
by rewrite always_elim wand_elim_r.
Qed.
Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊑ (P ★ R ={E1,E2}=> Q ★ R).
-Proof. rewrite !(commutative _ _ R); apply vs_frame_l. Qed.
+Proof. rewrite !(comm _ _ R); apply vs_frame_l. Qed.
Lemma vs_mask_frame E1 E2 Ef P Q :
Ef ∩ (E1 ∪ E2) = ∅ → (P ={E1,E2}=> Q) ⊑ (P ={E1 ∪ Ef,E2 ∪ Ef}=> Q).
@@ -91,11 +91,11 @@ Lemma vs_open_close N E P Q R :
(inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊑ (P ={E}=> Q).
Proof.
intros; apply (always_intro' _ _), impl_intro_l.
- rewrite always_and_sep_r' associative [(P ★ _)%I]commutative -associative.
+ rewrite always_and_sep_r' assoc [(P ★ _)%I]comm -assoc.
rewrite -(pvs_open_close E N) //. apply sep_mono; first done.
apply wand_intro_l.
(* Oh wow, this is annyoing... *)
- rewrite associative -always_and_sep_r'.
+ rewrite assoc -always_and_sep_r'.
by rewrite /vs always_elim impl_elim_r.
Qed.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 6ceabb531..728a8042f 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -44,10 +44,10 @@ Next Obligation.
* constructor; eauto using uPred_weaken.
* intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???].
destruct (Hgo (rf' ⋅ rf) k Ef σ1) as [Hsafe Hstep];
- rewrite ?associative -?Hr; auto; constructor; [done|].
+ rewrite ?assoc -?Hr; auto; constructor; [done|].
intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
exists r2, (r2' â‹… rf'); split_ands; eauto 10 using (IH k), cmra_included_l.
- by rewrite -!associative (associative _ r2).
+ by rewrite -!assoc (assoc _ r2).
Qed.
Instance: Params (@wp) 4.
@@ -88,7 +88,7 @@ Proof.
{ constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. }
constructor; [done|]=> rf k Ef σ1 ???.
assert (E2 ∪ Ef = E1 ∪ (E2 ∖ E1 ∪ Ef)) as HE'.
- { by rewrite associative_L -union_difference_L. }
+ { by rewrite assoc_L -union_difference_L. }
destruct (Hgo rf k ((E2 ∖ E1) ∪ Ef) σ1) as [Hsafe Hstep]; rewrite -?HE'; auto.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
@@ -141,9 +141,9 @@ Proof.
destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo];
[|destruct (atomic_step e σ1 e2 σ2 ef); naive_solver].
apply pvs_trans in Hvs'; auto.
- destruct (Hvs' (r2' ⋅ rf) k Ef σ2) as (r3&[]); rewrite ?(associative _); auto.
+ destruct (Hvs' (r2' ⋅ rf) k Ef σ2) as (r3&[]); rewrite ?assoc; auto.
exists r3, r2'; split_ands; last done.
- * by rewrite -(associative _).
+ * by rewrite -assoc.
* constructor; apply pvs_intro; auto.
Qed.
Lemma wp_frame_r E e Q R : (wp E e Q ★ R) ⊑ wp E e (λ v, Q v ★ R).
@@ -155,12 +155,12 @@ Proof.
{ constructor; apply pvs_frame_r; auto. exists r, rR; eauto. }
constructor; [done|]=> rf k Ef σ1 ???.
destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep]; auto.
- { by rewrite (associative _). }
+ { by rewrite assoc. }
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
exists (r2 â‹… rR), r2'; split_ands; auto.
- * by rewrite -(associative _ r2)
- (commutative _ rR) !associative -(associative _ _ rR).
+ * by rewrite -(assoc _ r2)
+ (comm _ rR) !assoc -(assoc _ _ rR).
* apply IH; eauto using uPred_weaken.
Qed.
Lemma wp_frame_later_r E e Q R :
@@ -169,12 +169,12 @@ 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|].
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.
+ 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 -(associative _ r2)
- (commutative _ rR) !associative -(associative _ _ 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.
Qed.
@@ -207,11 +207,11 @@ Proof. move=>->. by rewrite pvs_wp. Qed.
Lemma wp_value' E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value. Qed.
Lemma wp_frame_l E e Q R : (R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).
-Proof. setoid_rewrite (commutative _ R); apply wp_frame_r. Qed.
+Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
Lemma wp_frame_later_l E e Q R :
to_val e = None → (▷ R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).
Proof.
- rewrite (commutative _ (â–· R)%I); setoid_rewrite (commutative _ R).
+ rewrite (comm _ (â–· R)%I); setoid_rewrite (comm _ R).
apply wp_frame_later_r.
Qed.
Lemma wp_always_l E e Q R `{!AlwaysStable R} :
@@ -226,7 +226,7 @@ Proof.
by rewrite always_elim (forall_elim v) impl_elim_l.
Qed.
Lemma wp_impl_r E e Q1 Q2 : (wp E e Q1 ∧ □ ∀ v, Q1 v → Q2 v) ⊑ wp E e Q2.
-Proof. by rewrite commutative wp_impl_l. Qed.
+Proof. by rewrite comm wp_impl_l. Qed.
Lemma wp_mask_weaken E1 E2 e Q : E1 ⊆ E2 → wp E1 e Q ⊑ wp E2 e Q.
Proof. auto using wp_mask_frame_mono. Qed.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index d0805d447..7d8db791f 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -49,13 +49,13 @@ Proof.
destruct n as [|n], n' as [|n']; simpl; try by (auto with lia).
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].
+ [apply (inj Some) in HiP|inversion_clear HiP].
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 Next), (injective to_agree).
+ { apply (inj iProp_unfold), (inj Next), (inj 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. }
@@ -83,7 +83,7 @@ Proof.
intros HiP Hi [rs [Hval Hσ HE Hwld]].
destruct (Hwld i P) as (rP&?&?); [solve_elem_of +|by apply lookup_wld_op_l|].
assert (rP ⋅ r ⋅ big_opM (delete i rs) ≡ r ⋅ big_opM rs) as Hr.
- { by rewrite (commutative _ rP) -associative big_opM_delete. }
+ { by rewrite (comm _ rP) -assoc big_opM_delete. }
exists rP; split; [exists (delete i rs); constructor; rewrite ?Hr|]; auto.
* intros j; rewrite lookup_delete_is_Some Hr.
generalize (HE j); solve_elem_of +Hi.
@@ -98,15 +98,14 @@ Proof.
intros HiP HiE [rs [Hval Hσ HE Hwld]] ?.
assert (rs !! i = None) by (apply eq_None_not_Some; naive_solver).
assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
- { by rewrite (commutative _ rP) -associative big_opM_insert. }
+ { by rewrite (comm _ rP) -assoc big_opM_insert. }
exists (<[i:=rP]>rs); constructor; rewrite ?Hr; auto.
* intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst.
+ rewrite !lookup_op HiP !op_is_Some; solve_elem_of -.
+ destruct (HE j) as [Hj Hj']; auto; solve_elem_of +Hj Hj'.
* 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 Next), (injective iProp_unfold) in HP.
+ apply (inj Some), (inj to_agree), (inj Next), (inj 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,13 +116,13 @@ 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 (S n) σ1); rewrite -Hpst_r associative. }
+ { by apply: (excl_validN_inv_l (S n) σ1); rewrite -Hpst_r assoc. }
assert (σ1' = σ1) as ->.
{ apply leibniz_equiv, (timeless _), dist_le with (S n); auto.
- apply (injective Excl).
- by rewrite -Hpst_r -Hpst -associative Hpst' (right_id _). }
+ apply (inj Excl).
+ by rewrite -Hpst_r -Hpst -assoc Hpst' right_id. }
split; [done|exists rs].
- by constructor; split_ands'; try (rewrite /= -associative Hpst').
+ by constructor; split_ands'; try (rewrite /= -assoc Hpst').
Qed.
Lemma wsat_update_gst n E σ r rf mm1 (P : iGst Λ Σ → Prop) :
mm1 ≼{S n} gst r → mm1 ~~>: (λ mm2, default False mm2 P) →
@@ -131,7 +130,7 @@ Lemma wsat_update_gst n E σ r rf mm1 (P : iGst Λ Σ → Prop) :
Proof.
intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
destruct (Hup (mf â‹… gst (rf â‹… big_opM rs)) (S n)) as ([m2|]&?&Hval'); try done.
- { by rewrite /= (associative _ mm1) -Hr associative. }
+ { by rewrite /= (assoc _ mm1) -Hr assoc. }
exists m2; split; [exists rs; split; split_ands'; auto|done].
Qed.
Lemma wsat_alloc n E1 E2 σ r P rP :
@@ -152,22 +151,21 @@ Proof.
{ apply eq_None_not_Some=>?; destruct (HE i) as [_ Hri']; auto; revert Hri'.
rewrite /= !lookup_op !op_is_Some -!not_eq_None_Some; tauto. }
assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
- { by rewrite (commutative _ rP) -associative big_opM_insert. }
+ { by rewrite (comm _ rP) -assoc big_opM_insert. }
exists i; split_ands; [exists (<[i:=rP]>rs); constructor| |]; auto.
- * destruct Hval as (?&?&?); rewrite -associative Hr.
+ * destruct Hval as (?&?&?); rewrite -assoc Hr.
split_ands'; rewrite /= ?left_id; [|eauto|eauto].
intros j; destruct (decide (j = i)) as [->|].
- + by rewrite !lookup_op Hri HrPi Hrsi !(right_id _ _) lookup_singleton.
- + by rewrite lookup_op lookup_singleton_ne // (left_id _ _).
- * by rewrite -associative Hr /= left_id.
- * intros j; rewrite -associative Hr; destruct (decide (j = i)) as [->|].
+ + by rewrite !lookup_op Hri HrPi Hrsi !right_id lookup_singleton.
+ + by rewrite lookup_op lookup_singleton_ne // left_id.
+ * by rewrite -assoc Hr /= left_id.
+ * intros j; rewrite -assoc Hr; destruct (decide (j = i)) as [->|].
+ rewrite /= !lookup_op lookup_singleton !op_is_Some; solve_elem_of +Hi.
+ rewrite lookup_insert_ne //.
rewrite lookup_op lookup_singleton_ne // left_id; eauto.
- * intros j P'; rewrite -associative Hr; destruct (decide (j=i)) as [->|].
+ * intros j P'; rewrite -assoc Hr; destruct (decide (j=i)) as [->|].
+ rewrite /= !lookup_op Hri HrPi Hrsi right_id lookup_singleton=>? HP.
- apply (injective Some), (injective to_agree),
- (injective Next), (injective iProp_unfold) in HP.
+ apply (inj Some), (inj to_agree), (inj Next), (inj 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