## Stream: metaprogramming / tactics

### Topic: to_expr with hint

#### Patrick Massot (Jan 19 2021 at 16:23):

How can I help to_expr when I have partial information about the expected type? In

open tactic
run_cmd do
mv ← mk_mvar,
let e' := ((0 : ℤ) < %%mv),
e ← to_expr (0 < 1),
match e with
| (%%L < %%R) := infer_type R >>= tactic.trace
| _ := skip
end


I'd like to replace the to_expr line with "please elaborate  (0 < 1) so that it unifies with e' so that the trace will print int.

#### Simon Hudon (Jan 19 2021 at 16:25):

use unify e e' before the match

#### Patrick Massot (Jan 19 2021 at 16:25):

Isn't it too late? Lean will have already elaborated, right?

#### Patrick Massot (Jan 19 2021 at 16:26):

And Lean complains e' is a pexpr.

#### Simon Hudon (Jan 19 2021 at 16:26):

It will be it won't have assigned types to meta variables. In your case, I hadn't considered it but the numerals will have been defaulted to nat

#### Patrick Massot (Jan 19 2021 at 16:27):

That's the main point: I want to get around that nat by default crazyness.

#### Simon Hudon (Jan 19 2021 at 16:27):

Patrick Massot said:

And Lean complains e' is a pexpr.

You can solve that issue with e' <- to_expr ((0 : ℤ) < %%mv),

#### Simon Hudon (Jan 19 2021 at 16:28):

If you know what type you want them to be, you can write to_expr (0 < (1 : %%t))

#### Simon Hudon (Jan 19 2021 at 16:28):

(where t is the expected type)

#### Patrick Massot (Jan 19 2021 at 16:29):

Maybe I minimized too much. I want to use change_core, but it wants a expr as the new goal and if I use to_expr it gets the wrong numerals.

#### Simon Hudon (Jan 19 2021 at 16:30):

Where do you get that pexpr from?

#### Patrick Massot (Jan 19 2021 at 16:31):

It's an argument of the tactic.

#### Patrick Massot (Jan 19 2021 at 16:31):

I'm super confused, now I no longer understand why the interactive change tactic doesn't have this issue.

Oh it does

#### Patrick Massot (Jan 19 2021 at 16:32):

example : (0 : ℤ) < 1 :=
begin
change 0 < 1,

end


#### Patrick Massot (Jan 19 2021 at 16:32):

This doesn't work, and it's exactly the minimized version of the problem that's driving me crazy.

#### Patrick Massot (Jan 19 2021 at 16:33):

Can anyone make a version of change that succeeds in the above example?

#### Simon Hudon (Jan 19 2021 at 16:37):

def force_type (p : Sort*) (x : p) := p

meta def my_change (p : pexpr) : tactic unit :=
do g :: gs <- get_goals,
(force_type %%p _) <- to_expr (force_type %%p %%g),
/- etc -/


#### Simon Hudon (Jan 19 2021 at 16:37):

I think that should work. Can you try it and tell me how it goes?

#### Simon Hudon (Jan 19 2021 at 16:37):

(don't forget the edit)

#### Patrick Massot (Jan 19 2021 at 16:43):

It works a bit too much, it creates two copies of my goal:

import tactic

namespace tactic
setup_tactic_parser
def force_type (p : Sort*) (x : p) := p

@[interactive]
meta def my_change (p : parse texpr) : tactic unit :=
do g ← get_goal,
(force_type %%p _) ←  to_expr (force_type %%p %%g),
skip
end tactic

example : (0 : ℤ) < 1 :=
begin
my_change 0 < 1,
/-
2 goals
⊢ 0 < 1

⊢ 0 < 1
-/
end


#### Simon Hudon (Jan 19 2021 at 16:48):

What if you use i_to_expr instead of to_expr?

same

#### Simon Hudon (Jan 19 2021 at 16:50):

Sorry, what we want is i_to_expr_no_subgoals

#### Patrick Massot (Jan 19 2021 at 16:53):

That one seems to work! I'll try it in the real use case.

#### Patrick Massot (Jan 19 2021 at 17:08):

It doesn't work in the real world :sad:

example (n : ℕ) : 1/(n+1 : ℝ) > 0 :=
begin
my_change 1/(n+1) > 0, -- fails
sorry
end


Error message?

#### Patrick Massot (Jan 19 2021 at 17:10):

type mismatch at application
tactic.force_type (1 / (n + 1) > 0) ?m_1
term
?m_1
has type
1 / (↑n + 1) > 0
but is expected to have type
1 / (n + 1) > 0
state:
n : ℕ
⊢ 1 / (↑n + 1) > 0


#### Patrick Massot (Jan 19 2021 at 17:13):

I understand Lean finds this tricky, but it's very sad.

#### Patrick Massot (Jan 19 2021 at 17:15):

This coercion from nat to real is so important for my course that I'm tempted to have a specific hack trying to put it in front of local variable that has type nat in case the change fails.

#### Patrick Massot (Jan 19 2021 at 17:18):

Your version is still performing better than the official one, my_change 1/(↑n+1) > 0, works whereas change 1/(↑n+1) > 0, fails

#### Patrick Massot (Jan 19 2021 at 17:48):

I've spent way too much time fighting this. I give up. I'd still be very grateful if someone can get this to work (including by hard-wiring a special treatment of the nat to real coercion).

#### Yakov Pechersky (Jan 19 2021 at 19:49):

Is it possible to get a can_lift working here?
For example:

instance : can_lift ℝ ℤ :=
⟨coe, λ x, x = floor x, λ x h, ⟨floor x, h.symm⟩⟩

example (n : ℤ) (hn : 0 ≤ n) : 1/(n+1 : ℝ) > 0 :=
begin
lift ((n + 1) : ℝ) to ℤ with z hz,
{ simp only [hz, one_div, gt_iff_lt, inv_pos],

The proof construction for the second goal can probably be automated. And there seem to be some lemmas necessary to make the can_lift to work transitively from real to nat`.