diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 11:54:18 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 11:54:18 +0200 |
| commit | 6d1223d053f1ff10792d5ed5d00d3830ff61e9d7 (patch) | |
| tree | d8c12f44f23d87f73027f392bbc3f454dedf85be | |
| parent | 2f549eaf7f6bc7e97d8f8a830d18808c2ae66186 (diff) | |
| download | compcert-kvx-6d1223d053f1ff10792d5ed5d00d3830ff61e9d7.tar.gz compcert-kvx-6d1223d053f1ff10792d5ed5d00d3830ff61e9d7.zip | |
simplify proof slightlyv3.5_k1c_1.1
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 36 |
1 files changed, 16 insertions, 20 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 8bc8c96b..4df87bea 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -322,22 +322,20 @@ Proof. rewrite BOUNDS. destruct v1; try (simpl; apply Val.lessdef_undef). replace (Z.sub Int.zwordsize - (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1). + (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega. replace (Z.sub Int.zwordsize (Z.sub (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one) (Z.sub (Z.add (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))) - Z.one) Int.zwordsize))) with (Int.unsigned n). - * rewrite Int.repr_unsigned. - rewrite Int.repr_unsigned. - simpl. - destruct (Int.ltu n1 Int.iwordsize) eqn:Hltu_n1; simpl; trivial. - simpl. - destruct (Int.ltu n Int.iwordsize) eqn:Hltu_n; simpl; trivial. - * omega. - * omega. + Z.one) Int.zwordsize))) with (Int.unsigned n) by omega. + rewrite Int.repr_unsigned. + rewrite Int.repr_unsigned. + simpl. + destruct (Int.ltu n1 Int.iwordsize) eqn:Hltu_n1; simpl; trivial. + simpl. + destruct (Int.ltu n Int.iwordsize) eqn:Hltu_n; simpl; trivial. + TrivialExists. constructor. econstructor. constructor. eassumption. constructor. simpl. reflexivity. constructor. simpl. reflexivity. - TrivialExists. - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. @@ -381,22 +379,20 @@ Proof. rewrite BOUNDS. destruct v1; try (simpl; apply Val.lessdef_undef). replace (Z.sub Int.zwordsize - (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1). + (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega. replace (Z.sub Int.zwordsize (Z.sub (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one) (Z.sub (Z.add (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))) - Z.one) Int.zwordsize))) with (Int.unsigned n). - * rewrite Int.repr_unsigned. - rewrite Int.repr_unsigned. - simpl. - destruct (Int.ltu n1 Int.iwordsize) eqn:Hltu_n1; simpl; trivial. - simpl. - destruct (Int.ltu n Int.iwordsize) eqn:Hltu_n; simpl; trivial. - * omega. - * omega. + Z.one) Int.zwordsize))) with (Int.unsigned n) by omega. + rewrite Int.repr_unsigned. + rewrite Int.repr_unsigned. + simpl. + destruct (Int.ltu n1 Int.iwordsize) eqn:Hltu_n1; simpl; trivial. + simpl. + destruct (Int.ltu n Int.iwordsize) eqn:Hltu_n; simpl; trivial. + TrivialExists. constructor. econstructor. constructor. eassumption. constructor. simpl. reflexivity. constructor. simpl. reflexivity. - TrivialExists. - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. |