termination of syntax consumption

Stream: lean4

[Arthur Paulino]

Hello everyone!
Something got me thinking: is there a way to infer the termination of Syntax → ... functions when every recursive call uses a fragment of the entire syntax we're matching on?
I'm asking this because a piece of code that I'm writing has multiple partial definitions that I believe should always terminate. And this is not the first time that I end up with many partial functions like this

[Henrik Böving]

I'm definitely not an expert on Syntax but I think the issue with this might be the following: Syntax itself is actually a very trivial datatype: docs4#Lean.Syntax however the notation we have allows to match on fairly elaborate (elaborate to denote with a pattern on Syntax) Syntax tree nodes so maybe the information about being a "subtree" just gets lost along the way?

[Mario Carneiro]

The way syntax matches are currently desugared, it would not be easy. You can use a well founded measure to determine that the array accesses are at smaller members, but it doesn't seem like it is worth complicating the desugaring

[Henrik Böving]

Regarding this topic, I also have a similar question regarding Expr transformers, I wrote this function here:
https://github.com/hargoniX/mathlib4/blob/slim_check/Mathlib/Testing/SlimCheck/Testable.lean#L463-L472
but due to recursing into addDecorations again inside the argument to replace It cannot be trivially shown to terminate, do we have tricks to do this as well ?

[Mario Carneiro]

nope, that one is even harder because changing the type of replace would interfere with the (very important!) caching optimization

[Leonardo de Moura]

The test file https://github.com/leanprover/lean4/blob/master/tests/lean/run/syntaxWF.lean contains the necessary "plumbing" for writing functions such as

def visit (stx : Syntax) : Syntax :=
  match stx with
  | `(if $c then $t else $e) => visit c
  | `(let $x:ident := $v:term; if $c then $t else $e) => visit c
  | _ => stx

without partial.
For the addDecorations example, we can define a refine' function with type

def replace' (e0 : Expr) (f? : (e : Expr) → sizeOf e ≤ sizeOf e0 → Option Expr) : Expr :=

It is the same trick we use for other combinators. Then, we can write

def addDecorations (e : Expr) : Expr :=
  e.replace' fun expr h =>
    match expr with
    | Expr.forallE name type body data =>
      let n := name.toString
      let newType := addDecorations type
      let newBody := addDecorations body
      let rest := Expr.forallE name newType newBody data
      some <| mkApp2 (mkConst `SlimCheck.NamedBinder) (mkStrLit n) rest
    | _ => none
decreasing_by exact Nat.le_trans (by simp_arith) h

The complete example is here: https://github.com/leanprover/lean4/blob/master/tests/lean/run/addDecorationsWithoutPartial.lean
We are saving all these examples in our test suite because we want all of them to go through without any extra annotation even if the user uses Expr.replace. Our goal is to allow users to register replacements such as Expr.replace => Expr.replace' that are applied when we try to prove termination. We have some notes here:
https://github.com/leanprover/lean4/blob/master/tests/lean/run/combinatorsAndWF.lean#L37

[Arthur Paulino]

Starred the message so I can come back to it later :+1:

I forgot to mention another motivation for my question. Sebastian mentioned the builtin syntax which will help us build powerful parsers without the gymnastics that were implemented in my repo. Then, if writing recursive functions that consume syntax terms is easier and possible without partial, then we'll be able to reason about them more easily