How can I use induction when the base case doesn't apply?

Stream: general

[Alex Zani]

I'm trying to write a function which takes a proof that ((x :: xs).length > n) to get a proof that xs.length > n) but I can't figure out how to do induction. If I try to do induction on xs, the base case is the empty list. However, xs.length > n+1 precludes xs.length=0. So how do I do this?

def recnth (n : Nat) (x : α) (xs : List α) (ok : (x :: xs).length > n) : xs.length > n-1 := by

[Alex Zani]

(deleted)

[Bjørn Kjos-Hanssen]

Since 0-1=0 for natural numbers in Lean, you can try replacing n by n+1 throughout.

[Richard Kiss]

A problem is that this is not true. For xs = [] and n=0, we get (x::xs).length > n but xs.length > n - 1 is false for n: Nat because 0-1=0 for Nat 0

[Richard Kiss]

use n+1 and n instead

[Alex Zani]

@Richard Kiss Thanks, but that doesn't solve the problem I'm having because it's still not true since [].length > n is not true for any value of Nat. I think I need to think more about what my preconditions are...

[Matt Diamond]

maybe docs#Nat.le_induction could help?

[Jireh Loreaux]

Do you really need this? I mean, we have docs#List.length_cons.

[Jireh Loreaux]

(If you do you can take (x :: xs).length > n, or (x :: xs).length ≥ n + 1 as a hypothesis and prove x.length ≥ n.)

[Richard Kiss]

I’m on mobile so can’t try much atm but I’d recommend using xs.length ≥ ninstead of >. Or at least tell us what variation of your original post you’re willing to accept a proof for since we can’t prove the false one. Maybe add n>0 ?