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.
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 (_ :: _).