From 7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 29 Mar 2021 11:12:07 +0200 Subject: replacing omega with lia in some file --- common/Events.v | 3 ++- common/Memdata.v | 3 ++- common/Values.v | 13 +++++++------ 3 files changed, 11 insertions(+), 8 deletions(-) (limited to 'common') diff --git a/common/Events.v b/common/Events.v index 13741ebd..aff9e256 100644 --- a/common/Events.v +++ b/common/Events.v @@ -25,6 +25,7 @@ Require Import Values. Require Import Memory. Require Import Globalenvs. Require Import Builtins. +Require Import Lia. (** * Events and traces *) @@ -1443,7 +1444,7 @@ Proof. econstructor; eauto. red; intros; congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - inv H; inv H0. exists Vundef, m1; constructor. (* determ *) diff --git a/common/Memdata.v b/common/Memdata.v index 1d651db2..6f04db36 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -23,6 +23,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. +Require Import Lia. (** * Properties of memory chunks *) @@ -48,7 +49,7 @@ Definition largest_size_chunk := 8. Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8. Proof. - destruct chunk; simpl; omega. + destruct chunk; simpl; lia. Qed. Lemma size_chunk_pos: diff --git a/common/Values.v b/common/Values.v index 1d272932..c48dca25 100644 --- a/common/Values.v +++ b/common/Values.v @@ -20,6 +20,7 @@ Require Import Coqlib. Require Import AST. Require Import Integers. Require Import Floats. +Require Import Lia. Definition block : Type := positive. Definition eq_block := peq. @@ -1535,14 +1536,14 @@ Proof. replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl. replace (Int.ltu n Int.iwordsize) with true. f_equal; apply Int.shrx_shr_2; assumption. - symmetry; apply zlt_true. change (Int.unsigned n < 32); omega. + symmetry; apply zlt_true. change (Int.unsigned n < 32); lia. symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32. assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } rewrite Int.unsigned_repr. - change (Int.unsigned Int.iwordsize) with 32; omega. - assert (32 < Int.max_unsigned) by reflexivity. omega. + change (Int.unsigned Int.iwordsize) with 32; lia. + assert (32 < Int.max_unsigned) by reflexivity. lia. Qed. Theorem or_rolm: @@ -1848,12 +1849,12 @@ simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl. replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl. replace (Int.ltu n Int64.iwordsize') with true. f_equal; apply Int64.shrx'_shr_2; assumption. - symmetry; apply zlt_true. change (Int.unsigned n < 64); omega. + symmetry; apply zlt_true. change (Int.unsigned n < 64); lia. symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64. assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } rewrite Int.unsigned_repr. - change (Int.unsigned Int64.iwordsize') with 64; omega. - assert (64 < Int.max_unsigned) by reflexivity. omega. + change (Int.unsigned Int64.iwordsize') with 64; lia. + assert (64 < Int.max_unsigned) by reflexivity. lia. Qed. Theorem negate_cmp_bool: -- cgit