diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
| commit | af16cdae6d58033cc8aa06bca330f98b96ba12f2 (patch) | |
| tree | 4985e9ae8fa0d580bbf95a198edeca4f0bd6ff46 /kvx/SelectLongproof.v | |
| parent | 21c979fce33b068ce4b86e67d3d866b203411c6c (diff) | |
| parent | 02b169b444c435b8d1aacf54969dd7de57317a5c (diff) | |
| download | compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.tar.gz compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.zip | |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
Diffstat (limited to 'kvx/SelectLongproof.v')
| -rw-r--r-- | kvx/SelectLongproof.v | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/kvx/SelectLongproof.v b/kvx/SelectLongproof.v index fb38bbce..c3abdbc7 100644 --- a/kvx/SelectLongproof.v +++ b/kvx/SelectLongproof.v @@ -23,6 +23,7 @@ Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. Require Import DecBoolOps. +Require Import Lia. Local Open Scope cminorsel_scope. Local Open Scope string_scope. @@ -408,14 +409,14 @@ Proof. rewrite BOUNDS. destruct v1; try (simpl; apply Val.lessdef_undef). replace (Z.sub Int64.zwordsize - (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega. + (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by lia. replace (Z.sub Int64.zwordsize (Z.sub (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one) (Z.sub (Z.add (Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one))) - Z.one) Int64.zwordsize))) with (Int.unsigned n) by omega. + Z.one) Int64.zwordsize))) with (Int.unsigned n) by lia. simpl. destruct (Int.ltu n1 Int64.iwordsize') eqn:Hltu_n1; simpl; trivial. destruct (Int.ltu n Int64.iwordsize') eqn:Hltu_n; simpl; trivial. @@ -460,14 +461,14 @@ Proof. rewrite BOUNDS. destruct v1; try (simpl; apply Val.lessdef_undef). replace (Z.sub Int64.zwordsize - (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega. + (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by lia. replace (Z.sub Int64.zwordsize (Z.sub (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one) (Z.sub (Z.add (Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one))) - Z.one) Int64.zwordsize))) with (Int.unsigned n) by omega. + Z.one) Int64.zwordsize))) with (Int.unsigned n) by lia. simpl. destruct (Int.ltu n1 Int64.iwordsize') eqn:Hltu_n1; simpl; trivial. destruct (Int.ltu n Int64.iwordsize') eqn:Hltu_n; simpl; trivial. @@ -708,9 +709,9 @@ Proof. rewrite Int64.shl'_zero. reflexivity. *** simpl. unfold Int.max_unsigned. unfold Int.modulus. - simpl. omega. + simpl. lia. ** unfold Int.max_unsigned. unfold Int.modulus. - simpl. omega. + simpl. lia. * TrivialExists. + TrivialExists. - TrivialExists. |