我是 Coq 的新手,正在尝试弄清楚如何使用 Program
来更轻松地定义事物然后解决义务,但是,有时我会遇到无法解决的义务,因为某些信息有迷路了。
例如,如果我定义了以下内容(有点做作,但这是我能想到的最简单的示例),那么函数 f 如果函数接受两个相同的偶数并返回该数字的两倍。
Program Definition f {n : nat} (k1 k2 : {j : nat | j + j = n}) : {j : nat | j = n} := k1 + k2.
Next Obligation.
问题是,当我开始解决第一个义务时,这就是我剩下的
k1, k2 : nat
============================
k1 + k2 = k2 + k2
witch 显然无法解决,因为我丢失了有关 k1 + k1 = k2 + k2
的信息,剩下的就是证明两个任意自然数相等。
为什么会发生这种情况,在这种情况下您如何做才能让 Coq 记住“所有假设”?
最佳答案
这是 program_simpl
策略的工作,它是默认的 Obligation Tactic
,每当您打开一个 Obligation
时应用(并且还可以完全解决打开它们之前的义务)。您可以通过将其设置为 idtac
来关闭它。如果这太过激了,如果它不能彻底解决义务(因此可以自动解决的义务是),您可以丢弃它的结果。
Require Import Psatz.
#[local] Obligation Tactic := try now program_simpl.
#[program] Definition f {n : nat} (k1 k2 : {j : nat | j + j = n}) : {j : nat | j = n} := k1 + k2.
Next Obligation.
intros n [k1 ?] [k2 ?]. (* program_simpl is responsible for the usual automatic intros, but now we have to do it *)
simpl.
lia.
Qed.
关于coq - 在 Coq 中定义使用程序时,义务中缺少信息的问题,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/69138674/