app builder unification problem

Stream: metaprogramming / tactics

[Bhavik Mehta]

Here's my example:

constant r : ℕ → ℕ → ℕ → Prop

lemma my_lemma {x y z : ℕ} (xyz : r x y z) : x ≠ z → x ≠ y := sorry

meta def tactic.my_tac : expr → expr → tactic unit := λ e₁ e₂,
do i ← tactic.mk_app `my_lemma [e₁, e₂],
   tactic.note `my_hyp none i,
   tactic.skip

example {x y z : ℕ} (xyz : r x y z) (h : x ≠ z) : x ≠ y :=
begin
  have my_hyp := my_lemma xyz h,
  -- I'm happy
end

set_option trace.app_builder true

example {x y z : ℕ} (xyz : r x y z) (h : x ≠ z) : x ≠ y :=
begin
  do e₁ ← tactic.get_local `xyz,
     e₂ ← tactic.get_local `h,
     tactic.my_tac e₁ e₂
  -- app builder is unhappy
end

My desired goal is for the do block to act like the have := in the example before (in my actual case I'll be running my_tac on a list, but for now I'm just treating them as local constants). The second block gives an app_builder_exception, with error message

[app_builder] failed to create an 'my_lemma'-application, failed to solve unification constraint for #2 argument (?x_0 = ?x_1 =?= x ≠ z)

I don't really know how I can fix this - why is app_builder failing, is there an easy way to fix this, or is there another way I should be making my expression?

[Rob Lewis]

I'm not sure why mk_app isn't working here, but mk_mapp and to_expr ``(my_lemma %%e₁ %%e₂) both work

[Bhavik Mehta]

My guess is that mk_app works by trying to unify arguments from the right-most, and it counts the equality in the implication for the disequality as an argument, leading to failure. The to_expr way works well in my case, thanks!