Переписать единственный случай в ltac

Question

Как я могу призвать rewrite в ltac переписать только одно вхождение? Я думаю, что документация Coq упоминает что-то о rewrite at но я не смог использовать его на практике, и нет примеров.

Это пример того, что я пытаюсь сделать:

Definition f (a b: nat): nat.
Admitted.

Theorem theorem1: forall a b: nat, f a b = 4.
Admitted.

Theorem theorem2: forall (a b: nat), (f a b) + (f a b) = 8.
Proof.
intros a b.
(*
my goal here is f a b + f a b = 8
I want to only rewrite the first f a b
The following tactic call doesn't work
*)
rewrite -> theorem1 at 1.

Answer 1

Вы используете rewrite at вариант тактики, который, как указано в руководстве, всегда выполняется посредством переписывания сетоидов (см. https://coq.inria.fr/refman/Reference-Manual010.html).

Другая возможность иметь более точный контроль над вашими правилами переписывания - это утверждать общую форму желаемого переписывания (что здесь можно было бы доказать с помощью theorem1), затем выполните целенаправленную переписку с новой гипотезой.

Это работает без обращения к каким-либо библиотекам:

intros a b.
assert (H: f a b + f a b = 4 + f a b) by (rewrite theorem1; reflexivity).
rewrite H.

Answer 2

Когда я пытаюсь rewrite -> theorem1 at 1. как вы предлагаете, я получаю следующее сообщение об ошибке:

Error: Tactic failure: Setoid library not loaded.

Итак, в качестве реакции я перезапустил ваш скрипт, включая следующую команду в самом начале.

Require Import Setoid.

И теперь, это работает (я тестирую с coq 8.6).

Answer 3

Есть несколько вариантов, один из них был отмечен @Yves.

Другой вариант заключается в использовании pattern тактика:

pattern (f a b) at 1.
rewrite theorem1.

Хитрость здесь в том, что pattern (f a b) at 1. поворачивает цель

f a b + f a b = 8

в

(fun n : nat => n + f a b = 8) (f a b)

По сути, это бета-версия расширяет вашу цель, абстрагируясь от первого появления f a b, Также нормально rewrite не будет переписывать под связывателями (например, лямбда-выражения), потому что, если это так, вы сможете перейти от, скажем, fun x => x + 0 в fun x => x, которые не равны в ванильной Coq.

затем rewrite theorem1. переписывает аргумент (f a b) в 4 и немного упрощает (это делает бета-сокращение), следовательно, вы получаете 4 + f a b = 8,

Примечание: вы также можете использовать replace тактика вроде так:

replace (f a b + f a b) with (4 + f a b) by now rewrite theorem1.