Zulip Chat Archive

Stream: new members

Topic: Tactic writing: forall to lambda


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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".

view this post on Zulip Mario Carneiro (Mar 31 2020 at 01:55):

don't quote it

view this post on Zulip 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,

view this post on Zulip Alastair Horn (Mar 31 2020 at 01:57):

Ah I see

view this post on Zulip Alastair Horn (Mar 31 2020 at 02:18):

Yep I've sorted it after some struggle

view this post on Zulip Alastair Horn (Mar 31 2020 at 02:18):

Thank you again Kevin and Mario


Last updated: May 06 2021 at 20:13 UTC