coq - 展开定义而不减少

Question

Coq manual声明 unfold qualid 策略展开目标中每次出现的 qualid 并将其替换为其 beta-iota-normal 形式。

有没有一种简单的方法可以在不触发 beta/iota 减少的情况下展开定义？

Answer 1

您可能想尝试例如cbv tactic像这样:

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