How to apply a constructor in an hypothesis?

Question

I am trying to prove the following theorem

Theorem subseq_subset : forall l1 l2, subseq l1 l2 -> sublist l1 l2.

with the inductive type subseq :

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

and the definition of sublist:

 Definition sublist (l1 l2 : list A) : Prop := forall x : A, In x l1 -> In x l2.

this is the proof i started to do

Theorem subseq_subset : forall l1 l2, subseq l1 l2 -> sublist l1 l2.
Proof.
intros.

unfold sublist. intros.
induction l2.
+ inversion H in H0. simpl. simpl in H0. assumption.
+ apply in_cons. apply IHl2.
Qed.

i have this context now

1 subgoals
l1 : list A
a : A
l2 : list A
H : subseq l1 (a :: l2)
x : A
H0 : In x l1
IHl2 : subseq l1 l2 -> In x l2
______________________________________(1/1)
subseq l1 l2

i thought to apply sub_right on H so i can end the proof with assumption but apply sub_right in H is not working. Is this possible? and how can i end this proof?

Thanks.

ana-borges ana-borges · Accepted Answer · 2020-10-17T10:48:31

First of all note that you stated definition

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

uses uppercase for the branches, so it would be apply Sub_right in H. Furthermore I think you switched the both and right branches. For the rest of this answer I'll assume the definition is

Inductive subseq {A:Type} : list A -> list A -> Prop :=
| subNil   : forall (l:list A), subseq  nil l
| sub_right : forall (s l:list A) (x:A), subseq  s l -> subseq s (x::l)
| sub_both : forall (s l: list A) (x:A), subseq s l -> subseq (x::s) (x::l).

Now to your actual question. When you say that apply sub_right in H doesn't work, what error message do you get? Coq told me that it couldn't find an x. This makes sense: if you are applying a theorem that has an x on the right-hand-side and no x on the left-hand-side, then Coq cannot guess which x to use. You can explicitly pick an x by saying apply (sub_right _ _ x) in H.

That said, I don't see how to complete your proof from where you are. I think you need an induction hypothesis. For example, if you're trying to prove subseq l1 (x :: l2) -> sublist l1 (x :: l2), it would be nice to know that subseq l1 l2 -> sublist l1 l2. You can achieve this by using induction on the proof of subseq l1 l2 instead of on one of the lists:

intros l1 l2 subseql1l2.
unfold sublist.
induction subseql1l2.
...

This gives you three nice cases that can be intuitively seen to be true. In order to prove them you will need some facts about In and lists, which you can look for by using, for example, Search In (_ :: _).

How to apply a constructor in an hypothesis?

1 Answers