coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Assumptions in ListSet.set_union_nodup

From: "Ramsdell, John D." <ramsdell AT mitre.org>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Assumptions in ListSet.set_union_nodup
Date: Fri, 22 Sep 2017 13:45:29 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ramsdell AT mitre.org; spf=None smtp.mailfrom=ramsdell AT mitre.org; spf=None smtp.helo=postmaster AT smtpvmsrv1.mitre.org
Ironport-phdr: 9a23:6rk9RBJP0VOoSL15LdmcpTZWNBhigK39O0sv0rFitYgXIv/xwZ3uMQTl6Ol3ixeRBMOAtKIC1rKempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBWB6kG1uHQZHQy6Pg5oLMz0HJTThoK5zar6r5bUekBDgCe3SbJ0NhS/6wvL4Jo4m4xnf+wLwx7SrnZMf6Ae52RoIxq/2Vy0st25+YVv/iBUk/cg69RNF6LgcPJrHvRjED06PjVtt4XQvh7ZQF7X6w==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Does anyone know why ListSet.set_union_nodup has two NoDup
assumptions, when one will do?

John

(** In Lists/ListSet.v

<<
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.
>>
*)

Require Import List ListSet.

Section Union.
Variable A : Type.
Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}.

Lemma alt_set_union_nodup l l':
NoDup l -> NoDup (set_union Aeq_dec l l').
Proof.
induction l'; intros; auto.
simpl.
apply set_add_nodup.
apply IHl'; auto.
Qed.
End Union.

[Coq-Club] Assumptions in ListSet.set_union_nodup, Ramsdell, John D., 09/22/2017