(****************************************************************************
                                                                             
          IEEE754  :  Zenum                                                  
                                                                             
          Laurent Thery                                                      
                                                                             
  *****************************************************************************
  Simple functions to enumerate relative numbers *)
Require Export Faux.
Require Export Omega.
Require Export List.
(* 
   Returns the list of relative numbers from z to z+n *)
 
Fixpoint mZlist_aux (p : Z) (n : nat) {struct n} : 
 list Z :=
  match n with
  | O => p :: nil
  | S n1 => p :: mZlist_aux (Zsucc p) n1
  end.
 
Theorem mZlist_aux_correct :
 forall (n : nat) (p q : Z),
 (p <= q)%Z -> (q <= p + Z_of_nat n)%Z -> In q (mZlist_aux p n).
(* Goal: forall (n : nat) (p q : Z) (_ : @In Z q (mZlist_aux p n)), Z.le q (Z.add p (Z.of_nat n)) *)
intros n; elim n; clear n; auto.
(* Goal: forall (p q : Z) (_ : Z.le p q) (_ : Z.le q (Z.add p (Z.of_nat O))), @In Z q (mZlist_aux p O) *)
(* Goal: forall (n : nat) (_ : forall (p q : Z) (_ : Z.le p q) (_ : Z.le q (Z.add p (Z.of_nat n))), @In Z q (mZlist_aux p n)) (p q : Z) (_ : Z.le p q) (_ : Z.le q (Z.add p (Z.of_nat (S n)))), @In Z q (mZlist_aux p (S n)) *)
intros p q; try rewrite <- Zplus_0_r_reverse.
(* Goal: forall (_ : Z.le p q) (_ : Z.le q p), @In Z q (mZlist_aux p O) *)
(* Goal: forall (n : nat) (_ : forall (p q : Z) (_ : Z.le p q) (_ : Z.le q (Z.add p (Z.of_nat n))), @In Z q (mZlist_aux p n)) (p q : Z) (_ : Z.le p q) (_ : Z.le q (Z.add p (Z.of_nat (S n)))), @In Z q (mZlist_aux p (S n)) *)
intros H' H'0; simpl in |- *; left.
(* Goal: @eq Z p q *)
(* Goal: forall (n : nat) (_ : forall (p q : Z) (_ : Z.le p q) (_ : Z.le q (Z.add p (Z.of_nat n))), @In Z q (mZlist_aux p n)) (p q : Z) (_ : Z.le p q) (_ : Z.le q (Z.add p (Z.of_nat (S n)))), @In Z q (mZlist_aux p (S n)) *)
apply Zle_antisym; auto.
(* Goal: forall (n : nat) (_ : forall (p q : Z) (_ : Z.le p q) (_ : Z.le q (Z.add p (Z.of_nat n))), @In Z q (mZlist_aux p n)) (p q : Z) (_ : Z.le p q) (_ : Z.le q (Z.add p (Z.of_nat (S n)))), @In Z q (mZlist_aux p (S n)) *)
intros n H' p q H'0 H'1; case (Zle_lt_or_eq _ _ H'0); intros H'2.
(* Goal: @In Z q (mZlist_aux p (S n)) *)
(* Goal: @In Z q (mZlist_aux p (S n)) *)
simpl in |- *; right.
(* Goal: @In Z q (mZlist_aux (Z.succ p) n) *)
(* Goal: @In Z q (mZlist_aux p (S n)) *)
apply H'; auto with zarith.
(* Goal: Z.le q (Z.add (Z.succ p) (Z.of_nat n)) *)
(* Goal: @In Z q (mZlist_aux p (S n)) *)
rewrite Zplus_succ_comm.
(* Goal: Z.le q (Z.add p (Z.succ (Z.of_nat n))) *)
(* Goal: @In Z q (mZlist_aux p (S n)) *)
rewrite <- inj_S; auto.
(* Goal: @In Z q (mZlist_aux p (S n)) *)
simpl in |- *; auto.
Qed.
 
