From 8edee98efdd755e953c8129724217a63d333afb6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 30 Nov 2018 11:34:39 +0100
Subject: [PATCH] Make `set_seq` lemmas for consistent w.r.t. those of maps.

---
 theories/sets.v | 27 ++++++++++++++++++++-------
 1 file changed, 20 insertions(+), 7 deletions(-)

diff --git a/theories/sets.v b/theories/sets.v
index d9c06d42..d1400a31 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1055,23 +1055,36 @@ Section set_seq.
     - rewrite elem_of_union, elem_of_singleton, IH. lia.
   Qed.
 
-  Lemma set_seq_start_disjoint start len :
+  Lemma set_seq_plus_disjoint start len1 len2 :
+    set_seq (C:=C) start len1 ## set_seq (start + len1) len2.
+  Proof. intros x. rewrite !elem_of_set_seq. lia. Qed.
+  Lemma set_seq_plus start len1 len2 :
+    set_seq (C:=C) start (len1 + len2)
+    ≡ set_seq start len1 ∪ set_seq (start + len1) len2.
+  Proof. intros x. rewrite elem_of_union, !elem_of_set_seq. lia. Qed.
+  Lemma set_seq_plus_L `{!LeibnizEquiv C} start len1 len2 :
+    set_seq (C:=C) start (len1 + len2)
+    = set_seq start len1 ∪ set_seq (start + len1) len2.
+  Proof. unfold_leibniz. apply set_seq_plus. Qed.
+
+  Lemma set_seq_S_start_disjoint start len :
     {[ start ]} ## set_seq (C:=C) (S start) len.
   Proof. intros x. rewrite elem_of_singleton, elem_of_set_seq. lia. Qed.
+  Lemma set_seq_S_start start len :
+    set_seq (C:=C) start (S len) ≡ {[ start ]} ∪ set_seq (S start) len.
+  Proof. done. Qed.
 
-  Lemma set_seq_S_disjoint start len :
+  Lemma set_seq_S_end_disjoint start len :
     {[ start + len ]} ## set_seq (C:=C) start len.
   Proof. intros x. rewrite elem_of_singleton, elem_of_set_seq. lia. Qed.
-
-  Lemma set_seq_S_union start len :
+  Lemma set_seq_S_end_union start len :
     set_seq start (S len) ≡@{C} {[ start + len ]} ∪ set_seq start len.
   Proof.
     intros x. rewrite elem_of_union, elem_of_singleton, !elem_of_set_seq. lia.
   Qed.
-
-  Lemma set_seq_S_union_L `{!LeibnizEquiv C} start len :
+  Lemma set_seq_S_end_union_L `{!LeibnizEquiv C} start len :
     set_seq start (S len) =@{C} {[ start + len ]} ∪ set_seq start len.
-  Proof. unfold_leibniz. apply set_seq_S_union. Qed.
+  Proof. unfold_leibniz. apply set_seq_S_end_union. Qed.
 End set_seq.
 
 (** Mimimal elements *)
-- 
GitLab