proof on named pattern

Stream: lean4

[Locria Cyber]

The following doesn't work

private def foo : (l : List α) -> 0 < .succ l.length
| [] => Nat.zero_lt_succ 0
| c@(x::xs) => Nat.zero_lt_succ c.length
-- ok:
-- | c => Nat.zero_lt_succ c.length

[Locria Cyber]

It definitely should

[Henrik Böving]

The reason it doesnt work is due to the definition of namedPattern I'd say, it views the namedPattern c as x :: xs and not as c. You can make it work:

def foo (l : List α) : 0 < .succ l.length :=
  match l with
  | [] => Nat.zero_lt_succ 0
  | c@(x::xs) =>
    have hidden : c = x :: xs := by assumption
    have h := Nat.zero_lt_succ c.length
    hidden ▸ h

But I don't really know how to fix it systematically.

[Chris Bailey]

This works too:

private def foo : (l : List α) -> 0 < .succ l.length
| [] => Nat.zero_lt_succ 0
| c@(x::xs) => by simp [Nat.zero_lt_succ c.length]

[Henrik Böving]

It would be nice if the match compiler could be smart enough for this on its own though

[Locria Cyber]

Henrik Böving said:

It would be nice if the match compiler could be smart enough for this on its own though

Should I open an issue?

[Locria Cyber]

This does work: | c@(x::xs) => Nat.zero_lt_succ (x::xs).length

[Henrik Böving]

Yes this is due to the way it views the c but it is not desirable, you might as well leave the c away