diff --git a/theories/fin_maps.v b/theories/fin_maps.v index 45a0cc67c8a0ec769052f38eb5f7f1a83cfda162..a445bc4f28e35a0f3063204ab22560af25d7b146 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 aaa8564acb4ff7cafa1955aee1124435b97b6c76..6e8a6ff06347b5d31f207191251242b637f7f586 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 b17f5efb18ce7dba0ff671ef7582f32ffc180318..cfb8a4bc656ad657e582deceeff3eaafe8f4ebe1 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.