(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                                ListSet.v                                 *)
(****************************************************************************)

(* A Library for finite sets, implemented as lists *)
(* A Library with similar interface will soon be available under
  the name TreeSet in the theories/TREES directory *)

(* PolyList is loaded, but not exported *)
(* This allow to "hide" the definitions, functions and theorems of PolyList
 and to see only the ones of ListSet *)
Require Import List.

Set Implicit Arguments.
Unset Strict Implicit.
Section first_definitions.


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

Definition set := list A.

Definition empty_set := nil (A:=A). 
 
  Fixpoint set_add (a : A) (x : set) {struct x} : 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) {struct x} : 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 *) 
  Fixpoint set_remove (a : A) (x : set) {struct x} : set :=
    match x with
    | nil => empty_set
    | a1 :: x1 =>
        match Aeq_dec a a1 with
        | left _ => set_remove a x1
        | right _ => a1 :: set_remove a x1
        end
    end.
 
  Fixpoint set_inter (x : set) : set -> set :=
    match x with
    | nil => fun y => nil (A:=A)
    | 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) {struct y} : 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 : set) : set -> set :=
    fun y =>
    match x with
    | nil => nil (A:=A)
    | a1 :: x1 =>
        if set_mem a1 y then set_diff x1 y else set_add a1 (set_diff x1 y)
    end. 
    
  (**  
  Inductive set_In : A -> set -> Prop := 
    set_In_singl : (a:A)(x:set)(set_In a (cons a (nil A)))  
  | set_In_add : (a,b:A)(x:set)(set_In a x)->(set_In a (set_add b x)) 
  . 
  **) 
 
  Definition set_In : A -> set -> Prop := In (A:=A). 
 
Lemma Set_remove1 : forall (B : set) (x : A), ~ set_In x (set_remove x B). 
(* Goal: forall (B : set) (x : A), not (set_In x (set_remove x B)) *)
intro; intro. 
induction  B as [| a B HrecB]. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
auto. 
 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
simpl in |- *. 
(* Goal: not (set_In x (if Aeq_dec x a then set_remove x B else @cons A a (set_remove x B))) *)
elim (Aeq_dec x a). 
(* Goal: forall _ : and (@eq A a x) (not (@eq A a x)), False *)
(* Goal: and (@eq A a x) (not (@eq A a x)) *)
(* Goal: forall _ : set_In x (set_remove x B), False *)
intro. 
(* Goal: not (set_In x (@cons A a (set_remove x B))) *)
unfold not in |- *. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
unfold not in HrecB. 
(* Goal: forall _ : and (@eq A a x) (not (@eq A a x)), False *)
(* Goal: and (@eq A a x) (not (@eq A a x)) *)
(* Goal: forall _ : set_In x (set_remove x B), False *)
intro. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
apply HrecB; auto. 
 
(* Goal: forall _ : and (@eq A a x) (not (@eq A a x)), False *)
(* Goal: and (@eq A a x) (not (@eq A a x)) *)
(* Goal: forall _ : set_In x (set_remove x B), False *)
intro. 
(* Goal: not (set_In x (@cons A a (set_remove x B))) *)
unfold not in |- *. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
unfold not in HrecB. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
simpl in |- *. 
(* Goal: forall _ : and (@eq A a x) (not (@eq A a x)), False *)
(* Goal: and (@eq A a x) (not (@eq A a x)) *)
(* Goal: forall _ : set_In x (set_remove x B), False *)
intro. 
(* Goal: forall _ : not (@eq A a a0), sumbool (@In A a (@cons A a0 l)) (not (@In A a (@cons A a0 l))) *)
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
elim H. 
(* Goal: forall _ : and (@eq A a x) (not (@eq A a x)), False *)
(* Goal: and (@eq A a x) (not (@eq A a x)) *)
(* Goal: forall _ : set_In x (set_remove x B), False *)
intro. 
(* Goal: False *)
(* Goal: forall _ : set_In x (set_remove x B), False *)
cut (a = x /\ a <> x). 
(* Goal: forall _ : and (@eq A a x) (not (@eq A a x)), False *)
(* Goal: and (@eq A a x) (not (@eq A a x)) *)
(* Goal: forall _ : set_In x (set_remove x B), False *)
intro. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
auto. 
 
(* Goal: and (@eq A a x) (not (@eq A a x)) *)
(* Goal: forall _ : set_In x (set_remove x B), False *)
split. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
auto. 
 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
auto. 
 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
auto. 
 
