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

Question

Насколько я понимаю, вызовы функций в 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. Мой вопрос сводится к:

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

Answer 1

Ты можешь использовать 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 работает лучше.