Theorem mZlist_aux_correct_rev1 :
 forall (n : nat) (p q : Z), In q (mZlist_aux p n) -> (p <= q)%Z.
(* Goal: @In Z q (mZlist_aux p (S n)) *)
intros n; elim n; clear n; simpl in |- *; auto.
(* Goal: forall (p q : Z) (_ : @In Z q (mZlist_aux p O)), Z.le q (Z.add p (Z.of_nat O)) *)
(* Goal: forall (n : nat) (_ : forall (p q : Z) (_ : @In Z q (mZlist_aux p n)), Z.le q (Z.add p (Z.of_nat n))) (p q : Z) (_ : @In Z q (mZlist_aux p (S n))), Z.le q (Z.add p (Z.of_nat (S n))) *)
intros p q H'; elim H'; auto with zarith.
(* Goal: forall (n : nat) (_ : forall (p q : Z) (_ : @In Z q (mZlist_aux p n)), Z.le q (Z.add p (Z.of_nat n))) (p q : Z) (_ : @In Z q (mZlist_aux p (S n))), Z.le q (Z.add p (Z.of_nat (S n))) *)
intros n H' p q H'0; elim H'0; auto with zarith.
(* Goal: forall _ : @In Z q (mZlist_aux (Z.succ p) n), Z.le p q *)
intros H'1; apply Zle_succ_le; auto with zarith.
Qed.
 
Theorem mZlist_aux_correct_rev2 :
 forall (n : nat) (p q : Z),
 In q (mZlist_aux p n) -> (q <= p + Z_of_nat n)%Z.
(* Goal: forall (n : nat) (p q : Z) (_ : @In Z q (mZlist_aux p n)), Z.le q (Z.add p (Z.of_nat n)) *)
intros n; elim n; clear n; auto.
(* Goal: forall (p q : Z) (_ : @In Z q (mZlist_aux p O)), Z.le q (Z.add p (Z.of_nat O)) *)
(* Goal: forall (n : nat) (_ : forall (p q : Z) (_ : @In Z q (mZlist_aux p n)), Z.le q (Z.add p (Z.of_nat n))) (p q : Z) (_ : @In Z q (mZlist_aux p (S n))), Z.le q (Z.add p (Z.of_nat (S n))) *)
intros p q H'; elim H'; auto with zarith.
(* Goal: forall _ : @In Z q (@Datatypes.nil Z), Z.le q (Z.add p (Z.of_nat O)) *)
(* Goal: forall (n : nat) (_ : forall (p q : Z) (_ : @In Z q (mZlist_aux p n)), Z.le q (Z.add p (Z.of_nat n))) (p q : Z) (_ : @In Z q (mZlist_aux p (S n))), Z.le q (Z.add p (Z.of_nat (S n))) *)
intros H'0; elim H'0.
(* Goal: forall (n : nat) (_ : forall (p q : Z) (_ : @In Z q (mZlist_aux p n)), Z.le q (Z.add p (Z.of_nat n))) (p q : Z) (_ : @In Z q (mZlist_aux p (S n))), Z.le q (Z.add p (Z.of_nat (S n))) *)
intros n H' p q H'0; elim H'0; auto with zarith.
(* Goal: forall _ : @In Z q (mZlist_aux (Z.succ p) n), Z.le q (Z.add p (Z.of_nat (S n))) *)
intros H'1; rewrite inj_S; rewrite <- Zplus_succ_comm; auto.
Qed.
(* Return the list of of relative numbres from p to p+q if p=<q,
   otherwise the empty list *)
 
Definition mZlist (p q : Z) : list Z :=
  match (q - p)%Z with
  | Z0 => p :: nil
  | Zpos d => mZlist_aux p (nat_of_P d)
  | Zneg _ => nil (A:=Z)
  end.
 
