diff --git a/prelude/collections.v b/prelude/collections.v index 7762ce91a3398701a4cb186635d3d664a4afa9f2..850226e1571c4a65910ed62910d035490568c18c 100644 --- a/prelude/collections.v +++ b/prelude/collections.v @@ -948,3 +948,38 @@ Section more_finite. intros x ?; destruct (decide (x ∈ Y)); rewrite elem_of_app; set_solver. Qed. End more_finite. + +(** Sets of sequences of natural numbers *) +(* The set [seq_seq start len] of natural numbers contains the sequence +[start, start + 1, ..., start + (len-1)]. *) +Fixpoint seq_set `{Singleton nat C, Union C, Empty C} (start len : nat) : C := + match len with + | O => ∅ + | S len' => {[ start ]} ∪ seq_set (S start) len' + end. + +Section seq_set. + Context `{SimpleCollection nat C}. + Implicit Types start len x : nat. + + Lemma elem_of_seq_set start len x : + x ∈ seq_set start len ↔ start ≤ x < start + len. + Proof. + revert start. induction len as [|len IH]; intros start; simpl. + - rewrite elem_of_empty. omega. + - rewrite elem_of_union, elem_of_singleton, IH. omega. + Qed. + + Lemma seq_set_S_disjoint start len : {[ start + len ]} ⊥ seq_set start len. + Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed. + + Lemma seq_set_S_union start len : + seq_set start (C:=C) (S len) ≡ {[ start + len ]} ∪ seq_set start len. + Proof. + intros x. rewrite elem_of_union, elem_of_singleton, !elem_of_seq_set. omega. + Qed. + + Lemma seq_set_S_union_L `{!LeibnizEquiv C} start len : + seq_set start (S len) = {[ start + len ]} ∪ seq_set start len. + Proof. unfold_leibniz. apply seq_set_S_union. Qed. +End seq_set.