Переписать эквивалентность под существует в цели

Question

Я доказал эквивалентность and_distributes_over_or:

Theorem and_distributes_over_or : forall P Q R : Prop,
  P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).

В другом месте у меня есть цель

exists x0 : A, f x0 = y /\ (x = x0 \/ In x0 xs)

(Для контекста я работаю через Логические основы ; Я на In_map_iff упражнении главы по конструктивной логике . Пожалуйста, не говорите мне решение к упражнению!)

Я пытался использовать rewrite and_distributes_over_or для своей цели (чтобы получить exists x0 : A, (f x0 = y /\ x = x0) \/ (f x0 = y /\ In x0 xs)). Я получил ошибку:

Found no subterm matching "?P /\ (?P0 \/ ?P1)" in the current goal.

Используя свой человеческий мозг, я вижу в цели то, что кажется очень очевидным проявлением этой формы. Почему Coq, с нечеловеческим не-мозгом, не видит его под экзистенциальным квантификатором? Есть ли у вас какие-либо советы, чтобы сделать эту работу?

Я прочитал предыдущий вопрос с названием, похожим на этот , но он касается переписывания в гипотезах, а не в целях, и ответ, похоже, не применим к моей ситуации.

Answer 1

Просто используйте setoid_rewrite вместо rewrite и убедитесь, что Require Setoid. (хотя загрузка List уже сделала это в этом случае).

Шаблон, который ищет Coq, находится подСвязующее;то есть он находится в теле функции.Связующее не очевидно, потому что оно является частью exists, но ваша цель на самом деле ex (fun (x0:A) => f x0 = y /\ (x = x0 \/ In x0 xs)), и механизм обозначений Coq хорошо печатает его как exists x0, ....Базовая тактика rewrite не может переписывать внутри функций, но setoid_rewrite может.

В сторону: обратите внимание, что определение ex и его обозначение exists x, ... не встроены в Coq, ноопределены в стандартной библиотеке!Вы можете проверять подобные вещи с помощью Locate exists (чтобы найти обозначения) и Print ex (для просмотра определения).Также есть Unset Printing Notations., если вы не уверены, какие нотации используются, хотя имейте в виду, что существует множество нотаций, которые вы, вероятно, воспринимаете как должное, например /\, = и даже ->.