From cac968116358345091ffd5eb2d78956ee327a651 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Aug 2016 15:20:12 +0200
Subject: [PATCH] Sets of sequences of natural numbers.

---
 theories/collections.v | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/theories/collections.v b/theories/collections.v
index 60dc3718..6f4e526e 100644
--- a/theories/collections.v
+++ b/theories/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.
-- 
GitLab