Proofs and Tactics

Stream: new members

[Simon Daniel]

By now i have been proving all my assumptions with "by decide/simp/trivial", but those cannot prove the following (while being seemingly trivial):

variable (l: List Unit)
def proof: l.length < (l.concat ()).length := sorry

The theorem proving book seems a little scary to me, maybe someone can give me a pointer where to start :)

[Timo Carlin-Burns]

Do you have an informal idea about how to prove this? Sometimes it can help to sketch out a proof in words and then see how you can translate that into Lean

[Simon Daniel]

(l.concat x) should return a list of length l.length +1 for any x and any l.

/-- `l.concat a` appends `a` at the *end* of `l`, that is, `l ++ [a]`. -/
def List.concat {α : Type u} : List α → α → List α
  | nil,       b => cons b nil
  | cons a as, b => cons a (concat as b)

i can see that concat always appends (cons b nil) to the end of the list, but struggle to formulate this as a proof

[Kyle Miller]

Rule of thumb: if you need to reason about a recursive definition, you usually need induction

(In this case, you can also look into the library for docs#List.length_concat, which I guessed the name of using the naming convention. If you click "source" you can see it's proved by induction.)

[Notification Bot]

Simon Daniel has marked this topic as resolved.

[Simon Daniel]

thanks, i didnt know that that could be something to search for in the std library, and the source is helpful

[Kyle Miller]

Another thing you can do is

import Mathlib

variable (l: List Unit)
def proof: l.length < (l.concat ()).length := by simp?

and see which lemmas it needed. (With everything imported, simp succeeds in closing the goal.)