(**************************************************************************)
(*       ___                                                              *)
(*      ||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___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)

(*   \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.2.1 2004/07/16 19:31:21 herbelin 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'\195\\169\valuation des vecteurs de bool\195\\169\ens se font \195\\160\ la fois en binaire et
en compl\195\\169\ment \195\\160\ deux. Le nombre appartient \195\\160\ Z. 
On utilise donc Omega pour faire les calculs dans Z.
De plus, on utilise les fonctions 2^n o\195\\185\ 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\195\\169\s dans la convention positive usuelle.
Les valeurs correspondent soit \195\\160\ l'\195\\169\criture binaire (nat), 
soit au compl\195\\169\ment \195\\160\ deux (int).
On effectue le calcul suivant le sch\195\\169\ma de Horner.
Le compl\195\\169\ment \195\\160\ deux n'a de sens que sur les vecteurs de taille 
sup\195\\169\rieure ou \195\\169\gale \195\\160\ un, le bit de signe \195\\169\tant \195\\169\valu\195\\169\ n\195\\169\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 \195\\160\ la longueur du vecteur sans v\195\\169\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\195\\169\ment \195\\160\ deux est calcul\195\\169\e selon un schema de Horner
avec Zmod2, le param\195\\168\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\195\\169\rifie que dans l'intervalle de d\195\\169\finition les fonctions sont 
r\195\\169\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
*)