Zulip Chat Archive

Stream: general

Topic: help with `has_to_pexpr`

Scott Morrison (May 23 2020 at 13:46):

I'm not sure how to construct has_to_pexpr instances, and there are few useful examples around. In particular, I'd like to make the following work:

import tactic

open tactic

meta instance nat_pexpr : has_to_pexpr  := pexpr.of_expr  λ n, reflect n
meta instance int_pexpr : has_to_pexpr  := pexpr.of_expr  λ n, reflect n

meta def turkle (p : ) : tactic unit :=
do M  to_expr ``(2^%%p - 1 : ) >>= eval_expr ,
   t  to_expr ``(2^%%p - 1 = %%M),
   v  to_expr ``(by norm_num : 2^%%p - 1 = %%M),
   assertv `w t v,

example : true :=
  turkle 5,
  -- This produces `w : 2^5 - 1 = int.of_nat 31`,
  -- but I want:
  guard_hyp w := 2^5 - 1 = (31 : ),

Scott Morrison (May 23 2020 at 13:48):

I guess this is the int_pexpr instance's fault, but I don't know what to replace it with.

Scott Morrison (May 23 2020 at 13:55):

Oh... maybe I undestand. I just have to calculate the binary digits of my integer, and build the pexpr out of bit0 and bit1 directly? (And put in a negative sign if the integer is negative...)

Scott Morrison (May 23 2020 at 13:56):

Does this exist somewhere already? It seems like the sort of thing that someone would have wanted before me.

Scott Morrison (May 23 2020 at 14:15):

Alternatively, adding `[simp at w] at the end of turkle achieves the desired result, so I'm going to leave this for now.

Reid Barton (May 23 2020 at 14:17):

Presumably whatever is building int.of_nat 31 already knows how to do the bit0/bit1 part.

Simon Hudon (May 23 2020 at 17:20):

You may want to look at the has_reflect instance for nat. I believe that's where the bit0 / bit1 logic is. My guess is that has_reflect on int is done by pattern matching on the int, reflecting the nat and then applying the constructor. Instead, you can treat the int as a number in its own right and do the binary division and add a minus when necessary

Mario Carneiro (May 23 2020 at 19:42):

the eval_expr on the first line is completely unnecessary, just do let M := 2^p-1

Last updated: Aug 03 2023 at 10:10 UTC