Как применить функцию один раз во время упрощения в Coq?

Насколько я понимаю, вызовы функций в Coq непрозрачны. Иногда мне нужно использовать unfold, чтобы применить его, а затем fold, чтобы вернуть определение / тело функции к ее имени. Это часто бывает утомительно. Мой вопрос: есть ли более простой способ применить конкретный экземпляр вызова функции?

В качестве минимального примера для списка l, чтобы доказать, что правое добавление [] не меняет l:

Theorem nil_right_app: forall {Y} (l: list Y), l ++ [] = l.
Proof.
  induction l. 
    reflexivity.

Это оставляет:

1 subgoals
Y : Type
x : Y
l : list Y
IHl : l ++ [] = l
______________________________________(1/1)
(x :: l) ++ [] = x :: l

Теперь мне нужно применить определение ++ (т.е. app) один раз (притворившись, что в цели есть другие ++, которые я не хочу применять / расширять). В настоящее время единственный известный мне способ реализовать это одноразовое приложение - сначала развернуть ++, а затем свернуть его:

    unfold app at 1. fold (app l []).

давая:

______________________________________(1/1)
x :: l ++ [] = x :: l

Но это неудобно, так как мне нужно выяснить форму термина для использования в fold. Я выполнял вычисления, а не Coq. Мой вопрос сводится к следующему:

Есть ли более простой способ реализовать это одноразовое функциональное приложение с таким же эффектом?


coq coq-tactic
person tinlyx    schedule 11.10.2015    source источник
comment
Все определения Coq не являются непрозрачными, но есть способы предотвратить автоматическое развертывание определения Coq (например, используя Qed. Вместо Defined при определении функции с использованием тактики).   -  person Vinz    schedule 12.10.2015
comment
что вы имеете в виду под непрозрачным?   -  person Charlie Parker    schedule 01.01.2019

Ответы (1)


arrow_upward
3
arrow_downward

Вы можете использовать simpl, compute или vm_compute, если хотите попросить Coq выполнить некоторые вычисления за вас. Если определение функции Opaque, приведенное выше решение не сработает, но вы можете сначала доказать лемму о переписывании, например:

forall (A:Type) (a:A) (l1 l2: list A), (a :: l1) ++ l2 = a :: (l1 ++ l2).

используя вашу технику, а затем rewrite с ней, когда это необходимо.

Вот пример использования simpl:

Theorem nil_right_app: forall {Y} (l: list Y), l ++ nil = l.
Proof.
(* solve the first case directly *)
intros Y; induction l as [ | hd tl hi]; [reflexivity | ]. 
simpl app. (* or simply "simpl." *)
rewrite hi.
reflexivity.
Qed.

Отвечая на ваш комментарий, я не знаю, как указать cbv или compute вычислять только определенный символ. Обратите внимание, что в вашем случае они, кажется, слишком быстро вычисляют и simpl работают лучше.

person Vinz    schedule 12.10.2015
comment
благодаря. Вы имеете в виду, что я могу использовать «вычислить» как «вычислить приложение на 1» или что-то подобное? Не могли бы вы привести пример, если да. Я просмотрел документ coq для вычислений и cbv, но не нашел конкретного примера. - person tinlyx; 12.10.2015
comment
Обновите пример и несколько слов - person Vinz; 12.10.2015