aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst4
-rw-r--r--theories/Lists/List.v122
-rw-r--r--theories/MSets/MSetRBT.v10
3 files changed, 129 insertions, 7 deletions
diff --git a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst
new file mode 100644
index 0000000000..9850a96e1e
--- /dev/null
+++ b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst
@@ -0,0 +1,4 @@
+- New lemmas on combine, filter, and nodup functions on lists. The lemma
+ filter_app was moved to the List module.
+
+ See `#10651 <https://github.com/coq/coq/pull/10651>`_, by Oliver Nash.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 7f36edf5bb..f45317ba50 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1227,6 +1227,20 @@ End Fold_Right_Recursor.
case_eq (f a); intros; simpl; intuition congruence.
Qed.
+ Lemma filter_app (l l':list A) :
+ filter (l ++ l') = filter l ++ filter l'.
+ Proof.
+ induction l as [|x l IH]; simpl; trivial.
+ destruct (f x); simpl; now rewrite IH.
+ Qed.
+
+ Lemma concat_filter_map : forall (l : list (list A)) (f : A -> bool),
+ concat (map filter l) = filter (concat l).
+ Proof.
+ induction l as [| v l IHl]; [auto|].
+ simpl. rewrite (IHl f). rewrite filter_app. reflexivity.
+ Qed.
+
(** [find] *)
Fixpoint find (l:list A) : option A :=
@@ -1309,6 +1323,55 @@ End Fold_Right_Recursor.
End Bool.
+ (*******************************)
+ (** ** Further filtering facts *)
+ (*******************************)
+
+ Section Filtering.
+ Variables (A : Type).
+
+ Lemma filter_map : forall (f g : A -> bool) (l : list A),
+ filter f l = filter g l <-> map f l = map g l.
+ Proof.
+ induction l as [| a l IHl]; [firstorder|].
+ simpl. destruct (f a) eqn:Hfa; destruct (g a) eqn:Hga; split; intros H.
+ - inversion H. apply IHl in H1. rewrite H1. reflexivity.
+ - inversion H. apply IHl in H1. rewrite H1. reflexivity.
+ - assert (Ha : In a (filter g l)). { rewrite <- H. apply in_eq. }
+ apply filter_In in Ha. destruct Ha as [_ Hga']. rewrite Hga in Hga'. inversion Hga'.
+ - inversion H.
+ - assert (Ha : In a (filter f l)). { rewrite H. apply in_eq. }
+ apply filter_In in Ha. destruct Ha as [_ Hfa']. rewrite Hfa in Hfa'. inversion Hfa'.
+ - inversion H.
+ - rewrite IHl in H. rewrite H. reflexivity.
+ - inversion H. apply IHl. assumption.
+ Qed.
+
+ Lemma filter_ext_in : forall (f g : A -> bool) (l : list A),
+ (forall a, In a l -> f a = g a) -> filter f l = filter g l.
+ Proof.
+ intros f g l H. rewrite filter_map. apply map_ext_in. auto.
+ Qed.
+
+ Lemma ext_in_filter : forall (f g : A -> bool) (l : list A),
+ filter f l = filter g l -> (forall a, In a l -> f a = g a).
+ Proof.
+ intros f g l H. rewrite filter_map in H. apply ext_in_map. assumption.
+ Qed.
+
+ Lemma filter_ext_in_iff : forall (f g : A -> bool) (l : list A),
+ filter f l = filter g l <-> (forall a, In a l -> f a = g a).
+ Proof.
+ split; [apply ext_in_filter | apply filter_ext_in].
+ Qed.
+
+ Lemma filter_ext : forall (f g : A -> bool),
+ (forall a, f a = g a) -> forall l, filter f l = filter g l.
+ Proof.
+ intros f g H l. rewrite filter_map. apply map_ext. assumption.
+ Qed.
+
+ End Filtering.
(******************************************************)
@@ -1845,6 +1908,56 @@ Section Cutting.
End Cutting.
+(**************************************************************)
+(** ** Combining pairs of lists of possibly-different lengths *)
+(**************************************************************)
+
+Section Combining.
+ Variables (A B : Type).
+
+ Lemma combine_nil : forall (l : list A),
+ combine l (@nil B) = @nil (A*B).
+ Proof.
+ intros l.
+ apply length_zero_iff_nil.
+ rewrite combine_length. simpl. rewrite Nat.min_0_r.
+ reflexivity.
+ Qed.
+
+ Lemma combine_firstn_l : forall (l : list A) (l' : list B),
+ combine l l' = combine l (firstn (length l) l').
+ Proof.
+ induction l as [| x l IHl]; intros l'; [reflexivity|].
+ destruct l' as [| x' l']; [reflexivity|].
+ simpl. specialize IHl with (l':=l'). rewrite <- IHl.
+ reflexivity.
+ Qed.
+
+ Lemma combine_firstn_r : forall (l : list A) (l' : list B),
+ combine l l' = combine (firstn (length l') l) l'.
+ Proof.
+ intros l l'. generalize dependent l.
+ induction l' as [| x' l' IHl']; intros l.
+ - simpl. apply combine_nil.
+ - destruct l as [| x l]; [reflexivity|].
+ simpl. specialize IHl' with (l:=l). rewrite <- IHl'.
+ reflexivity.
+ Qed.
+
+ Lemma combine_firstn : forall (l : list A) (l' : list B) (n : nat),
+ firstn n (combine l l') = combine (firstn n l) (firstn n l').
+ Proof.
+ induction l as [| x l IHl]; intros l' n.
+ - simpl. repeat (rewrite firstn_nil). reflexivity.
+ - destruct l' as [| x' l'].
+ + simpl. repeat (rewrite firstn_nil). rewrite combine_nil. reflexivity.
+ + simpl. destruct n as [| n]; [reflexivity|].
+ repeat (rewrite firstn_cons). simpl.
+ rewrite IHl. reflexivity.
+ Qed.
+
+End Combining.
+
(**********************************************************************)
(** ** Predicate for List addition/removal (no need for decidability) *)
(**********************************************************************)
@@ -1959,6 +2072,15 @@ Section ReDun.
| x::xs => if in_dec decA x xs then nodup xs else x::(nodup xs)
end.
+ Lemma nodup_fixed_point : forall (l : list A),
+ NoDup l -> nodup l = l.
+ Proof.
+ induction l as [| x l IHl]; [auto|]. intros H.
+ simpl. destruct (in_dec decA x l) as [Hx | Hx]; rewrite NoDup_cons_iff in H.
+ - destruct H as [H' _]. contradiction.
+ - destruct H as [_ H']. apply IHl in H'. rewrite -> H'. reflexivity.
+ Qed.
+
Lemma nodup_In l x : In x (nodup l) <-> In x l.
Proof.
induction l as [|a l' Hrec]; simpl.
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index a3e0ec5884..b5389e9121 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -1049,12 +1049,8 @@ Qed.
(** ** Filter *)
-Lemma filter_app A f (l l':list A) :
- List.filter f (l ++ l') = List.filter f l ++ List.filter f l'.
-Proof.
- induction l as [|x l IH]; simpl; trivial.
- destruct (f x); simpl; now rewrite IH.
-Qed.
+#[deprecated(since="8.11",note="Lemma filter_app has been moved to module List.")]
+Notation filter_app := List.filter_app.
Lemma filter_aux_elements s f acc :
filter_aux f s acc = List.filter f (elements s) ++ acc.
@@ -1062,7 +1058,7 @@ Proof.
revert acc.
induction s as [|c l IHl x r IHr]; trivial.
intros acc.
- rewrite elements_node, filter_app. simpl.
+ rewrite elements_node, List.filter_app. simpl.
destruct (f x); now rewrite IHl, IHr, app_ass.
Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:15:04 +0000