Zulip Chat Archive

Stream: general

Topic: help with `has_to_pexpr`


view this post on Zulip 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,
   skip

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

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: May 14 2021 at 07:19 UTC