ListSet.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

A library for finite sets, implemented as lists

This is a light implementation of finite sets as lists; for a more extensive library, you might rather consider MSetWeakList.v. In addition, if your domain is totally ordered, you might also consider implementations of finite sets with access in logarithmic time (e.g. MSetRBT.v which is based on red-black trees).

Require Import List.

Set Implicit Arguments.

Section first_definitions.

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

  Definition set := list A.

  Definition empty_set : set := nil.

  Fixpoint set_add (a:A) (x:set) : set :=
    match x with
    | nil => a :: nil
    | a1 :: x1 =>
        match Aeq_dec a a1 with
        | left _ => a1 :: x1
        | right _ => a1 :: set_add a x1
        end
    end.


  Fixpoint set_mem (a:A) (x:set) : bool :=
    match x with
    | nil => false
    | a1 :: x1 =>
        match Aeq_dec a a1 with
        | left _ => true
        | right _ => set_mem a x1
        end
    end.

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
    | a1 :: x1 =>
        match Aeq_dec a a1 with
        | left _ => x1
        | right _ => a1 :: set_remove a x1
        end
    end.

  Fixpoint set_inter (x:set) : set -> set :=
    match x with
    | nil => fun y => nil
    | a1 :: x1 =>
        fun y =>
          if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y
    end.

  Fixpoint set_union (x y:set) : set :=
    match y with
    | nil => x
    | a1 :: y1 => set_add a1 (set_union x y1)
    end.

returns the set of all els of x that does not belong to y

  Fixpoint set_diff (x y:set) : set :=
    match x with
    | nil => nil
    | a1 :: x1 =>
        if set_mem a1 y then set_diff x1 y else set_add a1 (set_diff x1 y)
    end.


  Definition set_In : A -> set -> Prop := In (A:=A).

  Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set),
{set_In a x} + {~ set_In a x}

  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set),
{set_In a x} + {~ set_In a x}
    unfold set_In.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set), {In a x} + {~ In a x}
    (*** Realizer set_mem. Program_all. ***)
    simple induction x.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
{In a nil} + {~ In a nil}
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
{In a l} + {~ In a l} ->
{In a (a0 :: l)} + {~ In a (a0 :: l)}
    auto.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
{In a l} + {~ In a l} ->
{In a (a0 :: l)} + {~ In a (a0 :: l)}
    intros a0 x0 Ha0.A:Type
Aeq_dec:forall x1 y : A, {x1 = y} + {x1 <> y}
a:A
x:set
a0:A
x0:list A
Ha0:{In a x0} + {~ In a x0}
{In a (a0 :: x0)} + {~ In a (a0 :: x0)} case (Aeq_dec a a0); intro eq.A:Type
Aeq_dec:forall x1 y : A, {x1 = y} + {x1 <> y}
a:A
x:set
a0:A
x0:list A
Ha0:{In a x0} + {~ In a x0}
eq:a = a0
{In a (a0 :: x0)} + {~ In a (a0 :: x0)}
A:Type
Aeq_dec:forall x1 y : A, {x1 = y} + {x1 <> y}
a:A
x:set
a0:A
x0:list A
Ha0:{In a x0} + {~ In a x0}
eq:a <> a0
{In a (a0 :: x0)} + {~ In a (a0 :: x0)}
    rewrite eq; simpl; auto with datatypes.A:Type
Aeq_dec:forall x1 y : A, {x1 = y} + {x1 <> y}
a:A
x:set
a0:A
x0:list A
Ha0:{In a x0} + {~ In a x0}
eq:a <> a0
{In a (a0 :: x0)} + {~ In a (a0 :: x0)}
    elim Ha0.A:Type
Aeq_dec:forall x1 y : A, {x1 = y} + {x1 <> y}
a:A
x:set
a0:A
x0:list A
Ha0:{In a x0} + {~ In a x0}
eq:a <> a0
In a x0 -> {In a (a0 :: x0)} + {~ In a (a0 :: x0)}
A:Type
Aeq_dec:forall x1 y : A, {x1 = y} + {x1 <> y}
a:A
x:set
a0:A
x0:list A
Ha0:{In a x0} + {~ In a x0}
eq:a <> a0
~ In a x0 -> {In a (a0 :: x0)} + {~ In a (a0 :: x0)}
    auto with datatypes.A:Type
Aeq_dec:forall x1 y : A, {x1 = y} + {x1 <> y}
a:A
x:set
a0:A
x0:list A
Ha0:{In a x0} + {~ In a x0}
eq:a <> a0
~ In a x0 -> {In a (a0 :: x0)} + {~ In a (a0 :: x0)}
    right; simpl; unfold not; intros [Hc1| Hc2];
     auto with datatypes.
  Qed.

  Lemma set_mem_ind :
   forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set),
     (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (B : Type) (P : B -> Prop) (y z : B) (a : A)
  (x : set),
(set_In a x -> P y) ->
P z -> P (if set_mem a x then y else z)

  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (B : Type) (P : B -> Prop) (y z : B) (a : A)
  (x : set),
(set_In a x -> P y) ->
P z -> P (if set_mem a x then y else z)
    simple induction x; simpl; intros.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
B:Type
P:B -> Prop
y, z:B
a:A
x:set
H:False -> P y
H0:P z
P z
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
B:Type
P:B -> Prop
y, z:B
a:A
x:set
a0:A
l:list A
H:(set_In a l -> P y) ->
P z -> P (if set_mem a l then y else z)
H0:a0 = a \/ set_In a l -> P y
H1:P z
P
  (if if Aeq_dec a a0 then true else set_mem a l
   then y
   else z)
    assumption.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
B:Type
P:B -> Prop
y, z:B
a:A
x:set
a0:A
l:list A
H:(set_In a l -> P y) ->
P z -> P (if set_mem a l then y else z)
H0:a0 = a \/ set_In a l -> P y
H1:P z
P
  (if if Aeq_dec a a0 then true else set_mem a l
   then y
   else z)
    elim (Aeq_dec a a0); auto with datatypes.
  Qed.

  Lemma set_mem_ind2 :
   forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set),
     (set_In a x -> P y) ->
     (~ set_In a x -> P z) -> P (if set_mem a x then y else z).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (B : Type) (P : B -> Prop) (y z : B) (a : A)
  (x : set),
