Развертывание определения без сокращения

Question

В руководстве Coq говорится, что тактика unfold qualid разворачивает каждое вхождение qualid в цели и заменяет ее своей бета-йота-нормальной формой.

Есть ли простой способ развернуть определение, не вызывая снижение бета / йоты?

Answer 1

Вы можете попробовать, например, cbv тактика примерно так:

Definition foo := (fun (x : nat) => x) 42.
Definition bar := (fun (x : nat) => x) 42.

Goal foo = bar.
  cbv delta [foo].

Это приводит к следующему состоянию проверки:

(fun x : nat => x) 42 = bar