与 map 函数相关的逻辑 Coq 证明

Question

我试图证明以下引理：

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.

我先拆分处理第一个方向，然后对l做归纳，基本情况就简单了。但是过去我被卡住了。我认为这与 exists x 有关，以及无论我在哪里尝试引入 x，我都无法让 x 与 x0 对齐。求助！

Answer 1

我不明白你关于 x0 的问题，如果这是关于 Coq 自动将 x 重命名为 x0。

如果我要解决你的目标，我会这样做：

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.

也许您想将归纳假设与直接应用它的目标对齐？不幸的是，我认为您必须像我一样做，首先将归纳假设分解为 x 及其属性，然后在您规定的目标位于 l.[=16= 的尾部重建目标。 ]

与 map 函数相关的逻辑 Coq 证明

Logical Coq Proof related to map function

functional-programming

logic

coq

proof