В чем разница между тактикой возврата и обобщения в Coq?

Из справочного руководства Coq (8.5p1) у меня сложилось впечатление, что revert является обратным intro, но в определенной степени generalize тоже. Например, revert и generalize dependent ниже кажутся одинаковыми.

Goal forall x y: nat, 1 + x = 2 + y -> 1 + x + 5 = 7 + y.
intros x y. revert x y.
intros x y. generalize dependent y. generalize dependent x.

Просто generalize мощнее revert?

Кроме того, документация немного циклична в объяснении вещей о generalize:

Эта тактика применима к любой цели. Он обобщает вывод относительно некоторого термина.

Похож ли generalize на оператор абстракции в лямбда-исчислении?


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

Ответы (2)


arrow_upward
7
arrow_downward

Да, generalize мощнее. Вы продемонстрировали, что он имеет по крайней мере ту же мощность, что и revert, имитируя revert с generalize. Обратите внимание, что generalize работает с любыми терминами, revert -- только с идентификаторами.

Например, revert не может сделать пример из мануала:

  x, y : nat
  ============================
  0 <= x + y + y

Coq < generalize (x + y + y).
1 subgoal

  x, y : nat
  ============================
  forall n : nat, 0 <= n

Что касается «цикличности» определения, настоящее объяснение находится прямо под примером:

Если целью является G, а t является вложенным термином типа T в цели, то generalize t заменяет цель на forall x:T, G0, где G0 получается из G путем замены всех вхождений t на x.

По сути, это говорит о том, что generalize заключает вашу цель в forall, заменяя некоторый термин новой переменной (x).

Конечно, generalize следует использовать с некоторыми размышлениями и осторожностью, так как после его использования можно получить ложное утверждение для доказательства:

Goal forall x y, x > 0 -> 0 < x + y + y.
  intros x y H.
  generalize dependent (x + y + y).

(* results in this proof state: *)
  x, y : nat
  H : x > 0
  ============================
   forall n : nat, 0 < n
person Anton Trunov    schedule 28.06.2016
comment
Спасибо за ответ, но я до сих пор не понимаю, почему эта операция вообще называется обобщением, несмотря на заданную операционную семантику. Кроме того, приведенный вами пример цели кажется ложным с самого начала. Я не понимаю, как обобщение сделало здесь что-то еще хуже. - person tinlyx; 06.07.2016
comment
Он называется generalize, потому что вы заменяете конкретный и, возможно, сложный термин, имеющий некоторую внутреннюю структуру, на заполнитель без какой-либо внутренней структуры того же типа. т.е. вы абстрагируетесь от некоторых деталей и получаете более общую вещь. И последний пример (цель верная, кстати, попробуй intros; omega. на ней) показывает, что нельзя без ограничений отбрасывать какие-то конкретные детали, если хочешь сохранить справедливость формулы. - person Anton Trunov; 06.07.2016
comment
Благодарю за разъяснение. - person tinlyx; 06.07.2016

arrow_upward
1
arrow_downward

Насколько я помню, revert — это просто более простая форма generalize, которую обычно легче использовать новичкам: она противоположна intro. Используя вариант generalize, вы можете сделать гораздо больше (особенно с зависимостью между терминами и типами).

person Vinz    schedule 28.06.2016