RFC: pattern matching on (syntactically equal) functions

Stream: lean4

[Jozef Mikušinec]

I'd like to propose allowing match expressions to unify terms containing syntactically equal functions. I am unqualified to comment on realizability, but I'd like to sketch why I think it would be beneficial, and document workarounds I'm aware of.

I have to admit one workaround I discovered during the writing of this proposal is relatively decent, but still has drawbacks. If nothing else, this proposal will serve as documentation for that workaround :sweat_smile: Update: more drawbacks found

Minified example

Ideally, Lean ought to accept the following code as valid.

inductive ArityTwo | zth | fst
abbrev TwoNats := ArityTwo → Nat

inductive TwoNatWrapper: TwoNats → Type
| intro (a b: Nat): TwoNatWrapper (fun | .zth => a | .fst => b)

def extract {a b} (value: TwoNatWrapper (fun | .zth => a | .fst => b)): Nat :=
  -- ``Tactic `cases` failed with a nested error: [...]``
  match value with
  | .intro _ _ => 42

Notice that the functions in the example are syntactically equal up to the variables that ought to be unified.

A specific use case example

Similar to universal algebras, I work with expressions that accept a signature that specifies custom operators and their arities.

structure Signature.{u, v} where
  Op: Type u
  Params: Op → Type v

inductive Expr (sig: Signature) where
| var (x: Nat)
| op (op: sig.Op) (args: sig.Params op → Expr sig)

Let's say we have a particular signature (with one nullary and one binary operation) that represents the following type.

inductive PairExpr
| var (x: Nat)
| null
| pair (l r: PairExpr)

Matching on types defined in terms of PairExpr is not problematic at all, it's a simple type. However, the Expr pairSignature version of PairExpr.pair .null .null is Expr.op .pair fun | .zth => N | .fst => N, where N is Expr.op .null nofun.

Unifying two Expr pairSignature values, (unless they are both var), will fail because they are defined using functions that carry the arguments.

Fuller code

structure Signature.{u, v} where
  Op: Type u
  Params: Op → Type v

inductive Expr (sig: Signature) where
| var (x: Nat)
| op (op: sig.Op) (args: sig.Params op → Expr sig)


inductive ArityZero
inductive ArityOne | zth
inductive ArityTwo | zth | fst

inductive pairSignature.Op where
| null
| pair

def pairSignature.Params: Op → Type
| Op.null => ArityZero
| Op.pair => ArityTwo

open pairSignature in
def pairSignature: Signature := { Op, Params }

def Expr.null: Expr pairSignature := Expr.op .null nofun
def Expr.pair (l r: Expr pairSignature): Expr pairSignature :=
  Expr.op .pair fun | .zth => l | .fst => r


inductive IsSubset: Expr pairSignature → Expr pairSignature → Prop
| null: IsSubset .null .null
| pair {la lb ra rb} (subL: IsSubset la lb) (subR: IsSubset ra rb): IsSubset (.pair la ra) (.pair lb rb)

def IsSubset.foo {l r b} (sub: IsSubset (.pair l r) b): True :=
  match sub with
  | .pair pl pr => trivial

Related

My proposal is loosely related to a problem described by Andrej Bauer in his answer about representing universal algebras vs concrete algebraic structures. While my proposal does not solve the crux of that problem, it does make it easier to work with the general setting where n-ary function applications are represented as functions whose domain is a size-n type.

Current state

Tactic `cases` failed with a nested error:
Dependent elimination failed: Failed to solve equation
  (fun x =>
      match x with
      | ArityTwo.zth => l
      | ArityTwo.fst => r) =
    fun x =>
    match x with
    | ArityTwo.zth => la✝
    | ArityTwo.fst => ra✝
at case `pair` after processing
  _, _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil

Ideally, the dependent pattern matcher would be extended to handle <function> = <function> as long as the bodies are compatible.

Known workarounds

Have two types (Expr and PairExpr) and convert between them as necessary

This means lots of duplication and boilerplate code.

Use recursors directly

Very clumsy and time consuming. All this ↴ just to eliminate IsSubset.pair:

Example

def IsSubset.elimPairLeft {la lb ra rb: Expr pairSignature} (sub: IsSubset (.pair la ra) (.pair ra rb)): IsSubset la ra :=
  sub.rec
    (motive := fun a b _ => ∀ {la lb ra rb}, a = .pair la ra → b = .pair lb rb → IsSubset la lb)
    (fun eq => Expr.noConfusion eq fun opEq => pairSignature.Op.noConfusion opEq)
    (fun {la lb ra rb} isSubL _ _ _ la' lb' ra' rb' eqA eqB =>
      let eqA := eq_of_heq (Expr.noConfusion eqA (fun _ => id))
      let eqB := eq_of_heq (Expr.noConfusion eqB (fun _ => id))
      let eqLa: la = la' := congr eqA (rfl: ArityTwo.zth = .zth)
      let eqLb: lb = lb' := congr eqB (rfl: ArityTwo.zth = .zth)
      eqLa ▸ eqLb ▸ isSubL)
    rfl
    rfl

Bake in arguments directly into Expr

Unidiomatic, unintuitive/not-easy-to-think-of solution that employs extra constructors in the Expr type to encode variable number of arguments. Essentially, we'd like to build something like

