如何消除表达式内部的析取

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.
split.
- generalize dependent y.
  generalize dependent f.
  induction l.
  + intros. inversion H.
  + intros.
    simpl.
    simpl in H.
    destruct H.
    * exists x.
      split.
      apply H.
      left. reflexivity.
    * 

---

1 subgoal
A : Type
B : Type
x : A
l : list A
IHl : forall (f : A -> B) (y : B),
      In y (map f l) -> exists x : A, f x = y / In x l
f : A -> B
y : B
H : In y (map f l)
______________________________________(1/1)
exists x0 : A, f x0 = y / (x = x0 / In x0 l)

由于证明exists x0 : A, f x0 = y / (x = x0 / In x0 l)与证明exists x0 : A, f x0 = y / In x0 l相同，我想在这里消除目标内部的x = x0，以便我可以应用归纳假设，但我不确定如何做到这一点。我已经尝试了left in (x = x0 / In x0 l)和其他各种事情，但我没有成功地实现它。事实证明，定义一个 forall a b c, (a / c) -> a / (b / c) 类型的辅助函数来重写也不适用于存在主义下的项。

怎么能做到这一点呢？

请注意，以上是SF书籍练习之一。

Answer 1

您可以通过以下任何一种方式访问归纳假设的组件：

• specialize (IHl f y h); destruct IHl
• destruct (IHl f y H)
• edestruct IHl

然后，您可以使用exists和split将目标操作为更易于使用的形式。

Answer 2

事实证明，有必要定义一个帮助程序。

Lemma In_map_iff_helper : forall (X : Type) (a b c : X -> Prop), 
  (exists q, (a q / c q)) -> (exists q, a q / (b q / c q)).
Proof.
intros.
destruct H.
exists x.
destruct H.
split.
apply H.
right.
apply H0.
Qed.

这会立即完成所需的重写。我犯了一个非常愚蠢的错误，认为我需要一种策略而不是辅助引理。我应该更仔细地研究前面的例子——如果我这样做了，我会意识到存在主义是需要解释的。