Require Export List. 
Require Export ListSet. 
Set Implicit Arguments.
Unset Strict Implicit. 
 
(*********************************************************************) 
(*                  Some List Functions                              *) 
(*********************************************************************) 

Definition front (A : Set) (l : list A) : list A := rev (tail (rev l)). 
 
Definition last (A : Set) (l : list A) := head (rev l). 
 
Fixpoint take (A : Set) (n : nat) (l : list A) {struct l} : 
 list A :=
  match l with
  | nil => nil (A:=A)
  | a :: l' => match n with
               | O => nil (A:=A)
               | S m => a :: take m l'
               end
  end. 

Fixpoint allunique (A : Set) (l : list A) {struct l} : Prop :=
  match l with
  | nil => True
  | x :: l' => IF In x l' then False else allunique l'
  end. 
 
(*********************************************************************) 
(*                  Some Functions for ListSet                       *) 
(*********************************************************************) 
 
Definition IsEmpty (A : Set) (B : set A) := forall x : A, ~ set_In x B. 
 
Definition Included (A : Set) (B C : set A) :=
  forall x : A, set_In x B -> set_In x C. 
 
Lemma AllWaysIncluded : forall (A : Set) (B : set A), Included B B. 
(* Goal: forall (a : A) (b : B) (a0 : A) (b0 : B), sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intros. 
(* Goal: @Included A B B *)
unfold Included in |- *. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
Qed. 
 
(*********************************************************************) 
(*                  Some Results about ListSet                       *) 
(*********************************************************************) 
Section ListSetLemmas. 
 
Variable A : Set. 
 
Hypothesis Aeq_dec : forall x y : A, {x = y} + {x <> y}. 
 
Lemma Set_union1 :
 forall (B C : set A) (x : A),
 set_In x (set_union Aeq_dec B C) -> ~ set_In x B -> set_In x C. 
(* Goal: forall (a : A) (b : B) (a0 : A) (b0 : B), sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intros. 
(* Goal: or (@set_In A x C) (@set_In A x B) *)
cut (set_In x B \/ set_In x C). 
(* Goal: forall _ : or (@set_In A x B) (@set_In A x C), @set_In A x C *)
(* Goal: or (@set_In A x B) (@set_In A x C) *)
intro H1; elim H1. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
tauto. 
 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
eapply (set_union_elim (Aeq_dec:=Aeq_dec)); auto. 
 
Qed. 
 
Lemma Set_union2 :
 forall (B C : set A) (x : A),
 set_In x (set_union Aeq_dec B C) -> set_In x (set_union Aeq_dec C B). 
(* Goal: forall (a : A) (b : B) (a0 : A) (b0 : B), sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intros. 
(* Goal: @set_In A x (@set_union A Aeq_dec C B) *)
cut (set_In x C \/ set_In x B). 
(* Goal: forall _ : or (@set_In A x C) (@set_In A x B), @set_In A x (@set_union A Aeq_dec C B) *)
(* Goal: or (@set_In A x C) (@set_In A x B) *)
intro; apply set_union_intro. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
(* Goal: or (@set_In A x C) (@set_In A x B) *)
cut (set_In x B \/ set_In x C). 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
tauto. 
 
(* Goal: or (@set_In A x B) (@set_In A x C) *)
eapply (set_union_elim (Aeq_dec:=Aeq_dec)). 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
Qed. 
 
 
Lemma Set_remove2 :
 forall (B : set A) (x y : A),
 set_In x (set_remove Aeq_dec y B) -> set_In x B. 
(* Goal: forall (B : set A) (x y : A) (_ : @set_In A x (@set_remove A Aeq_dec y B)), @set_In A x B *)
intro; intro; intro. 
induction  B as [| a B HrecB]. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
(* Goal: forall (_ : not (@eq A y a)) (_ : @set_In A x (@cons A a (@set_remove A Aeq_dec y B))), or (@eq A a x) (@set_In A x B) *)
simpl in |- *. 
(* Goal: forall _ : @set_In A x (if Aeq_dec y a then @set_remove A Aeq_dec y B else @cons A a (@set_remove A Aeq_dec y B)), or (@eq A a x) (@set_In A x B) *)
elim (Aeq_dec y a). 
(* Goal: forall (a : A) (b : B) (a0 : A) (b0 : B), sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intros. 
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
right. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
(* Goal: forall (_ : not (@eq A y a)) (_ : @set_In A x (@cons A a (@set_remove A Aeq_dec y B))), or (@eq A a x) (@set_In A x B) *)
simpl in |- *. 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: or (@eq A a x) (@set_In A x B) *)
elim H. 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
left; auto. 
 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
right. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
Qed. 
 
 
Lemma Set_add1 :
 forall (B : set A) (x y : A),
 set_In x (set_add Aeq_dec y B) -> x <> y -> set_In x B. 
(* Goal: forall (a : A) (b : B) (a0 : A) (b0 : B), sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intros. 
(* Goal: @set_In A x B *)
cut (x = y \/ set_In x B). 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: @set_In A x B *)
(* Goal: or (@eq A x y) (@set_In A x B) *)
elim H1. 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: @set_In A x B *)
(* Goal: forall _ : @set_In A x B, @set_In A x B *)
(* Goal: or (@eq A x y) (@set_In A x B) *)
absurd (x = y). 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
(* Goal: or (@eq A x y) (@set_In A x B) *)
eapply (set_add_elim (A:=A) (Aeq_dec:=Aeq_dec) (a:=x) (b:=y) (x:=B)). 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
Qed. 
 
 
Lemma Set_add2 :
 forall (B : set A) (x y : A),
 x <> y -> ~ set_In x B -> ~ set_In x (set_add Aeq_dec y B). 
(* Goal: forall (a : A) (b : B) (a0 : A) (b0 : B), sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intros. 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: False *)
apply H0. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
eapply (Set_add1 (B:=B) (x:=x) (y:=y)); auto. 
 
Qed. 
 
End ListSetLemmas. 
 
Hint Unfold IsEmpty Included. 
Hint Resolve Set_remove2 Set_add1 AllWaysIncluded Set_union1 Set_union2
  Set_add2. 
 
 
 
Lemma Listeq_dec :
 forall A : Set,
 (forall a b : A, {a = b} + {a <> b}) ->
 forall x y : list A, {x = y} + {x <> y}. 
(* Goal: forall (A : Set) (_ : forall a b : A, sumbool (@eq A a b) (not (@eq A a b))) (x y : list A), sumbool (@eq (list A) x y) (not (@eq (list A) x y)) *)
simple induction x. 
(* Goal: forall y : list A, sumbool (@eq (list A) (@nil A) y) (not (@eq (list A) (@nil A) y)) *)
(* Goal: forall (a : A) (l : list A) (_ : forall y : list A, sumbool (@eq (list A) l y) (not (@eq (list A) l y))) (y : list A), sumbool (@eq (list A) (@cons A a l) y) (not (@eq (list A) (@cons A a l) y)) *)
simple induction y. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
(* Goal: forall (a : A) (b : B) (a0 : A) (b0 : B), sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intros. 
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
right. 
(* Goal: not (@eq (list A) (@nil A) (@cons A a l)) *)
(* Goal: forall (a : A) (l : list A) (_ : forall y : list A, sumbool (@eq (list A) l y) (not (@eq (list A) l y))) (y : list A), sumbool (@eq (list A) (@cons A a l) y) (not (@eq (list A) (@cons A a l) y)) *)
unfold not in |- *; intro D; discriminate D. 
 
(* Goal: forall (a : A) (b : B) (a0 : A) (b0 : B), sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intros. 
induction  y as [| a0 y Hrecy]. 
(* Goal: not (@eq (list A) (@nil A) (@cons A a l)) *)
(* Goal: forall (a : A) (l : list A) (_ : forall y : list A, sumbool (@eq (list A) l y) (not (@eq (list A) l y))) (y : list A), sumbool (@eq (list A) (@cons A a l) y) (not (@eq (list A) (@cons A a l) y)) *)
right; unfold not in |- *; intro D; discriminate D. 
 
(* Goal: sumbool (@eq (list A) (@cons A a l) (@cons A a0 y)) (not (@eq (list A) (@cons A a l) (@cons A a0 y))) *)
elim (H0 y). 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
rewrite a1. 
(* Goal: sumbool (@eq (list A) (@cons A a y) (@cons A a0 y)) (not (@eq (list A) (@cons A a y) (@cons A a0 y))) *)
(* Goal: forall _ : not (@eq (list A) l y), sumbool (@eq (list A) (@cons A a l) (@cons A a0 y)) (not (@eq (list A) (@cons A a l) (@cons A a0 y))) *)
elim (H a a0). 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
rewrite a2. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
left; auto. 
 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
right. 
(* Goal: not (@eq (list A) (@cons A a y) (@cons A a0 y)) *)
(* Goal: forall _ : not (@eq (list A) l y), sumbool (@eq (list A) (@cons A a l) (@cons A a0 y)) (not (@eq (list A) (@cons A a l) (@cons A a0 y))) *)
unfold not in |- *. 
(* Goal: forall _ : @eq (list A) (@cons A a y) (@cons A a0 y), False *)
(* Goal: forall _ : not (@eq (list A) l y), sumbool (@eq (list A) (@cons A a l) (@cons A a0 y)) (not (@eq (list A) (@cons A a l) (@cons A a0 y))) *)
unfold not in b. 
(* Goal: forall _ : @eq (list A) (@cons A a l) (@cons A a0 y), False *)
intro; apply b. 
(* Goal: @eq (list A) l y *)
injection H1. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
unfold not in |- *; intro. 
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
right. 
(* Goal: forall _ : @eq (list A) (@cons A a l) (@cons A a0 y), False *)
intro; apply b. 
(* Goal: @eq (list A) l y *)
injection H1. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
auto. 
 
Qed. 
 
Hint Resolve Listeq_dec. 
 
 
Lemma Prodeq_dec :
 forall A B : Set,
 (forall x y : A, {x = y} + {x <> y}) ->
 (forall v w : B, {v = w} + {v <> w}) ->
 forall c d : A * B, {c = d} + {c <> d}. 
(* Goal: forall (a : A) (b : B) (a0 : A) (b0 : B), sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intros. 
(* Goal: sumbool (@eq (prod A B) c d) (not (@eq (prod A B) c d)) *)
elim c. 
(* Goal: forall (a : A) (b : B), sumbool (@eq (prod A B) (@pair A B a b) d) (not (@eq (prod A B) (@pair A B a b) d)) *)
elim d. 
(* Goal: forall (a : A) (b : B) (a0 : A) (b0 : B), sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intros. 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
elim (H a a0); intro. 
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
rewrite a1. 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
elim (H0 b b0); intro. 
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
rewrite a2. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
left; auto. 
 
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b))) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
right. 
(* Goal: not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a0 b)) *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
intro. 
(* Goal: False *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
apply b1. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
injection H1; auto. 
 
(* Goal: False *)
(* Goal: sumbool (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b)) (not (@eq (prod A B) (@pair A B a0 b0) (@pair A B a b))) *)
right; intro; apply b1. 
(* Goal: forall (_ : @eq (list A) l y) (_ : @eq A a a0), @eq (list A) l y *)
injection H1; auto. 
 
Qed. 
 
Hint Resolve Prodeq_dec.