(set_In a x -> P y) ->
(~ set_In a x -> P z) ->
P (if set_mem a x then y else z)

  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (B : Type) (P : B -> Prop) (y z : B) (a : A)
  (x : set),
(set_In a x -> P y) ->
(~ set_In a x -> P z) ->
P (if set_mem a x then y else z)
    simple induction x; simpl; intros.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
B:Type
P:B -> Prop
y, z:B
a:A
x:set
H:False -> P y
H0:~ False -> P z
P z
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
B:Type
P:B -> Prop
y, z:B
a:A
x:set
a0:A
l:list A
H:(set_In a l -> P y) ->
(~ set_In a l -> P z) ->
P (if set_mem a l then y else z)
H0:a0 = a \/ set_In a l -> P y
H1:~ (a0 = a \/ set_In a l) -> P z
P
  (if if Aeq_dec a a0 then true else set_mem a l
   then y
   else z)
    apply H0; red; trivial.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
B:Type
P:B -> Prop
y, z:B
a:A
x:set
a0:A
l:list A
H:(set_In a l -> P y) ->
(~ set_In a l -> P z) ->
P (if set_mem a l then y else z)
H0:a0 = a \/ set_In a l -> P y
H1:~ (a0 = a \/ set_In a l) -> P z
P
  (if if Aeq_dec a a0 then true else set_mem a l
   then y
   else z)
    case (Aeq_dec a a0); auto with datatypes.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
B:Type
P:B -> Prop
y, z:B
a:A
x:set
a0:A
l:list A
H:(set_In a l -> P y) ->
(~ set_In a l -> P z) ->
P (if set_mem a l then y else z)
H0:a0 = a \/ set_In a l -> P y
H1:~ (a0 = a \/ set_In a l) -> P z
a <> a0 -> P (if set_mem a l then y else z)
    intro Hneg; apply H; intros; auto.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
B:Type
P:B -> Prop
y, z:B
a:A
x:set
a0:A
l:list A
H:(set_In a l -> P y) ->
(~ set_In a l -> P z) ->
P (if set_mem a l then y else z)
H0:a0 = a \/ set_In a l -> P y
H1:~ (a0 = a \/ set_In a l) -> P z
Hneg:a <> a0
H2:~ set_In a l
P z
    apply H1; red; intro.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
B:Type
P:B -> Prop
y, z:B
a:A
x:set
a0:A
l:list A
H:(set_In a l -> P y) ->
(~ set_In a l -> P z) ->
P (if set_mem a l then y else z)
H0:a0 = a \/ set_In a l -> P y
H1:~ (a0 = a \/ set_In a l) -> P z
Hneg:a <> a0
H2:~ set_In a l
H3:a0 = a \/ set_In a l
False
    case H3; auto.
  Qed.


  Lemma set_mem_correct1 :
   forall (a:A) (x:set), set_mem a x = true -> set_In a x.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set),
set_mem a x = true -> set_In a x
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set),
set_mem a x = true -> set_In a x
    simple induction x; simpl.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
false = true -> False
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(set_mem a l = true -> set_In a l) ->
(if Aeq_dec a a0 then true else set_mem a l) = true ->
a0 = a \/ set_In a l
    discriminate.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(set_mem a l = true -> set_In a l) ->
(if Aeq_dec a a0 then true else set_mem a l) = true ->
a0 = a \/ set_In a l
    intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
  Qed.

  Lemma set_mem_correct2 :
   forall (a:A) (x:set), set_In a x -> set_mem a x = true.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set),
set_In a x -> set_mem a x = true
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set),
set_In a x -> set_mem a x = true
    simple induction x; simpl.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
False -> false = true
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(set_In a l -> set_mem a l = true) ->
a0 = a \/ set_In a l ->
(if Aeq_dec a a0 then true else set_mem a l) = true
    intro Ha; elim Ha.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(set_In a l -> set_mem a l = true) ->
a0 = a \/ set_In a l ->
(if Aeq_dec a a0 then true else set_mem a l) = true
    intros a0 l; elim (Aeq_dec a a0); auto with datatypes.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
a0:A
l:list A
a <> a0 ->
(set_In a l -> set_mem a l = true) ->
a0 = a \/ set_In a l -> set_mem a l = true
    intros H1 H2 [H3| H4].A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
a0:A
l:list A
H1:a <> a0
H2:set_In a l -> set_mem a l = true
H3:a0 = a
set_mem a l = true
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
a0:A
l:list A
H1:a <> a0
H2:set_In a l -> set_mem a l = true
H4:set_In a l
set_mem a l = true
    absurd (a0 = a); auto with datatypes.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
a0:A
l:list A
H1:a <> a0
H2:set_In a l -> set_mem a l = true
H4:set_In a l
set_mem a l = true
    auto with datatypes.
  Qed.

  Lemma set_mem_complete1 :
   forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set),
set_mem a x = false -> ~ set_In a x
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set),
set_mem a x = false -> ~ set_In a x
    simple induction x; simpl.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
false = false -> ~ False
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(set_mem a l = false -> ~ set_In a l) ->
(if Aeq_dec a a0 then true else set_mem a l) = false ->
~ (a0 = a \/ set_In a l)
    tauto.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(set_mem a l = false -> ~ set_In a l) ->
(if Aeq_dec a a0 then true else set_mem a l) = false ->
~ (a0 = a \/ set_In a l)
    intros a0 l; elim (Aeq_dec a a0).A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
a0:A
l:list A
a = a0 ->
(set_mem a l = false -> ~ set_In a l) ->
true = false -> ~ (a0 = a \/ set_In a l)
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
a0:A
l:list A
a <> a0 ->
(set_mem a l = false -> ~ set_In a l) ->
set_mem a l = false -> ~ (a0 = a \/ set_In a l)
    intros _ _ [=].A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
a0:A
l:list A
a <> a0 ->
(set_mem a l = false -> ~ set_In a l) ->
set_mem a l = false -> ~ (a0 = a \/ set_In a l)
    unfold not; intros H H0 H1 [|]; auto with datatypes.
  Qed.

  Lemma set_mem_complete2 :
   forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set),
