From fd68e9d37164871cdcb4ee83ab649c5054b0f1cc Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 6 Jun 2021 19:24:10 +0200
Subject: More lemmas about list append

---
 lib/Coqlib.v | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

(limited to 'lib/Coqlib.v')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 1e93b91d..361ae924 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -773,6 +773,32 @@ Proof.
   exists (a0 :: l1); exists l2; intuition. simpl; congruence.
 Qed.
 
+(** Properties of [List.app] (concatenation) *)
+
+Lemma list_append_injective_l:
+  forall (A: Type) (l1 l2 l1' l2': list A),
+  l1 ++ l2 = l1' ++ l2' -> List.length l1 = List.length l1' -> l1 = l1' /\ l2 = l2'.
+Proof.
+  intros until l2'. revert l1 l1'. induction l1 as [ | a l1]; destruct l1' as [ | a' l1']; simpl; intros.
+- auto.
+- discriminate.
+- discriminate.
+- destruct (IHl1 l1'). congruence. congruence. split; congruence.
+Qed.
+
+Lemma list_append_injective_r:
+  forall (A: Type) (l1 l2 l1' l2': list A),
+  l1 ++ l2 = l1' ++ l2' -> List.length l2 = List.length l2' -> l1 = l1' /\ l2 = l2'.
+Proof.
+  intros.
+  assert (X: rev l2 = rev l2' /\ rev l1 = rev l1').
+  { apply list_append_injective_l.
+    rewrite <- ! rev_app_distr. congruence.
+    rewrite ! rev_length; auto. }
+  rewrite <- (rev_involutive l1), <- (rev_involutive l1'), <- (rev_involutive l2), <- (rev_involutive l2').
+  intuition congruence.
+Qed.
+
 (** Folding a function over a list *)
 
 Section LIST_FOLD.
-- 
cgit 


From 88589fa168a0b73f7d82c4ad2dcf9fde9d17f439 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 7 Jun 2021 11:27:44 +0200
Subject: More lemmas about `align`

---
 lib/Coqlib.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'lib/Coqlib.v')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 361ae924..706a5d49 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -525,6 +525,23 @@ Proof.
   intros. unfold align. apply Z.divide_factor_r.
 Qed.
 
+Lemma align_lt: forall x y, y > 0 -> align x y < x + y.
+Proof.
+  intros. unfold align.
+  generalize (Z_div_mod_eq (x + y - 1) y H); intro.
+  generalize (Z_mod_lt (x + y - 1) y H); intro.
+  lia.
+Qed.
+
+Lemma align_same:
+  forall x y, y > 0 -> (y | x) -> align x y = x.
+Proof.
+  unfold align; intros. destruct H0 as [k E].
+  replace (x  + y - 1) with (x + (y - 1)) by lia.
+  rewrite E, Z.div_add_l, Z.div_small by lia.
+  lia.
+Qed.
+
 (** * Definitions and theorems on the data types [option], [sum] and [list] *)
 
 Set Implicit Arguments.
-- 
cgit 


From 4fe221a26400fcf1aaca74889afffa5d01897b13 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 26 Jul 2021 11:39:36 +0200
Subject: Add `floor` and some properties

---
 lib/Coqlib.v | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

(limited to 'lib/Coqlib.v')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 706a5d49..c023bdd5 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -542,6 +542,43 @@ Proof.
   lia.
 Qed.
 
+(** Floor: [floor n amount] returns the greatest multiple of [amount]
+    less than or equal to [n]. *)
+
+Definition floor (n: Z) (amount: Z) := (n / amount) * amount.
+
+Lemma floor_interval:
+  forall x y, y > 0 -> floor x y <= x < floor x y + y.
+Proof.
+  unfold floor; intros.
+  generalize (Z_div_mod_eq x y H) (Z_mod_lt x y H).
+  set (q := x / y). set (r := x mod y). intros. lia.
+Qed.
+
+Lemma floor_divides:
+  forall x y, y > 0 -> (y | floor x y).
+Proof.
+  unfold floor; intros. exists (x / y); auto.
+Qed.
+
+Lemma floor_same:
+  forall x y, y > 0 -> (y | x) -> floor x y = x.
+Proof.
+  unfold floor; intros. rewrite (Zdivide_Zdiv_eq y x) at 2; auto; lia.
+Qed.
+
+Lemma floor_align_interval:
+  forall x y, y > 0 ->
+  floor x y <= align x y <= floor x y + y.
+Proof.
+  unfold floor, align; intros.
+  replace (x / y * y + y) with ((x + 1 * y) / y * y).
+  assert (A: forall a b, a <= b -> a / y * y <= b / y * y).
+  { intros. apply Z.mul_le_mono_nonneg_r. lia. apply Z.div_le_mono; lia. }
+  split; apply A; lia.
+  rewrite Z.div_add by lia. lia.
+Qed.
+
 (** * Definitions and theorems on the data types [option], [sum] and [list] *)
 
 Set Implicit Arguments.
-- 
cgit 


From c9fad7cd7bdc4e79fb06a1d39abfa0d5471623e5 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavierleroy@users.noreply.github.com>
Date: Wed, 15 Sep 2021 14:00:41 +0200
Subject: Avoid `Global Set Asymmetric Patterns` (#408)

Instead, add `Set Asymmetric Patterns` to the files that need it,
or use `Arguments` to make inductive types work better with symmetric patterns.

Closes: #403
---
 lib/Coqlib.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'lib/Coqlib.v')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index c023bdd5..045fb03a 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -25,8 +25,6 @@ Require Export List.
 Require Export Bool.
 Require Export Lia.
 
-Global Set Asymmetric Patterns.
-
 (** * Useful tactics *)
 
 Ltac inv H := inversion H; clear H; subst.
-- 
cgit