Как указать местоположение с помощью тактики перезаписи? - PullRequest
Новая
       36

Как указать местоположение с помощью тактики перезаписи?

0 голосов
/ 21 июня 2019

У меня есть простая лемма для списков, которая гласит: n::l = [n]++l, доказательство которого приводится ниже. 

Lemma cons_to_app : (forall (n: nat) (l: list nat),  n :: l = [n] ++ l).
Proof.
  simpl. reflexivity.
Qed.

Теперь я хочу использовать это доказательство, переписать термины "против" :: везде, где они появляются в цели доказательства.Например, рассмотрим следующее. 

Lemma easy_lemma : forall (n : nat) (xs ys : list nat), (n::xs) ++ (n::ys) = (n::xs) ++ ([n] ++ ys).

Я хотел бы переписать (n::ys) в [n] ++ ys, и доказательство сделано.Поскольку n::ys - второй раз, когда :: появляется в контрольной цели, я думал, что rewrite const_to_app at 2 будет работать, но на самом деле он действует на 3-й :: и изменяет контрольную цель на (n :: xs) ++ n :: ys = ([n] ++ xs) ++ [n] ++ ys.

Какое расположение можно указать, чтобы перезапись работала на (n::ys) термине?

1 Ответ

2 голосов
/ 26 июня 2019

Я до сих пор не могу найти исходный источник, который говорит о точном поведении rewrite at (кроме одного упомянутого eponier ).Сообщение по ссылке было написано в 2011 году, но, по-видимому, оно все еще действует на 2019 год с Coq версии 8.9.1 и, вероятно, не будет «исправлено», поскольку проблема была закрыта как «недействительная», говоря «изменение поведения приведет к сбою»обратная совместимость ".

Задача

rewrite lemma at n создает равенство с использованием первого вхождения, а затем переписывает его n-ное вхождение.

Учитывая лемму для доказательства

Lemma easy_lemma :
  forall (n : nat) (xs ys : list nat), (n::xs) ++ (n::ys) = (n::xs) ++ ([n] ++ ys).

и лемма, используемая для перезаписи 

Lemma cons_to_app : (forall (n: nat) (l: list nat),  n :: l = [n] ++ l).

rewrite cons_to_app at n. всегда выбирает подтерм n :: xs, затем переписывает n-е вхождение от n :: xs до [n] ++ xs.Второй n :: xs просто оказывается третьим _ :: _.

Решение

Простое решение состоит в том, чтобы дать достаточно аргументов, чтобы сообщить Coq точную вещь, которую нужно переписать.В этом случае достаточно rewrite (cons_to_app _ ys).

Одной из альтернатив является использование тактики setoid_rewrite, которая просматривает все применимые подтермы.Тем не менее, иногда это слишком глубоко смотрит в определения, и это действительно так для этого примера;setoid_rewrite cons_to_app at 1. дает 

1 subgoal
n : nat
xs, ys : list nat
______________________________________(1/1)
[n] ++
(fix app (l m : list nat) {struct l} : list nat := match l with
                                                   | [] => m
                                                   | a :: l1 => a :: app l1 m
                                                   end) xs (n :: ys) = (n :: xs) ++ [n] ++ ys

Сложение app дает [n] ++ (xs ++ n :: ys), что отличается от того, что мы хотим, т.е. ([n] ++ xs) ++ n :: ys.Мы можем заметить, что setoid_rewrite развернул app один раз, изменив LHS на n :: (xs ++ n :: ys), а затем создал лемму для перезаписи самого внешнего _ :: _.

Чтобы избежать развертывания app, мы можем объявить Opaque app. до переписывания.Тогда setoid_rewrite ... at 1 дает то, что мы хотим (как и at 2).Чтобы отменить эффект Opaque, используйте Transparent.

...