Helper functions for match?

Stream: metaprogramming / tactics

[Markus de Medeiros]

I'm writing some metaprograms which involve constructing Exprs that use match statements. So far, I've been able to get away with writing recursor applications "by hand", ie by manually constructing the motive, the types of each branch etc, which is not the same, but is good enough for my application.

This technique is getting fairly cumbersome as I try to support matching with more complex types, so I'm wondering if there's a better way. What is the "happy path" for generating an Expr that includes a match?

[Robin Arnez]

You need to use mkMatcher. Here's an example:

import Lean
import Qq

def simpleMatch (x : List (Nat × Nat)) : Bool :=
  match x with
  | [] => true
  | [_x@(_a, _b)] => false
  | _a :: (_b, 0) :: _c => false
  | _ => true

open Lean Meta Match Qq

elab "test " x:term : term => do
  let discr ← elabTermEnsuringTypeQ x q(List (Nat × Nat))
  let matcher ← mkMatcher {
    matcherName := ← mkAuxDeclName `match
    matchType := q(List (Nat × Nat) → Unit)
    discrInfos := #[{}]
    lhss := [
      {
        ref := ← getRef
        fvarDecls := []
        patterns := [.ctor ``List.nil [0] [q(Nat × Nat)] []]
      },
      ← withLocalDeclDQ `a q(Nat) fun a =>
      withLocalDeclDQ `b q(Nat) fun b =>
      withLocalDeclDQ `x q(Nat × Nat) fun x =>
      withLocalDeclDQ `x_eq q($x = ($a, $b)) fun x_eq =>
        return {
          ref := ← getRef
          fvarDecls := ← [a, b, x, x_eq].mapM (·.fvarId!.getDecl)
          patterns :=
            [.ctor ``List.cons [0] [q(Nat × Nat)]
              [.as x.fvarId!
                (.ctor ``Prod.mk [0, 0] [q(Nat), q(Nat)] [.var a.fvarId!, .var b.fvarId!])
                x_eq.fvarId!,
                .ctor ``List.nil [0] [q(Nat × Nat)] []]]
        },
      ← withLocalDeclDQ `a q(Nat × Nat) fun a =>
      withLocalDeclDQ `b q(Nat) fun b =>
      withLocalDeclDQ `c q(List (Nat × Nat)) fun c =>
        return {
          ref := ← getRef
          fvarDecls := ← [a, b, c].mapM (·.fvarId!.getDecl)
          patterns :=
            [.ctor ``List.cons [0] [q(Nat × Nat)]
              [.var a.fvarId!, .ctor ``List.cons [0] [q(Nat × Nat)]
                [.ctor ``Prod.mk [0, 0] [q(Nat), q(Nat)] [.var b.fvarId!, .val q((0 : Nat))],
                  .var c.fvarId!]]]
        },
      ← withLocalDeclDQ `x q(List (Nat × Nat)) fun x =>
        return {
          ref := ← getRef
          fvarDecls := [← x.fvarId!.getDecl]
          patterns := [.var x.fvarId!]
        }
    ]
  }
  matcher.addMatcher
  Lean.logInfo matcher.matcher
  let motive : Q(List (Nat × Nat) → Type) := q(fun _ => Bool)
  let alt1 : Q(Unit → Bool) := q(fun _ => true)
  let alt2 : Q((a : Nat) → (b : Nat) → (x : Nat × Nat) → (x_eq : x = (a, b)) → Bool) := q(fun _ _ _ _ => false)
  let alt3 : Q((a : Nat × Nat) → (b : Nat) → (c : List (Nat × Nat)) → Bool) := q(fun _ _ _ => false)
  let alt4 : Q((x : List (Nat × Nat)) → Bool) := q(fun _ => true)
  return mkAppN matcher.matcher #[motive, discr, alt1, alt2, alt3, alt4]

def simpleMatchWithElab (x : List (Nat × Nat)) : Bool :=
  test x

mkMatcher takes in a matcher input and then creates a matcher function and returns (among other things for error reporting) a side effect to add the matcher to the environment (addMatcher) and a matcher expression.
Let's first look through the matcher input:
First is the matcher name. This is the name under which the matcher will be added into the environment when addMatcher is run. You can use some specific name but usually you'll just use mkAuxDeclName `match which adds it under the name <declname>.match_<n>.
The next part is the matcher type. This should just consist of nested foralls (one for each discriminant) and one final inner type. Which type you choose here doesn't really matter as long as it lives in the same universe as the type the match should have at the end. For example you can use True here if you want to use match within a proof, or Unit if the type is of type Type (e.g. Bool in this example), or in general PUnit.{u} with the right universe level.
Then comes discrInfos: This contains information for each discriminant whether you want an equality hypothesis and if yes under which name (in the sense of match h : n with ... where you would have the equality hypothesis with name h).
Lastly and most importantly lhss: This provides the left-hand sides of all alternatives (i.e. what you match with). Each left-hand side then contains a ref for error reporting but more importantly, patterns and fvarDecls. Each pattern in the patterns list corresponds to a pattern in the left-hands side of the alternative so you have as many patterns as you have discriminants. fvarDecls then should contain LocalDecls for every variable bound by the pattern. Why do you need this? Well, for one this describes the order of variables for the alternative of the resulting matcher (so make sure the variables are in dependency order!) but also you might've noticed that I wrapped the AltLHS creation within docs#Lean.Meta.withLocalDecl​s -- that means that I added declarations to the local context that exist while we're constructing the AltLHS but don't exist anymore after that and in particular not when we run mkMatcher. So with fvarDecls we provide the information of the name, type and id of the free variables (retrievable through docs#Lean.FVarId.getDecl) so that mkMatcher can later add them back with docs#Lean.Meta.withExistingLocalDecls.
Now for the description of the different pattern kinds:

• .var v is simply a variable pattern, something like _a, _b, _c in my example. Note that free variables are usually passed around as expressions and here v is directly an FVarId so you might need to use docs#Lean.Expr.fvarId! to get what you need.
• .ctor ctorName levelParams params fields represents the application of constructor (specifically @ctorName.{levelParams...} params... fields...). params are the arguments to the constructor that you can't match on (usually implicits), specifically, #print <inductive type> shows you how many of them your inductive type has. The remaining arguments, the fields, are arguments of the constructor that you can match on, so in constrast to the parameters (which are provided as Exprs), those are provided as patterns. As an example, take the (_a, _b) in the second alternative of simpleMatch: With universes and explicit parameters, this looks like @Prod.mk.{0, 0} Nat Nat _a _b, so you have ctorName = ``Prod.mk, levelParams = [0, 0], params = [Nat, Nat] and patterns = [_a, _b].
• .val e allows you to have "exact matches", i.e. to match on a specific exact value. The usual case for these is numbers but match allows you to use any expression of a type with decidable equality.
• .as xId pattern hId represents the named pattern x@h:pattern. Note that in the usual match syntax, the equality variable is optional; here you need to specify it explicitly. In principle, this is similar to .var where you bind the pattern in the variable xId (again, FVarId, not Expr) but you additionally provide a pattern to match further and a variable hId : x = pattern.
• .inaccessible e is for inaccessible patterns (.(e)). Inaccessible patterns are values that aren't matched on any further but have a concrete value forced by the typing of the remaining patterns. As an example, take:

inductive TestType : Nat → Prop where
  | one : TestType 1

example (n : Nat) (h : TestType n) : n = 1 :=
  match h with
   | .one => rfl

Since the value for n needs to change in the .one branch (previously TestType n, now TestType 1), we also need to match on n. Since the value is here forced to be 1 through the typing of h : TestType 1, we use an inaccessible pattern:

example (n : Nat) (h : TestType n) : n = 1 :=
  match n, h with
   | .(1), .one => rfl

This is stuff match usually does for you but that needs to be taken into consideration when using mkMatcher.

• Finally, there's .arrayLit type patterns. This one is for the array literal (#[patterns...] : Array type). Similarly to .ctor we simply have the element type as a "parameter" and then patterns for each element we want to match on.

Finally some more information on the output of mkMatcher, specifically, the matcher expression: The first thing it takes is the motive which needs to have one parameter per discriminant and needs to live in the same universe as the body of matchType. After that come all of the discriminants that we want to match on. Lastly, we can provide all the right hand sides of the alternatives which should take in parameters in the order they were provided in fvarDecls and then (if applicable) for each discriminant with an equality hypothesis name specified in discrInfos, such an equality (h : discriminant = pattern). If an alternative has no fvarDecls and we also have no discriminants with equality hypotheses, the alternative will instead need to take in a single parameter of type Unit (such as seen in the first alternative in my example).

[Markus de Medeiros]

Thank you for the thorough explanation , I think this will take me a while to digest but it does look like what I'm after.