From 6d1223d053f1ff10792d5ed5d00d3830ff61e9d7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 25 Apr 2019 11:54:18 +0200 Subject: simplify proof slightly --- mppa_k1c/SelectOpproof.v | 36 ++++++++++++++++-------------------- 1 file changed, 16 insertions(+), 20 deletions(-) (limited to 'mppa_k1c/SelectOpproof.v') 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. -- cgit