diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-06-08 00:30:31 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-06-08 00:30:31 +0200 |
| commit | dbff5b8a016fe9f6667ea007be3de764a50b620a (patch) | |
| tree | c9b4b90f3efdb08ccf7c73b4439746ce5c67aeca /riscV | |
| parent | a14865049571f157896107ebf0b2f908b1b95cbc (diff) | |
| download | compcert-kvx-dbff5b8a016fe9f6667ea007be3de764a50b620a.tar.gz compcert-kvx-dbff5b8a016fe9f6667ea007be3de764a50b620a.zip | |
omega -> lia
Diffstat (limited to 'riscV')
| -rw-r--r-- | riscV/Asmgenproof1.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 6abde89f..42ab8375 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -821,18 +821,18 @@ Proof. unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. unfold Int.lt. rewrite zlt_false. auto. change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed. - generalize (Int.signed_range i); omega. + generalize (Int.signed_range i); lia. * exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1). exists rs1; split. eexact A1. split; auto. rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); 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. assert (Int.signed n <> Int.max_signed). { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); omega. + generalize (Int.signed_range n); lia. + apply DFL. + apply DFL. Qed. @@ -919,18 +919,18 @@ Proof. unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. unfold Int64.lt. rewrite zlt_false. auto. change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed. - generalize (Int64.signed_range i); omega. + generalize (Int64.signed_range i); lia. * exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1). exists rs1; split. eexact A1. split; auto. rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); 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. assert (Int64.signed n <> Int64.max_signed). { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); omega. + generalize (Int64.signed_range n); lia. + apply DFL. + apply DFL. Qed. |