Require Export PolyList.
Require Export ListSet.
Implicit Arguments On.

The front portion of a list



Definition front [A:Set;l:(list A)]:(list A) :=
   (rev (tail (rev l))).

The last element of a list



Definition last [A:Set;l:(list A)] :=
   (head (rev l)).

The first n elements of a list

Fixpoint take [A:Set; n:nat; l:(list A)] : (list A) :=
   Cases l of
      |nil => (nil A)
      |(cons a l') => Cases n of
                        |O => (nil A)
                        |(S m) => (cons a (take m l'))
                      end
   end.








Some Functions for ListSet

Decides when a set is empty or not



Definition IsEmpty [A:Set; B:(set A)] :=
   (x:A)~(set_In x B).

The standard set inclusion operator

Definition Included [A:Set; B,C:(set A)] :=
   (x:A)(set_In x B)->(set_In x C).




Lemmas for the previously defined functions



Lemma AllWaysIncluded:
     (A:Set; B:(set A))(Included B B).
Intros.
Unfold Included.
Auto.

Qed.



Section ListSetLemmas.



Variable A:Set.



Hypothesis Aeq_dec : (x,y:A){x=y}+{~x=y}.



Lemma Set_union1:
 (B,C:(set A); x:A)
  (set_In x (set_union Aeq_dec B C))
  ->~(set_In x B)
  ->(set_In x C).
Intros.
Cut (set_In x B)\/(set_In x C).
Intro H1; Elim H1.
Tauto.

Auto.

EApply (set_union_elim 2!Aeq_dec); Auto.

Qed.



Lemma Set_union2:
 (B,C:(set A); x:A)
  (set_In x (set_union Aeq_dec B C))
  ->(set_In x (set_union Aeq_dec C B)).
Intros.
Cut (set_In x C)\/(set_In x B).
Intro; Apply set_union_intro.
Auto.

Cut (set_In x B)\/(set_In x C).
Tauto.

EApply (set_union_elim 2!Aeq_dec).
Auto.

Qed.



Lemma Set_remove2:
 (B:(set A); x,y:A)
     (set_In x (set_remove Aeq_dec y B))
     ->(set_In x B).
Intro; Intro; Intro.
Induction B.
Auto.

Simpl.
Elim (Aeq_dec y a).
Intros.
Right.
Auto.

Simpl.
Intro.
Intro.
Elim H.
Intro.
Left; Auto.

Intro.
Right.
Auto.
Qed.



Lemma Set_add1:
 (B:(set A); x,y:A)
      (set_In x (set_add Aeq_dec y B))->~x=y->(set_In x B).
Intros.
Cut x=y\/(set_In x B).
Intro.
Elim H1.
Intro.
Absurd x=y.
Auto.

Auto.

Intro.
Auto.

EApply (set_add_elim 1!A 2!Aeq_dec 3!x 4!y 5!B).
Auto.

Qed.



Lemma Set_add2:
 (B:(set A); x,y:A)
  ~x=y
  ->~(set_In x B)
  ->~(set_In x (set_add Aeq_dec y B)).
Intros.
Intro.
Apply H0.
EApply (Set_add1 1!B 2!x 3!y); Auto.

Qed.



End ListSetLemmas.



Hints Unfold IsEmpty Included.
Hints Resolve Set_remove2 Set_add1 AllWaysIncluded Set_union1
              Set_union2 Set_add2.




Lemma Listeq_dec:
 (A:Set)((a,b:A){a=b}+{~a=b})->(x,y:(list A)){x=y}+{~x=y}.
Induction x.
Induction y.
Auto.

Intros.
Right.
Unfold not; Intro D; Discriminate D.

Intros.
Induction y.
Right; Unfold not; Intro D; Discriminate D.

Elim (H0 y).
Intro.
Rewrite a1.
Elim (H a a0).
Intro.
Rewrite a2.
Left; Auto.

Intro.
Right.
Unfold not.
Unfold not in b.
Intro; Apply b.
Injection H1.
Auto.

Unfold not; Intro.
Right.
Intro; Apply b.
Injection H1.
Auto.

Qed.


Hints Resolve Listeq_dec.



Lemma Prodeq_dec: (A,B:Set)
                    ((x,y:A){x=y}+{~x=y})
                    ->((v,w:B){v=w}+{~v=w})
                    ->(c,d:A*B){c=d}+{~c=d}.
Intros.
Elim c.
Elim d.
Intros.
Elim (H a a0); Intro.
Rewrite a1.
Elim (H0 b b0); Intro.
Rewrite a2.
Left; Auto.

Right.
Intro.
Apply b1.
Injection H1; Auto.

Right; Intro; Apply b1.
Injection H1; Auto.

Qed.



Hints Resolve Prodeq_dec.