Search code examples
functional-programminglogiccoqproof

Logical Coq Proof related to map function

I am trying to prove the following Lemma:

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

I begin by splitting to handle the first direction, then do induction on l, then the base case is easy. But past that I get stuck. I think it's something to do with exists x and how I cannot get x to line up with x0 no matter where I try introducing x. Help!

Solution

  • I don't understand your problem about x0, if this is about Coq automatically renaming x to x0.

    If I were to tackle your goal I would do it as follows:

    Goal forall (A B : Type) (f : A -> B) (l : list A) (y : B),
    In y (map f l) <->
    exists x, f x = y /\ In x l.
Proof.
  intros A B f l y. split.
  - intro h. induction l as [| a l ih].
    + contradict h.
    + simpl in h. destruct h as [h | h].
      * exists a. split.
        -- assumption.
        -- left. reflexivity.
      * specialize (ih h). destruct ih as [x [e i]].
        exists x. split.
        -- assumption.
        -- right. assumption.

    Perhaps you wanted to line up the induction hypothesis and the goal to apply it directly? Unfortunately I think you have to do as I do, by first destructing the induction hypothesis into an x and its properties and then reconstruct the goal where you stipulate it's in the tail of l.