Commit ef163e26 authored by Michael Sammler's avatar Michael Sammler

random collection of lemmas

parent 8fc1b24b
Pipeline #25874 passed with stage
in 10 minutes and 54 seconds
This file lists "large-ish" changes to the std++ Coq library, but not every
API-breaking change is listed.
## std++ master
- Rename `drop_length` into `drop_length_gt` and add `drop_length_le`.
## std++ 1.3 (released 2020-03-18)
Coq 8.11 is supported by this release.
......
......@@ -153,6 +153,9 @@ Existing Class TCEq.
Existing Instance TCEq_refl.
Hint Mode TCEq ! - - : typeclass_instances.
Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 x1 = x2.
Proof. split; destruct 1; reflexivity. Qed.
Inductive TCDiag {A} (C : A Prop) : A A Prop :=
| TCDiag_diag x : C x TCDiag C x x.
Existing Class TCDiag.
......
......@@ -629,8 +629,10 @@ Qed.
Lemma list_insert_commute l i j x y :
i j <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l).
Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal/=; auto. Qed.
Lemma list_insert_id' l i x : (i < length l l !! i = Some x) <[i:=x]>l = l.
Proof. revert i. induction l; intros [|i] ?; f_equal/=; naive_solver lia. Qed.
Lemma list_insert_id l i x : l !! i = Some x <[i:=x]>l = l.
Proof. revert i. induction l; intros [|i] [=]; f_equal/=; auto. Qed.
Proof. intros ?. by apply list_insert_id'. Qed.
Lemma list_insert_ge l i x : length l i <[i:=x]>l = l.
Proof. revert i. induction l; intros [|i] ?; f_equal/=; auto with lia. Qed.
Lemma list_insert_insert l i x y : <[i:=x]> (<[i:=y]> l) = <[i:=x]> l.
......@@ -1162,7 +1164,9 @@ Proof.
intros. apply list_eq. intros j.
by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
Qed.
Lemma drop_insert l n i x : i < n drop n (<[i:=x]>l) = drop n l.
Lemma drop_insert_le l n i x : n i drop n (<[i:=x]>l) = <[i-n:=x]>(drop n l).
Proof. revert i n. induction l; intros [] []; naive_solver lia. Qed.
Lemma drop_insert_gt l n i x : i < n drop n (<[i:=x]>l) = drop n l.
Proof.
intros. apply list_eq. intros j.
by rewrite !lookup_drop, !list_lookup_insert_ne by lia.
......@@ -1258,6 +1262,8 @@ Proof.
Qed.
Lemma replicate_false βs n : length βs = n replicate n false =.>* βs.
Proof. intros <-. by induction βs; simpl; constructor. Qed.
Lemma tail_replicate x n : tail (replicate n x) = replicate (pred n) x.
Proof. by destruct n. Qed.
(** ** Properties of the [resize] function *)
Lemma resize_spec l n x : resize n x l = take n l ++ replicate (n - length l) x.
......@@ -3631,7 +3637,7 @@ Section seq.
Qed.
Lemma imap_seq_0 {A} (l : list A) (g : nat A) :
imap (λ j _, g j) l = g <$> seq 0 (length l).
Proof. rewrite (imap_ext _ (λ i o, g (0 + i))%nat); [|done]. apply imap_seq. Qed.
Proof. rewrite (imap_ext _ (λ i o, g (0 + i))); [|done]. apply imap_seq. Qed.
Lemma lookup_seq_lt j n i : i < n seq j n !! i = Some (j + i).
Proof.
revert j i. induction n as [|n IH]; intros j [|i] ?; simpl; auto with lia.
......@@ -3829,6 +3835,12 @@ Definition foldr_app := @fold_right_app.
Lemma foldl_app {A B} (f : A B A) (l k : list B) (a : A) :
foldl f a (l ++ k) = foldl f (foldl f a l) k.
Proof. revert a. induction l; simpl; auto. Qed.
Lemma foldr_fmap {A B C} (f : B A A) x (l : list C) g :
foldr f x (g <$> l) = foldr (λ b a, f (g b) a) x l.
Proof. induction l; f_equal/=; auto. Qed.
Lemma foldr_ext {A B} (f1 f2 : B A A) x1 x2 l1 l2 :
( b a, f1 b a = f2 b a) l1 = l2 x1 = x2 foldr f1 x1 l1 = foldr f2 x2 l2.
Proof. intros Hf -> ->. induction l2 as [|x l2 IH]; f_equal/=; by rewrite Hf, IH. Qed.
Lemma foldr_permutation {A B} (R : relation B) `{!PreOrder R}
(f : A B B) (b : B) `{Hf : ! x, Proper (R ==> R) (f x)} (l1 l2 : list A) :
( j1 a1 j2 a2 b,
......
......@@ -121,6 +121,10 @@ Definition max_list_with {A} (f : A → nat) : list A → nat :=
end.
Notation max_list := (max_list_with id).
Lemma max_list_elem_of_le n ns:
n ns (n max_list ns)%nat.
Proof. induction 1; simpl; lia. Qed.
(** * Notations and properties of [positive] *)
Local Open Scope positive_scope.
......@@ -473,6 +477,10 @@ Lemma Z_succ_pred_induction y (P : Z → Prop) :
( x, x y P x P (Z.pred x))
( x, P x).
Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.
Lemma Zmod_in_range q a c :
q * c a < (q + 1) * c
a `mod` c = a - q * c.
Proof. intros ?. symmetry. apply Z.mod_unique_pos with q; lia. Qed.
Local Close Scope Z_scope.
......
......@@ -1029,11 +1029,8 @@ Section pred_finite_infinite.
Qed.
Lemma pred_infinite_lt n : pred_infinite (lt n).
Proof.
intros l. exists (S (n `max` max_list l)). split.
- induction l; simpl; lia.
- assert ( n, n l n max_list l) as help.
{ induction 1; simpl; lia. }
intros H%help; lia.
intros l. exists (S (n `max` max_list l)). split; [lia| ].
intros H%max_list_elem_of_le; lia.
Qed.
Lemma pred_finite_le n : pred_finite (flip le n).
......
Markdown is supported
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