(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                              Euclid_prog.v                               *)
(****************************************************************************)

Require Euclid_def.
Require Compare_dec.
Require Wf_nat.

Theorem eucl_dev : (b:nat)(gt b O)->(a:nat)(diveucl a b).
Realizer [b:nat]
          (<nat*nat>rec div :: :: { lt }
              [a:nat]if (le_gt_dec b a) then
			let (q,r) = (div (minus a b)) in
				((S q),r)
			 else (O,a)).
Program_all.
Simpl.
Rewrite plus_assoc_r.
Elim e; Auto with arith.
Save.

Lemma quotient : (b:nat)(gt b O)->
     (a:nat){q:nat|(EX r:nat | a=(plus (mult q b) r) /\ (gt b r))}.
Realizer [b:nat]
	  (<nat>rec div :: :: { lt }
              [a:nat]if (le_gt_dec b a) then
                        (S (div (minus a b)))
                        else O).
Program_all.
Elim e.
Intros.
Exists x0; Simpl; Elim H0; Intros.
Elim plus_assoc_l.
Elim H1; Auto with arith.
Exists a0; Simpl; Auto with arith.
Save.

Lemma modulo : (b:nat)(gt b O)->
     (a:nat){r:nat|(EX q:nat | a=(plus (mult q b) r) /\ (gt b r))}.
Realizer [b:nat]
           (<nat>rec div :: :: { lt }
              [a:nat]if (le_gt_dec b a) then
			    (div (minus a b))
			  else a).
Program_all.
Elim e; Intros q Hq.
Elim Hq; Intros; Exists (S q); Simpl.
Elim plus_assoc_l.
Elim H0; Auto with arith.
Exists O; Simpl; Auto with arith.
Save.

(* $Id: Euclid_prog.v,v 1.7 1999/10/21 15:52:16 herbelin Exp $ *)
