How do I write a `have:` into my function for termination

Stream: new members

[Philipp]

As always I want to prove termination for a function.

This time I am stuck with the Syntax(?) for have statements. I have an MVP:

def foo : List α → List α
  | [] => []
  | (_::fs) => fs

def bar (l : List Nat) : Nat :=
  let rest := foo l
  have h: sizeOf rest < sizeOf l := by
    -- I don't see the definitions of `rest` here in the context.
    -- So I assume I'm trying to make a broad (false) statement here that the sizeOf one arbitrary list is smaller than sizeOf another arbitrary list?
    sorry
  if rest == [] then 0 else bar rest

How do I see the preceding let definition in my have?
Also: Are there some good resources about proving functional programs in Lean?

[Edward van de Meent]

You could use rw [rest] to reveal its definition, but I believe there also is a tactic for undoing lets

[Edward van de Meent]

For your second question: #tpil is a great resource for this.

[Daniel Weber]

Edward van de Meent said:

You could use rw [rest] to reveal its definition, but I believe there also is a tactic for undoing lets

If you import Mathlib.Tactic there's unfold_let.

[Daniel Weber]

However note that the statement is still false because it's before the check if rest == [].

[Philipp]

Ah good point, thanks! So I would need to move the have into the else branch?

I realized that my MVP was a bit too minimized tho, because in this case I can see the definition for rest in the goal state. Closer to reality is that I'm destructuring a product in my let statement:

ef foo : List α → (List α × Nat)
  | [] => ([], 0)
  | (_::fs) => (fs, 1)

def bar (l : List Nat) : Nat :=
  let (rest, _) := foo l
  have h: sizeOf rest < sizeOf l := by
    sorry
  if rest == [] then 0 else bar rest

how would I get the definition for rest here?

PS: I'd rather not have to pull the whole Matlib into my project :(

[Daniel Weber]

It doesn't seem like let pattern matching keep the definition, so I'm not sure what's the best way to do this

[Daniel Weber]

Here's a mathlib-free proof of the original problem:

def foo : List α → List α
  | [] => []
  | (_::fs) => fs

def bar (l : List Nat) : Nat :=
  let rest := foo l
  if h : rest == [] then 0 else
    have : sizeOf rest < sizeOf l := by
      cases l
      · contradiction
      · simp only [rest, foo, List.cons.sizeOf_spec]
        omega
    bar rest

[Philipp]

Thanks!

Maybe I will not use pattern matching and instead .1 and .2 then

[Kyle Miller]

Rather than let you can use match to get an additional proof in context:

def foo : List α → (List α × Nat)
  | [] => ([], 0)
  | (_::fs) => (fs, 1)

def bar (l : List Nat) : Nat :=
  match hl : foo l with
  | (rest, _) =>
    have h: sizeOf rest < sizeOf l := by
      sorry
    if rest == [] then 0 else bar rest

[Kyle Miller]

Using .1/.2 is probably cleaner

[Philipp]

Thank you!
Related question: If I have a match statement that first matches [] and then rest, can I somehow get a proof for rest \neq [] in the second match arm?

In a minimum example:

def is_empty (l : List α) : Bool :=
  match hm: l with
  | [] => false
  | a =>
    have h: a ≠ [] := sorry
    true

[Philipp]

ok I guess that was a stupid question. I could just match a@(_::_)