diff options
Diffstat (limited to 'riscV/RTLpathSE_simplify.v')
| -rw-r--r-- | riscV/RTLpathSE_simplify.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index ca049962..2739bc5d 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -639,7 +639,7 @@ Remark ltu_12_wordsize: Proof. unfold Int.iwordsize, Int.zwordsize. simpl. unfold Int.ltu. apply zlt_true. - rewrite !Int.unsigned_repr; try cbn; try omega. + rewrite !Int.unsigned_repr; try cbn; try lia. Qed. (** ** Signed longs *) @@ -690,14 +690,14 @@ Proof. intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto. unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). destruct (zlt (Int.signed n) (Int.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int.add_signed. symmetry; apply Int.signed_repr. specialize (Int.eq_spec n (Int.repr Int.max_signed)). rewrite EQMAX; simpl; intros. assert (Int.signed n <> Int.max_signed). { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); omega. + generalize (Int.signed_range n); lia. Qed. Lemma cmpl_ltle_add_one: forall v n, @@ -708,14 +708,14 @@ Proof. intros v n EQMAX. unfold Val.cmpl_bool; destruct v; simpl; auto. unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). destruct (zlt (Int64.signed n) (Int64.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)). rewrite EQMAX; simpl; intros. assert (Int64.signed n <> Int64.max_signed). { red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); omega. + generalize (Int64.signed_range n); lia. Qed. Remark lt_maxsgn_false_int: forall i, |