Commit 14505877 by Robbert Krebbers

### Merge branch 'master' into 'master'

```Add a few lemmas

See merge request iris/stdpp!266```
parents ab9793a5 4492d5a5
 ... ... @@ -1458,6 +1458,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 : ... ... @@ -1638,6 +1643,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) = ∅. ... ...
 ... ... @@ -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. ... ...
 ... ... @@ -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. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!