Руководство завершает доказательство

Question

Буду признателен за некоторые рекомендации, завершающие это доказательство.Я застрял в последнем admit (остальные я выполнил без проблем, но я опускаю реальные доказательства).

Я добавил комментарии после моих рассуждений, потому что я думаю, что это объясняет лучше меняпытаясь описать это в абзаце.

Это определение используемых функций:

In = 
fix In (A : Type) (x : A) (l : list A) {struct l} : Prop := match l with
                                                            | [ ] => False
                                                            | x' :: l' => x' = x \/ In A x l'
                                                            end
     : forall A : Type, A -> list A -> Prop

Argument A is implicit and maximally inserted
Argument scopes are [type_scope _ _]

---

map = 
fix map (X Y : Type) (f : X -> Y) (l : list X) {struct l} : list Y := match l with
                                                                      | [ ] => [ ]
                                                                      | h :: t => f h :: map X Y f t
                                                                      end
     : forall X Y : Type, (X -> Y) -> list X -> list Y

Arguments X, Y are implicit and maximally inserted
Argument scopes are [type_scope type_scope function_scope _]

---

А вот и лемма:

Lemma foo :
  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.
  - admit.
  - induction l as [|x0 l' HIl'].
    * admit.
    * (*
      HIl': (exists x : A, f x = y /\ In x l') -> In y (map f l')
      Goal: (exists x : A, f x = y /\ In x (x0 :: l')) -> In y (map f (x0 :: l'))
      *)
      intros H. simpl.
      (*
      Goal: f x0 = y \/ In y (map f l')
      *)
      right.
      (*
      Taking the right side, because if `f x0 = y`, then the induction
      hypothesis would tell us nothing.
      *)
      apply HIl'.
      (*
      Goal: exists x : A, f x = y /\ In x l'
      *)
      destruct H as [x1 H']. exists x1.
      (*
      This `x1` should be the element that is in both `l'` and `x0 ::
      l'`, because we discarded the case when `f x0 = y`.

      Goal: f x1 = y /\ In x1 l'
      *)
      destruct H' as [H'l H'r]. split.
      + (* Goal: fx1 = y *) apply H'l .
      + (* Goal: In x1 l' *)
        (*
           `x1` must be in `l'`, because we know it is in x0 :: l` by H'r:
           H'r: In x1 (x0 :: l')
           and we discarded the case where `f x0 = y`.
        *)
        destruct H'r as [H'rl | H'rr].
        { (* Stuck!!! *) admit. }
        { apply H'rr. } Abort.

Answer 1

Lemma foo :
  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.
  induction l; split; intros.
  - now inversion H.
  - now firstorder.
  - inversion H.
    + now exists a; firstorder.
    + apply IHl in H0.
      destruct H0 as [x Hx].
      now exists x; firstorder.
  - destruct H as [x [Hx [Hi | Hi]]].
    + now left; subst.
    + right.
      apply IHl.
      exists x.
      firstorder.
Qed.

Answer 2

Тактика right. слишком рано.В этот момент H говорит нам, что x находится в (x0 :: l), но что, если это так, потому что x = x0?Тогда нет никакого способа доказать правильную альтернативу, но левая верна в этом случае.Следовательно, вы должны деконструировать H перед тем, как выбрать сторону left или right.

Answer 3

Lemma foo :
  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.
  - admit.
  - induction l as [|x0 l' HIl'].
    * admit.
    * (*
      -- HIl': (exists x : A, f x = y /\ In x l') -> In y (map f l')
      -- Goal: (exists x : A, f x = y /\ In x (x0 :: l')) -> In y (map f (x0 :: l'))
      *)
      intros H. simpl.
      (*
      -- Goal: f x0 = y \/ In y (map f l')

      you might need to destruct H first.
       *)
      destruct H.
      destruct H.
      (* right. *)
      (*
      -- Taking the right side, because if `f x0 = y`, then the induction
      -- hypothesis would tell us nothing.
      acatually, consider x = x0, we can subst and just apply H here.
      we will destruct on H0 to analysis case x = x0 || In x l'.
       *)
      destruct H0. {
        left.
        rewrite H0.
        assumption.
      }
      (* in this case we select rhs. *)
      {
        right.
        apply HIl'.
        exists x.
        split. {
          assumption.
        }
        {
          assumption.
        }
      }
Admitted.

Извините, что я был на работе, я думал, что отредактирую это через минуту.

Вы заметите, что гипотеза In x l должна быть разрушена, а затем проанализирована отдельно.Когда вы выполняете индукцию по l, она заменяется на In x (x0 :: l), конъюнктивное значение должно сохраняться либо для x = x0, либо для In x l.