(**************************************************************************)
(*       ___                                                              *)
(*      ||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: Zdiv.v,v 1.21.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)

(* Contribution by Claude March\233\ and Xavier Urbain *)

(*#*

Euclidean Division

Defines first of function that allows Coq to normalize. 
Then only after proves the main required property.

*)

include "ZArith/ZArith_base.ma".

include "ZArith/Zbool.ma".

include "ZArith/Zcomplements.ma".

(* UNEXPORTED
Open Local Scope Z_scope.
*)

(*#*

  Euclidean division of a positive by a integer 
  (that is supposed to be positive).

  total function than returns an arbitrary value when
  divisor is not positive
  
*)

inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl_POS.con" as definition.

(*#*

  Euclidean division of integers.
 
  Total function than returns (0,0) when dividing by 0. 

*)

(* 

  The pseudo-code is:
  
  if b = 0 : (0,0)
 
  if b <> 0 and a = 0 : (0,0)

  if b > 0 and a < 0 : let (q,r) = div_eucl_pos (-a) b in 
                       if r = 0 then (-q,0) else (-(q+1),b-r)

  if b < 0 and a < 0 : let (q,r) = div_eucl (-a) (-b) in (q,-r)

  if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in 
                       if r = 0 then (-q,0) else (-(q+1),b+r)

  In other word, when b is non-zero, q is chosen to be the greatest integer 
  smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b|.

*)

inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl.con" as definition.

(*#* Division and modulo are projections of [Zdiv_eucl] *)

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

inline procedural "cic:/Coq/ZArith/Zdiv/Zmod.con" as definition.

(* Tests:

Eval Compute in `(Zdiv_eucl 7 3)`. 

Eval Compute in `(Zdiv_eucl (-7) 3)`.

Eval Compute in `(Zdiv_eucl 7 (-3))`.

Eval Compute in `(Zdiv_eucl (-7) (-3))`.

*)

(*#*

  Main division theorem. 

  First a lemma for positive

*)

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mod_POS.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mod.con" as theorem.

(*#* Existence theorems *)

inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl_exist.con" as theorem.

(* UNEXPORTED
Implicit Arguments Zdiv_eucl_exist.
*)

inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl_extended.con" as theorem.

(* UNEXPORTED
Implicit Arguments Zdiv_eucl_extended.
*)

(*#* Auxiliary lemmas about [Zdiv] and [Zmod] *)

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mod_eq.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_lt.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_POS_ge0.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_ge0.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_lt.con" as lemma.

(*#* Syntax *)

(* NOTATION
Infix "/" := Zdiv : Z_scope.
*)

(* NOTATION
Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
*)

(*#* Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *)

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_ge.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_plus.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_plus.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mult.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_mult_div_ge.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_same.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_same.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_exact_1.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_exact_2.con" as lemma.

inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_zero_opp.con" as lemma.