Zulip Chat Archive

Stream: general

Topic: auto_param


Patrick Massot (Jul 19 2019 at 12:23):

I have a really dumb-sounding question: how can I get Lean to automatically use auto_params? I have a lemma with assumption (hconj : ∀ x₀ : α, tendsto (λ x: α, x₀*x*x₀⁻¹) 𝓝 1 𝓝 1 . prove_conj) where prove_conj tries to prove the assumption using commutativity of multiplication. My idea was that would succeed when the relevant multiplication is commutative, and leave the hypothesis to prove otherwise. But clearly I misunderstood how this all works. I can only use it by writing by apply_auto_param where wants a proof of hconj.

Rob Lewis (Jul 19 2019 at 13:59):

That is how it works in general, with the exception that the goal left when the tactic fails is kind of ugly. Do you have a MWE?

def my_fun {α} (a b : α) (h : a = b . tactic.interactive.reflexivity) : a = b := h

example : 1 = 1 := my_fun _ _

example : 1 = 1 := by apply my_fun

example : 1 = 2 :=
begin
  apply my_fun,
  dsimp, -- 1 = 2
end

Patrick Massot (Jul 19 2019 at 14:04):

I think I'm starting to understand. The magic argument has to come last, right?

Patrick Massot (Jul 19 2019 at 14:04):

This fails:

lemma my_fun {α} (a b : α) (h : a = b . tactic.interactive.reflexivity) (h' : 0 = 0) : a = b := h

example : 1 = 1 := my_fun 1 1 (rfl : 0 = 0)

Patrick Massot (Jul 19 2019 at 14:04):

which makes sense. But I was hoping to write:

lemma my_fun {α} (a b : α) (h : a = b . tactic.interactive.reflexivity) (h' : 0 = 0) : a = b := h

example : 1 = 1 := my_fun 1 1 _ (rfl : 0 = 0)

which also fails


Last updated: Dec 20 2023 at 11:08 UTC