Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: to_expr with hint


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

view this post on Zulip Simon Hudon (Jan 19 2021 at 16:25):

use unify e e' before the match

view this post on Zulip Patrick Massot (Jan 19 2021 at 16:25):

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

view this post on Zulip Patrick Massot (Jan 19 2021 at 16:26):

And Lean complains e' is a pexpr.

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

view this post on Zulip Patrick Massot (Jan 19 2021 at 16:27):

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

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

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

view this post on Zulip Simon Hudon (Jan 19 2021 at 16:28):

(where t is the expected type)

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

view this post on Zulip Simon Hudon (Jan 19 2021 at 16:30):

Where do you get that pexpr from?

view this post on Zulip Patrick Massot (Jan 19 2021 at 16:31):

It's an argument of the tactic.

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

view this post on Zulip Patrick Massot (Jan 19 2021 at 16:32):

Oh it does

view this post on Zulip Patrick Massot (Jan 19 2021 at 16:32):

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

end

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

view this post on Zulip Patrick Massot (Jan 19 2021 at 16:33):

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

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

view this post on Zulip Simon Hudon (Jan 19 2021 at 16:37):

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

view this post on Zulip Simon Hudon (Jan 19 2021 at 16:37):

(don't forget the edit)

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

view this post on Zulip Simon Hudon (Jan 19 2021 at 16:48):

What if you use i_to_expr instead of to_expr?

view this post on Zulip Patrick Massot (Jan 19 2021 at 16:48):

same

view this post on Zulip Simon Hudon (Jan 19 2021 at 16:50):

Sorry, what we want is i_to_expr_no_subgoals

view this post on Zulip Patrick Massot (Jan 19 2021 at 16:53):

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

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

view this post on Zulip Simon Hudon (Jan 19 2021 at 17:09):

Error message?

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

view this post on Zulip Patrick Massot (Jan 19 2021 at 17:13):

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

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

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

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

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

view this post on Zulip Yakov Pechersky (Jan 19 2021 at 19:51):

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.


Last updated: May 09 2021 at 21:10 UTC