diff options
| -rw-r--r-- | .depend | 3 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | backend/Registers.v | 1 | ||||
| -rw-r--r-- | lib/Coqlib.v | 1 | ||||
| -rw-r--r-- | lib/Floats.v | 2 | ||||
| -rw-r--r-- | lib/Inclusion.v | 1 | ||||
| -rw-r--r-- | lib/Integers.v | 36 | ||||
| -rw-r--r-- | lib/Sets.v | 1 |
8 files changed, 27 insertions, 20 deletions
@@ -2,12 +2,11 @@ lib/Coqlib.vo: lib/Coqlib.v lib/Maps.vo: lib/Maps.v lib/Coqlib.vo lib/Sets.vo: lib/Sets.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo lib/union_find.vo: lib/union_find.v -lib/Inclusion.vo: lib/Inclusion.v lib/Lattice.vo: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Iteration.vo: lib/Iteration.v lib/Coqlib.vo lib/Integers.vo: lib/Integers.v lib/Coqlib.vo -lib/Floats.vo: lib/Floats.v lib/Integers.vo +lib/Floats.vo: lib/Floats.v lib/Coqlib.vo lib/Integers.vo lib/Parmov.vo: lib/Parmov.v lib/Coqlib.vo common/AST.vo: common/AST.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Events.vo: common/Events.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo @@ -7,7 +7,7 @@ INCLUDES=-I lib -I common -I backend -I cfrontend # Files in lib/ -LIB=Coqlib.v Maps.v Sets.v union_find.v Inclusion.v Lattice.v Ordered.v \ +LIB=Coqlib.v Maps.v Sets.v union_find.v Lattice.v Ordered.v \ Iteration.v Integers.v Floats.v Parmov.v # Files in common/ diff --git a/backend/Registers.v b/backend/Registers.v index 30935893..5b1c7230 100644 --- a/backend/Registers.v +++ b/backend/Registers.v @@ -4,7 +4,6 @@ intermediate language, and of mappings from pseudo-registers to values as used in the dynamic semantics of RTL. *) -Require Import Bool. Require Import Coqlib. Require Import AST. Require Import Maps. diff --git a/lib/Coqlib.v b/lib/Coqlib.v index b5d59b86..0fc8613c 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -4,6 +4,7 @@ Require Export ZArith. Require Export List. +Require Export Bool. Require Import Wf_nat. (** * Logical axioms *) diff --git a/lib/Floats.v b/lib/Floats.v index 67b0e53a..f4c5119e 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -5,7 +5,7 @@ simply axiomatize a type [float] for IEEE double-precision floats and the associated operations. *) -Require Import Bool. +Require Import Coqlib. Require Import Integers. Parameter float: Set. diff --git a/lib/Inclusion.v b/lib/Inclusion.v index 1df7517f..15e37c46 100644 --- a/lib/Inclusion.v +++ b/lib/Inclusion.v @@ -22,6 +22,7 @@ A second tactic, [incl_tac], handles goals of the form *) Require Import List. +Require Import Bool. Require Import ArithRing. Ltac all_app e := 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, @@ -9,7 +9,6 @@ implementation of sets. *) -Require Import Relations. Require Import Coqlib. Require Import Maps. Require Import Lattice. |