diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-01-16 14:52:31 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-01-16 14:52:31 +0100 |
commit | b6aaeaf1f49088bac2dbe9dd2b2eafe55fb042c5 (patch) | |
tree | 9806dd4cd293f0de3632dea8e78f25e100e91072 /theories | |
parent | 2999e0bd62113b94024b55a4ef1406edd73bc87e (diff) |
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.
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Lists/ListSet.v | 161 |
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). |