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)).

Theorem mZlist_aux_correct_rev1:
  (n:nat) (p, q:Z) (In q (mZlist_aux p n)) ->(Zle p q).

Theorem mZlist_aux_correct_rev2:
  (n:nat) (p, q:Z) (In q (mZlist_aux p n)) ->(Zle q (Zplus p (inject_nat n))).

(* 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)).

Theorem mZlist_correct_rev1: (p, q, r:Z) (In r (mZlist p q)) ->(Zle p r).

Theorem mZlist_correct_rev2: (p, q, r:Z) (In r (mZlist p q)) ->(Zle r q).
(* 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)).

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).

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).

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).

30/05/01, 18:31