How to prove that the subsequence of an empty list is empty?

Question

I'm new in coq. i am trying to prove that the subsequence of an empty list is empty

This is the lemma i'm working on:

Lemma sub_nil : forall l , subseq l nil <-> l=nil. 

i tried to split so i can have

subseq l nil -> l = nil

and

l = nil -> subseq l nil

to prove the first one i tried an induction on l but i blocked when it comes to prove that

subseq (a :: l) nil -> a :: l = nil

thanks.

Answer 1

The tactic to use here is inversion. Paraphrasing the coq documentation for inversion! :

Given an inductive hypothesis (H:I t), then inversion applied to H derives for each possible constructor c i of (I t), all the necessary conditions that should hold for the instance (I t) to be proved by c i.

Assuming the subseq predicate is given as follows:

    Inductive subseq {A:Type} : list A -> list A -> Prop :=
    | SubNil   : forall (l:list A), subseq  nil l
    | SubCons1 : forall (s l:list A) (x:A), subseq  s l -> subseq s (x::l)
    | SubCons2 : forall (s l: list A) (x:A), subseq s l -> subseq (x::s) (x::l). 

The proof would be stuck here(exactly at the place you specified):

    Lemma sub_nil2 : forall (A:Type) (l: list A) , subseq l nil <-> l=nil.
    Proof.
     split.
     -  destruct l eqn:E; intros.
        *  reflexivity.
        (*Now unable to prove a::l0 = [] because the hypothesis: subseq (a :: l0) [] is absurd.*)
        * inversion H.(*Coq reasons that this hypothesis is not possible and discharges the proof trivially*)
     - intros. subst. apply SubNil.
   Qed.

Note that I used the destruct tactic but the issue remains even with induction tactic.

The entire proof can be written cleanly as below:

     Lemma sub_nil : forall (A:Type) (l: list A) , subseq l nil <-> l=nil.
     Proof.
      split; intros.
       - inversion H. reflexivity.
       - subst. apply SubNil.
     Qed.