diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-03-02 09:16:06 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-03-02 09:16:06 +0000 |
| commit | a5ea703d90b6337c0aa7501ba39f346e8f12c093 (patch) | |
| tree | cf7cefaf025551d16ba83246d9e19b34709d3fb5 | |
| parent | 9b11be0dc297779d899a7ca586513ee64236be0c (diff) | |
| download | compcert-a5ea703d90b6337c0aa7501ba39f346e8f12c093.tar.gz compcert-a5ea703d90b6337c0aa7501ba39f346e8f12c093.zip | |
Preuve des 2 axiomes restants
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@179 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
| -rw-r--r-- | lib/Integers.v | 19 |
1 files changed, 17 insertions, 2 deletions
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 *) |