# Zulip Chat Archive

## 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".

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

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,`

#### Alastair Horn (Mar 31 2020 at 01:57):

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: May 06 2021 at 20:13 UTC