~ set_In a x -> set_mem a x = false
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set),
~ set_In a x -> set_mem a x = false
    simple induction x; simpl.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
~ False -> false = false
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(~ set_In a l -> set_mem a l = false) ->
~ (a0 = a \/ set_In a l) ->
(if Aeq_dec a a0 then true else set_mem a l) = false
    tauto.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(~ set_In a l -> set_mem a l = false) ->
~ (a0 = a \/ set_In a l) ->
(if Aeq_dec a a0 then true else set_mem a l) = false
    intros a0 l; elim (Aeq_dec a a0).A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
a0:A
l:list A
a = a0 ->
(~ set_In a l -> set_mem a l = false) ->
~ (a0 = a \/ set_In a l) -> true = false
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
a0:A
l:list A
a <> a0 ->
(~ set_In a l -> set_mem a l = false) ->
~ (a0 = a \/ set_In a l) -> set_mem a l = false
    intros H H0 []; auto with datatypes.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
a0:A
l:list A
a <> a0 ->
(~ set_In a l -> set_mem a l = false) ->
~ (a0 = a \/ set_In a l) -> set_mem a l = false
    tauto.
  Qed.

  Lemma set_add_intro1 :
   forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a b : A) (x : set),
set_In a x -> set_In a (set_add b x)

  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a b : A) (x : set),
set_In a x -> set_In a (set_add b x)
    unfold set_In; simple induction x; simpl.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
False -> b = a \/ False
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
forall (a0 : A) (l : list A),
(In a l -> In a (set_add b l)) ->
a0 = a \/ In a l ->
In a
  (if Aeq_dec b a0 then a0 :: l else a0 :: set_add b l)
    auto with datatypes.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
forall (a0 : A) (l : list A),
(In a l -> In a (set_add b l)) ->
a0 = a \/ In a l ->
In a
  (if Aeq_dec b a0 then a0 :: l else a0 :: set_add b l)
    intros a0 l H [Ha0a| Hal].A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a l -> In a (set_add b l)
Ha0a:a0 = a
In a
  (if Aeq_dec b a0 then a0 :: l else a0 :: set_add b l)
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a l -> In a (set_add b l)
Hal:In a l
In a
  (if Aeq_dec b a0 then a0 :: l else a0 :: set_add b l)
    elim (Aeq_dec b a0); left; assumption.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a l -> In a (set_add b l)
Hal:In a l
In a
  (if Aeq_dec b a0 then a0 :: l else a0 :: set_add b l)
    elim (Aeq_dec b a0); right; [ assumption | auto with datatypes ].
  Qed.

  Lemma set_add_intro2 :
   forall (a b:A) (x:set), a = b -> set_In a (set_add b x).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a b : A) (x : set),
a = b -> set_In a (set_add b x)

  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a b : A) (x : set),
a = b -> set_In a (set_add b x)
    unfold set_In; simple induction x; simpl.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a = b -> b = a \/ False
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
forall (a0 : A) (l : list A),
(a = b -> In a (set_add b l)) ->
a = b ->
In a
  (if Aeq_dec b a0 then a0 :: l else a0 :: set_add b l)
    auto with datatypes.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
forall (a0 : A) (l : list A),
(a = b -> In a (set_add b l)) ->
a = b ->
In a
  (if Aeq_dec b a0 then a0 :: l else a0 :: set_add b l)
    intros a0 l H Hab.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:a = b -> In a (set_add b l)
Hab:a = b
In a
  (if Aeq_dec b a0 then a0 :: l else a0 :: set_add b l)
    elim (Aeq_dec b a0);
     [ rewrite Hab; intro Hba0; rewrite Hba0; simpl;
        auto with datatypes
     | auto with datatypes ].
  Qed.

  Hint Resolve set_add_intro1 set_add_intro2 : core.

  Lemma set_add_intro :
   forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a b : A) (x : set),
a = b \/ set_In a x -> set_In a (set_add b x)

  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a b : A) (x : set),
a = b \/ set_In a x -> set_In a (set_add b x)
    intros a b x [H1| H2]; auto with datatypes.
  Qed.

  Lemma set_add_elim :
   forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a b : A) (x : set),
set_In a (set_add b x) -> a = b \/ set_In a x

  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a b : A) (x : set),
set_In a (set_add b x) -> a = b \/ set_In a x
    unfold set_In.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a b : A) (x : set),
In a (set_add b x) -> a = b \/ In a x
    simple induction x.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
In a (set_add b nil) -> a = b \/ In a nil
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
forall (a0 : A) (l : list A),
(In a (set_add b l) -> a = b \/ In a l) ->
In a (set_add b (a0 :: l)) -> a = b \/ In a (a0 :: l)
    simpl; intros [H1| H2]; auto with datatypes.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
forall (a0 : A) (l : list A),
(In a (set_add b l) -> a = b \/ In a l) ->
In a (set_add b (a0 :: l)) -> a = b \/ In a (a0 :: l)
    simpl; do 3 intro.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a (set_add b l) -> a = b \/ In a l
In a
  (if Aeq_dec b a0 then a0 :: l else a0 :: set_add b l) ->
a = b \/ a0 = a \/ In a l
    elim (Aeq_dec b a0).A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a (set_add b l) -> a = b \/ In a l
b = a0 -> In a (a0 :: l) -> a = b \/ a0 = a \/ In a l
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a (set_add b l) -> a = b \/ In a l
b <> a0 ->
In a (a0 :: set_add b l) -> a = b \/ a0 = a \/ In a l
    simpl; tauto.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a (set_add b l) -> a = b \/ In a l
b <> a0 ->
In a (a0 :: set_add b l) -> a = b \/ a0 = a \/ In a l
    simpl; intros H0 [|].A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a (set_add b l) -> a = b \/ In a l
H0:b <> a0
H1:a0 = a
a = b \/ a0 = a \/ In a l
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a (set_add b l) -> a = b \/ In a l
H0:b <> a0
H1:In a (set_add b l)
a = b \/ a0 = a \/ In a l
    trivial with datatypes.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a (set_add b l) -> a = b \/ In a l
