proving termination

Stream: general

[Alexandre Rademaker]

any idea about how to prove termination of

def perm₂ : List a → List (List a)
  | [] => [[]]
  | xs => concatMap (λ p => (perm₂ p.2).map (p.1 :: ·)) (picks xs)
 termination_by xs => xs.length

any good documentation about it?

[Kim Morrison]

#mwe, please! :-)

[Alexandre Rademaker]

Sorry, let me give the remain functions:

def concat1 {a : Type} : List (List a) → List a :=
 List.foldr List.append []

def concatMap (f : a → List b) : List a → List b := concat1 ∘ (List.map f)

def picks {a : Type} : List a → List (a × List a)
| [] => []
| (x :: xs) =>
   (x, xs) :: ((picks xs).map (λ p => (p.1, x :: p.2)))

def perm : List a → List (List a)
  | [] => [[]]
  | xs => concatMap (λ p => (perm p.2).map (p.1 :: ·)) (picks xs)
 termination_by xs => xs.length

The function picks picks an arbitrary element from a list in all possible ways, returning both the element and what remains. The function perm computes a permutation by picking an arbitrary element of a nonempty list as a first element, and following it with a permutation of the rest of the list.

[Daniel Weber]

concatMap is docs#List.bind, you'll probably have an easier time using it due to existing API (And concat1 is docs#List.join)

[Daniel Weber]

To show termination what you can do is map on (picks ps).attach and prove that all elements of picks ps are shorter

[Alexandre Rademaker]

Can you elaborate on the last step? "map on (picks ps).attach and prove that all elements of picks ps are shorter?

[Daniel Weber]

You can do something like this

theorem length_lt_of_mem_picks_con {a : Type} (v : a) (l : List a) (l' : a × List a) (h : l' ∈ picks (v :: l)) :
      l'.2.length < (v :: l).length := by
   sorry

def perm : List a → List (List a)
  | [] => [[]]
  | x :: xs => concatMap (fun ⟨p, hp⟩ ↦
      have : p.2.length < (x :: xs).length := length_lt_of_mem_picks_con x xs p hp
      (perm p.2).map (p.1 :: ·))
      (picks (x :: xs)).attach
 termination_by xs => xs.length

[Alexandre Rademaker]

Thank you, testing now. Regarding the concatMap and concat1 the idea is to show the students how foldr can be useful.

[Alexandre Rademaker]

Hum, length_lt_of_mem_picks_con is not easy to prove...

[Alexandre Rademaker]

Is attach something new? It is working in the https://live.lean-lang.org/ but not on my local machine... I am using 4.10.0

[Kim Morrison]

You would need import Batteries on v4.10.0.

[Alexandre Rademaker]

Maybe it can be easier to upgrade to v4.11-rc2 ... can I just edit the lean-toolchain? Is there a safer way to upgrade? Sorry... maybe out of the topic.

[Kim Morrison]

Yes, just put leanprover/lean4:v4.11.0-rc2 into your lean-toolchain. If you have dependencies you may need to run lake update as well. (And if you've pinned your dependencies, move them to a commit that is also using v4.11.0-rc2.)

[Alexandre Rademaker]

Thank you! Nice, now back to the prove of the auxiliary theorem length_lt_of_mem_picks_con. I am half way to prove it using induction on the l. But I didn't understand the have : p.2.length < (x :: xs).length := ... inside the lambda function.. I mean, the presence of this anonymous proposition in the beginning of the lambda body is something automatically used by Lean to check termination?

[Andrés Goens]

Alexandre Rademaker said:

I mean, the presence of this anonymous proposition in the beginning of the lambda body is something automatically used by Lean to check termination?

short answer: yes! Lean uses a default tactic to prove termination, and if it fails, it'll tell you what it's proof obligation was that it couldn't prove. If you add that obligation with a have to the environment, the default tactic for termination will prove the rest for you

[Andrés Goens]

(you can remove the have and look at the error message you get)

[Andrés Goens]

there's more details in TPIL: https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html#well-founded-recursion-and-induction

[Alexandre Rademaker]

Thank you