Qed. 
 
 
 
Lemma set_In_dec : forall (a : A) (x : set), {set_In a x} + {~ set_In a x}. 

(* Goal: forall (a b : A) (x : set) (_ : set_In a (set_add b x)), or (@eq A a b) (set_In a x) *)
unfold set_In in |- *.
(* Goal: forall (a : A) (x y : set) (_ : set_In a (set_diff x y)), set_In a x *)
simple induction x.
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
auto.

(* Goal: forall (a0 : A) (l : list A) (_ : forall _ : set_In a (set_union x l), or (set_In a x) (set_In a l)) (_ : set_In a (set_add a0 (set_union x l))), or (set_In a x) (or (@eq A a0 a) (set_In a l)) *)
intros.
(* Goal: sumbool (@In A a (@cons A a0 l)) (not (@In A a (@cons A a0 l))) *)
cut ({a = a0} + {a <> a0}).
(* Goal: forall _ : sumbool (@eq A a a0) (not (@eq A a a0)), sumbool (@In A a (@cons A a0 l)) (not (@In A a (@cons A a0 l))) *)
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
intro Eq_dec; elim Eq_dec.
(* Goal: forall _ : @eq A a a0, sumbool (@In A a (@cons A a0 l)) (not (@In A a (@cons A a0 l))) *)
(* Goal: forall _ : not (@eq A a a0), sumbool (@In A a (@cons A a0 l)) (not (@In A a (@cons A a0 l))) *)
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
intro Eq; rewrite Eq; left; auto with datatypes.

(* Goal: forall _ : not (@eq A a a0), sumbool (@In A a (@cons A a0 l)) (not (@In A a (@cons A a0 l))) *)
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
elim H.
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
auto with datatypes.

(* Goal: forall _ : and (@eq A a x) (not (@eq A a x)), False *)
(* Goal: and (@eq A a x) (not (@eq A a x)) *)
(* Goal: forall _ : set_In x (set_remove x B), False *)
unfold not in |- *; intros; right; intro.
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
elim H0; auto.

