(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* This file was automatically generated: do not edit *********************)

include "Coq.ma".

(*#**********************************************************************)

(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)

(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)

(*   \VV/  *************************************************************)

(*    //   *      This file is distributed under the terms of the      *)

(*         *       GNU Lesser General Public License Version 2.1       *)

(*#**********************************************************************)

(*i $Id: Zbinary.v,v 1.6 2004/02/10 15:38:01 marche Exp $ i*)

(*#* Bit vectors interpreted as integers. 
    Contribution by Jean Duprat (ENS Lyon). *)

include "Bool/Bvector.ma".

include "ZArith/ZArith.ma".

include "ZArith/Zpower.ma".

(*
L'évaluation des vecteurs de booléens se font à la fois en binaire et
en complément à deux. Le nombre appartient à Z. 
On utilise donc Omega pour faire les calculs dans Z.
De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur.
	two_power_nat = [n:nat](POS (shift_nat n xH))
     		: nat->Z
	two_power_nat_S
	     : (n:nat)`(two_power_nat (S n)) = 2*(two_power_nat n)`
	Z_lt_ge_dec
	     : (x,y:Z){`x < y`}+{`x >= y`}
*)

(* UNEXPORTED
Section VALUE_OF_BOOLEAN_VECTORS
*)

(*
Les calculs sont effectués dans la convention positive usuelle.
Les valeurs correspondent soit à l'écriture binaire (nat), 
soit au complément à deux (int).
On effectue le calcul suivant le schéma de Horner.
Le complément à deux n'a de sens que sur les vecteurs de taille 
supérieure ou égale à un, le bit de signe étant évalué négativement.
*)

inline procedural "cic:/Coq/ZArith/Zbinary/bit_value.con" as definition.

inline procedural "cic:/Coq/ZArith/Zbinary/binary_value.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/two_compl_value.con" as lemma.

(*
Coq < Eval Compute in (binary_value (3) (Bcons true (2) (Bcons false (1) (Bcons true (0) Bnil)))).
     = `5`
     : Z
*)

(*
Coq < Eval Compute in (two_compl_value (3) (Bcons true (3) (Bcons false (2) (Bcons true (1) (Bcons true (0) Bnil))))).
     = `-3`
     : Z
*)

(* UNEXPORTED
End VALUE_OF_BOOLEAN_VECTORS
*)

(* UNEXPORTED
Section ENCODING_VALUE
*)

(*
On calcule la valeur binaire selon un schema de Horner.
Le calcul s'arrete à la longueur du vecteur sans vérification.
On definit une fonction Zmod2 calquee sur Zdiv2 mais donnant le quotient
de la division z=2q+r avec 0<=r<=1.
La valeur en complément à deux est calculée selon un schema de Horner
avec Zmod2, le paramètre est la taille moins un.
*)

inline procedural "cic:/Coq/ZArith/Zbinary/Zmod2.con" as definition.

inline procedural "cic:/Coq/ZArith/Zbinary/Zmod2_twice.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary.con" as lemma.

(*
Eval Compute in (Z_to_binary (5) `5`).
     = (Vcons bool true (4)
          (Vcons bool false (3)
            (Vcons bool true (2)
              (Vcons bool false (1) (Vcons bool false (0) (Vnil bool))))))
     :  (Bvector (5))
*)

inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl.con" as lemma.

(*
Eval Compute in (Z_to_two_compl (3) `0`).
     =  (Vcons bool false (3)
          (Vcons bool false (2)
            (Vcons bool false (1) (Vcons bool false (0) (Vnil bool)))))
     :  (vector bool (4))

Eval Compute in (Z_to_two_compl (3) `5`).
     = (Vcons bool true (3)
          (Vcons bool false (2)
            (Vcons bool true (1) (Vcons bool false (0) (Vnil bool)))))
     :  (vector bool (4))

Eval Compute in (Z_to_two_compl (3) `-5`).
     =  (Vcons bool true (3)
          (Vcons bool true (2)
            (Vcons bool false (1) (Vcons bool true (0) (Vnil bool)))))
     :  (vector bool (4))
*)

(* UNEXPORTED
End ENCODING_VALUE
*)

(* UNEXPORTED
Section Z_BRIC_A_BRAC
*)

(*
Bibliotheque de lemmes utiles dans la section suivante.
Utilise largement ZArith.
Meriterait d'etre reecrite.
*)

inline procedural "cic:/Coq/ZArith/Zbinary/binary_value_Sn.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary_Sn.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/binary_value_pos.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/two_compl_value_Sn.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl_Sn.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary_Sn_z.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Z_div2_value.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Pdiv2.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Zdiv2_two_power_nat.con" as lemma.

(*

Lemma Z_minus_one_or_zero : (z:Z)
	`z >= -1` ->
	`z < 1` ->
	{`z=-1`} + {`z=0`}.
Proof.
	NewDestruct z; Auto.
	NewDestruct p; Auto.
	Tauto.

	Tauto.

	Intros.
	Right; Omega.

	NewDestruct p.
	Tauto.

	Tauto.

	Intros; Left; Omega.
Save.
*)

inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl_Sn_z.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Zeven_bit_value.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Zodd_bit_value.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Zge_minus_two_power_nat_S.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Zlt_two_power_nat_S.con" as lemma.

(* UNEXPORTED
End Z_BRIC_A_BRAC
*)

(* UNEXPORTED
Section COHERENT_VALUE
*)

(*
On vérifie que dans l'intervalle de définition les fonctions sont 
réciproques l'une de l'autre.
Elles utilisent les lemmes du bric-a-brac.
*)

inline procedural "cic:/Coq/ZArith/Zbinary/binary_to_Z_to_binary.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/two_compl_to_Z_to_two_compl.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary_to_Z.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl_to_Z.con" as lemma.

(* UNEXPORTED
End COHERENT_VALUE
*)