Почему удаление предположений меняет поведение индуктивных тактов c? - PullRequest
Новая
       82

Почему удаление предположений меняет поведение индуктивных тактов c?

0 голосов
/ 13 февраля 2020

Я пытаюсь показать, что различные определения рефлексивно-транзитивного замыкания эквивалентны. Вот код, который работает: 

Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Relations.Relation_Operators.

Hint Constructors clos_refl_trans.
Hint Constructors clos_refl_trans_1n.

Lemma clos_refl_trans_1n_right:
  forall {A: Type} {R: relation A} (x y: A), 
    clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
Proof.
  intros A R x y H.
  induction H as [ | | x y z _ IH1 _ IH2]; eauto.
  induction IH1; eauto.
Qed.

Обратите внимание на подчеркивание, обозначающее выброшенные переменные. Если я даю имена этих переменных, автоматизация завершается неудачно: 

Lemma clos_refl_trans_1n_right:
  forall {A: Type} {R: relation A} (x y: A),
    clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
Proof.
  intros A R x y H.
  induction H as [ | | x y z H1 IH1 H2 IH2]; eauto.
  induction IH1; eauto. (* three subgoals left *)
Fail Qed.

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

Это где-нибудь задокументировано? Каково обоснование и как я могу предсказать, что это произойдет?

1 Ответ

2 голосов
/ 13 февраля 2020

Я думаю, что в основном это заставит вашу гипотезу индукции зависеть от всех предположений, которые связаны с тем, на что вы навязываете. Если вы введете x : P n m в контексте, где у вас есть h : Q n и y : h = h', он, вероятно, включит их в микс. Во многих случаях это не соответствует тому, что вы хотите, и некоторые clean заранее могут сделать вашу индукцию внезапно go через.

Существует также очень полезный вариант induction, induction ... in который позволяет вам указать, какую часть контекста вы хотите сохранить при выполнении индукции. 

Lemma clos_refl_trans_1n_right:
  forall {A: Type} {R: relation A} (x y: A),
    clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
Proof.
  intros A R x y H.
  induction H as [ | | x y z H1 IH1 H2 IH2]; eauto.
  induction IH1 in z, IH2 |- *. all: eauto.
Qed.

Здесь вы получите предупреждение, которое я не совсем понимаю, если честно (Cannot remove x и Cannot remove y) но вы получите ожидаемый результат. Это также имеет то преимущество, что позволяет вам указать, что следует обобщать.

Возможно, у кого-то есть лучшее объяснение.

...