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,
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


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: May 14 2021 at 07:19 UTC