H0:b <> a0
H1:a0 = a
a = b \/ a0 = a \/ In a l
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a (set_add b l) -> a = b \/ In a l
H0:b <> a0
H1:In a (set_add b l)
a = b \/ a0 = a \/ In a l
    tauto.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
a0:A
l:list A
H:In a (set_add b l) -> a = b \/ In a l
H0:b <> a0
H1:In a (set_add b l)
a = b \/ a0 = a \/ In a l
    tauto.
  Qed.

  Lemma set_add_elim2 :
   forall (a b:A) (x:set), set_In a (set_add b x) -> a <> b -> set_In a x.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a b : A) (x : set),
set_In a (set_add b x) -> a <> b -> set_In a x
   intros a b x H; case (set_add_elim _ _ _ H); intros; trivial.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b:A
x:set
H:set_In a (set_add b x)
H0:a = b
H1:a <> b
set_In a x
   case H1; trivial.
   Qed.

  Hint Resolve set_add_intro set_add_elim set_add_elim2 : core.

  Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set), set_add a x <> empty_set
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set), set_add a x <> empty_set
    simple induction x; simpl.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
a :: nil <> empty_set
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
set_add a l <> empty_set ->
(if Aeq_dec a a0 then a0 :: l else a0 :: set_add a l) <>
empty_set
    discriminate.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
set_add a l <> empty_set ->
(if Aeq_dec a a0 then a0 :: l else a0 :: set_add a l) <>
empty_set
    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.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
In a (set_add b l) <-> a = b \/ In a l
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
In a (set_add b l) <-> a = b \/ In a l
  split.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
In a (set_add b l) -> a = b \/ In a l
A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
a = b \/ In a l -> In a (set_add b l) apply set_add_elim.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
a = b \/ In a l -> In a (set_add b l) apply set_add_intro.
  Qed.

  Lemma set_add_nodup a l : NoDup l -> NoDup (set_add a l).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
NoDup l -> NoDup (set_add a l)
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
NoDup l -> NoDup (set_add a l)
   induction 1 as [|x l H H' IH]; simpl.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
NoDup (a :: nil)
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup (set_add a l)
NoDup
  (if Aeq_dec a x then x :: l else x :: set_add a l)
   -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
NoDup (a :: nil) constructor; [ tauto | constructor ].
   -A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup (set_add a l)
NoDup
  (if Aeq_dec a x then x :: l else x :: set_add a l) destruct (Aeq_dec a x) as [<-|Hax]; constructor; trivial.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup (set_add a l)
Hax:a <> x
~ In x (set_add a l)
     rewrite set_add_iff.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup (set_add a l)
Hax:a <> x
~ (x = a \/ In x l) intuition.
  Qed.

  Lemma set_remove_1 (a b : A) (l : set) :
    In a (set_remove b l) -> In a l.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
In a (set_remove b l) -> In a l
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
In a (set_remove b l) -> In a l
    induction l as [|x xs Hrec].A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
In a (set_remove b nil) -> In a nil
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
In a (set_remove b (x :: xs)) -> In a (x :: xs)
    -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
In a (set_remove b nil) -> In a nil intros.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
H:In a (set_remove b nil)
In a nil auto.
    -A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
In a (set_remove b (x :: xs)) -> In a (x :: xs) simpl.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
In a
  (if Aeq_dec b x then xs else x :: set_remove b xs) ->
x = a \/ In a xs destruct (Aeq_dec b x).A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
e:b = x
In a xs -> x = a \/ In a xs
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
n:b <> x
In a (x :: set_remove b xs) -> x = a \/ In a xs
      *A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
e:b = x
In a xs -> x = a \/ In a xs tauto.
      *A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
n:b <> x
In a (x :: set_remove b xs) -> x = a \/ In a xs intro H.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
n:b <> x
H:In a (x :: set_remove b xs)
x = a \/ In a xs destruct H.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
n:b <> x
H:x = a
x = a \/ In a xs
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
n:b <> x
H:In a (set_remove b xs)
x = a \/ In a xs
        +A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
n:b <> x
H:x = a
x = a \/ In a xs rewrite H.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
n:b <> x
H:x = a
a = a \/ In a xs apply in_eq.
      +A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
n:b <> x
H:In a (set_remove b xs)
x = a \/ In a xs apply in_cons.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
n:b <> x
H:In a (set_remove b xs)
In a xs apply Hrec.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a (set_remove b xs) -> In a xs
n:b <> x
H:In a (set_remove b xs)
In a (set_remove b xs) assumption.
  Qed.

  Lemma set_remove_2 (a b:A) (l : set) :
    NoDup l -> In a (set_remove b l) -> a <> b.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
NoDup l -> In a (set_remove b l) -> a <> b
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
NoDup l -> In a (set_remove b l) -> a <> b
    induction l as [|x l IH]; intro ND; simpl.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
ND:NoDup nil
False -> a <> b
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
l:list A
IH:NoDup l -> In a (set_remove b l) -> a <> b
ND:NoDup (x :: l)
In a (if Aeq_dec b x then l else x :: set_remove b l) ->
a <> b
    -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
ND:NoDup nil
False -> a <> b tauto.
    -A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
l:list A
IH:NoDup l -> In a (set_remove b l) -> a <> b
ND:NoDup (x :: l)
In a (if Aeq_dec b x then l else x :: set_remove b l) ->
a <> b inversion_clear ND.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
l:list A
IH:NoDup l -> In a (set_remove b l) -> a <> b
H:~ In x l
H0:NoDup l
In a (if Aeq_dec b x then l else x :: set_remove b l) ->
a <> b
      destruct (Aeq_dec b x) as [<-|Hbx].A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:list A
IH:NoDup l -> In a (set_remove b l) -> a <> b
H:~ In b l
H0:NoDup l
In a l -> a <> b
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
l:list A
IH:NoDup l -> In a (set_remove b l) -> a <> b
H:~ In x l
H0:NoDup l
Hbx:b <> x
In a (x :: set_remove b l) -> a <> b
      +A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:list A
IH:NoDup l -> In a (set_remove b l) -> a <> b
H:~ In b l
H0:NoDup l
In a l -> a <> b congruence.
      +A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
l:list A
IH:NoDup l -> In a (set_remove b l) -> a <> b
H:~ In x l
H0:NoDup l
Hbx:b <> x
In a (x :: set_remove b l) -> a <> b 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).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
In a l -> a <> b -> In a (set_remove b l)
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
In a l -> a <> b -> In a (set_remove b l)
    induction l as [|x xs Hrec].A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
