Commit 4492d5a5 authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Add a few lemmas

parent 64ec9b56
Pipeline #47622 passed with stage
in 11 minutes and 35 seconds
...@@ -1449,6 +1449,11 @@ Section map_Forall. ...@@ -1449,6 +1449,11 @@ Section map_Forall.
naive_solver eauto using map_Forall_insert_1_1, naive_solver eauto using map_Forall_insert_1_1,
map_Forall_insert_1_2, map_Forall_insert_2. map_Forall_insert_1_2, map_Forall_insert_2.
Qed. 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). 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. Proof. intros Hm j x; rewrite lookup_delete_Some. naive_solver. Qed.
Lemma map_Forall_lookup m : 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) ...@@ -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 map_zip_with f m1 m2 !! i = Some z
x y, z = f x y m1 !! i = Some x m2 !! i = Some y. 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. 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) : Lemma map_zip_with_empty {A B C} (f : A B C) :
map_zip_with f ( : M A) ( : M B) = . map_zip_with f ( : M A) ( : M B) = .
......
...@@ -187,7 +187,7 @@ Section seqZ. ...@@ -187,7 +187,7 @@ Section seqZ.
Proof. rewrite Forall_forall. setoid_rewrite elem_of_seqZ. auto with lia. Qed. Proof. rewrite Forall_forall. setoid_rewrite elem_of_seqZ. auto with lia. Qed.
End seqZ. End seqZ.
(** ** Properties of the [sum_list] and [max_list] functions *) (** ** Properties of the [sum_list] function *)
Section sum_list. Section sum_list.
Context {A : Type}. Context {A : Type}.
Implicit Types x y z : A. Implicit Types x y z : A.
...@@ -208,10 +208,29 @@ Section sum_list. ...@@ -208,10 +208,29 @@ Section sum_list.
Qed. Qed.
Lemma sum_list_replicate n m : sum_list (replicate m n) = m * n. Lemma sum_list_replicate n m : sum_list (replicate m n) = m * n.
Proof. induction m; simpl; auto. Qed. 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. n ns n max_list ns.
Proof. induction 1; simpl; lia. Qed. 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 *) (** ** Properties of the [Z_to_little_endian] and [little_endian_to_Z] functions *)
Section Z_little_endian. Section Z_little_endian.
......
...@@ -773,6 +773,11 @@ Infix "*" := Qp_mul : Qp_scope. ...@@ -773,6 +773,11 @@ Infix "*" := Qp_mul : Qp_scope.
Notation "/ q" := (Qp_inv q) : Qp_scope. Notation "/ q" := (Qp_inv q) : Qp_scope.
Infix "/" := Qp_div : 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) _. 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. Next Obligation. intros n. by rewrite <-Z2Qc_inj_0, <-Z2Qc_inj_lt. Qed.
Global Arguments pos_to_Qp : simpl never. 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!
Please register or to comment