help w/ recursion termination

Stream: new members

[Dapper Mink]

Hello, I'm new to lean but even newer to Zulip so sorry in advance if this shouldn't be posted here
I am playing with lean to learn how to prove termination and have this very simple example:

inductive Pic where
  | rect
  | pics (ps : List Pic)

def asString : Pic → String
| Pic.rect => "rect"
| Pic.pics ps =>
  let strs := ps.map asString
  let str := String.intercalate ", " strs
  s!"pics({str})"

My asString function fails to show termination. I have read this page on the book: https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html and feel like I should use WellFounded / Acc, however I also fail to define a "<" relation for Pic. Could someone tell me what is the easiest way to satisfy lean with that?

[Dapper Mink]

I've noticed messages are often ignored if you don't use your real name. Sorry, this is my google account but my real name is Quentin Januel. I am not a student, I am learning lean with the books and am trying to develop a game to verify my understanding. Also I am not specifically asking for a solution, a redirection towards a resource that explains this would be equally appreciated. It has been two days I am struggling with this problem because I feel like the book doesn't cover this kind of cases (lean is my first proof assistant btw).
To me, the problem is that this should be a structural recursion, but it is not probably because of the "List" indirection. I think I could maybe avoid this by using a mutual recursion with a custom list implementation, but I would like to stick with the standard list. Also I tried to implement sizeOf or a binary relation for this structure, but I feel like they all also require to show termination. Any help would be greatly appreciated.

[Dapper Mink]

Also the book (theorem proving) does not provide any example of "Acc" afaik

[Kevin Buzzard]

You're exactly right that I personally tend not to reply to people who are not using their full real name, but your question is completely reasonable as is your explanation of anonymity I guess. Another reason I didn't reply myself was that I didn't know the answer. I don't understand what s! does because I use Lean in a totally different way to the code you're posting, but here's some code which I do understand:

inductive Pic where
  | rect
  | pics (ps : List Pic)

def asString : Pic → Nat
| Pic.rect => 37
| Pic.pics ps =>
  let strs := ps.map asString
  strs.length

and this also doesn't compile; the issue is somehow that ps.map is taking Lean out of its comfort zone when it comes to proving that things are well-defined. We get the usual error

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

but I don't know how to fix it because I only ever do induction/recursion on naturals. Just bumping this and hoping that my simpler example will encourage someone who is less mean about replying to anonymous users and more CS-ish will help you out :-)

[Joachim Breitner]

The problem is that lean doesn't know that ps.map will call its argument only on pictures from ps. But you give it a hint:

def asString : Pic → String
| Pic.rect => "rect"
| Pic.pics ps =>
  let strs := ps.attach.map (fun ⟨p, _⟩ => asString p)
  let str := String.intercalate ", " strs
  s!"pics({str})"

See docs#List.attach for what it does (and feel free to ask more about it).

And it seems that some more magic is happening behind the scenes where lean knows that x ∈ xs implies that x is smaller than xs:
https://leanprover-community.github.io/mathlib4_docs/Init/Data/List/BasicAux.html#List.tacticSizeOf_list_dec

[Kevin Buzzard]

I decided to try and answer this question myself but I was totally bewildered by Pic.rec:

Pic.rec.{u} {motive_1 : Pic → Sort u} {motive_2 : List Pic → Sort u} (rect : motive_1 rect)
  (pics : (ps : List Pic) → motive_2 ps → motive_1 (pics ps)) (nil : motive_2 [])
  (cons : (head : Pic) → (tail : List Pic) → motive_1 head → motive_2 tail → motive_2 (head :: tail)) (t : Pic) :
  motive_1 t

Why are there two motives? I understand very little about this kind of an inductive type.

[Kevin Buzzard]

Is this actually provable?

def asString : Pic → String
| Pic.rect => "rect"
| Pic.pics ps =>
  let strs := ps.map asString
  let str := String.intercalate ", " strs
  s!"pics({str})"
  decreasing_by {
    simp
    /-
    a✝¹ a✝ : Pic
    ⊢ InvImage WellFoundedRelation.rel (fun a ↦ sizeOf a) a✝ a✝¹
    -/
    sorry
  }

[Kevin Buzzard]

'induction' tactic does not support nested inductive types, the eliminator 'Pic.rec' has multiple motives
:cry:

[Kevin Buzzard]

I'm having trouble proving it by induction ;-)

[Dapper Mink]

@Joachim Breitner Thank you for your solution, it indeed works great and reading through the definitions of List.attach, List.pmap and List.forall_mem_cons made made me understand better. Also I was confused because I didn't know std4 was a thing and was wondering why my List.attach function did not exit. Fortunately, this is all sorted out now

[Dapper Mink]

@Kevin Buzzard Yes I'm sorry about that, I will use another google account if I ever get any more questions from now on