termination in structures

Stream: lean4

[Filippo A. E. Nuccio]

I encounter the following problem

import Mathlib

inductive MyNat
| My_zero : MyNat
| My_succ : MyNat → MyNat
open MyNat

def MyNat_add : MyNat → MyNat → MyNat := fun n m ↦ match n, m with
  | My_zero, m => m
  | My_succ n, m => My_succ (MyNat_add n m)

def MyNatAdd : (AddZero MyNat) where
      add := MyNat_add
      zero := My_zero -- all good up to here

def MyRec : AddZero MyNat :=
  { zero := My_zero
    add n m := match n, m with
            | My_zero, m => m
            | My_succ n, m => My_succ (MyRec.add n m)} -- error, failed to show termination

So, if I unbundle the two fields, there is no termination requirement, but if I try to bundle the two in a structure this fails; and I do not know how to provide a termination_by clause since there are no MyNat parameters to the MyRec structure (I tried the termination_by structural n => n at the end of MyRec but this, expectedly, fails).

[Riccardo Brasca]

I think the issue is that in your mind you are defining addition, but technically you are defining a term of type AddZero MyNat, that, being a structure, is an inductive type with one constructor, and Lean is trying to do recursion on that thing somehow.

[Filippo A. E. Nuccio]

Sure, I agree. My question is whether there is a way to make it understand that only some of the fields of this structure are functions that I'm trying to define recursively; or, better, to insert the termination clause in the construction of the corresponding field.

[Riccardo Brasca]

import Mathlib

inductive MyNat
| My_zero : MyNat
| My_succ : MyNat → MyNat
open MyNat

def MyNat_add : MyNat → MyNat → MyNat := fun n m ↦ match n, m with
  | My_zero, m => m
  | My_succ n, m => My_succ (MyNat_add n m)

def MyNatAdd : (AddZero MyNat) where
      add := MyNat_add
      zero := My_zero -- all good up to here

def MyRec : AddZero MyNat :=
  { zero := My_zero
    add :=
      let foo : MyNat → MyNat → MyNat := fun n m ↦ match n, m with
      | My_zero, m => m
      | My_succ n, m => My_succ (MyNat_add n m)
      foo
      }

this works.

[Filippo A. E. Nuccio]

Yes, that I had also tried, but you use MyNat_add inside MyRec, if you try to use foo you can't.

[Filippo A. E. Nuccio]

(my whole point here is to understand the flexibility of the termination_by syntax, not so much to play with Addition, just in case you wonder)

[Riccardo Brasca]

I am not sure I understand what you want, MyRec is not a function.

[Sebastian Ullrich]

I think Riccardo meant

def MyRec : AddZero MyNat :=
  { zero := My_zero
    add :=
      let rec foo : MyNat → MyNat → MyNat := fun n m ↦ match n, m with
      | My_zero, m => m
      | My_succ n, m => My_succ (foo n m)
      foo
      }

[Riccardo Brasca]

Oh sorry, of course.

[Filippo A. E. Nuccio]

Oh great! But then I'm even more interested in understanding why this let call makes Lean try, and succeed, to find termination for this function foo whereas without the let this does not fire.

[Filippo A. E. Nuccio]

Ah, it's a let rec, not a let!

[Filippo A. E. Nuccio]

So my question becomes whether this behaviour is related to mutual inductive types as described in 4.4.5 of the reference manual or it is unrelated.

[Sebastian Ullrich]

If you want to define something recursively, you need to give it a name. That's the only syntax available. A field projection is not a name.

[Jakub Nowak]

MyRec.add means you're calling MyRec recursively and then you take the field .add of MyRec. You can't show that this recursive call to MyRec terminates, because MyRec doesn't even have any arguments.

[Jakub Nowak]

But being able to define recursive functions as fields of structures would be nice feature. Every time I have to do this I'm forced to define such functions as a separate definition (let rec is a bit ugly). Would be nice if that worked:

def MyRec : AddZero MyNat where
  zero := My_zero
  add
  | My_zero, m => m
  | My_succ n, m => My_succ (add n m)

[Filippo A. E. Nuccio]

Yes, this is what I had in mind, but I'd like to understand @Sebastian Ullrich 's answer better: when you say that "a field projection is not a name", I'm not sure to understand in which sense something "is" or "is not" a name. I though that the fact that in

structure Foo where
 a : Nat
 b : Nat

I can check that Foo.a : Foo -> Nat meant that Foo.a exists as well-typed and well-named term (of the relative function type).

[Sebastian Ullrich]

What you tried to do recursion on was MyRec.add, which looks like a name but is actually a function application. So you need to extract and name this part separately to use recursion.

[Filippo A. E. Nuccio]

Are you using "name" as in Lean.Name and "function application" as in Lean.Expr?