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
uses uppercase for the branches, so it would be
apply Sub_right in H
. Furthermore I think you switched theboth
andright
branches. For the rest of this answer I'll assume the definition isNow 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 anx
. This makes sense: if you are applying a theorem that has anx
on the right-hand-side and nox
on the left-hand-side, then Coq cannot guess whichx
to use. You can explicitly pick anx
by sayingapply (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 thatsubseq 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: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 (_ :: _).