Misc updates to the prelude.

theories/ars.v

@@ -170,8 +170,7 @@ Hint Extern 5 (subrelation _ (tc _)) =>
   eapply @tc_once_subrel : typeclass_instances.
 
 Hint Resolve
-  rtc_once rtc_r
-  tc_r
+  rtc_once rtc_r tc_r
   bsteps_once bsteps_r bsteps_refl bsteps_trans : ars.
 
 (** * Theorems on sub relations *)

theories/base.v

@@ -6,7 +6,7 @@ abstract interfaces for ordered structures, collections, and various other data
 structures. *)
 Global Generalizable All Variables.
 Global Set Automatic Coercions Import.
-Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid NArith.
+Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
 
 (** * General *)
 (** The following coercion allows us to use Booleans as propositions. *)
@@ -17,6 +17,7 @@ applied. *)
 Arguments id _ _/.
 Arguments compose _ _ _ _ _ _ /.
 Arguments flip _ _ _ _ _ _/.
+Typeclasses Transparent id compose flip.
 
 (** Change [True] and [False] into notations in order to enable overloading.
 We will use this in the file [assertions] to give [True] and [False] a
@@ -415,10 +416,6 @@ Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
   fold_right delete m l.
 Instance: Params (@delete_list) 3.
 
-Definition insert_consecutive `{Insert nat A M} (i : nat) (l : list A)
-  (m : M) : M := fold_right (λ x f i, <[i:=x]>(f (S i))) (λ _, m) l i.
-Instance: Params (@insert_consecutive) 3.
-
 (** The function [union_with f m1 m2] is supposed to yield the union of [m1]
 and [m2] using the function [f] to combine values of members that are in
 both [m1] and [m2]. *)
@@ -451,6 +448,10 @@ Class Injective {A B} (R : relation A) (S : relation B) (f : A → B) : Prop :=
 Class Injective2 {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.
+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 :=
@@ -475,6 +476,8 @@ Class AntiSymmetric {A} (R S : relation A) : Prop :=
 Arguments irreflexivity {_} _ {_} _ _.
 Arguments injective {_ _ _ _} _ {_} _ _ _.
 Arguments injective2 {_ _ _ _ _ _} _ {_} _ _ _ _ _.
+Arguments cancel {_ _ _} _ _ {_} _.
+Arguments surjective {_ _ _} _ {_} _.
 Arguments idempotent {_ _} _ {_} _.
 Arguments commutative {_ _ _} _ {_} _ _.
 Arguments left_id {_ _} _ _ {_} _.
@@ -486,55 +489,6 @@ Arguments left_distr {_ _} _ _ {_} _ _ _.
 Arguments right_distr {_ _} _ _ {_} _ _ _.
 Arguments anti_symmetric {_ _} _ {_} _ _ _ _.
 
-Lemma impl_transitive (P Q R : Prop) : (P → Q) → (Q → R) → (P → R).
-Proof. tauto. Qed.
-Instance: Commutative (↔) (@eq A).
-Proof. red. intuition. Qed.
-Instance: Commutative (↔) (λ x y, @eq A y x).
-Proof. red. intuition. Qed.
-Instance: Commutative (↔) (↔).
-Proof. red. intuition. Qed.
-Instance: Commutative (↔) (∧).
-Proof. red. intuition. Qed.
-Instance: Associative (↔) (∧).
-Proof. red. intuition. Qed.
-Instance: Idempotent (↔) (∧).
-Proof. red. intuition. Qed.
-Instance: Commutative (↔) (∨).
-Proof. red. intuition. Qed.
-Instance: Associative (↔) (∨).
-Proof. red. intuition. Qed.
-Instance: Idempotent (↔) (∨).
-Proof. red. intuition. Qed.
-Instance: LeftId (↔) True (∧).
-Proof. red. intuition. Qed.
-Instance: RightId (↔) True (∧).
-Proof. red. intuition. Qed.
-Instance: LeftAbsorb (↔) False (∧).
-Proof. red. intuition. Qed.
-Instance: RightAbsorb (↔) False (∧).
-Proof. red. intuition. Qed.
-Instance: LeftId (↔) False (∨).
-Proof. red. intuition. Qed.
-Instance: RightId (↔) False (∨).
-Proof. red. intuition. Qed.
-Instance: LeftAbsorb (↔) True (∨).
-Proof. red. intuition. Qed.
-Instance: RightAbsorb (↔) True (∨).
-Proof. red. intuition. Qed.
-Instance: LeftId (↔) True impl.
-Proof. unfold impl. red. intuition. Qed.
-Instance: RightAbsorb (↔) True impl.
-Proof. unfold impl. red. intuition. Qed.
-Instance: LeftDistr (↔) (∧) (∨).
-Proof. red. intuition. Qed.
-Instance: RightDistr (↔) (∧) (∨).
-Proof. red. intuition. Qed.
-Instance: LeftDistr (↔) (∨) (∧).
-Proof. red. intuition. Qed.
-Instance: RightDistr (↔) (∨) (∧).
-Proof. red. intuition. 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. *)
@@ -696,11 +650,9 @@ Notation "x .½" := (half x) (at level 20, format "x .½") : C_scope.
 Lemma proj1_sig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) :
   x↾Px = y↾Py → x = y.
 Proof. injection 1; trivial. Qed.
-Lemma not_symmetry `{R : relation A} `{!Symmetric R} (x y : A) :
-  ¬R x y → ¬R y x.
+Lemma not_symmetry `{R : relation A} `{!Symmetric R} x y : ¬R x y → ¬R y x.
 Proof. intuition. Qed.
-Lemma symmetry_iff `(R : relation A) `{!Symmetric R} (x y : A) :
-  R x y ↔ R y x.
+Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y ↔ R y x.
 Proof. intuition. Qed.
 
 (** ** Pointwise relations *)
@@ -765,11 +717,15 @@ Section prod_relation.
 End prod_relation.
 
 (** ** Other *)
-Definition proj_relation {A B} (R : relation A)
-  (f : B → A) : relation B := λ x y, R (f x) (f y).
-Definition proj_relation_equivalence {A B} (R : relation A) (f : B → A) :
-  Equivalence R → Equivalence (proj_relation R f).
-Proof. unfold proj_relation. firstorder auto. Qed.
+Definition proj_eq {A B} (f : B → A) : relation B := λ x y, f x = f y.
+Global Instance proj_eq_equivalence `(f : B → A) : Equivalence (proj_eq f).
+Proof. unfold proj_eq. repeat split; red; intuition congruence. Qed.
+Notation "x ~{ f } y" := (proj_eq f x y)
+  (at level 70, format "x  ~{ f }  y") : C_scope.
+Notation "(~{ f } )" := (proj_eq f) (f at level 10, only parsing) : C_scope.
+
+Hint Extern 0 (_ ~{_} _) => reflexivity.
+Hint Extern 0 (_ ~{_} _) => symmetry; assumption.
 
 Instance: ∀ A B (x : B), Commutative (=) (λ _ _ : A, x).
 Proof. red. trivial. Qed.
@@ -799,3 +755,96 @@ Proof. red. trivial. Qed.
 Instance idem_propholds {A} (R : relation A) f :
   Idempotent R f → ∀ x, PropHolds (R (f x x) x).
 Proof. red. trivial. 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.
+Proof. firstorder. Qed.
+Instance: Injective (=) (=) (@inl A B).
+Proof. injection 1; auto. Qed.
+Instance: Injective (=) (=) (@inr A B).
+Proof. injection 1; auto. Qed.
+Instance: Injective2 (=) (=) (=) (@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.
+
+Lemma cancel_injective `{Cancel A B R1 f g}
+  `{!Equivalence R1} `{!Proper (R2 ==> R1) f} : Injective 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.
+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).
+Proof. red. intuition. Qed.
+Instance: Commutative (↔) (λ x y, @eq A y x).
+Proof. red. intuition. Qed.
+Instance: Commutative (↔) (↔).
+Proof. red. intuition. Qed.
+Instance: Commutative (↔) (∧).
+Proof. red. intuition. Qed.
+Instance: Associative (↔) (∧).
+Proof. red. intuition. Qed.
+Instance: Idempotent (↔) (∧).
+Proof. red. intuition. Qed.
+Instance: Commutative (↔) (∨).
+Proof. red. intuition. Qed.
+Instance: Associative (↔) (∨).
+Proof. red. intuition. Qed.
+Instance: Idempotent (↔) (∨).
+Proof. red. intuition. Qed.
+Instance: LeftId (↔) True (∧).
+Proof. red. intuition. Qed.
+Instance: RightId (↔) True (∧).
+Proof. red. intuition. Qed.
+Instance: LeftAbsorb (↔) False (∧).
+Proof. red. intuition. Qed.
+Instance: RightAbsorb (↔) False (∧).
+Proof. red. intuition. Qed.
+Instance: LeftId (↔) False (∨).
+Proof. red. intuition. Qed.
+Instance: RightId (↔) False (∨).
+Proof. red. intuition. Qed.
+Instance: LeftAbsorb (↔) True (∨).
+Proof. red. intuition. Qed.
+Instance: RightAbsorb (↔) True (∨).
+Proof. red. intuition. Qed.
+Instance: LeftId (↔) True impl.
+Proof. unfold impl. red. intuition. Qed.
+Instance: RightAbsorb (↔) True impl.
+Proof. unfold impl. red. intuition. Qed.
+Instance: LeftDistr (↔) (∧) (∨).
+Proof. red. intuition. Qed.
+Instance: RightDistr (↔) (∧) (∨).
+Proof. red. intuition. Qed.
+Instance: LeftDistr (↔) (∨) (∧).
+Proof. red. intuition. Qed.
+Instance: RightDistr (↔) (∨) (∧).
+Proof. red. intuition. Qed.
+Lemma not_injective `{Injective 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).
+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).
+Proof.
+  intros ?? x. unfold compose. destruct (surjective g x) as [y ?].
+  destruct (surjective 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.
+  Proof.
+    intros ?? [x Hx] [y Hy]. injection 1. intros Hxy.
+    apply (injective f) in Hxy; subst. rewrite (proof_irrel _ Hy). auto.
+  Qed.
+End sig_map.

theories/collections.v

@@ -489,7 +489,7 @@ Section collection_monad.
     * revert l. induction k; esolve_elem_of.
     * induction 1; esolve_elem_of.
   Qed.
-  Lemma mapM_length {A B} (f : A → M B) l k :
+  Lemma collection_mapM_length {A B} (f : A → M B) l k :
     l ∈ mapM f k → length l = length k.
   Proof. revert l; induction k; esolve_elem_of. Qed.
 

theories/fin_collections.v

@@ -3,10 +3,11 @@
 (** This file collects definitions and theorems on finite collections. Most
 importantly, it implements a fold and size function and some useful induction
 principles on finite collections . *)
-Require Import Permutation ars.
-Require Export collections numbers listset.
+Require Import Permutation ars listset.
+Require Export numbers collections.
 
-Definition choose `{Elements A C} (X : C) : option A := head (elements X).
+Definition collection_choose `{Elements A C} (X : C) : option A :=
+  head (elements X).
 Instance collection_size `{Elements A C} : Size C := length ∘ elements.
 Definition collection_fold `{Elements A C} {B}
   (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
@@ -56,23 +57,27 @@ Proof.
   rewrite (nil_length l), !elem_of_list_singleton by done. congruence.
 Qed.
 
-Lemma choose_Some X x : choose X = Some x → x ∈ X.
+Lemma collection_choose_Some X x : collection_choose X = Some x → x ∈ X.
 Proof.
-  unfold choose. destruct (elements X) eqn:E; intros; simplify_equality.
-  rewrite elements_spec, E. by left.
+  unfold collection_choose. destruct (elements X) eqn:E; intros;
+    simplify_equality. rewrite elements_spec, E. by left.
 Qed.
-Lemma choose_None X : choose X = None → X ≡ ∅.
+Lemma collection_choose_None X : collection_choose X = None → X ≡ ∅.
 Proof.
-  unfold choose. destruct (elements X) eqn:E; intros; simplify_equality.
+  unfold collection_choose.
+  destruct (elements X) eqn:E; intros; simplify_equality.
   apply equiv_empty. intros x. by rewrite elements_spec, E, elem_of_nil.
 Qed.
 Lemma elem_of_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
-Proof. destruct (choose X) eqn:?; eauto using choose_Some, choose_None. Qed.
-Lemma choose_is_Some X : X ≢ ∅ ↔ is_Some (choose X).
 Proof.
-  destruct (choose X) eqn:?.
-  * rewrite elem_of_equiv_empty. split; eauto using choose_Some.
-  * split. intros []; eauto using choose_None. by intros [??].
+  destruct (collection_choose X) eqn:?;
+    eauto using collection_choose_Some, collection_choose_None.
+Qed.
+Lemma collection_choose_is_Some X : X ≢ ∅ ↔ is_Some (collection_choose X).
+Proof.
+  destruct (collection_choose X) eqn:?.
+  * rewrite elem_of_equiv_empty. split; eauto using collection_choose_Some.
+  * split. intros []; eauto using collection_choose_None. by intros [??].
 Qed.
 Lemma not_elem_of_equiv_empty X : X ≢ ∅ ↔ (∃ x, x ∈ X).
 Proof.
@@ -156,8 +161,7 @@ Qed.
 
 Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
   Proper ((=) ==> (≡) ==> iff) P →
-  P b ∅ →
-  (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
+  P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
   ∀ X, P (collection_fold f b X) X.
 Proof.
   intros ? Hemp Hadd.
@@ -184,7 +188,6 @@ Proof.
     abstract (unfold set_Forall; setoid_rewrite elements_spec;
       by rewrite <-Forall_forall).
 Defined.
-
 Global Instance set_Exists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X :
   Decision (set_Exists P X) | 100.
 Proof.
@@ -192,7 +195,6 @@ Proof.
     abstract (unfold set_Exists; setoid_rewrite elements_spec;
       by rewrite <-Exists_exists).
 Defined.
-
 Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X :
   Decision (elem_of_upto R x X) | 100 := decide (set_Exists (R x) X).
 End fin_collection.

theories/fin_maps.v

@@ -135,14 +135,21 @@ Lemma map_subset_empty {A} (m : M A) : m ⊄ ∅.
 Proof. intros [? []]. intros i x. by rewrite lookup_empty. Qed.
 
 (** ** Properties of the [partial_alter] operation *)
-Lemma partial_alter_compose {A} (m : M A) i f g :
+Lemma partial_alter_ext {A} (f g : option A → option A) (m : M A) i :
+  (∀ x, m !! i = x → f x = g x) → partial_alter f i m = partial_alter g i m.
+Proof.
+  intros Hfg. apply map_eq. intros j. destruct (decide (i = j)); subst.
+  * rewrite !lookup_partial_alter. by apply Hfg.
+  * by rewrite !lookup_partial_alter_ne.
+Qed.
+Lemma partial_alter_compose {A} f g (m : M A) i:
   partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m).
 Proof.
   intros. apply map_eq. intros ii. case (decide (i = ii)).
   * intros. subst. by rewrite !lookup_partial_alter.
   * intros. by rewrite !lookup_partial_alter_ne.
 Qed.
-Lemma partial_alter_commute {A} (m : M A) i j f g :
+Lemma partial_alter_commute {A} f g (m : M A) i j :
   i ≠ j → partial_alter f i (partial_alter g j m) =
     partial_alter g j (partial_alter f i m).
 Proof.
@@ -164,10 +171,10 @@ Qed.
 Lemma partial_alter_self {A} (m : M A) i : partial_alter (λ _, m !! i) i m = m.
 Proof. by apply partial_alter_self_alt. Qed.
 
-Lemma partial_alter_subseteq {A} (m : M A) i f :
+Lemma partial_alter_subseteq {A} f (m : M A) i :
   m !! i = None → m ⊆ partial_alter f i m.
 Proof. intros Hi j x Hj. rewrite lookup_partial_alter_ne; congruence. Qed.
-Lemma partial_alter_subset {A} (m : M A) i f :
+Lemma partial_alter_subset {A} f (m : M A) i :
   m !! i = None → is_Some (f (m !! i)) → m ⊂ partial_alter f i m.
 Proof.
   intros Hi Hfi. split.
@@ -178,11 +185,26 @@ Proof.
 Qed.
 
 (** ** Properties of the [alter] operation *)
+Lemma alter_ext {A} (f g : A → A) (m : M A) i :
+  (∀ x, m !! i = Some x → f x = g x) → alter f i m = alter g i m.
+Proof. intro. apply partial_alter_ext. intros [x|] ?; simpl; f_equal; auto. Qed.
+
 Lemma lookup_alter {A} (f : A → A) m i : alter f i m !! i = f <$> m !! i.
 Proof. apply lookup_partial_alter. Qed.
 Lemma lookup_alter_ne {A} (f : A → A) m i j : i ≠ j → alter f i m !! j = m !! j.
 Proof. apply lookup_partial_alter_ne. Qed.
 
+Lemma alter_compose {A} (f g : A → A) (m : M A) i:
+  alter (f ∘ g) i m = alter f i (alter g i m).
+Proof.
+  unfold alter, map_alter. rewrite <-partial_alter_compose.
+  apply partial_alter_ext. by intros [?|].
+Qed.
+
+Lemma alter_commute {A} (f g : A → A) (m : M A) i j :
+  i ≠ j → alter f i (alter g j m) = alter g j (alter f i m).
+Proof. apply partial_alter_commute. Qed.
+
 Lemma lookup_alter_Some {A} (f : A → A) m i j y :
   alter f i m !! j = Some y ↔
     (i = j ∧ ∃ x, m !! j = Some x ∧ y = f x) ∨ (i ≠ j ∧ m !! j = Some y).
@@ -456,7 +478,7 @@ Lemma map_of_list_inj {A} (l1 l2 : list (K * A)) :
   NoDup (fst <$> l1) → NoDup (fst <$> l2) →
   map_of_list l1 = map_of_list l2 → l1 ≡ₚ l2.
 Proof.
-  intros ?? Hl1l2. apply NoDup_Permutation; auto using (NoDup_fmap_1 fst).
+  intros ?? Hl1l2. apply NoDup_Permutation; auto using (fmap_nodup_1 fst).
   intros [i x]. by rewrite !elem_of_map_of_list, Hl1l2.
 Qed.
 Lemma map_of_to_list {A} (m : M A) : map_of_list (map_to_list m) = m.

theories/mapset.v

@@ -54,8 +54,9 @@ Proof.
     destruct (m1 !! x) as [[]|]; tauto.
   * unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
     intros [m1] [m2] ?. simpl. rewrite lookup_intersection_Some.
-    setoid_replace (is_Some (m2 !! x)) with (m2 !! x = Some ()); [done |].
-    split; eauto. by intros [[] ?].
+    assert (is_Some (m2 !! x) ↔ m2 !! x = Some ()).
+    { split; eauto. by intros [[] ?]. }
+    naive_solver.
   * unfold difference, elem_of, mapset_difference, mapset_elem_of.
     intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
     destruct (m2 !! x) as [[]|]; intuition congruence.

theories/natmap.v

@@ -170,14 +170,15 @@ Proof.
     induction l as [|[y|] l IH]; intros i j ?; simpl.
     + done.
     + destruct i as [|i]; simplify_equality; [left|].
-      right. rewrite NPeano.Nat.add_succ_comm. by apply (IH i (S j)).
+      right. rewrite Nat.add_succ_comm. by apply (IH i (S j)).
     + destruct i as [|i]; simplify_equality.
-      rewrite NPeano.Nat.add_succ_comm. by apply (IH i (S j)).
+      rewrite Nat.add_succ_comm. by apply (IH i (S j)).
 Qed.
 Lemma natmap_elem_of_to_list_raw {A} (l : natmap_raw A) i x :
   (i,x) ∈ natmap_to_list_raw 0 l ↔ mjoin (l !! i) = Some x.
 Proof.
-  rewrite natmap_elem_of_to_list_raw_aux. setoid_rewrite plus_0_r. naive_solver.
+  rewrite natmap_elem_of_to_list_raw_aux. setoid_rewrite Nat.add_0_r.
+  naive_solver.
 Qed.
 Lemma natmap_to_list_raw_nodup {A} i (l : natmap_raw A) :
   NoDup (natmap_to_list_raw i l).

theories/nmap.v

@@ -58,8 +58,8 @@ Proof.
   * intros ? [[x|] t]; unfold map_to_list; simpl.
     + constructor.
       - rewrite elem_of_list_fmap. by intros [[??] [??]].
-      - rewrite (NoDup_fmap _). apply map_to_list_nodup.
-    + rewrite (NoDup_fmap _). apply map_to_list_nodup.
+      - apply (fmap_nodup _), map_to_list_nodup.
+    + apply (fmap_nodup _), map_to_list_nodup.
   * intros ? t i x. unfold map_to_list. split.
     + destruct t as [[y|] t]; simpl.
       - rewrite elem_of_cons, elem_of_list_fmap.

theories/numbers.v

@@ -3,7 +3,7 @@
 (** This file collects some trivial facts on the Coq types [nat] and [N] for
 natural numbers, and the type [Z] for integers. It also declares some useful
 notations. *)
-Require Export Eqdep PArith NArith ZArith.
+Require Export Eqdep PArith NArith ZArith NPeano.
 Require Import Qcanon.
 Require Export base decidable.
 Open Scope nat_scope.
@@ -31,6 +31,10 @@ 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.
+Proof. by injection 1. Qed.
+Instance: PartialOrder (≤).
+Proof. repeat split; repeat intro; auto with lia. Qed.
 
 Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
 Proof.
@@ -38,8 +42,8 @@ Proof.
     y = y' → eq_dep nat (le x) y p y' q) as aux.
   { fix 3. intros x ? [|y p] ? [|y' q].
     * done.
-    * clear nat_le_pi. omega.
-    * clear nat_le_pi. omega.
+    * clear nat_le_pi. intros; exfalso; auto with lia.
+    * clear nat_le_pi. intros; exfalso; auto with lia.
     * injection 1. intros Hy. by case (nat_le_pi x y p y' q Hy). }
   intros x y p q.
   by apply (eq_dep_eq_dec (λ x y, decide (x = y))), aux.
@@ -47,11 +51,6 @@ Qed.
 Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y).
 Proof. apply _. Qed.
 
-Lemma lt_n_SS n : n < S (S n).
-Proof. auto with arith. Qed.
-Lemma lt_n_SSS n : n < S (S (S n)).
-Proof. auto with arith. Qed.
-
 Definition sum_list_with {A} (f : A → nat) : list A → nat :=
   fix go l :=
   match l with
@@ -60,23 +59,35 @@ Definition sum_list_with {A} (f : A → nat) : list A → nat :=
   end.
 Notation sum_list := (sum_list_with id).
 
-Lemma mult_split_eq n x1 x2 y1 y2 :
+Lemma Nat_lt_succ_succ n : n < S (S n).
+Proof. auto with arith. Qed.
+Lemma Nat_mul_split_l n x1 x2 y1 y2 :
   x2 < n → y2 < n → x1 * n + x2 = y1 * n + y2 → x1 = y1 ∧ x2 = y2.
 Proof.
-  intros Hx2 Hy2 E.
-  cut (x1 = y1); [intros; subst;lia |].
+  intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |].
   revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia.
 Qed.
+Lemma Nat_mul_split_r n x1 x2 y1 y2 :
+  x1 < n → y1 < n → x1 + x2 * n = y1 + y2 * n → x1 = y1 ∧ x2 = y2.
+Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
 
 (** * Notations and properties of [positive] *)
 Open Scope positive_scope.
 
-Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec.
-Instance positive_inhabited: Inhabited positive := populate 1.
-
+Infix "≤" := Pos.le : positive_scope.
+Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%positive : positive_scope.
+Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%positive : positive_scope.
+Notation "x < y < z" := (x < y ∧ y < z)%positive : positive_scope.
+Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%positive : positive_scope.
+Notation "(≤)" := Pos.le (only parsing) : positive_scope.
+Notation "(<)" := Pos.lt (only parsing) : positive_scope.
 Notation "(~0)" := xO (only parsing) : positive_scope.
 Notation "(~1)" := xI (only parsing) : positive_scope.
 
+Arguments Pos.of_nat _ : simpl never.
+Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec.
+Instance positive_inhabited: Inhabited positive := populate 1.
+
 Instance: Injective (=) (=) (~0).
 Proof. by injection 1. Qed.
 Instance: Injective (=) (=) (~1).
@@ -178,11 +189,13 @@ Next Obligation. congruence. Qed.
 Instance N_inhabited: Inhabited N := populate 1%N.
 
 (** * Notations and properties of [Z] *)
+Open Scope Z_scope.
+
 Infix "≤" := Z.le : Z_scope.
-Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%Z : Z_scope.
-Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%Z : Z_scope.
-Notation "x < y < z" := (x < y ∧ y < z)%Z : Z_scope.
-Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%Z : Z_scope.
+Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z) : Z_scope.
+Notation "x ≤ y < z" := (x ≤ y ∧ y < z) : Z_scope.
+Notation "x < y < z" := (x < y ∧ y < z) : Z_scope.
+Notation "x < y ≤ z" := (x < y ∧ y ≤ z) : Z_scope.
 Notation "(≤)" := Z.le (only parsing) : Z_scope.
 Notation "(<)" := Z.lt (only parsing) : Z_scope.
 
@@ -190,14 +203,28 @@ Infix "`div`" := Z.div (at level 35) : Z_scope.
 Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
 Infix "`quot`" := Z.quot (at level 35) : Z_scope.
 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 Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
-Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y)%Z := Z_le_dec.
-Instance Z_lt_dec: ∀ x y : Z, Decision (x < y)%Z := Z_lt_dec.
-Instance Z_inhabited: Inhabited Z := populate 1%Z.
+Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y) := Z_le_dec.
+Instance Z_lt_dec: ∀ x y : Z, Decision (x < y) := Z_lt_dec.
+Instance Z_inhabited: Inhabited Z := populate 1.
+
+Lemma Z_pow_pred_r n m : 0 < m → n * n ^ (Z.pred m) = n ^ m.
+Proof.
+  intros. rewrite <-Z.pow_succ_r, Z.succ_pred. done. by apply Z.lt_le_pred.
+Qed.
+Lemma Z_quot_range_nonneg k x y : 0 ≤ x < k → 0 < y → 0 ≤ x `quot` y < k.
+Proof.
+  intros [??] ?.
+  destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |].
+  destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |].
+  split. apply Z.quot_pos; lia. transitivity x; auto. apply Z.quot_lt; lia.
+Qed.
 
 (* Note that we cannot disable simpl for [Z.of_nat] as that would break
-[omega] and [lia]. *)
+tactics as [lia]. *)
 Arguments Z.to_nat _ : simpl never.
 Arguments Z.mul _ _ : simpl never.
 Arguments Z.add _ _ : simpl never.
@@ -208,16 +235,41 @@ Arguments Z.modulo _ _ : simpl never.
 Arguments Z.quot _ _ : simpl never.
 Arguments Z.rem _ _ : simpl never.
 
-Lemma Zmod_pos a b : (0 < b)%Z → (0 ≤ a `mod` b)%Z.
+Lemma Z_mod_pos a b : 0 < b → 0 ≤ a `mod` b.
 Proof. apply Z.mod_pos_bound. Qed.
 
 Hint Resolve Z.lt_le_incl : zpos.
 Hint Resolve Z.add_nonneg_pos Z.add_pos_nonneg Z.add_nonneg_nonneg : zpos.
 Hint Resolve Z.mul_nonneg_nonneg Z.mul_pos_pos : zpos.
-Hint Resolve Z.pow_pos_nonneg : zpos.
-Hint Resolve Zmod_pos Z.div_pos : zpos.
+Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
+Hint Resolve Z_mod_pos Z.div_pos : zpos.
 Hint Extern 1000 => lia : zpos.
 
+Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y.
+Proof.
+  induction y as [|y IH].
+  * by rewrite Z.pow_0_r, Nat.pow_0_r.
+  * by rewrite Nat.pow_succ_r, Nat2Z.inj_succ, Z.pow_succ_r,