Coq 在使用程序执行递归函数时丢失了 if 语句中的信息

Question

我想在Coq中尽可能简单和"自然"地编写gcd的递归变体。

Require Import Arith.
Require Import Program.
Program Fixpoint gcd (a b:nat) {measure b} :=
if 0 <? b then gcd b (a mod b) else a.
Next Obligation.
(* Here I need to prove that `a mod b < b` *)
apply Nat.mod_upper_bound.

现在我需要证明这一点b <> 0但我丢失了我们在0 <? b = false分支中的信息。

a, b : nat
gcd : nat -> forall b0 : nat, b0 < b -> nat
============================
b <> 0

如何保留 if 语句中的信息？

我知道我可以使用match，但是我如何用if写它？

Program Fixpoint gcd (a b:nat) {measure b} :=
match b with 0 => a | S b' => gcd b (a mod b) end.
Next Obligation.
apply Nat.mod_upper_bound.
(* Goal:  S b' <> 0 *)
congruence.
Defined.

=== 编辑 ===

我注意到Coq(在较新的版本中？)记得0 <? b和匹配模式(在这种情况下为true或false)之间的关联。 还是Program的一个特点？无论如何，我认为if基本上被扩展为这个match声明，但显然不是......

Program Fixpoint gcd (a b:nat) {measure b} : nat:=
match 0<?b with
| true => gcd b (a mod b)
| false => a
end.
Next Obligation.
apply Nat.mod_upper_bound.
(* now we have ` true = (0 <? b)` in the assumptions, and the goal `b <> 0` *)
now destruct b.
Defined.

Answer 1

可以使用lt_dec来做到这一点。

lt_dec
: forall n m : nat, {n < m} + {~ n < m}

这样我们就可以将所需的证明保存在上下文中，这与使用<?，返回一个bool.

Require Import Arith.
Require Import Program.
Program Fixpoint gcd (a b:nat) {measure b} :=
if lt_dec 0 b then gcd b (a mod b) else a.
Next Obligation.
apply Nat.mod_upper_bound.
now destruct H.
Defined.

---

是的，这是Program的一个功能。实际上，参考手册以非常清晰的方式解释了它(参见§24.1)：

平等的产生。match表达式总是通过相应的相等进行概括。例如，表达式：

match x with
| 0 => t
| S n => u
end.

将首先重写为：

(match x as y return (x = y -> _) with
| 0 => fun H : x = 0 -> t
| S n => fun H : x = S n -> u
end) (eq_refl n).

以下是if不同的原因：

为了更好地控制相等的生成，如果指定了return或in子句，类型检查器将直接回退到 Coq 通常键入的依赖模式匹配类型。同样，if构造也没有被Program特别处理，因此代码中的布尔测试不会自动反映在义务中。可以使用dec组合器来获得正确的假设，如下所示：

Coq < Program Definition id (n : nat) : { x : nat | x = n } :=
if dec (leb n 0) then 0
else S (pred n).