Convert Divisibility Hypothesis to pexpr

Stream: general

[Aaron Bryce]

I've come across an issue with a tactic I'm trying to write, which needs to have different behaviour based on the divisibility of the inputs, and I need to be able to convert the hypothesis generated by the if statement into a pexpr (or expr as the conversion between the two is not an issue) to use later in the tactic.

/-- If `x ∣ y` return an `expr` containing a proof! -/ meta def baz (x y : ℕ) : tactic (option expr) := if h : x ∣ y then some <$> to_expr ``(reflect %%h) else pure none

The above code currently errors with, failed to find type class instance for has_to_pexpr (x ∣ y). Does anyone know if this instance exists and just can't be inferred correctly, a way to make this instance if it doesn't exist, or an alternative way to convert the hypothesis to a (p)expr?

[Mario Carneiro]

It is not possible to do what you are attempting, because h does not exist in the VM

[Scott Morrison]

:-(

[Mario Carneiro]

Instead, you merely learn from that if statement that in fact x divides y, without a proof

[Mario Carneiro]

You can try to produce a proof by using dec_trivial

[Mario Carneiro]

by norm_num is probably the best method

[Scott Morrison]

Oh, I see. You have the if statement that is executed in the tactic logic, and then when it's time to build the expr you're after, you build the proof again inside a quotation.

[Scott Morrison]

Is this doing it?

open tactic

/-- If `x ∣ y` return an `expr` containing a proof! -/
meta def baz (x y : ℕ) : tactic (option expr) :=
if h : x ∣ y then
  some <$> to_expr ``(by norm_num : %%(reflect x) ∣ %%(reflect y))
else
  pure none

[Mario Carneiro]

/-- If `x ∣ y` return an `expr` containing a proof! -/
meta def baz (x y : ℕ) : tactic (option expr) :=
if x ∣ y then do
  (_, p) ← norm_num.derive `((%%(reflect x) : ℕ) ∣ %%(reflect y)),
  p' ← tactic.mk_eq_mpr p `(trivial),
  return (some p')
else
pure none

run_cmd do
  some e <- baz 2 6, tactic.infer_type e >>= tactic.trace

[Mario Carneiro]

you build the proof again

You never built a proof the first time. For all you know the reason x | y evaluated to true is because it evaluated it with GMP natural numbers

[Scott Morrison]

Huh. Okay!

[Scott Morrison]

Lean is awesome. :-)

[Aaron Bryce]

Indeed. Both dec_trivial and norm_num seem to work in this instance, this tactic is now appears to be fully working Scott.