Theorem mZlist_correct :
 forall p q r : Z, (p <= r)%Z -> (r <= q)%Z -> In r (mZlist p q).
intros p q r H' H'0; unfold mZlist in |- *; CaseEq (q - p)%Z;
(* Goal: Z.le r p *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)), @In Z r (mZlist_aux p (Pos.to_nat p0)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)), @In Z r (@Datatypes.nil Z) *)
 auto with zarith.
(* Goal: forall _ : @eq Z (Z.sub q p) Z0, @In Z r (@Datatypes.cons Z p (@Datatypes.nil Z)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)), @In Z r (mZlist_aux p (Pos.to_nat p0)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)), @In Z r (@Datatypes.nil Z) *)
intros H'1; rewrite (Zle_antisym r p); auto with datatypes.
(* Goal: Z.le r p *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)), @In Z r (mZlist_aux p (Pos.to_nat p0)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)), @In Z r (@Datatypes.nil Z) *)
auto with zarith.
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)), @In Z r (mZlist_aux p (Pos.to_nat p0)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)), @In Z r (@Datatypes.nil Z) *)
intros p0 H'1; apply mZlist_aux_correct; auto.
(* Goal: Z.le r p *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)), @In Z r (mZlist_aux p (Pos.to_nat p0)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)), @In Z r (@Datatypes.nil Z) *)
rewrite inject_nat_convert with (1 := H'1); auto with zarith.
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)), @In Z r (@Datatypes.nil Z) *)
intros p0 H'1; absurd (p <= q)%Z; auto.
(* Goal: not (Z.le p q) *)
(* Goal: Z.le p q *)
apply Zlt_not_le; auto.
(* Goal: Z.lt q p *)
(* Goal: Z.le p q *)
apply Zlt_O_minus_lt; auto.
(* Goal: Z.le r p *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)), @In Z r (mZlist_aux p (Pos.to_nat p0)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)), @In Z r (@Datatypes.nil Z) *)
replace (p - q)%Z with (- (q - p))%Z; auto with zarith.
(* Goal: Z.le r p *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)), @In Z r (mZlist_aux p (Pos.to_nat p0)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)), @In Z r (@Datatypes.nil Z) *)
rewrite H'1; simpl in |- *; auto with zarith.
(* Goal: @In Z q (mZlist_aux p (S n)) *)
unfold Zlt in |- *; simpl in |- *; auto.
(* Goal: Z.le p q *)
apply Zle_trans with (m := r); auto.
Qed.
 
Theorem mZlist_correct_rev1 :
 forall p q r : Z, In r (mZlist p q) -> (p <= r)%Z.
(* Goal: forall (p q r : Z) (_ : @In Z r (mZlist p q)), Z.le r q *)
intros p q r; unfold mZlist in |- *; CaseEq (q - p)%Z.
(* Goal: Z.le r p *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)), @In Z r (mZlist_aux p (Pos.to_nat p0)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)), @In Z r (@Datatypes.nil Z) *)
intros H' H'0; elim H'0; auto with zarith.
(* Goal: forall _ : @In Z r (@Datatypes.nil Z), Z.le r q *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)) (_ : @In Z r (mZlist_aux p (Pos.to_nat p0))), Z.le r q *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)) (_ : @In Z r (@Datatypes.nil Z)), Z.le r q *)
intros H'1; elim H'1.
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)) (_ : @In Z r (mZlist_aux p (Pos.to_nat p0))), Z.le r q *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)) (_ : @In Z r (@Datatypes.nil Z)), Z.le r q *)
intros p0 H' H'0.
(* Goal: Z.le p r *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)) (_ : @In Z r (@Datatypes.nil Z)), Z.le p r *)
apply mZlist_aux_correct_rev1 with (n := nat_of_P p0); auto.
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)) (_ : @In Z r (@Datatypes.nil Z)), Z.le r q *)
intros p0 H' H'0; elim H'0.
Qed.
 
