Grab the nth argument of a function call via metaprogramming

Stream: new members

[Malcolm Langfield]

I am guessing there's some basic type theoretic reason why this is impossible, but I am trying to pattern match on a specific function to extract an argument out a function call (with default). Here is a MWE:

import Mathlib

  @[match_pattern]
  def f (a b : ℕ) : ℕ := a + b

  def g : ℕ → ℕ
    | f a b => a
    | n => n

I get the following error: ■ invalid patterns, a is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching .(Nat.add a b)

Is anything like this possible without adding a constructor to the underlying type? Even with metaprogramming?

[Kevin Buzzard]

f 1 3 = f 2 2 = 4, so what do you expect g 4 to be?

[Malcolm Langfield]

I expect g 4 = 4, so I guess this reveals the issue. It requires that the argument to g is not evaluated until after the call to g, or something vaguely like that?

[Malcolm Langfield]

In fact the value of the function changes depending on whether the expression passed to it is simplified or not. But this is precisely the behavior I want. Would it be possible to write a tactic combinator that does this?

I suppose this means that if one were to write a thing that does this, it would not be a function in the mathematical sense, but maybe more like a parser.

[Malcolm Langfield]

Indeed this can be done.

  def f (a b : Nat) : Nat := a + b

  open Lean.Elab.Tactic in
  elab "extract_first_argument " n:ident " : " v:term " giving the aforementioned argument the name " name:ident : tactic =>
    let a :=
      match v with
        | `(f $a:term $_:term) => a
        | _ => v
    withMainContext do
      evalTactic <| ← `(tactic| generalize $n : $a = $name)

  example : f 3 4 = 7 := by
    extract_first_argument eq : f (1 + 2 + 3 + 4) 4 giving the aforementioned argument the name a
    simp only

[Adam Topaz]

You can even make a term elaborator that does this:

import Lean

open Lean Elab Term

elab "last_arg%" t:term : term => do
  match ← elabTerm t none with
    | .app _ f => return f
    | _ => throwError "Not a function call."


example (f : Nat → Nat → Nat) : (last_arg% (f 1)) = 1 := rfl

[Adam Topaz]

This doesn't do exactly what you want since it gets the last argument, not the first one, but you get the idea

[Adam Topaz]

Here's a variant that gets the first arg:

elab "first_arg%" t:term : term => do
  match (← elabTerm t none).getAppFnArgs with
    | (_, .mk (a :: _)) => return a
    | _ => throwError "Failed"

[Malcolm Langfield]

Oh this is extremely nice! Thanks so much, I will probably use this instead! :heart: