coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Int63, simplification and native computation
- Date: Fri, 5 Apr 2019 07:55:15 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga06.intel.com
- Dlp-product: dlpe-windows
- Dlp-reaction: no-action
- Dlp-version: 11.0.400.15
- Ironport-phdr: 9a23:qQNzMRy0smILtlXXCy+O+j09IxM/srCxBDY+r6Qd2+MUIJqq85mqBkHD//Il1AaPAdyCraoawLOM6+igATVGvc/Z9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMq8Uam5duJ6c+xhfUvHdEZ/ldyWd0KV6OhRrx6dq88IJ5/yhMp/4t8tNLXLnncag/UbFWFiktPXov5M3suxnDTA+P6WUZX24LjBdGABXL4Q/jUJvpvST0quRy2C+BPc3rVr80Qiit771qSBDzligKMSMy/XzNhcxxiKJbpw+hpwB6zoXJboyZKOZyc6XAdt4cWGFPXNteVzZZD428cYUBEvYBM+hboYn8u1QBogCzChOwCO7r0DJEmmP60bM83u88EQ/GxgsgH9cWvXjasdv1M7kdUe+pzKnSyjXDd+ta0ir65ojJbh8hoeuDUqx0ccbf1EIiEAbFjlSMpozlJTyayOANv3KA7+pnS+2vhHInqxt2oji33cosi4/Jhp4LxVDA7yl23IE1JdihRUN9fNWqHpxQtySAOIt3RMMvW2BouCAmyrIYvZ63ZjUFx4ohyhXCaPKHa5CF7g/tWeueOzt0mXxodb2lixqv/0Wty/fwW8ep3FpSsyZIk9fBumoD2hHd8MSLVPVw80O71TqS1A3f9vlILV01mKffMZIt3L49m5UJvUjdBCP6hlj6gamLfUs+4Oeo8f7oYrD+q5+cKYB0jgb+P7wrmsywG+s0LgkDU3Ka+eS6yL3s40n5TK9Wgf0xl6nVqJHaJcIFqa6lGwJZz4gu5hmlAzu73tkVkmMLIE9LdR+GlYTkNUzCLOj9DfilglSslDlrx+rBPr3kGpjNK3nDn6vhfbln9UFczBA/zctY551KBbEBPOjzWkjptNHDDx85NRC0zPjjCNlnyoweXmePDreDMKzOqV+I+v4vI+6UaYAJvzb9MuEp6OLqjX8kglAQZrKp3JsSaHCgBPtqOUSZYXz2gtcAC2gGpAQ+TPa5wGGFBHRYYG/3VKYh7Bk6DpinBMHNXMrl1LeGxWKwGoBcTmFAEFGFV3nyIdaqQfAJPWipJcJujiYDTfzpbo4q1RijsEWyn79mJerd9ylerpXu28Rv4PX7lBcu+DgyBMOYhTLeB1pol38FEmdllJt0plZwnw/agPpIxsdAHNkW3MtnFwIzNJrS1et/UomgWwTdc9PPQ1GjEIz/XWMBC+kpytpLWH5TXs24h0majSusH7IR0beMAc5sq/+O7z3KP894jk3++uwhgl0hG5QdMGKv3vA59g7PCoqPmEKcxf6n
Dear Coq Team,
I am currently adjusting CoqInterval to the changes in master. One thing which I would say is a bit of a nuisance is the handling of simplification for native computation in Int63.
E.g.
Require Import Int63. Require Import ZArith.
Goal Int63.to_Z 1 = 1%Z.
In this situation simpl doesn’t do anything. cbv does the reduction to 1%Z, but in many cases I can’t use it because it expands other terms in my goal I don’t want to be expanded. I know many ways around this (rewriting with an assert I solve with cbv, …) but in the end I think that simpl should simplify stuff which is natively computable.
If I do:
Goal Int63.to_Z 1 = 1%Z. unfold Int63.to_Z. simpl. unfold is_even.
I end up with
(if is_zero (1 land 1) then Z.double else Z.succ_double) ((if is_zero (1 >> 1 land 1) then Z.double else Z.succ_double) ((if is_zero ((1 >> 1) >> 1 land 1) then Z.double else Z.succ_double) ((if is_zero (((1 >> 1) >> 1) >> 1 land 1) then Z.double : :
This can be simplified by unfold "land" to:
(if is_zero 1 then Z.double else Z.succ_double) ((if is_zero (1 >> 1 land 1) then Z.double else Z.succ_double) ((if is_zero ((1 >> 1) >> 1 land 1) then Z.double else Z.succ_double) ((if is_zero (((1 >> 1) >> 1) >> 1 land 1) then Z.double : :
Is there something like a “simplify with native compute”? Is this a bug? How do others live with this definition of integers and simplification?
Best regards,
Michael
Intel Deutschland GmbH |
- [Coq-Club] Int63, simplification and native computation, Soegtrop, Michael, 04/05/2019
- RE: [Coq-Club] Int63, simplification and native computation, Soegtrop, Michael, 04/06/2019
Archive powered by MHonArc 2.6.18.