Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Int63, simplification and native computation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Int63, simplification and native computation


Chronological Thread 
  • 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
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928




Archive powered by MHonArc 2.6.18.

Top of Page