rewrite работает для =, но не для ‹-› (iff) в Coq

У меня есть следующее во время доказательства, в котором мне нужно заменить normal_form step t на value t, поскольку есть доказанная теорема о том, что есть эквиваленты.

H1 : t1 ==>* t1' /\ normal_form step t1'
t2' : tm
H2 : t2 ==>* t2' /\ normal_form step t2'
______________________________________(1/1)
exists t' : tm, P t1 t2 ==>* t' /\ normal_form step t'

Теорема эквивалентности:

Theorem nf_same_as_value
 : forall t : tm, normal_form step t <-> value t

Теперь я могу использовать эту теорему, чтобы переписать normal_form вхождений в гипотезах, но не в цели. Это

rewrite nf_same_as_value in H1; rewrite nf_same_as_value in H2.

работает над гипотезой, но rewrite nf_same_as_value. по цели дает:

Error:
Found no subterm matching "normal_form step ?4345" in the current goal.

Это rewrite на цели здесь теоретически невозможно, или это проблема реализации?

-- Редактировать --

Меня беспокоит то, что если мы определим normal_form step = value, перезапись сработает. Если мы определяем forall t, normal_form step t <-> value t, то rewrite работает, если normal_form step не цитируется в экзистенциальном, но не работает, если он находится в экзистенциальном.

Адаптируя пример @Matt,

Require Export Coq.Setoids.Setoid.
Inductive R1 : Prop -> Prop -> Prop :=
|T1_refl : forall P, R1 P P.

Inductive R2 : Prop -> Prop -> Prop :=
|T2_refl : forall P, R2 P P.

Theorem Requal : R1 = R2. 
Admitted. 

Theorem Requiv : forall x y, R1 x y <-> R2 x y. 
Admitted. 

Theorem test0 : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. rewrite <- Requal in H. (*works*) rewrite Requal. (*works as well*) 

Theorem test2 : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. rewrite <- Requiv in H. (*works*) rewrite Requiv. (*fails*)

Что меня смущает, так это то, почему последний шаг должен потерпеть неудачу.

1 subgoal
y : Prop
H : R1 y y
______________________________________(1/1)
exists x : Prop, R1 x x

Связан ли этот сбой с функциональной расширенностью?

Сообщение об ошибке особенно сбивает с толку:

Error:
Found no subterm matching "R1 ?P ?P0" in the current goal.

R1 _ _ соответствует ровно один подтермин, а именно R1 x x.

Кроме того, согласно @larsr, перезапись работает, если используется eexists

Theorem test1 : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. eexists. rewrite Requiv. (*works as well*) apply H. Qed.

Что здесь eexists добавили?


coq coq-tactic
person tinlyx    schedule 12.12.2015    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Перезапись не может подпадать под квантификатор существования. Вам нужно сначала создать экземпляр t', прежде чем вы сможете выполнить перезапись. Обратите внимание, что econstructor может быть полезной тактикой в ​​этом случае, которая может заменить квантор существования переменной объединения.

ИЗМЕНИТЬ в ответ на комментарий OP

Это все равно не сработает для равенства. В качестве примера попробуйте:

Inductive R1 : Prop -> Prop -> Prop :=
|T1_refl : forall P, R1 P P.

Inductive R2 : Prop -> Prop -> Prop :=
|T2_refl : forall P, R2 P P.

Theorem Req : forall x y, R1 x y = R2 x y. 
Admitted. 

Theorem test : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. rewrite Req. (*rewrite still fails*)

Проблема на самом деле не в равенстве по сравнению с iff, проблема связана с переписыванием под привязкой (в данном случае лямбда). Реализация exists x : A, P на самом деле просто синтаксис для ex A (fun x => P x), поэтому перезапись сбой не из-за iff, а из-за того, что тактика rewrite не хочет попадать под привязку для x в (fun x => P x). Кажется, что есть способ сделать это с помощью setoid_rewrite, однако у меня нет опыта в этом.

person Matt    schedule 12.12.2015
comment
Спасибо. Но отчасти мой вопрос заключается в том, что я не понимаю, почему переписывание не должно входить в состав экзистенциальных кванторов. Я предполагаю, что если бы это было равенство, а не iff, rewrite здесь сработал бы, не так ли? - person tinlyx; 13.12.2015
comment
@tinlyx Я добавил правку, которая может прояснить ситуацию. - person Matt; 13.12.2015
comment
@Matt, спасибо, я добавил обновление по твоему примеру. - person tinlyx; 15.12.2015
comment
Require Import Coq.Setoids.Setoid., а затем setoid_rewrite Requiv. должны работать с квантификатором существования. - person Anton Trunov; 10.05.2017