Zenum.v

(****************************************************************************                                                                                         IEEE754  :  Zenum                                                                                                                                           Laurent Thery                                                                                                                                     ***************************************************************************** Simple functions to enumerate relative numbers *)
Require Import PolyList.
Require Import Omega.
Require Import ZArith.
Require Import sTactic.
Require Import Faux.
(* Returns the list of relative numbers from z to z+n *)

Fixpoint mZlist_aux[p:Z; n:nat]: (list Z) :=
   Cases n of
       O => (cons p (nil ?))
      | (S n1) => (cons p (mZlist_aux (Zs p) n1))
   end.

Theorem mZlist_aux_correct:
  (n:nat) (p, q:Z) (Zle p q) -> (Zle q (Zplus p (inject_nat n))) ->
  (In q (mZlist_aux p n)).
Intros n; Elim n; Clear n; Auto.
Intros p q; Try Rewrite <- Zplus_n_O.
Intros H' H'0; Simpl; Left.
Apply Zle_antisym; Auto.
Intros n H' p q H'0 H'1; Case (Zle_lt_or_eq ? ? H'0); Intros H'2.
Simpl; Right.
Apply H'; Auto with zarith.
Rewrite Zplus_Snm_nSm.
Rewrite <- inj_S; Auto.
Simpl; Auto.
Qed.

Theorem mZlist_aux_correct_rev1:
  (n:nat) (p, q:Z) (In q (mZlist_aux p n)) ->(Zle p q).
Intros n; Elim n; Clear n; Simpl; Auto.
Intros p q H'; Elim H'; Auto with zarith.
Intros H'0; Elim H'0.
Intros n H' p q H'0; Elim H'0; Auto with zarith.
Intros H'1; Apply Zle_trans_S; Auto with zarith.
Qed.

Theorem mZlist_aux_correct_rev2:
  (n:nat) (p, q:Z) (In q (mZlist_aux p n)) ->(Zle q (Zplus p (inject_nat n))).
Intros n; Elim n; Clear n; Auto.
Intros p q H'; Elim H'; Auto with zarith.
Intros H'0; Elim H'0.
Intros n H' p q H'0; Elim H'0; Auto with zarith.
Intros H'1; Rewrite inj_S; Rewrite <- Zplus_Snm_nSm; Auto.
Qed.

(* Return the list of of relative numbres from p to p+q if p=<q,    otherwise the empty list *)

Definition mZlist: Z -> Z ->(list Z) :=
   [p, q:Z]
      Cases (Zminus q p) of
          ZERO => (cons p (nil Z))
         | (POS d) => (mZlist_aux p (convert d))
         | (NEG _) => (nil Z)
      end.

Theorem mZlist_correct:
  (p, q, r:Z) (Zle p r) -> (Zle r q) ->(In r (mZlist p q)).
Intros p q r H' H'0; Unfold mZlist; CaseEq (Zminus q p).
Intros H'1; Rewrite (Zle_antisym r p); Auto with datatypes.
Omega.
Intros p H'1; Apply mZlist_aux_correct; Auto.
Rewrite inject_nat_convert with 1 := H'1; Auto with zarith.
Intros p0 H'1; Absurd (Zle p q); Auto.
Apply Zlt_not_le; Auto.
Apply Zlt_O_minus_lt; Auto.
Replace (Zminus p q) with (Zopp (Zminus q p)); Auto with zarith.
Rewrite H'1; Simpl; Auto with zarith.
Unfold Zlt; Simpl; Auto.
Apply Zle_trans with m := r; Auto.
Qed.

Theorem mZlist_correct_rev1: (p, q, r:Z) (In r (mZlist p q)) ->(Zle p r).
Intros p q r; Unfold mZlist; CaseEq (Zminus q p).
Intros H' H'0; Elim H'0; Auto with zarith.
Intros H'1; Elim H'1.
Intros p0 H' H'0.
Apply mZlist_aux_correct_rev1 with n := (convert p0); Auto.
Intros p0 H' H'0; Elim H'0.
Qed.

Theorem mZlist_correct_rev2: (p, q, r:Z) (In r (mZlist p q)) ->(Zle r q).
Intros p q r; Unfold mZlist; CaseEq (Zminus q p).
Intros H' H'0; Elim H'0; Auto with zarith.
Intros H'1; Elim H'1.
Intros p0 H' H'0.
Rewrite <- (Zle_plus_minus p q).
Rewrite <- inject_nat_convert with 1 := H'.
Apply mZlist_aux_correct_rev2; Auto.
Intros p0 H' H'0; Elim H'0.
Qed.
(* Given two list returns the list of possible product of an element    of the first list with an element of the second list *)

Fixpoint mProd[A, B, C:Set; l1:(list A); l2:(list B)]: (list A * B) :=
   Cases l2 of
       nil => (nil ?)
      | (cons b l2') => (app (map [a:A](a, b) l1) (mProd A B C l1 l2'))
   end.

Theorem mProd_correct:
  (A, B, C:Set)
  (l1:(list A)) (l2:(list B)) (a:A) (b:B) (In a l1) -> (In b l2) ->
  (In (a, b) (mProd A B C l1 l2)).
Intros A B C l1 l2; Elim l2; Simpl; Auto.
Intros a l H' a0 b H'0 H'1; Elim H'1;
[Intros H'2; Rewrite <- H'2; Clear H'1 | Intros H'2; Clear H'1];
Auto with datatypes.
Apply in_or_app; Left; Auto with datatypes.
Generalize H'0; Elim l1; Simpl; Auto with datatypes.
Intros a1 l0 H'1 H'3; Elim H'3; Clear H'3; Intros H'4; [Rewrite <- H'4 | Idtac];
Auto with datatypes.
Qed.

Theorem mProd_correct_rev1:
  (A, B, C:Set)
  (l1:(list A)) (l2:(list B)) (a:A) (b:B) (In (a, b) (mProd A B C l1 l2)) ->
  (In a l1).
Intros A B C l1 l2; Elim l2; Simpl; Auto.
Intros a H' H'0; Elim H'0.
Intros a l H' a0 b H'0.
Case (in_app_or H'0); Auto with datatypes.
Elim l1; Simpl; Auto with datatypes.
Intros a1 l0 H'1 H'2; Elim H'2; Clear H'2; Intros H'3; [Inversion H'3 | Idtac];
Auto with datatypes.
Intros H'1; Apply H' with b := b; Auto.
Qed.

Theorem mProd_correct_rev2:
  (A, B, C:Set)
  (l1:(list A)) (l2:(list B)) (a:A) (b:B) (In (a, b) (mProd A B C l1 l2)) ->
  (In b l2).
Intros A B C l1 l2; Elim l2; Simpl; Auto.
Intros a l H' a0 b H'0.
Case (in_app_or H'0); Auto with datatypes.
Elim l1; Simpl; Auto with datatypes.
Intros H'1; Elim H'1; Auto.
Intros a1 l0 H'1 H'2; Elim H'2; Clear H'2; Intros H'3; [Inversion H'3 | Idtac];
Auto with datatypes.
Intros H'1; Right; Apply H' with a := a0; Auto.
Qed.

Theorem in_map_inv:
  (A, B:Set)
  (f:A ->B)
  (l:(list A)) (x:A) ((a, b:A) (f a)=(f b) ->a=b) -> (In (f x) (map f l)) ->
  (In x l).
Intros A B f l; Elim l; Simpl; Auto.
Intros a l0 H' x H'0 H'1; Elim H'1; Clear H'1; Intros H'2; Auto.
Qed.

22/10/100, 19:37