In a nil -> a <> b -> In a (set_remove b nil)
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a xs -> a <> b -> In a (set_remove b xs)
In a (x :: xs) ->
a <> b -> In a (set_remove b (x :: xs))
    -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
In a nil -> a <> b -> In a (set_remove b nil) now simpl.
    -A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a xs -> a <> b -> In a (set_remove b xs)
In a (x :: xs) ->
a <> b -> In a (set_remove b (x :: xs)) simpl.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, b, x:A
xs:list A
Hrec:In a xs -> a <> b -> In a (set_remove b xs)
x = a \/ In a xs ->
a <> b ->
In a
  (if Aeq_dec b x then xs else x :: set_remove b xs) destruct (Aeq_dec b x) as [<-|Hbx]; simpl; intuition.A:Type
Aeq_dec:forall x y : A, {x = y} + {x = y -> False}
a, b:A
xs:list A
Hrec:In a xs ->
(a = b -> False) -> In a (set_remove b xs)
H0:a = b -> False
H1:b = a
In a xs
      congruence.
  Qed.

  Lemma set_remove_iff (a b : A) (l : set) :
   NoDup l -> (In a (set_remove b l) <-> In a l /\ a <> b).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
NoDup l -> In a (set_remove b l) <-> In a l /\ a <> b
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
NoDup l -> In a (set_remove b l) <-> In a l /\ a <> b
   split; try split.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
H:NoDup l
H0:In a (set_remove b l)
In a l
A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
H:NoDup l
H0:In a (set_remove b l)
a <> b
A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
H:NoDup l
In a l /\ a <> b -> In a (set_remove b l)
   -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
H:NoDup l
H0:In a (set_remove b l)
In a l eapply set_remove_1; eauto.
   -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
H:NoDup l
H0:In a (set_remove b l)
a <> b eapply set_remove_2; eauto.
   -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a, b:A
l:set
H:NoDup l
In a l /\ a <> b -> In a (set_remove b l) destruct 1; apply set_remove_3; auto.
  Qed.

  Lemma set_remove_nodup a l : NoDup l -> NoDup (set_remove a l).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
NoDup l -> NoDup (set_remove a l)
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
NoDup l -> NoDup (set_remove a l)
   induction 1 as [|x l H H' IH]; simpl.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
NoDup empty_set
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup (set_remove a l)
NoDup (if Aeq_dec a x then l else x :: set_remove a l)
   -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
NoDup empty_set constructor.
   -A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup (set_remove a l)
NoDup (if Aeq_dec a x then l else x :: set_remove a l) destruct (Aeq_dec a x) as [<-|Hax]; trivial.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup (set_remove a l)
Hax:a <> x
NoDup (x :: set_remove a l)
     constructor; trivial.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup (set_remove a l)
Hax:a <> x
~ In x (set_remove a l)
     rewrite set_remove_iff; trivial.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a, x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup (set_remove a l)
Hax:a <> x
~ (In x l /\ x <> a) intuition.
  Qed.

  Lemma set_union_intro1 :
   forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a x -> set_In a (set_union x y)
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a x -> set_In a (set_union x y)
    simple induction y; simpl; auto with datatypes.
  Qed.

  Lemma set_union_intro2 :
   forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a y -> set_In a (set_union x y)
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a y -> set_In a (set_union x y)
    simple induction y; simpl.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
False -> set_In a x
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
forall (a0 : A) (l : list A),
(set_In a l -> set_In a (set_union x l)) ->
a0 = a \/ set_In a l ->
set_In a (set_add a0 (set_union x l))
    tauto.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
forall (a0 : A) (l : list A),
(set_In a l -> set_In a (set_union x l)) ->
a0 = a \/ set_In a l ->
set_In a (set_add a0 (set_union x l))
    intros; elim H0; auto with datatypes.
  Qed.

  Hint Resolve set_union_intro2 set_union_intro1 : core.

  Lemma set_union_intro :
   forall (a:A) (x y:set),
     set_In a x \/ set_In a y -> set_In a (set_union x y).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a x \/ set_In a y -> set_In a (set_union x y)
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a x \/ set_In a y -> set_In a (set_union x y)
    intros; elim H; auto with datatypes.
  Qed.

  Lemma set_union_elim :
   forall (a:A) (x y:set),
     set_In a (set_union x y) -> set_In a x \/ set_In a y.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a (set_union x y) -> set_In a x \/ set_In a y
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a (set_union x y) -> set_In a x \/ set_In a y
    simple induction y; simpl.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
set_In a x -> set_In a x \/ False
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
forall (a0 : A) (l : list A),
(set_In a (set_union x l) -> set_In a x \/ set_In a l) ->
set_In a (set_add a0 (set_union x l)) ->
set_In a x \/ a0 = a \/ set_In a l
    auto with datatypes.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
forall (a0 : A) (l : list A),
(set_In a (set_union x l) -> set_In a x \/ set_In a l) ->
set_In a (set_add a0 (set_union x l)) ->
set_In a x \/ a0 = a \/ set_In a l
    intros.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
a0:A
l:list A
H:set_In a (set_union x l) ->
set_In a x \/ set_In a l
H0:set_In a (set_add a0 (set_union x l))
set_In a x \/ a0 = a \/ set_In a l
    generalize (set_add_elim _ _ _ H0).A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
a0:A
l:list A
H:set_In a (set_union x l) ->
set_In a x \/ set_In a l
H0:set_In a (set_add a0 (set_union x l))
a = a0 \/ set_In a (set_union x l) ->
set_In a x \/ a0 = a \/ set_In a l
    intros [H1| H1].A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
a0:A
l:list A
H:set_In a (set_union x l) ->
set_In a x \/ set_In a l
H0:set_In a (set_add a0 (set_union x l))
H1:a = a0
set_In a x \/ a0 = a \/ set_In a l
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
a0:A
l:list A
H:set_In a (set_union x l) ->
set_In a x \/ set_In a l
H0:set_In a (set_add a0 (set_union x l))
H1:set_In a (set_union x l)
set_In a x \/ a0 = a \/ set_In a l
    auto with datatypes.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
a0:A
l:list A
H:set_In a (set_union x l) ->
set_In a x \/ set_In a l
H0:set_In a (set_add a0 (set_union x l))
H1:set_In a (set_union x l)
set_In a x \/ a0 = a \/ set_In a l
    tauto.
  Qed.

  Lemma set_union_iff a l l': In a (set_union l l') <-> In a l \/ In a l'.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a (set_union l l') <-> In a l \/ In a l'
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a (set_union l l') <-> In a l \/ In a l'
    split.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a (set_union l l') -> In a l \/ In a l'
A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a l \/ In a l' -> In a (set_union l l') apply set_union_elim.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a l \/ In a l' -> In a (set_union l l') apply set_union_intro.
  Qed.

  Lemma set_union_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_union l l').A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
