Search code examples
coqcoq-tactic

How to do case analysis on the length of a list in Coq?

I am in a situation during a proof where I need to do case analysis on the length of a list l.

  1. When the length l < 2 it's one case (in which a binary operation like + does not apply)
  2. When the length l >= 2 it's the other case (in which the binary operation applies)

How do I use destruct or some other tactic(s) to do this, and obtain two cases, i.e. True and False?

I tried:

destruct (length l < 2).

destruct (lt (length l) 2).

remember (length l < 2).
destruct HeqP.

But none worked.

Solution

  • You need a "constructive" version of <, because the standard one is in Prop, so you can't perform case analysis on it. You can either use compare, le_lt_dec or a boolean version of < (search through the doc for all the options, the easiest one should be this one).

    If you really need to test the length against 2, you could also destruct length n 3 times and handle by hand the 3 first cases.