diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 13:08:58 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 13:08:58 +0200 |
commit | 64d7dab2720d63e1b40ae893d76895a23c11e2d1 (patch) | |
tree | 825f95d64dc9bfa50565c03daf6e983d6c7ba5cc /mppa_k1c/SelectLongproof.v | |
parent | 43e2036b6f10efdb7e63613067da16fa7fa4b421 (diff) | |
download | compcert-kvx-64d7dab2720d63e1b40ae893d76895a23c11e2d1.tar.gz compcert-kvx-64d7dab2720d63e1b40ae893d76895a23c11e2d1.zip |
more simplifications
Diffstat (limited to 'mppa_k1c/SelectLongproof.v')
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 3fab35b3..d4893eb8 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -534,14 +534,16 @@ Theorem eval_xorlimm: forall n, unary_constructor_sound (xorlimm n) (fun v => Va Proof. unfold xorlimm; intros; red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. - exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.xor_zero; auto. - destruct (xorlimm_match a); InvEval; subst. -- econstructor; split. apply eval_longconst. simpl. rewrite Int64.xor_commut; auto. -- rewrite Val.xorl_assoc. simpl. rewrite (Int64.xor_commut n2). - predSpec Int64.eq Int64.eq_spec (Int64.xor n n2) Int64.zero. -+ rewrite H. exists v1; split; auto. destruct v1; simpl; auto. rewrite Int64.xor_zero; auto. -+ TrivialExists. -- TrivialExists. + - exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.xor_zero; auto. + - predSpec Int64.eq Int64.eq_spec n Int64.mone. + -- subst n. intros. rewrite <- Val.notl_xorl. TrivialExists. + -- destruct (xorlimm_match a); InvEval; subst. + + econstructor; split. apply eval_longconst. simpl. rewrite Int64.xor_commut; auto. + + rewrite Val.xorl_assoc. simpl. rewrite (Int64.xor_commut n2). + predSpec Int64.eq Int64.eq_spec (Int64.xor n n2) Int64.zero. + * rewrite H. exists v1; split; auto. destruct v1; simpl; auto. rewrite Int64.xor_zero; auto. + * TrivialExists. + + TrivialExists. Qed. Theorem eval_xorl: binary_constructor_sound xorl Val.xorl. |