NoDup l -> NoDup l' -> NoDup (set_union l l')
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
NoDup l -> NoDup l' -> NoDup (set_union l l')
   induction 2 as [|x' l' ? ? IH]; simpl; trivial.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
l:list A
H:NoDup l
x':A
l':list A
H0:~ In x' l'
H1:NoDup l'
IH:NoDup (set_union l l')
NoDup (set_add x' (set_union l l')) 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.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
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.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
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).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a x -> set_In a y -> set_In a (set_inter x y)
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a x -> set_In a y -> set_In a (set_inter x y)
    simple induction x.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall y : set,
set_In a nil ->
set_In a y -> set_In a (set_inter nil y)
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(forall y : set,
 set_In a l -> set_In a y -> set_In a (set_inter l y)) ->
forall y : set,
set_In a (a0 :: l) ->
set_In a y -> set_In a (set_inter (a0 :: l) y)
    auto with datatypes.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(forall y : set,
 set_In a l -> set_In a y -> set_In a (set_inter l y)) ->
forall y : set,
set_In a (a0 :: l) ->
set_In a y -> set_In a (set_inter (a0 :: l) y)
    simpl; intros a0 l Hrec y [Ha0a| Hal] Hy.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Ha0a:a0 = a
Hy:set_In a y
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y)
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Hal:set_In a l
Hy:set_In a y
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y)
    simpl; rewrite Ha0a.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Ha0a:a0 = a
Hy:set_In a y
set_In a
  (if set_mem a y
   then a :: set_inter l y
   else set_inter l y)
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Hal:set_In a l
Hy:set_In a y
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y)
    generalize (set_mem_correct1 a y).A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Ha0a:a0 = a
Hy:set_In a y
(set_mem a y = true -> set_In a y) ->
set_In a
  (if set_mem a y
   then a :: set_inter l y
   else set_inter l y)
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Hal:set_In a l
Hy:set_In a y
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y)
    generalize (set_mem_complete1 a y).A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Ha0a:a0 = a
Hy:set_In a y
(set_mem a y = false -> ~ set_In a y) ->
(set_mem a y = true -> set_In a y) ->
set_In a
  (if set_mem a y
   then a :: set_inter l y
   else set_inter l y)
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Hal:set_In a l
Hy:set_In a y
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y)
    elim (set_mem a y); simpl; intros.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Ha0a:a0 = a
Hy:set_In a y
H:true = false -> ~ set_In a y
H0:true = true -> set_In a y
a = a \/ set_In a (set_inter l y)
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Ha0a:a0 = a
Hy:set_In a y
H:false = false -> ~ set_In a y
H0:false = true -> set_In a y
set_In a (set_inter l y)
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Hal:set_In a l
Hy:set_In a y
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y)
    auto with datatypes.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Ha0a:a0 = a
Hy:set_In a y
H:false = false -> ~ set_In a y
H0:false = true -> set_In a y
set_In a (set_inter l y)
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Hal:set_In a l
Hy:set_In a y
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y)
    absurd (set_In a y); auto with datatypes.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
set_In a y0 -> set_In a (set_inter l y0)
y:set
Hal:set_In a l
Hy:set_In a y
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y)
    elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ].
  Qed.

  Lemma set_inter_elim1 :
   forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a x.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a (set_inter x y) -> set_In a x
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a (set_inter x y) -> set_In a x
    simple induction x.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall y : set,
set_In a (set_inter nil y) -> set_In a nil
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(forall y : set,
 set_In a (set_inter l y) -> set_In a l) ->
forall y : set,
set_In a (set_inter (a0 :: l) y) -> set_In a (a0 :: l)
    auto with datatypes.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(forall y : set,
 set_In a (set_inter l y) -> set_In a l) ->
forall y : set,
set_In a (set_inter (a0 :: l) y) -> set_In a (a0 :: l)
    simpl; intros a0 l Hrec y.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_inter l y0) -> set_In a l
y:set
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y) -> a0 = a \/ set_In a l
    generalize (set_mem_correct1 a0 y).A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_inter l y0) -> set_In a l
y:set
(set_mem a0 y = true -> set_In a0 y) ->
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y) -> a0 = a \/ set_In a l
    elim (set_mem a0 y); simpl; intros.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_inter l y0) -> set_In a l
y:set
H:true = true -> set_In a0 y
H0:a0 = a \/ set_In a (set_inter l y)
a0 = a \/ set_In a l
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_inter l y0) -> set_In a l
y:set
H:false = true -> set_In a0 y
H0:set_In a (set_inter l y)
a0 = a \/ set_In a l
    elim H0; eauto with datatypes.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_inter l y0) -> set_In a l
y:set
H:false = true -> set_In a0 y
H0:set_In a (set_inter l y)
a0 = a \/ set_In a l
    eauto with datatypes.
  Qed.

  Lemma set_inter_elim2 :
   forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a (set_inter x y) -> set_In a y
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a (set_inter x y) -> set_In a y
    simple induction x.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall y : set,
