From a5ea703d90b6337c0aa7501ba39f346e8f12c093 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 2 Mar 2007 09:16:06 +0000 Subject: Preuve des 2 axiomes restants git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@179 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Integers.v | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/Integers.v b/lib/Integers.v index 4eb95845..a3240e81 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -812,8 +812,23 @@ Proof. decEq; apply mul_commut. Qed. -Axiom neg_mul_distr_l: forall x y, neg(mul x y) = mul (neg x) y. -Axiom neg_mul_distr_r: forall x y, neg(mul x y) = mul x (neg y). +Theorem neg_mul_distr_l: + forall x y, neg(mul x y) = mul (neg x) y. +Proof. + intros. unfold mul, neg. + set (x' := unsigned x). set (y' := unsigned y). + apply eqm_samerepr. apply eqm_trans with (- (x' * y')). + auto with ints. + replace (- (x' * y')) with ((-x') * y') by ring. + auto with ints. +Qed. + +Theorem neg_mul_distr_r: + forall x y, neg(mul x y) = mul x (neg y). +Proof. + intros. rewrite (mul_commut x y). rewrite (mul_commut x (neg y)). + apply neg_mul_distr_l. +Qed. (** ** Properties of binary decompositions *) -- cgit