在 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

显然无法解决，因为我已经丢失了 的信息k1 + k1 = k2 + k2，并且我只能证明两个任意自然数相等。

为什么会发生这种情况？在这种情况下你会做什么来让 Coq 记住“所有假设”？

Answer 1

这就是该策略的作用，这是每当您打开一个帐户时都会应用的program_simpl默认设置（并且也是在您打开义务之前完全解决义务）。您可以通过将其设置为 来将其关闭。如果这太激烈了，如果它无法彻底解决义务（因此可以自动解决的义务），您可以丢弃其结果。Obligation TacticObligationidtac

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.