set_In a (set_inter nil y) -> set_In a y
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(forall y : set,
 set_In a (set_inter l y) -> set_In a y) ->
forall y : set,
set_In a (set_inter (a0 :: l) y) -> set_In a y
    simpl; tauto.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(forall y : set,
 set_In a (set_inter l y) -> set_In a y) ->
forall y : set,
set_In a (set_inter (a0 :: l) y) -> set_In a y
    simpl; intros a0 l Hrec y.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_inter l y0) -> set_In a y0
y:set
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y) -> set_In a y
    generalize (set_mem_correct1 a0 y).A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_inter l y0) -> set_In a y0
y:set
(set_mem a0 y = true -> set_In a0 y) ->
set_In a
  (if set_mem a0 y
   then a0 :: set_inter l y
   else set_inter l y) -> set_In a y
    elim (set_mem a0 y); simpl; intros.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_inter l y0) -> set_In a y0
y:set
H:true = true -> set_In a0 y
H0:a0 = a \/ set_In a (set_inter l y)
set_In a y
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_inter l y0) -> set_In a y0
y:set
H:false = true -> set_In a0 y
H0:set_In a (set_inter l y)
set_In a y
    elim H0;
     [ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ].A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_inter l y0) -> set_In a y0
y:set
H:false = true -> set_In a0 y
H0:set_In a (set_inter l y)
set_In a y
    eauto with datatypes.
  Qed.

  Hint Resolve set_inter_elim1 set_inter_elim2 : core.

  Lemma set_inter_elim :
   forall (a:A) (x y:set),
     set_In a (set_inter x y) -> set_In a x /\ set_In a y.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a (set_inter x y) -> set_In a x /\ set_In a y
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a (set_inter x y) -> set_In a x /\ set_In a y
    eauto with datatypes.
  Qed.

  Lemma set_inter_iff a l l' : In a (set_inter l l') <-> In a l /\ In a l'.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a (set_inter l l') <-> In a l /\ In a l'
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a (set_inter l l') <-> In a l /\ In a l'
    split.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a (set_inter l l') -> In a l /\ In a l'
A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a l /\ In a l' -> In a (set_inter l l')
    -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a (set_inter l l') -> In a l /\ In a l' apply set_inter_elim.
    -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a l /\ In a l' -> In a (set_inter l l') destruct 1.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
H:In a l
H0:In a l'
In a (set_inter l l') now apply set_inter_intro.
  Qed.

  Lemma set_inter_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_inter l l').A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
NoDup l -> NoDup l' -> NoDup (set_inter l l')
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
NoDup l -> NoDup l' -> NoDup (set_inter l l')
   induction 1 as [|x l H H' IH]; intro Hl'; simpl.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
l':list A
Hl':NoDup l'
NoDup nil
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
l':list A
x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup l' -> NoDup (set_inter l l')
Hl':NoDup l'
NoDup
  (if set_mem x l'
   then x :: set_inter l l'
   else set_inter l l')
   -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
l':list A
Hl':NoDup l'
NoDup nil constructor.
   -A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
l':list A
x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup l' -> NoDup (set_inter l l')
Hl':NoDup l'
NoDup
  (if set_mem x l'
   then x :: set_inter l l'
   else set_inter l l') destruct (set_mem x l'); auto.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
l':list A
x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup l' -> NoDup (set_inter l l')
Hl':NoDup l'
NoDup (x :: set_inter l l')
     constructor; auto.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
l':list A
x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup l' -> NoDup (set_inter l l')
Hl':NoDup l'
~ In x (set_inter l l') 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).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a x -> ~ set_In a y -> set_In a (set_diff x y)
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a x -> ~ set_In a y -> set_In a (set_diff x y)
    simple induction x.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall y : set,
set_In a nil ->
~ set_In a y -> set_In a (set_diff nil y)
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(forall y : set,
 set_In a l -> ~ set_In a y -> set_In a (set_diff l y)) ->
forall y : set,
set_In a (a0 :: l) ->
~ set_In a y -> set_In a (set_diff (a0 :: l) y)
    simpl; tauto.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(forall y : set,
 set_In a l -> ~ set_In a y -> set_In a (set_diff l y)) ->
forall y : set,
set_In a (a0 :: l) ->
~ set_In a y -> set_In a (set_diff (a0 :: l) y)
    simpl; intros a0 l Hrec y [Ha0a| Hal] Hay.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
~ set_In a y0 -> set_In a (set_diff l y0)
y:set
Ha0a:a0 = a
Hay:~ set_In a y
set_In a
  (if set_mem a0 y
   then set_diff l y
   else set_add a0 (set_diff l y))
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
~ set_In a y0 -> set_In a (set_diff l y0)
y:set
Hal:set_In a l
Hay:~ set_In a y
set_In a
  (if set_mem a0 y
   then set_diff l y
   else set_add a0 (set_diff l y))
    rewrite Ha0a; generalize (set_mem_complete2 _ _ Hay).A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
~ set_In a y0 -> set_In a (set_diff l y0)
y:set
Ha0a:a0 = a
Hay:~ set_In a y
set_mem a y = false ->
set_In a
  (if set_mem a y
   then set_diff l y
   else set_add a (set_diff l y))
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
~ set_In a y0 -> set_In a (set_diff l y0)
y:set
Hal:set_In a l
Hay:~ set_In a y
set_In a
  (if set_mem a0 y
   then set_diff l y
   else set_add a0 (set_diff l y))
    elim (set_mem a y);
     [ intro Habs; discriminate Habs | auto with datatypes ].A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a l ->
~ set_In a y0 -> set_In a (set_diff l y0)
y:set
Hal:set_In a l
Hay:~ set_In a y
set_In a
  (if set_mem a0 y
   then set_diff l y
   else set_add a0 (set_diff l y))
    elim (set_mem a0 y); auto with datatypes.
  Qed.

  Lemma set_diff_elim1 :
   forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a (set_diff x y) -> set_In a x
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a (set_diff x y) -> set_In a x
    simple induction x.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall y : set,
set_In a (set_diff nil y) -> set_In a nil
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(forall y : set, set_In a (set_diff l y) -> set_In a l) ->
forall y : set,
set_In a (set_diff (a0 :: l) y) -> set_In a (a0 :: l)
    simpl; tauto.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
forall (a0 : A) (l : list A),
(forall y : set, set_In a (set_diff l y) -> set_In a l) ->
forall y : set,
set_In a (set_diff (a0 :: l) y) -> set_In a (a0 :: l)
    simpl; intros a0 l Hrec y; elim (set_mem a0 y).A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_diff l y0) -> set_In a l
