ListSet: follow-up of Sebastien's last commit

  More results on set_remove, in particular explicit the NoDup
  pre-condition. Show that NoDup is preserved by other operations.

1 files changed, 106 insertions, 55 deletions

diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index f4139f4c4..c8ed95cd4 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -48,7 +48,11 @@ Section first_definitions.
         end
     end.
 
-  (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *)
+  (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing.
+      Invariant: any element should occur at most once in [x], see for
+      instance [set_add]. We hence remove here only the first occurrence
+      of [a] in [x]. *)
+
   Fixpoint set_remove (a:A) (x:set) : set :=
     match x with
     | nil => empty_set
@@ -59,58 +63,6 @@ Section first_definitions.
         end
     end.
 
-  Lemma set_remove_eq1 (a b:A) (l:set):
-    a=b -> (set_remove b (a::l))=l.
-  Proof.
-    intro Heqab. simpl. destruct (Aeq_dec b a).
-    - reflexivity.
-    - subst. tauto.
-  Qed.
-
-  Lemma set_remove_eq2 (a b:A) (l:set):
-    a<>b -> (set_remove b (a::l))=a::(set_remove b l).
-  Proof.
-    intro Hneqab. simpl. destruct (Aeq_dec b a).
-    - contradiction Hneqab. now apply eq_sym.
-    - reflexivity.
-  Qed.
-
-  Lemma In_set_remove1 (a b : A) (l : set):
-    In a (set_remove b l) -> In a l.
-  Proof.
-    induction l as [|x xs Hrec].
-    - intros. auto.
-    - simpl. destruct (Aeq_dec b x).
-      * tauto.
-      * intro H. destruct H.
-        + rewrite H. apply in_eq.
-      + apply in_cons. apply Hrec. assumption.
-  Qed.
-
-(*
-  Lemma In_set_remove2 : forall (a b : A) (l : list A),
-    In a (set_remove b l) -> a<>b.
-  Proof. induction l as [|x xs Hrec]; simpl.
-    - auto.
-    - destruct (Aeq_dec b x).
-      *
-
-      intro H. generalize (In_set_remove1 _ _ _ H). intro H'. destruct (in_inv H').
-      * intro H. apply Hrec. eapply In_set_remove1.
-  Qed.
- *)
-
-  Lemma In_set_remove3 : forall (a b : A) (l : list A),
-    In a l -> a <> b -> In a (set_remove b l).
-  Proof. induction l as [|x xs Hrec].
-    - now simpl.
-    - destruct 1 as [->|Ha]; intro Hab.
-      * rewrite (set_remove_eq2 _ Hab). apply in_eq.
-      * destruct (Aeq_dec a b).
-        + now contradiction Hab.
-        + simpl. destruct (Aeq_dec b x) as [->|_]; [trivial | now apply in_cons, Hrec].
-  Qed.
-  
   Fixpoint set_inter (x:set) : set -> set :=
     match x with
     | nil => fun y => nil
@@ -279,6 +231,68 @@ Section first_definitions.
     intros; elim (Aeq_dec a a0); intros; discriminate.
   Qed.
 
