Coq 在使用 Program 执行递归函数时从 if 语句中丢失信息

Question

我想在 Coq 中尽可能简单地 "naturally" 编写 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}

这样我们可以在上下文中保留我们需要的证明，这与使用 <? 时不同，returns 和 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）：

Generation of equalities. A match expression is always generalized by the corresponding equality. As an example, the expression:
match x with
  | 0 => t
  | S n => u
  end.
will be first rewritten to:
(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 不同的原因：

To give more control over the generation of equalities, the typechecker will fall back directly to Coq’s usual typing of dependent pattern-matching if a return or in clause is specified. Likewise, the if construct is not treated specially by Program so boolean tests in the code are not automatically reflected in the obligations. One can use the dec combinator to get the correct hypotheses as in:
Coq < Program Definition id (n : nat) : { x : nat | x = n } :=
        if dec (leb n 0) then 0
        else S (pred n).

Coq 在使用 Program 执行递归函数时从 if 语句中丢失信息

Coq losing information from if-statement when doing recursive function with Program

coq