PolyListAux.v

(* Definition of rem a function that removes elt from polymorphic lists *)

Require Import Arith.
Require Import PolyList.
Section Auxrem.
Variable A:Set.
Variable ADec:(a, b:A){a=b}+{~ a=b}.

Theorem NotInCons1:
  (a, b:A) (L:(list A)) ~ (In a (cons b L)) ->~ (In a L).
Intros a b L H'; Red; Intros H'0; Apply H'; Simpl; Auto.
Qed.

Theorem map_id:
  (f:A ->A) ((x:A)(f (f x))=x) ->(L:(list A))(map f (map f L))=L.
Intros f H' L; Elim L; Simpl; Auto.
Intros a l H'0.
Rewrite H'; Rewrite H'0; Auto.
Qed.

Fixpoint rem[a:A; L:(list A)]: (list A) :=
   Cases L of
       nil => (nil ?)
      | (cons b L1) => Cases (ADec a b) of
                           (left _) => (rem a L1)
                          | (right _) => (cons b (rem a L1))
                       end
   end.

Theorem remNotIn: (a:A) (L:(list A))~ (In a (rem a L)).
Intros a L; Elim L; Simpl; Auto.
Intros a0 l H'; Case (ADec a a0); Auto.
Intros H'0; Red; Intros H'1; Case H'1; Auto.
Qed.

Theorem remIn: (a, b:A) (L:(list A)) (In b L) -> ~ a=b ->(In b (rem a L)).
Intros a b L; Elim L; Simpl; Auto.
Intros a0 l H' H'0 H'1; Case (ADec a a0); Case H'0; Auto with datatypes.
Intros H'2 H'3; Case H'1; Rewrite H'3; Auto.
Intros H'2; Rewrite H'2; Auto with datatypes.
Qed.

Theorem remEq: (a:A) (L:(list A)) ~ (In a L) ->(rem a L)=L.
Intros a L; Elim L; Simpl; Auto.
Intros a0 l H' H'0; Case (ADec a a0); Auto with datatypes.
Intros H'1; Case H'0; Auto.
Intros H'1; Rewrite H'; Auto.
Qed.

Theorem remSizeLess:
  (a:A) (L:(list A)) (In a L) ->(lt (length (rem a L)) (length L)).
Intros a L; Elim L; Simpl; Auto.
Intros H'; Elim H'.
Intros a0 l H' H'0; Case (ADec a a0); Simpl; Auto with datatypes.
Intros H'1; Case (In_dec ADec a l); Auto with arith.
Intros H'2; Rewrite remEq; Auto.
Intros H'1; Case H'0; Auto with arith.
Intros H'2; Case H'1; Auto.
Qed.
End Auxrem.
Hints Resolve remSizeLess remEq remIn remNotIn.

29/06/100, 12:53