Termination if we recurse via List.map

Stream: lean4

[Geoffrey Irving]

What's the cleanest way to show that this function terminates? It's straightforward recursion, except that part of the recursion goes via List.map.

import Mathlib

inductive Tower : Type where
  | node : List Tower → (List Bool → Bool) → Tower

-- fail to show termination for Tower.value
def Tower.value : Tower → Bool
| .node s f => f (s.map value)

[Henrik Böving]

Explained in https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/, tldr List.attach will do the job

[Geoffrey Irving]

Perfect, thank you!

def Tower.value : Tower → Bool
| .node s f => f (s.attach.map fun ⟨t,_⟩ ↦ t.value)

[Kim Morrison]

And language support for this happening automatically is coming soon!

[Joachim Breitner]

On nightly, this already works:
https://live.lean-lang.org/#project=lean-nightly&codez=FASwdgJgrgxgLiAbgUwAQBUD2B3ZAnVALgwE8AHNbAC32WFVQB9UxMI1iAZEAZzgxz5UgJMJUACm59UAIUyYANiJlz5ASiVZceYMAC0u1ADMAhiEVxMqHlRyo4+ALbhjCTGCOYCm/ADpEx+Sg6dkMBLT8AoKIwoVFZBWBmH1Z2KyNUAF4APnSxHh8HYzJUf0DkVWAgA

[Joachim Breitner]

If you get a red squiggly error, that’s because of a bug in lean4web (https://github.com/leanprover-community/lean4web/issues/41) that processes the file with both versions of lean at the same time, and shows you the diagnostics from the old one. @Jon Eugster , is there any chance to fix this? This would also affect for example @Patrick Massot should he use a lean4web instance for his course.

[Patrick Massot]

Thanks for the warning! I confirm it would be great to fix such a bug before next Friday (the 28th).

[Jon Eugster]

Patrick Massot said:

Thanks for the warning! I confirm it would be great to fix such a bug before next Friday (the 28th).

(At least it would like not bother you too much because the faulty Lean version running in the background should be "Mathlib stable" which is what you'll use anyways.)

[Joachim Breitner]

If they import a file that doesn’t exist in the background, the import would have a permanent squiggly line, I assume?
(As seen on https://lean.math.hhu.de/#project=DuperDemo&codez=JYWwDg9gTgLgBAEQK5gKZQakEBQOg)

[Floris van Doorn]

Joachim Breitner said:

If you get a red squiggly error, that’s because of a bug in lean4web (https://github.com/leanprover-community/lean4web/issues/41) that processes the file with both versions of lean at the same time, and shows you the diagnostics from the old one. Jon Eugster , is there any chance to fix this? This would also affect for example Patrick Massot should he use a lean4web instance for his course.

That seems also to cause some other weird behavior, such as the infoView-popup with the type and docstring of identifiers being duplicated, and autocomplete suggesting the same declaration twice.

[Jon Eugster]

fixed

[Patrick Massot]

Thanks Jon!