(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
auto.

Qed.


  Lemma set_mem_ind :
   forall (B : Set) (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. 
(* Goal: forall (a0 : A) (l : list A) (_ : forall _ : set_In a (set_union x l), or (set_In a x) (set_In a l)) (_ : set_In a (set_add a0 (set_union x l))), or (set_In a x) (or (@eq A a0 a) (set_In a l)) *)
    simple induction x; simpl in |- *; intros. 
(* Goal: P z *)
(* Goal: P (if if Aeq_dec a a0 then true else set_mem a l then y else z) *)
    assumption. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    elim (Aeq_dec a a0); auto with datatypes. 
  Qed. 
 
  Lemma set_mem_correct1 :
   forall (a : A) (x : set), set_mem a x = true -> set_In a x. 
  Proof. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
    simple induction x; simpl in |- *. 
(* Goal: not (@eq set (@cons A a (@nil A)) empty_set) *)
(* Goal: forall (a0 : A) (l : list A) (_ : not (@eq set (set_add a l) empty_set)), not (@eq set (if Aeq_dec a a0 then @cons A a0 l else @cons A a0 (set_add a l)) empty_set) *)
    discriminate. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 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. 
  Proof. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
    simple induction x; simpl in |- *. 
(* Goal: forall _ : False, @eq bool false true *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall _ : set_In a l, @eq bool (set_mem a l) true) (_ : or (@eq A a0 a) (set_In a l)), @eq bool (if Aeq_dec a a0 then true else set_mem a l) true *)
    intro Ha; elim Ha. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    intros a0 l; elim (Aeq_dec a a0); auto with datatypes. 
(* Goal: forall (_ : not (@eq A a a0)) (_ : forall _ : set_In a l, @eq bool (set_mem a l) true) (_ : or (@eq A a0 a) (set_In a l)), @eq bool (set_mem a l) true *)
    intros H1 H2 [H3| H4]. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    absurd (a0 = a); auto with datatypes. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    auto with datatypes. 
  Qed. 
 
  Lemma set_mem_complete1 :
   forall (a : A) (x : set), set_mem a x = false -> ~ set_In a x. 
  Proof. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
    simple induction x; simpl in |- *. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
    tauto. 
(* Goal: forall (a0 : A) (l : list A) (_ : forall _ : not (set_In a l), @eq bool (set_mem a l) false) (_ : not (or (@eq A a0 a) (set_In a l))), @eq bool (if Aeq_dec a a0 then true else set_mem a l) false *)
    intros a0 l; elim (Aeq_dec a a0). 
(* Goal: forall (_ : @eq A a a0) (_ : forall _ : @eq bool (set_mem a l) false, not (set_In a l)) (_ : @eq bool true false), not (or (@eq A a0 a) (set_In a l)) *)
(* Goal: forall (_ : not (@eq A a a0)) (_ : forall _ : @eq bool (set_mem a l) false, not (set_In a l)) (_ : @eq bool (set_mem a l) false), not (or (@eq A a0 a) (set_In a l)) *)
    intros; discriminate H0. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    unfold not in |- *; intros; elim H1; auto with datatypes. 
  Qed. 
 
  Lemma set_mem_complete2 :
   forall (a : A) (x : set), ~ set_In a x -> set_mem a x = false. 
  Proof. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
    simple induction x; simpl in |- *. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
    tauto. 
(* Goal: forall (a0 : A) (l : list A) (_ : forall _ : not (set_In a l), @eq bool (set_mem a l) false) (_ : not (or (@eq A a0 a) (set_In a l))), @eq bool (if Aeq_dec a a0 then true else set_mem a l) false *)
    intros a0 l; elim (Aeq_dec a a0). 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    intros; elim H0; auto with datatypes. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
    tauto. 
  Qed. 
 
  Lemma set_add_intro1 :
   forall (a b : A) (x : set), set_In a x -> set_In a (set_add b x). 
 
  Proof. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
    unfold set_In in |- *; simple induction x; simpl in |- *. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    auto with datatypes. 
(* Goal: forall (a0 : A) (l : list A) (_ : forall _ : @In A a l, @In A a (set_add b l)) (_ : or (@eq A a0 a) (@In A a l)), @In A a (if Aeq_dec b a0 then @cons A a0 l else @cons A a0 (set_add b l)) *)
    intros a0 l H [Ha0a| Hal]. 
(* Goal: P z *)
(* Goal: P (if if Aeq_dec a a0 then true else set_mem a l then y else z) *)
    elim (Aeq_dec b a0); left; assumption. 
(* Goal: @In A a (if Aeq_dec b a0 then @cons A a0 l else @cons A 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). 
 
  Proof. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
    unfold set_In in |- *; simple induction x; simpl in |- *. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    auto with datatypes. 
(* Goal: forall (a0 : A) (l : list A) (_ : forall _ : @eq A a b, @In A a (set_add b l)) (_ : @eq A a b), @In A a (if Aeq_dec b a0 then @cons A a0 l else @cons A a0 (set_add b l)) *)
    intros a0 l H Hab. 
    elim (Aeq_dec b a0);
     [ rewrite Hab; intro Hba0; rewrite Hba0; simpl in |- *;
        auto with datatypes
     | auto with datatypes ]. 
  Qed. 
 
  Hint Resolve set_add_intro1 set_add_intro2 Set_remove1. 
 
 
 
  Lemma set_add_intro :
   forall (a b : A) (x : set), a = b \/ set_In a x -> set_In a (set_add b x). 
   
  Proof. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    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. 
 
  Proof. 
(* Goal: forall (a b : A) (x : set) (_ : set_In a (set_add b x)), or (@eq A a b) (set_In a x) *)
    unfold set_In in |- *. 
(* Goal: forall (a : A) (x y : set) (_ : set_In a (set_diff x y)), set_In a x *)
    simple induction x. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    simpl in |- *; intros [H1| H2]; auto with datatypes. 
(* Goal: forall _ : and (@eq A a x) (not (@eq A a x)), False *)
(* Goal: and (@eq A a x) (not (@eq A a x)) *)
(* Goal: forall _ : set_In x (set_remove x B), False *)
    simpl in |- *; do 3 intro. 
(* Goal: forall _ : @In A a (if Aeq_dec b a0 then @cons A a0 l else @cons A a0 (set_add b l)), or (@eq A a b) (or (@eq A a0 a) (@In A a l)) *)
    elim (Aeq_dec b a0). 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
    tauto. 
(* Goal: forall (_ : not (@eq A b a0)) (_ : @In A a (@cons A a0 (set_add b l))), or (@eq A a b) (or (@eq A a0 a) (@In A a l)) *)
    simpl in |- *; intros; elim H0. 
(* Goal: forall _ : @eq A a0 a, or (@eq A a b) (or (@eq A a0 a) (@In A a l)) *)
(* Goal: forall _ : @In A a (set_add b l), or (@eq A a b) (or (@eq A a0 a) (@In A a l)) *)
    trivial with datatypes. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
    tauto. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
    tauto. 
  Qed. 
 
  Hint Resolve set_add_intro set_add_elim. 
 
  Lemma set_add_not_empty :
   forall (a : A) (x : set), set_add a x <> empty_set. 
  Proof. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
    simple induction x; simpl in |- *. 
(* Goal: not (@eq set (@cons A a (@nil A)) empty_set) *)
(* Goal: forall (a0 : A) (l : list A) (_ : not (@eq set (set_add a l) empty_set)), not (@eq set (if Aeq_dec a a0 then @cons A a0 l else @cons A a0 (set_add a l)) empty_set) *)
    discriminate. 
(* Goal: not (@eq set (@cons A a (@nil A)) empty_set) *)
(* Goal: forall (a0 : A) (l : list A) (_ : not (@eq set (set_add a l) empty_set)), not (@eq set (if Aeq_dec a a0 then @cons A a0 l else @cons A a0 (set_add a l)) empty_set) *)
    intros; elim (Aeq_dec a a0); intros; discriminate. 
  Qed.    
 
 
  Lemma set_union_intro1 :
   forall (a : A) (x y : set), set_In a x -> set_In a (set_union x y). 
  Proof. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    simple induction y; simpl in |- *; 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). 
  Proof. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
    simple induction y; simpl in |- *. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
    tauto. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    intros; elim H0; auto with datatypes. 
  Qed. 
 
  Hint Resolve set_union_intro2 set_union_intro1. 
 
  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). 
  Proof. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    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. 
  Proof. 
