применить тактику перезаписи к подвыражению - PullRequest
Новая
       22

применить тактику перезаписи к подвыражению

2 голосов
/ 22 апреля 2019

Как я могу применить rewrite ->, ориентируясь только на подвыражение?Например, рассмотрим эту теорему: 

Parameter add : nat -> nat -> nat.
Axiom comm : forall a b, add a b = add b a.

Theorem t1 : forall a b : nat,
(add (add a b) (add a (add a b))) =
(add (add a b) (add a (add b a))).

Интуитивно, она требует коммутирования только одного подвыражения (add a b), но если я сделаю rewrite -> (comm a b), он переписывает все вхождения.Как я могу настроить таргетинг на конкретное подвыражение?

Ответы [ 2 ]

2 голосов
/ 22 апреля 2019

Это тот случай, когда средства сопоставления ssreflect обычно более удобны, чем "at" [Я бы осмелился сказать, что переопределенные термины часто являются причиной того, что люди переключаются на перезапись ssreflect]. В частности:

  • rewrite {pos}[pat]lemma выберет вхождения pos шаблона pat для перезаписи,
  • pat может быть контекстным шаблоном , который может позволить вам повысить надежность ваших сценариев.
2 голосов
/ 22 апреля 2019

Вы можете выбрать конкретный случай с помощью тактики rewrite, используя суффикс at <em>N</em>.Вхождения нумеруются от 1 в порядке слева направо.Вы можете переписать несколько вхождений, разделяя их индексы пробелами.Вам нужно Require Import Setoid.Суффикс at также доступен с некоторыми другими тактиками, нацеленными на вхождения термина, включая многие тактики, выполняющие преобразования (change, unfold, fold и т. Д.), set, destruct,и т. д. 

intros.
rewrite -> (comm a b) at 2.
rewrite -> (comm _ _).
reflexivity.

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

assert (Comm := comm).
congruence.

Для большей автоматизации Hint Rewrite создает базу данных теорем, которые попытается применить тактика autorewrite.Для более продвинутой автоматизации, посмотрите обобщенное переписывание с сетоидами, с которым я не достаточно знаком, чтобы разъяснять.

...