The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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