(* Goal: forall _ : set_In x (@cons A a (set_remove x B)), False *)
    simple induction y; simpl in |- *. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    auto with datatypes. 
(* Goal: forall (a0 : A) (l : list A) (_ : forall _ : set_In a (set_union x l), or (set_In a x) (set_In a l)) (_ : set_In a (set_add a0 (set_union x l))), or (set_In a x) (or (@eq A a0 a) (set_In a l)) *)
    intros. 
(* Goal: or (set_In a x) (or (@eq A a0 a) (set_In a l)) *)
    generalize (set_add_elim H0). 
(* Goal: forall _ : or (@eq A a a0) (set_In a (set_union x l)), or (set_In a x) (or (@eq A a0 a) (set_In a l)) *)
    intros [H1| H1]. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    auto with datatypes. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
    tauto. 
  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). 
  Proof. 
(* Goal: forall (a : A) (x y : set) (_ : set_In a (set_diff x y)), set_In a x *)
    simple induction x. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    auto with datatypes. 
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a l) (_ : set_In a y), set_In a (set_inter l y)) (y : set) (_ : set_In a (@cons A a0 l)) (_ : set_In a y), set_In a (set_inter (@cons A a0 l) y) *)
    simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hy. 
(* Goal: set_In a (if set_mem a0 y then @cons A a0 (set_inter l y) else set_inter l y) *)
(* Goal: set_In a (if set_mem a0 y then @cons A a0 (set_inter l y) else set_inter l y) *)
    simpl in |- *; rewrite Ha0a. 
(* Goal: set_In a (if set_mem a y then @cons A a (set_inter l y) else set_inter l y) *)
(* Goal: set_In a (if set_mem a0 y then @cons A a0 (set_inter l y) else set_inter l y) *)
    generalize (set_mem_correct1 (a:=a) (x:=y)). 
(* Goal: forall _ : forall _ : @eq bool (set_mem a y) true, set_In a y, set_In a (if set_mem a y then @cons A a (set_inter l y) else set_inter l y) *)
(* Goal: set_In a (if set_mem a0 y then @cons A a0 (set_inter l y) else set_inter l y) *)
    generalize (set_mem_complete1 (a:=a) (x:=y)). 
(* Goal: forall (a0 : A) (l : list A) (_ : forall _ : set_In a (set_union x l), or (set_In a x) (set_In a l)) (_ : set_In a (set_add a0 (set_union x l))), or (set_In a x) (or (@eq A a0 a) (set_In a l)) *)
    elim (set_mem a y); simpl in |- *; intros. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    auto with datatypes. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    absurd (set_In a y); auto with datatypes. 
(* Goal: set_In a (if set_mem a0 y then @cons A 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. 
  Proof. 
(* Goal: forall (a : A) (x y : set) (_ : set_In a (set_diff x y)), set_In a x *)
    simple induction x. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    auto with datatypes. 
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a y) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a y *)
    simpl in |- *; intros a0 l Hrec y. 
