to_expr with hint

Stream: metaprogramming / tactics

[Patrick Massot]

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]

use unify e e' before the match

[Patrick Massot]

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

[Patrick Massot]

And Lean complains e' is a pexpr.

[Simon Hudon]

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]

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

[Simon Hudon]

Patrick Massot said:

And Lean complains e' is a pexpr.

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

[Simon Hudon]

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

[Simon Hudon]

(where t is the expected type)

[Patrick Massot]

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]

Where do you get that pexpr from?

[Patrick Massot]

It's an argument of the tactic.

[Patrick Massot]

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

[Patrick Massot]

Oh it does

[Patrick Massot]

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

end

[Patrick Massot]

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

[Patrick Massot]

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

[Simon Hudon]

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]

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

[Simon Hudon]

(don't forget the edit)

[Patrick Massot]

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]

What if you use i_to_expr instead of to_expr?

[Patrick Massot]

same

[Simon Hudon]

Sorry, what we want is i_to_expr_no_subgoals

[Patrick Massot]

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

[Patrick Massot]

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

[Simon Hudon]

Error message?

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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]

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]

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],
    refine add_pos_of_nonneg_of_pos _ (by norm_num),
    simpa using hn },
  { norm_cast,
    rw floor_coe }
end

[Yakov Pechersky]

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.