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.