Coq: Problems with List In inductive

Question

I'm new to Coq, but with some effort I was able to prove various inductive lemmas. However I get stuck on all exercises that uses the following inductive definition:

Inductive In (A:Type) (y:A) : list A -> Prop :=
     | InHead : forall xs:list A, In y (cons y xs)
     | InTail : forall (x:A) (xs:list A), In y xs -> In y (cons x xs).

The furthest i got was with the following lemma:

Lemma my_In_rev : forall (A:Type) (x:A) (l:list A), In x l -> In x (rev l).
Proof.
induction l.
simpl.
trivial.
simpl.
intros.

The following two lemmas I cant get past the first steps, because I get stuck on the exists goal right after using intros.

Lemma my_In_map :  forall (A B:Type) (y:B) (f:A->B) (l:list A), In y (map f l) -> exists x : A, In x l /\ y = f x.

Lemma my_In_split : forall (A:Type) (x:A) (l : list A), In x l -> exists l1, exists l2, l = l1 ++ (x::l2).
Proof.

Any help would be appreciated!

Answer 1

For your first lemma, I added two simple sublemmas (that you can find in the list library). The two others are more straightforward.

Require Import List.

Lemma In_concat_l: forall (A: Type) (l1 l2: list A) (x:A), 
   In x l1 -> In x (l1 ++ l2).
Proof.
intros A.
induction l1 as [ | hd tl hi ]; intros l2 x hIn; simpl in *.
- contradiction.
- destruct hIn.
  + left; assumption.
  + right; now apply hi.
Qed.

Lemma In_concat_r: forall (A: Type) (l1 l2: list A) (x:A), 
   In x l2 -> In x (l1 ++ l2).
intros A.
induction l1 as [ | hd tl hi ]; intros l2 x hIn; simpl in *.
- assumption.
- right; now apply hi.
Qed.

Lemma my_In_rev : forall (A:Type) (x:A) (l:list A), In x l -> In x (rev l).
Proof.
intros A x l.
induction l as [ | hd tl hi ]; intros hIn; simpl in *.
- contradiction.
- destruct hIn.
  + apply In_concat_r.
    rewrite H.
    now constructor.
  + apply In_concat_l.
    now apply hi.
Qed.

Lemma my_In_map :  forall (A B:Type) (y:B) (f:A->B) (l:list A), In y (map f l) -> exists x : A, In x l /\ y = f x.
Proof.
intros A B y f l.
induction l as [ | hd tl hi]; intros hIn; simpl in *.
- contradiction.
- destruct hIn.
  + exists hd; split.
    left; reflexivity.
    symmetry; assumption.
  + destruct (hi H) as [x0 [ h1 h2]].
    exists x0; split.
    right; assumption.
    assumption.
Qed.

Lemma my_In_split : forall (A:Type) (x:A) (l : list A), In x l -> exists l1, exists l2, l = l1 ++ (x::l2).
Proof.
intros A x l.
induction l as [ | hd tl hi]; intros hIn; simpl in *.
- contradiction.
- destruct hIn.
  rewrite H.
  exists nil; exists tl; simpl; reflexivity.
  destruct (hi H) as [ l1 [ l2 h ]].
  exists (hd :: l1); exists l2.
  rewrite <- app_comm_cons; rewrite h.
  reflexivity.
Qed.

I won't say it's less complex than Rui's answer, but I find this solution a little bit easier to understand. But in the end, they are relatively close.

Cheers, V.

Answer 2

When the goal is existentially quantified, you have to give a concrete example of an object with the stated property, and when a hypothesis is existentially quantified, you're allowed to assume one such object exists and introduce it. See FAQs 47, 53, and 54. By the way, an In predicate is already defined in Coq.Lists.List. Check it out here. A reference for Coq tactics is here.

A proof of the first lemma:

Require Import Coq.Lists.List.
Require Import Coq.Setoids.Setoid.

Inductive In {A : Type} (y : A) : list A -> Prop :=
  | InHead : forall xs : list A, In y (cons y xs)
  | InTail : forall (x : A) (xs : list A), In y xs -> In y (cons x xs).

Lemma L1 : forall (t1 : Type) (l1 : list t1) (o1 o2 : t1),
  In o1 (o2 :: l1) <-> o1 = o2 \/ In o1 l1.
Proof.
intros t1 l1 o1 o2. split.
  intros H1. inversion H1 as [l2 [H3 H4] | o3 l2 H2 [H3 H4]].
    left. reflexivity.
    right. apply H2.
  intros H1. inversion H1 as [H2 | H2].
    rewrite H2. apply InHead.
    apply InTail. apply H2.
Qed.

Lemma my_In_map : forall (A B : Type) (l : list A) (y : B) (f : A -> B),
  In y (map f l) -> exists x : A, In x l /\ y = f x.
Proof.
intros A B. induction l as [| z l H1].
  intros y f H2. simpl in *. inversion H2.
  intros y f H2. simpl in *. rewrite L1 in H2. inversion H2 as [H3 | H3].
    exists z. split.
      apply InHead.
      apply H3.
    assert (H4 := H1 _ _ H3). inversion H4 as [x [H5 H6]]. exists x. split.
      rewrite L1. right. apply H5.
      apply H6.
Qed.