Tactic writing: forall to lambda

Stream: new members

[Alastair Horn]

Continuing from earlier, I've been learning more about writing tactics. This time my problem is harder to describe, please bear with me.

Background:
I'm now trying to write a tactic (a basic imitation of mathlib's wlog) for a project a friend and I are working on (a basic continuation of the natural numbers game). I've called it wlog_le, and it should take two naturals m n and give two goals, the first is to show that the original goal is symmetric in m and n, and the second is to show that the original goal holds under the assumption that m <= n. Here's my code:

-- The theorem to be applied (proof isn't relevant)
theorem wlogle (p: nat → nat → Prop)
(hsymm: ∀ m n: nat, p m n → p n m):
(∀ m n: nat, m ≤ n → p m n) → (∀ m n: nat, p m n)
:= sorry

open tactic
open tactic.interactive
open interactive (parse)
open interactive.types (texpr)
open lean.parser

-- Convert a goal relating two variables into two goals
-- One showing symmetry of the goal,
-- One with hypothesis m ≤ n showing the original goal.
meta def tactic.interactive.wlog_le
(m n : parse ident)
(hsymm : parse (optional (tk "with" *> ident)))
(hle : parse (optional ident)): tactic unit :=
do
  em ← get_local m,
  en ← get_local n,
  symm_name ← get_unused_name `hsymm,
  le_name ← get_unused_name `hle,
  let symm := hsymm.get_or_else symm_name,
  let le := hle.get_or_else le_name,
  revert_lst [en, em],
  -- We fail to apply wlogle, because it cannot unify
  -- Need to convert a goal of the form ∀ m n : nat, p m n
  -- into λ m n : nat, p m n
  tactic.applyc ``wlogle,
  tactic.intro_lst [m, n, symm],
  swap,
  tactic.intro_lst [m, n, le],
  swap

variables {m n k : nat}

-- As an example of something we could prove
theorem mul_cancel_: m ≠ 0 → m * n = m * k → n = k :=
begin
  assume hmnz,
  -- The tactic needs to turn the reverted ∀ into a λ
  wlog_le k n with hs hl,
end

I've proven the general result as a theorem (the proof I've omitted here) and now I want to make its application into a more friendly tactic wlog_le, that modifies goals and assumptions.

Problem:
This tactic fails. The wlogle theorem needs to be supplied with a p : nat -> nat -> Prop, to unify (in more basic cases it can manage). How can I convert a goal of the form ∀ m n : p m n into a function λ m n: p m n using tactics?

Sorry for how complicated this is, I couldn't think of a more basic case which brought about the same problem.

[Kevin Buzzard]

"How can I convert a goal of type forall... Into a function lambda..." sounds to me like the question "how can I convert a type P into a term of type P?" and I guess that's impossible in general

[Alastair Horn]

Hmm, well, I'm not trying to convert it, I just need to form a lambda expression that is similar to the forall, if that makes sense. You might be right though.

[Mario Carneiro]

you could match on expr.pi a (expr.pi b body) and produce expr.lam a (expr.lam b body) (there are more arguments than that, this is just illustrative)

[Alastair Horn]

I think I tried something similar. For example, putting `(expr.pi %%a %%b %%c %%d) ← target, above my applyc, gives me "match failed".

[Mario Carneiro]

don't quote it

[Mario Carneiro]

expr.pi is literally a constructor of expr, so you should just write expr.pi a b c d ← target,

[Alastair Horn]

Ah I see

[Alastair Horn]

Yep I've sorted it after some struggle

[Alastair Horn]

Thank you again Kevin and Mario