Naturality of `match`

Stream: Is there code for X?

[Ayhon]

Continuation of #Is there code for X? > Naturality of `ite`., but asking a different question.

Basically, is there an apply_match in the same way there is an docs#apply_ite?

[Aaron Liu]

Every matcher is different, what would the statement be? You can use split to split matches. What's your use case?

[Ayhon]

I'm guessing this may be a bit more complicated, since match works on arbitrary inductive data types, and not just boolean expressions like ite. I know that for every inductive data type some special functions are defined like rec, although I'm not sure if match is implemented in terms of those.

[Aaron Liu]

def Nat.isZero : Nat → Bool
| 0 => true
| _ + 1 => false

#print Nat.isZero.match_1

#print Nat.pow.match_1

example : @Nat.isZero.match_1 = @Nat.pow.match_1 := rfl

def Nat.isSucc : Nat → Bool
| 0 => false
| _ + 1 => true

-- uses Nat.isZero.match_1
set_option pp.explicit true in
#print Nat.isSucc

[Ayhon]

Aaron Liu said:

Every matcher is different, what would the statement be? You can use split to split matches. What's your use case?

I have a function toSet which transforms binary search trees into the sets they represent. As an example, consider this code

import Mathlib

inductive BSTree: Type where
| Nil : BSTree
| Node (x: Nat)(left right: BSTree): BSTree

def BSTree.toSet: BSTree -> Set Nat
| Nil => ∅
| Node x left right => {x} ∪ left.toSet ∪ right.toSet

def BSTree.create: Nat -> BSTree
| 0   => Nil
| h+1 => Node h (BSTree.create h) (BSTree.create h)


example(h: Nat)
: (BSTree.create h).toSet = (Finset.range h).toSet
:= by
  unfold BSTree.create
  simp
  sorry

Admittedly, in this example the gains are not substantial since I'd need to destruct h in any case. Some of the proofs I've been doing, however, try to show the equivalence of two operations, and I've found myself wanting match to work this way to simplify expressions a bit (because the operation is the identity unless some specific conditions apply, for instance)

[Jz Pan]

Aaron Liu said:

Every matcher is different, what would the statement be? You can use split to split matches. What's your use case?

Maybe there can be a tactic to do this.

[Eric Wieser]

A simproc would work too

[Joachim Breitner]

I worked in that direction in https://github.com/leanprover/lean4/pull/5923. Unclear when I’ll pick it up again, but I think it has merit.