coq - 在 Coq 中定义使用程序时，义务中缺少信息的问题

Question

我是 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 记住“所有假设”？

Answer 1

这是 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.