y:set
set_In a (set_diff l y) -> a0 = a \/ set_In a l
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_diff l y0) -> set_In a l
y:set
set_In a (set_add a0 (set_diff l y)) ->
a0 = a \/ set_In a l
    eauto with datatypes.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_diff l y0) -> set_In a l
y:set
set_In a (set_add a0 (set_diff l y)) ->
a0 = a \/ set_In a l
    intro; generalize (set_add_elim _ _ _ H).A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x:set
a0:A
l:list A
Hrec:forall y0 : set,
set_In a (set_diff l y0) -> set_In a l
y:set
H:set_In a (set_add a0 (set_diff l y))
a = a0 \/ set_In a (set_diff l y) ->
a0 = a \/ set_In a l
    intros [H1| H2]; eauto with datatypes.
  Qed.

  Lemma set_diff_elim2 :
   forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x y : set),
set_In a (set_diff x y) -> ~ set_In a y
  intros a x y; elim x; simpl.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
False -> ~ set_In a y
A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
forall (a0 : A) (l : list A),
(set_In a (set_diff l y) -> ~ set_In a y) ->
set_In a
  (if set_mem a0 y
   then set_diff l y
   else set_add a0 (set_diff l y)) -> 
~ set_In a y
  intros; contradiction.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
forall (a0 : A) (l : list A),
(set_In a (set_diff l y) -> ~ set_In a y) ->
set_In a
  (if set_mem a0 y
   then set_diff l y
   else set_add a0 (set_diff l y)) -> ~ set_In a y
  intros a0 l Hrec.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
a0:A
l:list A
Hrec:set_In a (set_diff l y) -> ~ set_In a y
set_In a
  (if set_mem a0 y
   then set_diff l y
   else set_add a0 (set_diff l y)) -> ~ set_In a y
  apply set_mem_ind2; auto.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
a0:A
l:list A
Hrec:set_In a (set_diff l y) -> ~ set_In a y
~ set_In a0 y ->
set_In a (set_add a0 (set_diff l y)) -> ~ set_In a y
  intros H1 H2; case (set_add_elim _ _ _ H2); intros; auto.A:Type
Aeq_dec:forall x0 y0 : A, {x0 = y0} + {x0 <> y0}
a:A
x, y:set
a0:A
l:list A
Hrec:set_In a (set_diff l y) -> ~ set_In a y
H1:~ set_In a0 y
H2:set_In a (set_add a0 (set_diff l y))
H:a = a0
~ set_In a y
  rewrite H; trivial.
  Qed.

  Lemma set_diff_iff a l l' : In a (set_diff l l') <-> In a l /\ ~In a l'.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a (set_diff l l') <-> In a l /\ ~ In a l'
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a (set_diff l l') <-> In a l /\ ~ In a l'
  split.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a (set_diff l l') -> In a l /\ ~ In a l'
A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a l /\ ~ In a l' -> In a (set_diff l l')
  -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a (set_diff l l') -> In a l /\ ~ In a l' split; [eapply set_diff_elim1 | eapply set_diff_elim2]; eauto.
  -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
In a l /\ ~ In a l' -> In a (set_diff l l') destruct 1.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':set
H:In a l
H0:~ In a l'
In a (set_diff l l') now apply set_diff_intro.
  Qed.

  Lemma set_diff_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_diff l l').A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
NoDup l -> NoDup l' -> NoDup (set_diff l l')
  Proof.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
NoDup l -> NoDup l' -> NoDup (set_diff l l')
   induction 1 as [|x l H H' IH]; intro Hl'; simpl.A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
l':list A
Hl':NoDup l'
NoDup nil
A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
l':list A
x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup l' -> NoDup (set_diff l l')
Hl':NoDup l'
NoDup
  (if set_mem x l'
   then set_diff l l'
   else set_add x (set_diff l l'))
   -A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
l':list A
Hl':NoDup l'
NoDup nil constructor.
   -A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
l':list A
x:A
l:list A
H:~ In x l
H':NoDup l
IH:NoDup l' -> NoDup (set_diff l l')
Hl':NoDup l'
NoDup
  (if set_mem x l'
   then set_diff l l'
   else set_add x (set_diff l l')) 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).A:Type
Aeq_dec:forall x y : A, {x = y} + {x <> y}
forall (a : A) (x : set), ~ set_In a (set_diff x x)
  red; intros a x H.A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
H:set_In a (set_diff x x)
False
  apply (set_diff_elim2 _ _ _ H).A:Type
Aeq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
x:set
H:set_In a (set_diff x x)
set_In a x
  apply (set_diff_elim1 _ _ _ H).
  Qed.

Hint Resolve set_diff_intro set_diff_trivial : core.


End first_definitions.

Section other_definitions.

  Definition set_prod : forall {A B:Type}, set A -> set B -> set (A * B) :=
    list_prod.

B^A, set of applications from A to B

  Definition set_power : forall {A B:Type}, set A -> set B -> set (set (A * B)) :=
    list_power.

  Definition set_fold_left {A B:Type} : (B -> A -> B) -> set A -> B -> B :=
    fold_left (A:=B) (B:=A).

  Definition set_fold_right {A B:Type} (f:A -> B -> B) (x:set A)
    (b:B) : B := fold_right f b x.

  Definition set_map {A B:Type} (Aeq_dec : forall x y:B, {x = y} + {x <> y})
    (f : A -> B) (x : set A) : set B :=
    set_fold_right (fun a => set_add Aeq_dec (f a)) x (empty_set B).

End other_definitions.

Unset Implicit Arguments.