Newcomer question about termination proof

Stream: lean4

[Youngju Song]

Hi,
I am coming from Coq and have just started playing with Lean.
I have trouble proving the following example, even after some Googling:

inductive Tree :=
| Leaf (v: Int)
| Node (ts: List Tree)

def map (f: Int → Int): Tree → Tree := λ tr =>
  match tr with
  | .Leaf v => .Leaf (f v)
  | .Node ts => .Node (List.map (map f) ts)
termination_by tr => tr._sizeOf_1
decreasing_by
. simp [InvImage]
  sorry -- How can I get some relation between `ts` and `a✝`?

Can someone help me with this? Thank you in advance :)

[Daniel Weber]

In general when you have a decreasing_by proof you should start it with simp_wf. It's also better to use sizeOf instead of directly accessing ._sizeOf_1. You also don't need to give the termination_by, the size is used by default

[Daniel Weber]

you can use ts.attach to keep a membership proof attached to the elements

inductive Tree :=
| Leaf (v: Int)
| Node (ts: List Tree)

def map (f: Int → Int): Tree → Tree := λ tr =>
  match tr with
  | .Leaf v => .Leaf (f v)
  | .Node ts => .Node (ts.attach.map (fun x ↦ map f x.1))
decreasing_by
  simp_wf
  have := List.sizeOf_lt_of_mem x.2
  omega

[Daniel Weber]

Note that there is syntactic sugar for a function which is just a match, so you can do this:

inductive Tree :=
| Leaf (v: Int)
| Node (ts: List Tree)

def map (f: Int → Int): Tree → Tree
| .Leaf v => .Leaf (f v)
| .Node ts => .Node (ts.attach.map (fun x ↦ map f x.1))
decreasing_by
  simp_wf
  have := List.sizeOf_lt_of_mem x.2
  omega

[Youngju Song]

@Daniel Weber Thank you for the answer and advices! This is quite different from Coq and very interesting.

[Youngju Song]

@Daniel Weber I have one follow up question:

• Is there a systematic way to figure out the definitions that are "derived" from inductive Tree := ...?
• I have tried this def Tree.size (tr: Tree): Nat := sizeOf tr and, apparently, sizeOf function is non-computable. Reading the comments for SizeOf typeclass, I am curious if there is a fundamental issue in making this computable. Do you have any idea? (I understand that for "large" types, sizeOf just returns the default (1), but it is s till computable)

[Kim Morrison]

Rather than dealing with decreasing_by in every function on Tree, it's nice to set up an appropriate measure first:

inductive Tree :=
| Leaf (v: Int)
| Node (ts: List Tree)

namespace Tree

def height : Tree → Nat
| Leaf _ => 0
| Node ts => (ts.attach.map (fun x => height x.1)).maximum?.getD 0 + 1
decreasing_by
  simp_wf
  have := List.sizeOf_lt_of_mem x.2
  omega

theorem height_lt : ∀ {t: Tree} {ts: List Tree}, t ∈ ts → height t < height (Node ts) := by
  intro t ts h
  simp only [height]
  sorry

def map (f: Int → Int): Tree → Tree
| .Leaf v => .Leaf (f v)
| .Node ts => .Node (ts.attach.map (fun x => have := height_lt x.2; map f x.1))
termination_by t => height t

end Tree

[Kim Morrison]

(sorry left as an exercise :-)

[Youngju Song]

@Kim Morrison Thank you for the suggestion and the template code! I was able to prove it as follows:

theorem height_lt : ∀ {t: Tree} {ts: List Tree}, t ∈ ts → height t < height (Node ts) := by
  intro t ts h
  simp only [height]
  rw [@Nat.lt_succ]
  rw [@List.attach_map_coe]
  generalize H : (List.map height ts).maximum? = tmp
  cases tmp with
  | none =>
    simp_all
  | some x =>
    simp_all
    rw [List.maximum?_eq_some_iff'] at H
    cases H with
    | _ A B =>
      apply B
      apply List.mem_map_of_mem height
      assumption

Do you have any advice on making this proof more concise? Specifically, I wonder if there is a shorthand for (i) successive generalize and cases, and (ii) cases H with | _ A B =>. In Coq, (i) is done in a single destruct tactic, and (ii) is done with destruct H as [A B].

[Kim Morrison]

(i) you can just write match H : (List.map height ts).maximum? with

[Kim Morrison]

(ii) you might like rcases

[Youngju Song]

@Kim Morrison That works well. Thank you for the advice!