Commit e3040bdb authored by Simon Spies's avatar Simon Spies

Merge branch 'master' of https://gitlab.mpi-sws.org/iris/stdpp

parents 705bb406 0b3d1e9f
Pipeline #19183 failed with stage
in 0 seconds
This file lists "large-ish" changes to the std++ Coq library, but not every
API-breaking change is listed.
## std++ 1.2.1 (unreleased)
This release of std++ received contributions by Michael Sammler, Paolo
G. Giarrusso, Paulo Emílio de Vilhena, Ralf Jung, Robbert Krebbers,
Rodolphe Lepigre, and Simon Spies.
Noteworthy additions and changes:
- Introduce `max` and `min` infix notations for `N` and `Z` like we have for `nat`.
- Make `solve_ndisj` tactic more powerful.
- Add type class `Involutive`.
- Improve `naive_solver` performance in case the goal is trivially solvable.
- Add a bunch of new lemmas for list, set, and map operations.
- Rename `lookup_imap` into `map_lookup_imap`.
## std++ 1.2.0 (released 2019-04-26)
Coq 8.9 is supported by this release, but Coq 8.6 is no longer supported. Use
......
......@@ -94,6 +94,9 @@ Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
Lemma bool_decide_decide P `{!Decision P} :
bool_decide P = if decide P then true else false.
Proof. reflexivity. Qed.
Lemma decide_bool_decide P {Hdec: Decision P} {X : Type} (x1 x2 : X):
(if decide P then x1 else x2) = (if bool_decide P then x1 else x2).
Proof. unfold bool_decide, decide. destruct Hdec; reflexivity. Qed.
Tactic Notation "case_bool_decide" "as" ident (Hd) :=
match goal with
......
......@@ -860,7 +860,7 @@ Proof.
Defined.
(** Properties of the imap function *)
Lemma lookup_imap {A B} (f : K A option B) (m : M A) i :
Lemma map_lookup_imap {A B} (f : K A option B) (m : M A) i :
map_imap f m !! i = m !! i = f i.
Proof.
unfold map_imap; destruct (m !! i = f i) as [y|] eqn:Hi; simpl.
......@@ -876,6 +876,39 @@ Proof.
rewrite elem_of_map_to_list in Hj; simplify_option_eq.
Qed.
Lemma map_imap_Some {A} (m : M A) : map_imap (λ _, Some) m = m.
Proof.
apply map_eq. intros i. rewrite map_lookup_imap. by destruct (m !! i).
Qed.
Lemma map_imap_insert {A B} (f : K A option B) (i : K) (v : A) (m : M A) :
map_imap f (<[i:=v]> m) = match f i v with
| None => delete i (map_imap f m)
| Some w => <[i:=w]> (map_imap f m)
end.
Proof.
destruct (f i v) as [w|] eqn:Hw.
- apply map_eq. intros k. rewrite map_lookup_imap.
destruct (decide (k = i)) as [->|Hk_not_i].
+ by rewrite lookup_insert, lookup_insert.
+ rewrite !lookup_insert_ne by done.
by rewrite map_lookup_imap.
- apply map_eq. intros k. rewrite map_lookup_imap.
destruct (decide (k = i)) as [->|Hk_not_i].
+ by rewrite lookup_insert, lookup_delete.
+ rewrite lookup_insert_ne, lookup_delete_ne by done.
by rewrite map_lookup_imap.
Qed.
Lemma map_imap_ext {A1 A2 B} (f1 : K A1 option B)
(f2 : K A2 option B) (m1 : M A1) (m2 : M A2) :
( k, f1 k <$> (m1 !! k) = f2 k <$> (m2 !! k))
map_imap f1 m1 = map_imap f2 m2.
Proof.
intros HExt. apply map_eq. intros i. rewrite !map_lookup_imap.
specialize (HExt i). destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
(** ** Properties of the size operation *)
Lemma map_size_empty {A} : size ( : M A) = 0.
Proof. unfold size, map_size. by rewrite map_to_list_empty. Qed.
......@@ -1081,13 +1114,18 @@ Section map_filter.
naive_solver.
Qed.
Lemma map_filter_insert_not m i x :
( y, ¬ P (i, y)) filter P (<[i:=x]> m) = filter P m.
Lemma map_filter_insert_not' m i x :
¬ P (i, x) ( y, m !! i = Some y ¬ P (i, y))
filter P (<[i:=x]> m) = filter P m.
Proof.
intros HP. apply map_filter_lookup_eq. intros j y Hy.
by rewrite lookup_insert_ne by naive_solver.
intros Hx HP. apply map_filter_lookup_eq. intros j y Hy.
rewrite lookup_insert_Some. naive_solver.
Qed.
Lemma map_filter_insert_not m i x :
( y, ¬ P (i, y)) filter P (<[i:=x]> m) = filter P m.
Proof. intros HP. by apply map_filter_insert_not'. Qed.
Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
Proof.
apply map_eq. intros j. apply option_eq; intros y.
......@@ -1106,6 +1144,16 @@ Section map_filter.
Lemma map_filter_empty : filter P ( : M A) = .
Proof. apply map_fold_empty. Qed.
Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).
Proof.
apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind.
{ by rewrite map_to_list_empty, map_filter_empty, map_to_list_empty. }
rewrite map_to_list_insert, filter_cons by done. destruct (decide (P _)).
- rewrite map_filter_insert by done.
by rewrite map_to_list_insert, IH by (rewrite map_filter_lookup_None; auto).
- by rewrite map_filter_insert_not' by naive_solver.
Qed.
End map_filter.
(** ** Properties of the [map_Forall] predicate *)
......
......@@ -279,6 +279,13 @@ Section gset.
- by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
- by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
Qed.
Lemma dom_gset_to_gmap {A} (X : gset K) (x : A) :
dom _ (gset_to_gmap x X) = X.
Proof.
induction X as [| y X not_in IH] using set_ind_L.
- rewrite gset_to_gmap_empty, dom_empty_L; done.
- rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done.
Qed.
End gset.
Typeclasses Opaque gset.
......@@ -572,6 +572,9 @@ 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.
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.
Proof. revert i. induction l; intros [|i]; f_equal/=; auto. Qed.
Lemma list_lookup_other l i x :
length l 1 l !! i = Some x j y, j i l !! j = Some y.
......@@ -665,6 +668,42 @@ Proof.
revert i j. induction k; intros i j ?; simpl;
rewrite 1?list_insert_commute by lia; auto with f_equal.
Qed.
Lemma list_inserts_app_l l1 l2 l3 i :
list_inserts i (l1 ++ l2) l3 = list_inserts (length l1 + i) l2 (list_inserts i l1 l3).
Proof.
revert l1 i; induction l1 as [|x l1 IH]; [done|].
intro i. simpl. rewrite IH, Nat.add_succ_r. apply list_insert_inserts_lt. lia.
Qed.
Lemma list_inserts_app_r l1 l2 l3 i :
list_inserts (length l2 + i) l1 (l2 ++ l3) = l2 ++ list_inserts i l1 l3.
Proof.
revert l1 i; induction l1 as [|x l1 IH]; [done|].
intros i. simpl. by rewrite plus_n_Sm, IH, insert_app_r.
Qed.
Lemma list_inserts_nil l1 i : list_inserts i l1 [] = [].
Proof.
revert i; induction l1 as [|x l1 IH]; [done|].
intro i. simpl. by rewrite IH.
Qed.
Lemma list_inserts_cons l1 l2 i x :
list_inserts (S i) l1 (x :: l2) = x :: list_inserts i l1 l2.
Proof.
revert i; induction l1 as [|y l1 IH]; [done|].
intro i. simpl. by rewrite IH.
Qed.
Lemma list_inserts_0_r l1 l2 l3 :
length l1 = length l2 list_inserts 0 l1 (l2 ++ l3) = l1 ++ l3.
Proof.
revert l2. induction l1 as [|x l1 IH]; intros [|y l2] ?; simplify_eq/=; [done|].
rewrite list_inserts_cons. simpl. by rewrite IH.
Qed.
Lemma list_inserts_0_l l1 l2 l3 :
length l1 = length l3 list_inserts 0 (l1 ++ l2) l3 = l1.
Proof.
revert l3. induction l1 as [|x l1 IH]; intros [|z l3] ?; simplify_eq/=.
{ by rewrite list_inserts_nil. }
rewrite list_inserts_cons. simpl. by rewrite IH.
Qed.
(** ** Properties of the [elem_of] predicate *)
Lemma not_elem_of_nil x : x [].
......@@ -904,8 +943,41 @@ Section find.
induction 1 as [|x y l ? IH]; intros; simplify_option_eq; eauto.
by destruct IH as [[i x'] ->]; [|exists (S i, x')].
Qed.
Lemma list_find_fmap {B : Type} (f : B A) (l : list B) :
list_find P (f <$> l) = prod_map id f <$> list_find (P f) l.
Proof.
induction l as [|x l IH]; [done|]. csimpl. (* csimpl re-folds fmap *)
case_decide; [done|].
rewrite IH. by destruct (list_find (P f) l).
Qed.
Lemma list_find_ext (Q : A Prop) `{ x, Decision (Q x)} l :
( x, P x Q x)
list_find P l = list_find Q l.
Proof.
intros HPQ. induction l as [|x l IH]; simpl; [done|].
by rewrite (decide_iff (P x) (Q x)), IH by done.
Qed.
End find.
(** ** Properties of the [omap] function *)
Lemma list_fmap_omap {B C : Type} (f : A option B) (g : B C) (l : list A) :
g <$> omap f l = omap (λ x, g <$> (f x)) l.
Proof.
induction l as [|x y IH]; [done|]. csimpl.
destruct (f x); [|done]. csimpl. by f_equal.
Qed.
Lemma list_omap_ext {B C : Type} (f : A option C) (g : B option C)
(l1 : list A) (l2 : list B) :
Forall2 (λ a b, f a = g b) l1 l2
omap f l1 = omap g l2.
Proof.
induction 1 as [|x y l l' Hfg ? IH]; [done|].
csimpl. rewrite Hfg. destruct (g y); [|done].
by f_equal.
Qed.
(** ** Properties of the [reverse] function *)
Lemma reverse_nil : reverse [] =@{list A} [].
Proof. done. Qed.
......@@ -962,6 +1034,8 @@ Proof.
Qed.
Lemma take_nil n : take n [] =@{list A} [].
Proof. by destruct n. Qed.
Lemma take_S_r l n x : l !! n = Some x take (S n) l = take n l ++ [x].
Proof. revert n. induction l; intros []; naive_solver eauto with f_equal. Qed.
Lemma take_app l k : take (length l) (l ++ k) = l.
Proof. induction l; f_equal/=; auto. Qed.
Lemma take_app_alt l k n : n = length l take n (l ++ k) = l.
......@@ -1019,6 +1093,9 @@ Lemma drop_0 l : drop 0 l = l.
Proof. done. Qed.
Lemma drop_nil n : drop n [] =@{list A} [].
Proof. by destruct n. Qed.
Lemma drop_S l x n :
l !! n = Some x drop n l = x :: drop (S n) l.
Proof. revert n. induction l; intros []; naive_solver. Qed.
Lemma drop_length l n : length (drop n l) = length l - n.
Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
Lemma drop_ge l n : length l n drop n l = [].
......@@ -1114,9 +1191,14 @@ Lemma elem_of_replicate_inv x n y : x ∈ replicate n y → x = y.
Proof. induction n; simpl; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Lemma replicate_S n x : replicate (S n) x = x :: replicate n x.
Proof. done. Qed.
Lemma replicate_S_end n x : replicate (S n) x = replicate n x ++ [x].
Proof. induction n; f_equal/=; auto. Qed.
Lemma replicate_plus n m x :
replicate (n + m) x = replicate n x ++ replicate m x.
Proof. induction n; f_equal/=; auto. Qed.
Lemma replicate_cons_app n x :
x :: replicate n x = replicate n x ++ [x].
Proof. induction n; f_equal/=; eauto. Qed.
Lemma take_replicate n m x : take n (replicate m x) = replicate (min n m) x.
Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
Lemma take_replicate_plus n m x : take n (replicate (n + m) x) = replicate n x.
......@@ -1395,6 +1477,10 @@ Lemma imap_fmap {B C} (f : nat → B → C) (g : A → B) l :
imap f (g <$> l) = imap (λ n, f n g) l.
Proof. revert f. induction l; intros; f_equal/=; eauto. Qed.
Lemma fmap_imap {B C} (f : nat A B) (g : B C) l :
g <$> imap f l = imap (λ n, g f n) l.
Proof. revert f. induction l; intros; f_equal/=; eauto. Qed.
Lemma imap_const {B} (f : A B) l : imap (const f) l = f <$> l.
Proof. induction l; f_equal/=; auto. Qed.
......@@ -1404,6 +1490,25 @@ Proof.
by rewrite IH.
Qed.
Lemma imap_length {B} (f : nat A B) l :
length (imap f l) = length l.
Proof. revert f. induction l; simpl; eauto. Qed.
Lemma elem_of_lookup_imap_1 {B} (f : nat A B) l (x : B) :
x imap f l i y, x = f i y l !! i = Some y.
Proof.
intros [i Hin]%elem_of_list_lookup. rewrite list_lookup_imap in Hin.
simplify_option_eq; naive_solver.
Qed.
Lemma elem_of_lookup_imap_2 {B} (f : nat A B) l x i : l !! i = Some x f i x imap f l.
Proof.
intros Hl. rewrite elem_of_list_lookup.
exists i. by rewrite list_lookup_imap, Hl.
Qed.
Lemma elem_of_lookup_imap {B} (f : nat A B) l (x : B) :
x imap f l i y, x = f i y l !! i = Some y.
Proof. naive_solver eauto using elem_of_lookup_imap_1, elem_of_lookup_imap_2. Qed.
(** ** Properties of the [mask] function *)
Lemma mask_nil f βs : mask f βs [] =@{list A} [].
Proof. by destruct βs. Qed.
......@@ -1454,6 +1559,16 @@ Qed.
(** ** Properties of the [seq] function *)
Lemma fmap_seq j n : S <$> seq j n = seq (S j) n.
Proof. revert j. induction n; intros; f_equal/=; auto. Qed.
Lemma imap_seq {B} l (g : nat B) i :
imap (λ j _, g (i + j)) l = g <$> seq i (length l).
Proof.
revert i. induction l as [|x l IH]; [done|].
csimpl. intros n. rewrite <-IH, <-plus_n_O. f_equal.
apply imap_ext. intros. simpl. f_equal. lia.
Qed.
Lemma imap_seq_0 {B} l (g : nat B) :
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.
Lemma lookup_seq 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.
......@@ -1466,6 +1581,13 @@ Proof.
destruct (le_lt_dec n i); [by rewrite lookup_seq_ge|].
rewrite lookup_seq by done. intuition congruence.
Qed.
Lemma NoDup_seq j n : NoDup (seq j n).
Proof. apply NoDup_ListNoDup, seq_NoDup. Qed.
Lemma seq_S_end_app j n : seq j (S n) = seq j n ++ [j + n].
Proof.
revert j. induction n as [|n IH]; intros j; simpl in *; f_equal; [done |].
rewrite IH. f_equal. f_equal. lia.
Qed.
(** ** Properties of the [Permutation] predicate *)
......@@ -3049,7 +3171,7 @@ Section fmap.
( x, f x g x) f <$> l g <$> l.
Proof. induction l; constructor; auto. Qed.
Global Instance: Inj (=) (=) f Inj (=) (=) (fmap f).
Global Instance fmap_inj: Inj (=) (=) f Inj (=) (=) (fmap f).
Proof.
intros ? l1. induction l1 as [|x l1 IH]; [by intros [|??]|].
intros [|??]; intros; f_equal/=; simplify_eq; auto.
......@@ -3673,6 +3795,35 @@ Section zip_with.
Forall (λ x, y, P y Q (f x y)) l Forall P k
Forall Q (zip_with f l k).
Proof. intros Hl. revert k. induction Hl; destruct 1; simpl in *; auto. Qed.
Lemma elem_of_lookup_zip_with_1 l k (z : C) :
z zip_with f l k i x y, z = f x y l !! i = Some x k !! i = Some y.
Proof.
intros [i Hin]%elem_of_list_lookup. rewrite lookup_zip_with in Hin.
simplify_option_eq; naive_solver.
Qed.
Lemma elem_of_lookup_zip_with_2 l k x y (z : C) i :
l !! i = Some x k !! i = Some y f x y zip_with f l k.
Proof.
intros Hl Hk. rewrite elem_of_list_lookup.
exists i. by rewrite lookup_zip_with, Hl, Hk.
Qed.
Lemma elem_of_lookup_zip_with l k (z : C) :
z zip_with f l k i x y, z = f x y l !! i = Some x k !! i = Some y.
Proof.
naive_solver eauto using
elem_of_lookup_zip_with_1, elem_of_lookup_zip_with_2.
Qed.
Lemma elem_of_zip_with l k (z : C) :
z zip_with f l k x y, z = f x y x l y k.
Proof.
intros ?%elem_of_lookup_zip_with.
naive_solver eauto using elem_of_list_lookup_2.
Qed.
End zip_with.
Lemma zip_with_sublist_alter {A B} (f : A B A) g l k i n l' k' :
......@@ -3711,6 +3862,14 @@ Section zip.
rewrite <-Forall2_same_length. intros Hlk1 Hlk2. revert l1 k1 Hlk1.
induction Hlk2; intros ?? [|??????]; simpl; auto.
Qed.
Lemma elem_of_zip_l x1 x2 l k :
(x1, x2) zip l k x1 l.
Proof. intros ?%elem_of_zip_with. naive_solver. Qed.
Lemma elem_of_zip_r x1 x2 l k :
(x1, x2) zip l k x2 k.
Proof. intros ?%elem_of_zip_with. naive_solver. Qed.
End zip.
Lemma elem_of_zipped_map {A B} (f : list A list A A B) l k x :
......
......@@ -50,6 +50,26 @@ Inductive TlRel {A} (R : relation A) (a : A) : list A → Prop :=
Section sorted.
Context {A} (R : relation A).
Lemma elem_of_StronglySorted_app l1 l2 x1 x2 :
StronglySorted R (l1 ++ l2) x1 l1 x2 l2 R x1 x2.
Proof.
induction l1 as [|x1' l1 IH]; simpl; [by rewrite elem_of_nil|].
intros [? Hall]%StronglySorted_inv [->|?]%elem_of_cons ?; [|by auto].
rewrite Forall_app, !Forall_forall in Hall. naive_solver.
Qed.
Lemma StronglySorted_app_inv_l l1 l2 :
StronglySorted R (l1 ++ l2) StronglySorted R l1.
Proof.
induction l1 as [|x1' l1 IH]; simpl;
[|inversion_clear 1]; decompose_Forall; constructor; auto.
Qed.
Lemma StronglySorted_app_inv_r l1 l2 :
StronglySorted R (l1 ++ l2) StronglySorted R l2.
Proof.
induction l1 as [|x1' l1 IH]; simpl;
[|inversion_clear 1]; decompose_Forall; auto.
Qed.
Lemma Sorted_StronglySorted `{!Transitive R} l :
Sorted R l StronglySorted R l.
Proof. by apply Sorted.Sorted_StronglySorted. Qed.
......
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