From a3bc7b24d5f21b99a37a529d06707c5f0e550679 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 11 Nov 2006 14:24:33 +0000 Subject: Petites adaptations pour Coq 8.1gamma git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Integers.v | 36 ++++++++++++++++++++++-------------- 1 file changed, 22 insertions(+), 14 deletions(-) (limited to 'lib/Integers.v') diff --git a/lib/Integers.v b/lib/Integers.v index 5a18dc0c..4eb95845 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -1787,26 +1787,34 @@ End REFLECTION. Remark modu_and_masks_1: forall logn, 0 <= unsigned logn < Z_of_nat wordsize -> rol (shru mone logn) logn = shl mone logn. -Proof (equal_on_range - (fun l => rol (shru mone l) l) - (fun l => shl mone l) - (refl_equal true)). +Proof. + apply (equal_on_range + (fun l => rol (shru mone l) l) + (fun l => shl mone l)). + vm_compute; auto. +Qed. + Remark modu_and_masks_2: forall logn, 0 <= unsigned logn < Z_of_nat wordsize -> and (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = zero. -Proof (equal_on_range - (fun l => and (shl mone l) - (sub (repr (two_p (unsigned l))) one)) - (fun l => zero) - (refl_equal true)). +Proof. + apply (equal_on_range + (fun l => and (shl mone l) + (sub (repr (two_p (unsigned l))) one)) + (fun l => zero)). + vm_compute; auto. +Qed. + Remark modu_and_masks_3: forall logn, 0 <= unsigned logn < Z_of_nat wordsize -> or (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = mone. -Proof (equal_on_range - (fun l => or (shl mone l) - (sub (repr (two_p (unsigned l))) one)) - (fun l => mone) - (refl_equal true)). +Proof. + apply (equal_on_range + (fun l => or (shl mone l) + (sub (repr (two_p (unsigned l))) one)) + (fun l => mone)). + vm_compute; auto. +Qed. Theorem modu_and: forall x n logn, -- cgit