Theorem mZlist_correct_rev2 :
 forall p q r : Z, In r (mZlist p q) -> (r <= q)%Z.
(* Goal: forall (p q r : Z) (_ : @In Z r (mZlist p q)), Z.le r q *)
intros p q r; unfold mZlist in |- *; CaseEq (q - p)%Z.
(* Goal: Z.le r p *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)), @In Z r (mZlist_aux p (Pos.to_nat p0)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)), @In Z r (@Datatypes.nil Z) *)
intros H' H'0; elim H'0; auto with zarith.
(* Goal: forall _ : @In Z r (@Datatypes.nil Z), Z.le r q *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)) (_ : @In Z r (mZlist_aux p (Pos.to_nat p0))), Z.le r q *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)) (_ : @In Z r (@Datatypes.nil Z)), Z.le r q *)
intros H'1; elim H'1.
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zpos p0)) (_ : @In Z r (mZlist_aux p (Pos.to_nat p0))), Z.le r q *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)) (_ : @In Z r (@Datatypes.nil Z)), Z.le r q *)
intros p0 H' H'0.
(* Goal: Z.le r q *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)) (_ : @In Z r (@Datatypes.nil Z)), Z.le r q *)
rewrite <- (Zplus_minus p q).
(* Goal: Z.le r (Z.add p (Z.sub q p)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)) (_ : @In Z r (@Datatypes.nil Z)), Z.le r q *)
rewrite <- inject_nat_convert with (1 := H').
(* Goal: Z.le r (Z.add p (Z.of_nat (Pos.to_nat p0))) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)) (_ : @In Z r (@Datatypes.nil Z)), Z.le r q *)
apply mZlist_aux_correct_rev2; auto.
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub q p) (Zneg p0)) (_ : @In Z r (@Datatypes.nil Z)), Z.le r q *)
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) {struct l2} :
 list (A * B) :=
  match l2 with
  | nil => nil
  | b :: l2' => map (fun a : A => (a, b)) l1 ++ mProd A B C l1 l2'
  end.
 
Theorem mProd_correct :
 forall (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).