+  Lemma set_add_iff a b l : In a (set_add b l) <-> a = b \/ In a l.
+  Proof.
+  split. apply set_add_elim. apply set_add_intro.
+  Qed.
+
+  Lemma set_add_nodup a l : NoDup l -> NoDup (set_add a l).
+  Proof.
+   induction 1 as [|x l H H' IH]; simpl.
+   - constructor; [ tauto | constructor ].
+   - destruct (Aeq_dec a x) as [<-|Hax]; constructor; trivial.
+     rewrite set_add_iff. intuition.
+  Qed.
+
+  Lemma set_remove_1 (a b : A) (l : set) :
+    In a (set_remove b l) -> In a l.
+  Proof.
+    induction l as [|x xs Hrec].
+    - intros. auto.
+    - simpl. destruct (Aeq_dec b x).
+      * tauto.
+      * intro H. destruct H.
+        + rewrite H. apply in_eq.
+      + apply in_cons. apply Hrec. assumption.
+  Qed.
+
+  Lemma set_remove_2 (a b:A) (l : set) :
+    NoDup l -> In a (set_remove b l) -> a <> b.
+  Proof.
+    induction l as [|x l IH]; intro ND; simpl.
+    - tauto.
+    - inversion_clear ND.
+      destruct (Aeq_dec b x) as [<-|Hbx].
+      + congruence.
+      + destruct 1; subst; auto.
+  Qed.
+
+  Lemma set_remove_3 (a b : A) (l : set) :
+    In a l -> a <> b -> In a (set_remove b l).
+  Proof.
+    induction l as [|x xs Hrec].
+    - now simpl.
+    - simpl. destruct (Aeq_dec b x) as [<-|Hbx]; simpl; intuition.
+      congruence.
+  Qed.
+
+  Lemma set_remove_iff (a b : A) (l : set) :
+   NoDup l -> (In a (set_remove b l) <-> In a l /\ a <> b).
+  Proof.
+   split; try split.
+   - eapply set_remove_1; eauto.
+   - eapply set_remove_2; eauto.
+   - destruct 1; apply set_remove_3; auto.
+  Qed.
+
+  Lemma set_remove_nodup a l : NoDup l -> NoDup (set_remove a l).
+  Proof.
+   induction 1 as [|x l H H' IH]; simpl.
+   - constructor.
+   - destruct (Aeq_dec a x) as [<-|Hax]; trivial.
+     constructor; trivial.
+     rewrite set_remove_iff; trivial. intuition.
+  Qed.
 
   Lemma set_union_intro1 :
    forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).
@@ -316,18 +330,26 @@ Section first_definitions.
     tauto.
   Qed.
 
+  Lemma set_union_iff a l l': In a (set_union l l') <-> In a l \/ In a l'.
+  Proof.
+    split. apply set_union_elim. apply set_union_intro.
+  Qed.
+
+  Lemma set_union_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_union l l').
+  Proof.
+   induction 2 as [|x' l' ? ? IH]; simpl; trivial. now apply set_add_nodup.
+  Qed.
+
   Lemma set_union_emptyL :
    forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x.
     intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
   Qed.
 
-
   Lemma set_union_emptyR :
    forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x.
     intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
   Qed.
 
-
   Lemma set_inter_intro :
    forall (a:A) (x y:set),
      set_In a x -> set_In a y -> set_In a (set_inter x y).
@@ -378,6 +400,21 @@ Section first_definitions.
     eauto with datatypes.
   Qed.
 
+  Lemma set_inter_iff a l l' : In a (set_inter l l') <-> In a l /\ In a l'.
+  Proof.
+    split.
+    - apply set_inter_elim.
+    - destruct 1. now apply set_inter_intro.
+  Qed.
+
+  Lemma set_inter_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_inter l l').
+  Proof.
+   induction 1 as [|x l H H' IH]; intro Hl'; simpl.
+   - constructor.
+   - destruct (set_mem x l'); auto.
+     constructor; auto. rewrite set_inter_iff; tauto.
+  Qed.
+
   Lemma set_diff_intro :
    forall (a:A) (x y:set),
      set_In a x -> ~ set_In a y -> set_In a (set_diff x y).
@@ -412,6 +449,20 @@ Section first_definitions.
   rewrite H; trivial.
   Qed.
 
+  Lemma set_diff_iff a l l' : In a (set_diff l l') <-> In a l /\ ~In a l'.
+  Proof.
+  split.
+  - split; [eapply set_diff_elim1 | eapply set_diff_elim2]; eauto.
+  - destruct 1. now apply set_diff_intro.
+  Qed.
+
+  Lemma set_diff_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_diff l l').
+  Proof.
+   induction 1 as [|x l H H' IH]; intro Hl'; simpl.
+   - constructor.
+   - destruct (set_mem x l'); auto using set_add_nodup.
+  Qed.
+
   Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x).
   red; intros a x H.
   apply (set_diff_elim2 _ _ _ H).