замена / переписывание внутри экзистенциальной гипотезы

Question

У меня есть следующее состояние доказательства:

H: exists x : A, f x = y /\ In x l
----------------------
Goal: exists x0 : A, f x0 = y /\ In x0 (x :: l)

Я знаю, что In x l подразумевает In x (x :: l). Поэтому я хотел бы закончить sh с доказательством переписав что-то вроде этого:

rewrite ___ in H.

, приводя к состоянию доказательства:

H: exists x : A, f x = y /\ In x (x :: l)
----------------------
Goal: exists x0 : A, f x0 = y /\ In x0 (x :: l)

Что может быть завершено (я подумайте) с:

exact H.

Возможно ли такое переписывание? Есть ли правильный метод, который я могу использовать в этом направлении?

rewrite терпит неудачу, и replace в гипотезе, похоже, фактически не меняет гипотезу.

Answer 1

Нет, насколько я знаю, такое переписывание невозможно.

Но вы можете попробовать destruct H as [x H]. exists x.. Это даст вам x, что удовлетворяет f x = y /\ In x 1.

Answer 2

После разрушения гипотезы, чтобы получить f x = y /\ In x l, мы можем выполнить переписывание сетоидов, используя in_cons : In x l -> In x (x' :: l) (из модуля List), но с небольшой дополнительной работой.

Нам как-то нужно сначала бета -разверните лемму до in_cons : impl (In x l) (In x (x' :: l)) (ниже, используя fold tacti c), чтобы она распознавалась как правило перезаписи (impl регистрируется как отношение перезаписи, тогда как -> является сахаром для примитивного синтаксиса , это не распознается плагином для перезаписи).

Насколько я могу судить, переписать невозможно, пока есть exists, даже с вариантом setoid_rewrite, который работает под связывателями справа ситуации.

Require Import List.

Lemma foo {A B} (f : A -> B) (x' : A) (y : B) (l : list A)
  (H: exists x : A, f x = y /\ In x l) :
exists x0 : A, f x0 = y /\ In x0 (x' :: l).
Proof.
  destruct H.
  pose proof (in_cons x' x l) as E.
  fold (Basics.impl (In x l) (In x (x' :: l))) in E.
  rewrite E in H.
  eauto.
Qed.