I want to destruct my object of type list on two cases like:
H: lst = nil.
H: lst <> nil
One possible pattern for your custom case analysis is to provide a custom case analysis lemma, the pattern goes like this:
From Coq Require Import List.
Import ListNotations.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Inductive list_spec A : list A -> Type :=
| Nil_case : forall x, x = [] -> list_spec x
| Cons_case : forall x, x <> [] -> list_spec x.
Lemma listP A (l : list A) : list_spec l.
Proof. now case l; constructor. Qed.
Lemma foo A (l : list A) : False.
Proof.
case (listP l); intros x Hx.
Then you will get the right hypothesis in your context. Using destruct
instead of case
will clean the spurious l
remaining.
Note that ssreflect
's case
tactic includes special support for this kind of case analysis lemmas, you'd usually do case: l / listP.