From 0d2f62951562228ce65b5a3e3a4bd8735142b623 Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 25 Jan 2002 13:09:02 +0000 Subject: Zdiv et Zmod dans Zcomplements git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2437 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Zcomplements.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 4f9e43be5..5130c9807 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -303,6 +303,33 @@ NewDestruct a; ]. Save. +Definition Zdiv [a,b:Z] : Z := + Cases (Z_gt_le_dec b `0`) of + (left bpos) => let (qr,_) = (Zdiv_eucl bpos a) in + let (q,_) = qr in q + | (right _) => `0` end. + +Definition Zmod [a,b:Z] : Z := + Cases (Z_gt_le_dec b `0`) of + (left bpos) => let (qr,_) = (Zdiv_eucl bpos a) in + let (_,r) = qr in r + | (right _) => `0` end. + +Lemma Z_div_mod : (a,b:Z)`b > 0` -> `a = (Zdiv a b)*b + (Zmod a b)`. +Proof. +Intros; Unfold Zdiv Zmod; Case (Z_gt_le_dec b `0`); Simpl; Intros. +Case (Zdiv_eucl z a); Simpl; Induction x; Intros. +Rewrite <- Zmult_sym; Tauto. +Absurd `b > 0`; Omega. +Save. + +Lemma Z_mod_bounds : (a,b:Z)`b > 0` -> `0 <= (Zmod a b) < b`. +Proof. +Intros; Unfold Zdiv Zmod; Case (Z_gt_le_dec b `0`); Simpl; Intros. +Case (Zdiv_eucl z a); Simpl; Induction x; Intros; Omega. +Absurd `b > 0`; Omega. +Save. + Theorem Zdiv_eucl_extended : (b:Z)`b <> 0` -> (a:Z) { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < |b|` }. Proof. -- cgit v1.2.3