如何处理右侧存在的函数？

Question

我不确定我在问题标题中是否使用了正确的词，所以这里是代码：

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

基本上，这个证明没什么可继续的，我只能在l上真正使用induction，在目标中替换x后，我得到了上面的形式。如果 IHl 有一个 forall 而不是 exists 也许我可以在那里替换一些东西，但我完全不确定在这里做什么。

我已经在这个问题上停留了一段时间，但与发生过的其他问题不同的是，我无法在网上找到这个问题的解决方案。这是一个问题，因为我正在自己阅读这本书，所以除了像 SO 这样的地方，没有人可以问。

我希望得到一些提示。谢谢。

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

我设法完成了一个案例，但现在陷入了另一个案例。老实说，由于我已经花了 5 个小时解决一个本应需要 15 分钟的问题，我开始认为也许此时我应该考虑遗传编程。

Answer 1

H 可以通过两种不同的方式实现，请尝试 destruct H。由此，我认为证明很容易得出，但要注意你破坏 H 和实例化存在的顺序。

Answer 2

这是一个与纸笔证明具有相同结构的证明（至少第一 -> 部分）。当您看到 <tactic>... 时，它意味着 ; intuition（因为 Proof with intuition. 声明），即将 intuition 策略应用于 <tactic> 生成的所有子目标。 intuition 使我们不必进行繁琐的逻辑推理，并且可以用一系列 apply 和 rewrite 策略代替，利用一些逻辑引理。

正如@ejgallego 指出的那样，这里的关键是，在证明你可以 destruct 存在假设并从中获取某些类型的居民的同时。这在试图证明存在主义目标时至关重要。

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.

如何处理右侧存在的函数？

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

coq