structure Arities.{u} where
  Op: Type u
  arity: Op → Nat -- Note: the codomain is Nat instead of Type as in Signature

inductive VectorExpr (sig: Arities) where
| var (x: Nat)
| op (op: sig.Op) (args: List.Vector (VectorExpr sig) (sig.arity op))

but that does not work because List.Vector does not accept the type that we're defining. ((kernel) arg #3 of 'VectorExpr.op' contains a non valid occurrence of the datatypes being declared).

So we have to implement "vectors" ourselves directly in Expr.

inductive ExprKind
| expr
| args (n: Nat)

inductive VectorExpr (sig: Arities): ExprKind → Type
| var (x: Nat): VectorExpr sig .expr
| op
    (op: sig.Op)
    (args: VectorExpr sig (.args (sig.arity op)))
  :
    VectorExpr sig .expr

| nil: VectorExpr sig (.args 0)
| cons
    (head: VectorExpr sig .expr)
    {n}
    (tail: VectorExpr sig (.args n))
  :
    VectorExpr sig (.args n.succ)

with the above, VectorExpr arities .expr is accepted by match expressions. However:

• It restricts us to only finite arities. With function pattern matching, Expr would be more user-friendly with finite signatures, and still accept infinite signatures in the general case.
• Additional boilerplate is required for destructuring VectorExpr. Things that were trivial like "There exists an argument such that" now aren't. Imagine defining an interpretation function for these expressions. It gets more complicated as you find yourself reimplementing list traversal every time. (You can't just define a helper traversal function as that breaks structural termination checking.)

Example of successfully matching on VectorExpr

def pairArities.arity: pairSignature.Op → Nat
| .null => 0
| .pair => 2

def pairArities: Arities := { Op := pairSignature.Op, arity := pairArities.arity }

abbrev PairExpr := VectorExpr pairArities .expr
def PairExpr.null: PairExpr := VectorExpr.op .null VectorExpr.nil
def PairExpr.pair (a b: PairExpr): PairExpr :=
  VectorExpr.op .pair (VectorExpr.cons a (VectorExpr.cons b VectorExpr.nil))

inductive PairExpr.IsSubset: PairExpr → PairExpr → Prop
| null: IsSubset .null .null
| pair {la lb ra rb} (subL: IsSubset la lb) (subR: IsSubset ra rb): IsSubset (.pair la ra) (.pair lb rb)

def PairExpr.IsSubset.foo {la ra lb rb} (sub: IsSubset (.pair la ra) (.pair lb rb)): IsSubset la lb :=
  match sub with
  | .pair subL _ => subL

def PairExpr.sumVars: PairExpr → Nat
| .var x => x
| .null => 0
| .pair a b => a.sumVars + b.sumVars

[Aaron Liu]

unfortunately these are not syntactically equal

[Aaron Liu]

because of the variables

[Aaron Liu]

you would need to know that it's injective wrt the variables for the unification to be sound

[Jozef Mikušinec]

But they are syntactically equal up to the variables to be unified, are they not?

[Aaron Liu]

notice how when I change your example a little bit it becomes unsound to unify the variable

inductive ArityZero | zth : ArityZero → ArityZero
abbrev NoNats := ArityZero → Nat

inductive OneNatWrapper : NoNats → Type
| intro (a : Nat) : OneNatWrapper (fun | .zth _ => a)

theorem NoNats.subsingleton : Subsingleton NoNats where
  allEq _ _ := funext (ArityZero.rec fun _ => id)

def wrapZero : OneNatWrapper (fun | .zth _ => 0) := .intro 0
def wrapOne : OneNatWrapper (fun | .zth _ => 0) :=
  NoNats.subsingleton.elim (fun | .zth _ => 1) (fun | .zth _ => 0) ▸ .intro 1

theorem wrapZero_ne_wrapOne : wrapZero ≠ wrapOne := fun h =>
  (Eq.rec (motive := fun _ h => 0 ≠ OneNatWrapper.rec id (h ▸ OneNatWrapper.intro 1))
    Nat.zero_ne_one (NoNats.subsingleton.elim (fun | .zth _ => 1) (fun | .zth _ => 0)) :)
      (congrArg (OneNatWrapper.rec (motive := fun _ _ => Nat) id) h)

def extract {a} (value : OneNatWrapper (fun | .zth _ => a)) :
    { n : Nat // ∃ h : n = a, value = h ▸ .intro n } :=
  -- uhoh
  match value with
  | .intro n => ⟨n, rfl, rfl⟩

-- contradiction!
theorem wrapZero_eq_wrapOne : wrapZero = wrapOne := by
  obtain ⟨_, rfl, h⟩ := extract wrapOne
  exact h.symm

[Aaron Liu]

Due in part to a related problem and also due to some limitations of the structural recursion compiler the workaround I have been using is to pass a (sc : ...) (hsc : sc = ...) everywhere and have sc in all the types so when I match on them it unifies the free variable sc and now I have an hsc I can work with.

[Jozef Mikušinec]

Ouch.

Would it be too much of a hack to only support functions whose domains are inductives whose constructors have no parameters? This should still cover lots of common cases, and we could guarantee soundness if the function just enumerates all its values for all its inputs, is that correct?

[Jozef Mikušinec]

Thank you for the counterexample