From 4492d5a5a42a5c0082d5e641856c6e9ac8b83b4e Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Wed, 26 May 2021 15:14:28 +0200
Subject: [PATCH] Add a few lemmas

---
 theories/fin_maps.v     |  8 ++++++++
 theories/list_numbers.v | 25 ++++++++++++++++++++++---
 theories/numbers.v      |  5 +++++
 3 files changed, 35 insertions(+), 3 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 45a0cc67..a445bc4f 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1449,6 +1449,11 @@ Section map_Forall.
     naive_solver eauto using map_Forall_insert_1_1,
       map_Forall_insert_1_2, map_Forall_insert_2.
   Qed.
+  Lemma map_Forall_singleton (i : K) (x : A) :
+    map_Forall P ({[i := x]} : M A) ↔ P i x.
+  Proof.
+    unfold map_Forall. setoid_rewrite lookup_singleton_Some. naive_solver.
+  Qed.
   Lemma map_Forall_delete m i : map_Forall P m → map_Forall P (delete i m).
   Proof. intros Hm j x; rewrite lookup_delete_Some. naive_solver. Qed.
   Lemma map_Forall_lookup m :
@@ -1629,6 +1634,9 @@ Lemma map_lookup_zip_with_Some {A B C} (f : A → B → C) (m1 : M A) (m2 : M B)
   map_zip_with f m1 m2 !! i = Some z ↔
     ∃ x y, z = f x y ∧ m1 !! i = Some x ∧ m2 !! i = Some y.
 Proof. rewrite map_lookup_zip_with. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
+Lemma map_lookup_zip_with_None {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i :
+  map_zip_with f m1 m2 !! i = None ↔ m1 !! i = None ∨ m2 !! i = None.
+Proof. rewrite map_lookup_zip_with. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
 
 Lemma map_zip_with_empty {A B C} (f : A → B → C) :
   map_zip_with f (∅ : M A) (∅ : M B) = ∅.
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index aaa8564a..6e8a6ff0 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -187,7 +187,7 @@ Section seqZ.
   Proof. rewrite Forall_forall. setoid_rewrite elem_of_seqZ. auto with lia. Qed.
 End seqZ.
 
-(** ** Properties of the [sum_list] and [max_list] functions *)
+(** ** Properties of the [sum_list] function *)
 Section sum_list.
   Context {A : Type}.
   Implicit Types x y z : A.
@@ -208,10 +208,29 @@ Section sum_list.
   Qed.
   Lemma sum_list_replicate n m : sum_list (replicate m n) = m * n.
   Proof. induction m; simpl; auto. Qed.
-  Lemma max_list_elem_of_le n ns:
+End sum_list.
+
+(** ** Properties of the [max_list] function *)
+Section max_list.
+  Context {A : Type}.
+
+  Lemma max_list_elem_of_le n ns :
     n ∈ ns → n ≤ max_list ns.
   Proof. induction 1; simpl; lia. Qed.
-End sum_list.
+
+  Lemma max_list_not_elem_of_gt n ns : max_list ns < n → n ∉ ns.
+  Proof. intros ??%max_list_elem_of_le. lia. Qed.
+
+  Lemma max_list_elem_of ns : ns ≠ [] → max_list ns ∈ ns.
+  Proof.
+    intros. induction ns as [|n ns IHns]; [done|]. simpl.
+    destruct (Nat.max_spec n (max_list ns)) as [[? ->]|[? ->]].
+    - destruct ns.
+      + simpl in *. lia.
+      + by apply elem_of_list_further, IHns.
+    - apply elem_of_list_here.
+  Qed.
+End max_list.
 
 (** ** Properties of the [Z_to_little_endian] and [little_endian_to_Z] functions *)
 Section Z_little_endian.
diff --git a/theories/numbers.v b/theories/numbers.v
index b17f5efb..cfb8a4bc 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -773,6 +773,11 @@ Infix "*" := Qp_mul : Qp_scope.
 Notation "/ q" := (Qp_inv q) : Qp_scope.
 Infix "/" := Qp_div : Qp_scope.
 
+Lemma Qp_to_Qc_inj_add p q : (Qp_to_Qc (p + q) = Qp_to_Qc p + Qp_to_Qc q)%Qc.
+Proof. by destruct p, q. Qed.
+Lemma Qp_to_Qc_inj_mul p q : (Qp_to_Qc (p * q) = Qp_to_Qc p * Qp_to_Qc q)%Qc.
+Proof. by destruct p, q. Qed.
+
 Program Definition pos_to_Qp (n : positive) : Qp := mk_Qp (Qc_of_Z $ Z.pos n) _.
 Next Obligation. intros n. by rewrite <-Z2Qc_inj_0, <-Z2Qc_inj_lt. Qed.
 Global Arguments pos_to_Qp : simpl never.
-- 
GitLab