Логическое Coq Proof, связанное с функцией карты - PullRequest
Новая
       93

Логическое Coq Proof, связанное с функцией карты

0 голосов
/ 27 сентября 2019

Я пытаюсь доказать следующую лемму: 

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, тогда базовый случай прост.Но мимо этого я застреваю.Я думаю, что это как-то связано с существующим х и как я не могу заставить х выровняться с х0 независимо от того, где я пытаюсь ввести х.Помогите!

1 Ответ

1 голос
/ 27 сентября 2019

Я не понимаю вашей проблемы с 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.

...