pattern matching in declaration binders

Stream: lean4

[Jakob von Raumer]

I want to transpile to Lean from a language that allows for pattern matching in the argument binders of top level declarations, not only to destruct variables, but also to express partiality. So for example to define the predecessor function you'd be able to simply write

def pred (n + 1 : Nat) : Nat := n

and the function wouldn't evaluate on anything that doesn't match.

Funnily there's a really neat way to mimic this behaviour in Lean, which is to use autoParams to resolve the match:

def pred (m : Nat) {n : Nat} (h : m = n + 1 := by rfl) : Nat := n

As far as I can tell, there's exactly one place, where this pattern is used in Mathlib, namely docs#List.TFAE.out

(Sidenote: An alternative would be to use the existing pattern matching machinery by changing h to (h : m matches _ + 1 := by simp), but then we couldn't have n as a function body but we'd need to simplify ((match m with | n.succ => true | x => false) = true) which is a bit nasty)

This begs the question of how to best have some syntax sugar to emulate this feature in Lean? The syntax around declSig doesn't seem to be built with overloading or extension in mind? Best thing I have managed so far is to make my own version of the def and theorem parsers, but I'm not sure if that's the easiest way. /cc @Sebastian Ullrich @Leo Stefanesco @Tobias Grosser

[Kyle Miller]

What language are you transpiling from? I'm curious to learn more about how partiality works in it.

[Jakob von Raumer]

Sail. It's not a total language in general, but in particular it uses the above pattern to spread multiple "clauses" of one function across different files in order to successively specify different instructions in an ISA.

[Jakob von Raumer]

FWIW I wrote a little prototype for the feature:

syntax extension

import Mathlib.Data.Set.Basic
import Lean.Elab.Command

open Lean Parser Command Term

def smartBinder := leading_parser ppGroup <| "⟦" >> termParser >> ":" >> termParser >> "⟧"

def smartDeclSig := leading_parser
  many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder <|> smartBinder)) >> Term.optType

def smartDefinition := leading_parser
  "sdef " >> declId >> smartDeclSig >> declVal >> optDefDeriving

syntax smartDefinition : command

macro_rules
  | `(sdef $n $bis* $[: $t]? := $b) => do
    let bis' : Array (Array (TSyntax [`ident, `Lean.Parser.Term.hole,
        `Lean.Parser.Term.bracketedBinder])) ← bis.mapM fun bi =>
      match bi with
      | `($i:ident) => pure #[i]
      | `(hole|$h:hole) => pure #[h]
      | `(bracketedBinder|($i $[: $ty]?)) => do pure #[← `(bracketedBinder|($i $[: $ty]?))]
      | `(bracketedBinder|{$i $[: $ty]?}) => do pure #[← `(bracketedBinder|{$i $[: $ty]?})]
      | `(smartBinder|⟦$n:ident + 1 : $_⟧) => do
        pure #[← `(bracketedBinder|(m : Nat)), ← `(bracketedBinder|{$n : Nat}), -- TODO hygiene
          ← `(bracketedBinder|(h : m = $n + 1 := by rfl))]
      | stx => panic s!"unsupported binder type in sdef {stx}"
    let bis := Array.join bis'
    `(def $n $bis* $[: $t]? := $b)

Generalizing it to arbitrary inductive types seems to require to do lots of work that match already does, not sure yet how to fuse the two things...

[Kyle Miller]

Would it be bad to compile these as match with a panic! for the catch-all case?

[Kyle Miller]

Maybe you could also generate an "in-domain" function, and when you call a function and want to make sure it's in the domain, you check that pred.inDomain n = true, also transpiled to a match, but with true/false instead of body/panic!

[Jakob von Raumer]

Kyle Miller said:

Would it be bad to compile these as match with a panic! for the catch-all case?

Yes, that's the alternative solution. We just have set ourselves the goal that the generated code should look as nice and succinct as possible :grinning_face_with_smiling_eyes:

[Kyle Miller]

Does Sail check that functions are called with values inside their domain at compile time? If not, then this would be sufficient, right?

def pred : Nat → Nat
  | n + 1 => n
  | _ => panic! "outside domain"

[Jakob von Raumer]

Yes, semantically definitely. My goal would just be to not have the match in the translated function body.

[Kyle Miller]

How does transpiling work when it can't prove side-goals like (h : m = n + 1 := by rfl)?

[Jakob von Raumer]

Yes, we'd have to figure that out at some point. :sweat_smile:

[Jakob von Raumer]

I guess my actual question would be: Could you make the syntax for binders a bit more sugarable, @Sebastian Ullrich ?

[Kyle Miller]

One issue I see here is that auto-parameters are still explicit arguments, so even if you had macro expansion capabilities for binders (using the obvious implementation that individual binders should be allowed to expand into binder lists), you'd be expanding

def pred_add (n + 1 : Nat) (m : Nat) : Nat := n + m

to

def pred_add (n' : Nat) {n : Nat} (_ : n' = n + 1 := by rfl) (m : Nat) : Nat := n + m

and then to pass two arguments you'd have to write pred_add num1 rfl num2 anyway.

[Kyle Miller]

I'm still not clear that this use case satisfies your goal of having the generated code as nice and succinct as possible — I'm not seeing how you'd be able to fill in these proofs. The elaborator is going to be checking that the first argument to pred_add is defeq to _ + 1. The rfl proof won't work for the _ in fun (n : Nat) => pred_add (1 + n) _ 2 for example.

It seems to me that the following sort of translation would need the least amount of pomp and circumstance, and it's relatively clean:

def pred_add : Nat → (m : Nat) → Nat
  | n + 1, m => n + m
  | _, _ => panic! "outside domain"

[Jakob von Raumer]

Ah you're right, we'd have to shift the autoParams to the end of the argument list :thinking:

[Jakob von Raumer]

The autoParam with the tactic defers the resolution of the defeq from the point of the function definition to the point of the elab of the function call, but not to execution time, the match does the latter, that's right