## Stream: new members

### Topic: Tactic writing: forall to lambda

#### Alastair Horn (Mar 30 2020 at 22:55):

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 (Mar 30 2020 at 23:20):

"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 (Mar 30 2020 at 23:50):

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 (Mar 31 2020 at 01:35):

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 (Mar 31 2020 at 01:53):

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

don't quote it

#### Mario Carneiro (Mar 31 2020 at 01:55):

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

Ah I see

#### Alastair Horn (Mar 31 2020 at 02:18):

Yep I've sorted it after some struggle

#### Alastair Horn (Mar 31 2020 at 02:18):

Thank you again Kevin and Mario

Last updated: Dec 20 2023 at 11:08 UTC