Commit cac96811 authored by Robbert Krebbers's avatar Robbert Krebbers

Sets of sequences of natural numbers.

parent bcaf2016
......@@ -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.
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