Search code examples
coqcoq-tacticcoqide

How do destruct list in Coq (nil or not nil)

I want to destruct my object of type list on two cases like:

H: lst = nil.
H: lst <> nil
Solution

  • 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.