(* Goal: @In Z q (mZlist_aux p (S n)) *)
intros A B C l1 l2; elim l2; simpl in |- *; 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.
(* Goal: @In (prod A B) (@pair A B a0 a) (@app (prod A B) (@map A (prod A B) (fun a0 : A => @pair A B a0 a) l1) (mProd A B C l1 l)) *)
apply in_or_app; left; auto with datatypes.
(* Goal: @In (prod A B) (@pair A B a0 a) (@map A (prod A B) (fun a0 : A => @pair A B a0 a) l1) *)
generalize H'0; elim l1; simpl in |- *; 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 :
 forall (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.
(* Goal: @In Z q (mZlist_aux p (S n)) *)
intros A B C l1 l2; elim l2; simpl in |- *; auto.
(* Goal: forall (a : A) (_ : B) (_ : False), @In A a l1 *)
(* Goal: forall (a : B) (l : list B) (_ : forall (a0 : A) (b : B) (_ : @In (prod A B) (@pair A B a0 b) (mProd A B C l1 l)), @In A a0 l1) (a0 : A) (b : B) (_ : @In (prod A B) (@pair A B a0 b) (@app (prod A B) (@map A (prod A B) (fun a1 : A => @pair A B a1 a) l1) (mProd A B C l1 l))), @In A a0 l1 *)
intros a H' H'0; elim H'0.
(* Goal: forall (a : B) (l : list B) (_ : forall (a0 : A) (b : B) (_ : @In (prod A B) (@pair A B a0 b) (mProd A B C l1 l)), @In B b l) (a0 : A) (b : B) (_ : @In (prod A B) (@pair A B a0 b) (@app (prod A B) (@map A (prod A B) (fun a1 : A => @pair A B a1 a) l1) (mProd A B C l1 l))), or (@eq B a b) (@In B b l) *)
intros a l H' a0 b H'0.
(* Goal: or (@eq B a b) (@In B b l) *)
case (in_app_or _ _ _ H'0); auto with datatypes.
(* Goal: forall _ : @In (prod A B) (@pair A B a0 b) (@map A (prod A B) (fun a0 : A => @pair A B a0 a) l1), or (@eq B a b) (@In B b l) *)
(* Goal: forall _ : @In (prod A B) (@pair A B a0 b) (mProd A B C l1 l), or (@eq B a b) (@In B b l) *)
elim l1; simpl in |- *; 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.
(* Goal: forall _ : @In (prod A B) (@pair A B a0 b) (mProd A B C l1 l), @In A a0 l1 *)
intros H'1; apply H' with (b := b); auto.
Qed.
 
Theorem mProd_correct_rev2 :
 forall (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.
(* Goal: @In Z q (mZlist_aux p (S n)) *)
intros A B C l1 l2; elim l2; simpl in |- *; auto.
(* Goal: forall (a : B) (l : list B) (_ : forall (a0 : A) (b : B) (_ : @In (prod A B) (@pair A B a0 b) (mProd A B C l1 l)), @In B b l) (a0 : A) (b : B) (_ : @In (prod A B) (@pair A B a0 b) (@app (prod A B) (@map A (prod A B) (fun a1 : A => @pair A B a1 a) l1) (mProd A B C l1 l))), or (@eq B a b) (@In B b l) *)
intros a l H' a0 b H'0.
(* Goal: or (@eq B a b) (@In B b l) *)
case (in_app_or _ _ _ H'0); auto with datatypes.
(* Goal: forall _ : @In (prod A B) (@pair A B a0 b) (@map A (prod A B) (fun a0 : A => @pair A B a0 a) l1), or (@eq B a b) (@In B b l) *)
(* Goal: forall _ : @In (prod A B) (@pair A B a0 b) (mProd A B C l1 l), or (@eq B a b) (@In B b l) *)
elim l1; simpl in |- *; auto with datatypes.
(* Goal: forall _ : False, or (@eq B a b) (@In B b l) *)
(* Goal: forall (a1 : A) (l0 : list A) (_ : forall _ : @In (prod A B) (@pair A B a0 b) (@map A (prod A B) (fun a0 : A => @pair A B a0 a) l0), or (@eq B a b) (@In B b l)) (_ : or (@eq (prod A B) (@pair A B a1 a) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) (@map A (prod A B) (fun a0 : A => @pair A B a0 a) l0))), or (@eq B a b) (@In B b l) *)
(* Goal: forall _ : @In (prod A B) (@pair A B a0 b) (mProd A B C l1 l), or (@eq B a b) (@In B b l) *)
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.
(* Goal: forall _ : @In (prod A B) (@pair A B a0 b) (mProd A B C l1 l), or (@eq B a b) (@In B b l) *)
intros H'1; right; apply H' with (a := a0); auto.
Qed.
 
Theorem in_map_inv :
 forall (A B : Set) (f : A -> B) (l : list A) (x : A),
 (forall a b : A, f a = f b -> a = b) -> In (f x) (map f l) -> In x l.
(* Goal: @In Z q (mZlist_aux p (S n)) *)
intros A B f l; elim l; simpl in |- *; auto.
(* Goal: forall (a : A) (l : list A) (_ : forall (x : A) (_ : forall (a0 b : A) (_ : @eq B (f a0) (f b)), @eq A a0 b) (_ : @In B (f x) (@map A B f l)), @In A x l) (x : A) (_ : forall (a0 b : A) (_ : @eq B (f a0) (f b)), @eq A a0 b) (_ : or (@eq B (f a) (f x)) (@In B (f x) (@map A B f l))), or (@eq A a x) (@In A x l) *)
intros a l0 H' x H'0 H'1; elim H'1; clear H'1; intros H'2; auto.
Qed.
