From 5f1da4ecdf9166f3eda24ddf21ff9ffbccfc1554 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 29 Nov 2018 13:42:00 +0100
Subject: [PATCH] Relation between `map_seq` and `set_seq`.

---
 theories/fin_map_dom.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 114ae30d..d020c194 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -143,3 +143,14 @@ Proof. unfold_leibniz; apply dom_difference. Qed.
 Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <$> m) = dom D m.
 Proof. unfold_leibniz; apply dom_fmap. Qed.
 End fin_map_dom.
+
+Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
+  dom D (map_seq start xs) ≡ set_seq start (length xs).
+Proof.
+  revert start. induction xs as [|x xs IH]; intros start; simpl.
+  - by rewrite dom_empty.
+  - by rewrite dom_insert, IH.
+Qed.
+Lemma dom_seq_L `{FinMapDom nat M D, !LeibnizEquiv D} {A} start (xs : list A) :
+  dom D (map_seq start xs) = set_seq start (length xs).
+Proof. unfold_leibniz. apply dom_seq. Qed.
-- 
GitLab