diff --git a/theories/base.v b/theories/base.v index 82a05497e9f4bec84769bf699127e6d1c4d78c13..3f30a1122c5cd19255ebdd8cf3bb02011c9e0252 100644 --- a/theories/base.v +++ b/theories/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/theories/countable.v b/theories/countable.v index ab860ddf677228e3cf49060c021ffab5fa1e61db..1635bac2995c67b00ab1cde29730f0d63e4f2d62 100644 --- a/theories/countable.v +++ b/theories/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/theories/decidable.v b/theories/decidable.v index 184372c8bf37317d0d2e82ca40da4ae3a3ed1f6c..817357de205b1063d3b2454c72a9a5b4d2fcb5c6 100644 --- a/theories/decidable.v +++ b/theories/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/theories/error.v b/theories/error.v index 0eb6c33f51b4baaf128cacc1fb15a47c210c6fd3..b2eb18522711f044d7ffeed32bc2d86f4860b10b 100644 --- a/theories/error.v +++ b/theories/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/theories/fin_collections.v b/theories/fin_collections.v index 2f7a573d0ed171de1a6fcfe86a5c92cb5ccf5b1d..7fe2529002d66e54dfd9ef5eb0d1376fc485a107 100644 --- a/theories/fin_collections.v +++ b/theories/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/theories/fin_maps.v b/theories/fin_maps.v index 09c65cdad1dafa8551775965b2daa890b07266d9..9ed4f6986413411e56105cccc07f146e53852ce0 100644 --- a/theories/fin_maps.v +++ b/theories/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/theories/finite.v b/theories/finite.v index 76006bf3a8d8596ce3256f95c0e0271f7e8e5cad..a529a1a040d7aeedf44ac7736e61a18ef337a88d 100644 --- a/theories/finite.v +++ b/theories/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/theories/gmap.v b/theories/gmap.v index 1c2cd5ec7865d8fb95e8b64bfb27d7443543f975..a3466c307cd76edcf60291c4f6e04c7eee7bf1a3 100644 --- a/theories/gmap.v +++ b/theories/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/theories/list.v b/theories/list.v index ef167dc392dd8dbcd7307416bb4e333f26e57bc4..d0e0eafb0b74e606bcc6a212063f8e12f481c750 100644 --- a/theories/list.v +++ b/theories/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/theories/numbers.v b/theories/numbers.v index 65b9621e9377f9720ca2ba31bcf158a03ac2c302..e2e728b3ffc7c56126783c42c4033561dcdb1115 100644 --- a/theories/numbers.v +++ b/theories/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/theories/option.v b/theories/option.v index 4a28e666c318c4464495435fbf43429ec9e50149..f6e217602c1ec45725c6192d87cfd5c5d4f18f1e 100644 --- a/theories/option.v +++ b/theories/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/theories/orders.v b/theories/orders.v index 0dd57462b40c49e54521da8409918aac0cab8397..2203764820e562bfe45d07183b24bd03b5003f2f 100644 --- a/theories/orders.v +++ b/theories/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/theories/pmap.v b/theories/pmap.v index ec91cd490a96c06daf0604f7c7ef86f2e850d07f..00cd7e874b9352e3c70555374a3070de2a2c2b14 100644 --- a/theories/pmap.v +++ b/theories/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/theories/pretty.v b/theories/pretty.v index dbd0311de05aea0cfe6c1f044dc6ad51081db88a..b246ec428a2cfb16d918d51ed796d59efc90e10b 100644 --- a/theories/pretty.v +++ b/theories/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/theories/strings.v b/theories/strings.v index fd41ea2dee75363cae661bdb916fdc8aa5fe871d..f2074f2488ae2cd40f474b2d1beca5c45efd0236 100644 --- a/theories/strings.v +++ b/theories/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/theories/tactics.v b/theories/tactics.v index 8a0551fb89a73076b660765f8e0069dca927cd15..357f4fbde4633748810a9bcf6c4982add7b316d9 100644 --- a/theories/tactics.v +++ b/theories/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/theories/vector.v b/theories/vector.v index da77f8fd936010db1d0f13fb1ec49117126231e1..4b11efe4a387abef0b512d38a160589da779b483 100644 --- a/theories/vector.v +++ b/theories/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.