CODEWITHSUNDEEP
coq
Marko Grdinić
Marko Grdinić

Reputation: 4062

How to deal with a function with an exists on the right side?

I am not sure whether I am using the right words in the question title, so here is the code:

Lemma In_map_iff :
  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.
  - intros.
    induction l.
    + intros. inversion H.
    + exists x.
      simpl.
      simpl in H.
      destruct H.
      * split.
        { apply H. } 
        { left. reflexivity. }
      * split.

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

Basically, there is not much to go on with this proof, I can only really use induction on l and after substituting for x in the goal I get the above form. If IHl had a forall instead of exists maybe I could substitute something there, but I am not sure at all what to do here.

I've been stuck on this one for a while now, but unlike the other problems where that has happened, I could not find the solution online for this one. This is a problem as I am going through the book on my own, so have nobody to ask except in places like SO.

I'd appreciate a few hints. Thank you.

Lemma In_map_iff :
  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.
  - intros.
    induction l.
    + intros. inversion H.
    + simpl.
      simpl in H.
      destruct H.
      * exists x.
        split.
        { apply H. }
        { left. reflexivity. }
      * destruct IHl.
        -- apply H.
        -- exists x0.
           destruct H0.
           ++ split.
              ** apply H0.
              ** right. apply H1.
  - intros.
    inversion H.
    induction l.
    + intros.
      inversion H.
      inversion H1.
      inversion H3.
    + simpl.
      right.
      apply IHl.
      * inversion H.
        inversion H0.
        inversion H2.
        exists x.
        split.
        -- reflexivity.
        -- destruct H3.

  A : Type
  B : Type
  f : A -> B
  x0 : A
  l : list A
  y : B
  H : exists x : A, f x = y /\ In x (x0 :: l)
  x : A
  H0 : f x = y /\ In x (x0 :: l)
  IHl : (exists x : A, f x = y /\ In x l) ->
        f x = y /\ In x l -> In y (map f l)
  x1 : A
  H1 : f x1 = y /\ In x1 (x0 :: l)
  H2 : f x = y
  H3 : x0 = x
  H4 : f x = y
  ============================
  In x l

I managed to do one case, but am now stuck in the other. To be honest, since I've already spent 5 hours on a problem that should need like 15 minutes, I am starting to think that maybe I should consider genetic programming at this point.

Upvotes: 2

Views: 833

Answers (2)

Anton Trunov
Anton Trunov

Reputation: 15424

Here is a proof that has the same structure as would have a pen-and-paper proof (at least the first -> part). When you see <tactic>... it means ; intuition (because of Proof with intuition. declaration), i.e. apply the intuition tactic to all the subgoals generated by <tactic>. intuition enables us not to do tedious logical deductions and can be replaced by a sequence of apply and rewrite tactics, utilizing some logical lemmas.

As @ejgallego pointed out the key here is that while proving you can destruct existential hypotheses and get inhabitants of some types out of them. Which is crucial when trying to prove existential goals.

Require Import Coq.Lists.List.

Lemma some_SF_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.
Proof with intuition.
  intros A B f l y. split; intro H.
  - (* -> *)
    induction l as [ | h l'].
    + (* l = [] *)
      contradiction.
    + (* l = h :: l' *)
      destruct H.
      * exists h...
      * destruct (IHl' H) as [x H'].
        exists x...
  - (* <- *)
    admit.
Admitted.

Upvotes: 1

ejgallego
ejgallego

Reputation: 6852

H can be true on two different ways, try destruct H. From that, the proof follows easily I think, but be careful on the order you destruct H and instantiate the existential thou.

Upvotes: 2

Related Questions