(* Goal: forall _ : set_In a (if set_mem a0 y then @cons A a0 (set_inter l y) else set_inter l y), set_In a y *)
    generalize (set_mem_correct1 (a:=a0) (x:=y)). 
(* Goal: forall (a0 : A) (l : list A) (_ : forall _ : set_In a (set_union x l), or (set_In a x) (set_In a l)) (_ : set_In a (set_add a0 (set_union x l))), or (set_In a x) (or (@eq A a0 a) (set_In a l)) *)
    elim (set_mem a0 y); simpl in |- *; intros. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    elim H0; eauto with datatypes. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 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. 
  Proof. 
(* Goal: forall (a : A) (x y : set) (_ : set_In a (set_diff x y)), set_In a x *)
    simple induction x. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
    unfold set_In, set_inter in |- *; unfold In in |- *; tauto.
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a y) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a y *)
    simpl in |- *; intros a0 l Hrec y. 
(* Goal: forall _ : set_In a (if set_mem a0 y then @cons A a0 (set_inter l y) else set_inter l y), set_In a y *)
    generalize (set_mem_correct1 (a:=a0) (x:=y)). 
(* Goal: forall (a0 : A) (l : list A) (_ : forall _ : set_In a (set_union x l), or (set_In a x) (set_In a l)) (_ : set_In a (set_add a0 (set_union x l))), or (set_In a x) (or (@eq A a0 a) (set_In a l)) *)
    elim (set_mem a0 y); simpl in |- *; intros. 
    elim H0;
     [ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ]. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    eauto with datatypes. 
  Qed. 
 
  Hint Resolve set_inter_elim1 set_inter_elim2. 
 
  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. 
  Proof. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    eauto with datatypes. 
  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). 
  Proof. 
(* Goal: forall (a : A) (x y : set) (_ : set_In a (set_diff x y)), set_In a x *)
    simple induction x. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
    tauto. 
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a l) (_ : not (set_In a y)), set_In a (set_diff l y)) (y : set) (_ : set_In a (@cons A a0 l)) (_ : not (set_In a y)), set_In a (set_diff (@cons A a0 l) y) *)
    simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hay. 
(* Goal: set_In a (if set_mem a0 y then set_diff l y else set_add a0 (set_diff l y)) *)
(* Goal: 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). 
    elim (set_mem a y);
     [ intro Habs; discriminate Habs | auto with datatypes ]. 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    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. 
  Proof. 
(* Goal: forall (a : A) (x y : set) (_ : set_In a (set_diff x y)), set_In a x *)
    simple induction x. 
(* Goal: sumbool (@eq A a a0) (not (@eq A a a0)) *)
    tauto. 
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_diff l y)), set_In a l) (y : set) (_ : set_In a (set_diff (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    simpl in |- *; intros a0 l Hrec y; elim (set_mem a0 y). 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    eauto with datatypes. 
(* Goal: forall _ : set_In a (set_add a0 (set_diff l y)), or (@eq A a0 a) (set_In a l) *)
    intro; generalize (set_add_elim H). 
(* Goal: forall (y : set) (_ : set_In a (set_inter (@nil A) y)), set_In a (@nil A) *)
(* Goal: forall (a0 : A) (l : list A) (_ : forall (y : set) (_ : set_In a (set_inter l y)), set_In a l) (y : set) (_ : set_In a (set_inter (@cons A a0 l) y)), set_In a (@cons A a0 l) *)
    intros [H1| H2]; eauto with datatypes. 
  Qed. 
 
End first_definitions. 
 
Section other_definitions. 
 
  Variable A B : Set. 
 
  Definition set_prod : set A -> set B -> set (A * B) :=
    list_prod (A:=A) (B:=B). 
 
  (* B^A, set of applications from A to B *) 
  Definition set_power : set A -> set B -> set (set (A * B)) :=
    list_power (A:=A) (B:=B). 
 
  Definition set_map : (A -> B) -> set A -> set B := map (A:=A) (B:=B). 
 
  Definition set_fold_left : (B -> A -> B) -> set A -> B -> B :=
    fold_left (A:=B) (B:=A). 
 
  Definition set_fold_right (f : A -> B -> B) (x : set A) 
    (b : B) : B := fold_right f b x. 
 
  
End other_definitions. 
 
Set Strict Implicit.
Unset Implicit Arguments. 

 