右側に存在する関数を扱うにはどうすればよいですか？

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 

は基本的には、この証明で上に行くために多くはありません私は実際にinductionをlに使って、xの代わりに上記の形式を得ています。 IHlがexistsの代わりにforallを持っていたとしたら、私はそこに何かを置き換えることができたかもしれませんが、ここで何をすべきか全くわかりません。

私はしばらくこの問題に悩まされていましたが、それが起こった他の問題とは異なり、私はこの解決策をオンラインで見つけることができませんでした。これは私が本を読んでいくうちに問題になるので、SOのような場所を除いては誰にも聞かせてはいけません。

私はいくつかのヒントをいただきたいと思います。ありがとうございました。

---

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 

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. 

---

は、私は1つのケースを行うことに成功し、今他で立ち往生しています。正直言って、私はすでに15分のような問題に5時間を費やしていたので、私はこの時点で遺伝的プログラミングを考慮すべきかもしれないと考え始めています。

Answer 1

ここには、ペンとペーパーのプルーフ（少なくとも最初の->部分）と同じ構造の証明があります。 <tactic>...が表示されている場合は; intuition（Proof with intuition.宣言のため）を意味します。すなわち<tactic>によって生成されたすべてのサブゴールにintuitionの戦術を適用します。 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. 

Answer 2

Hは、2つの異なる方法で真である場合があります。destruct Hを試してください。それで、証拠は簡単に続くと思いますが、あなたが破棄した順番に注意して、Hを実在させてください。