COQ:如何引用特定构造函数生成的类型?

函数必须是完整的,因此必须使用某种子类型,而不是 nat 或者添加减少输入空间的参数,例如 (H: a<>0)

Definition plusfive(a:nat) (H:a<>0) :=
  match a as e return a=e -> _ with
  | S _ => fun _  => a + 5
  | _   => fun H0 => match (H H0) with end
  end eq_refl.

然而,这些技巧被发现在大的开发中很难使用,通常情况下,人们会在基类型上使用完整的函数,这些函数返回错误输入值的伪值,并证明使用正确的参数分别调用函数定义。例如,请参见如何在标准库中定义划分。

Require Import Nat.
Print div.

div = 
fun x y : nat => match y with
                 | 0 => y
                 | S y' => fst (divmod x y' 0 y')
                 end
     : nat -> nat -> nat

所以 Compute (div 1 0). 给你 0 .

好的是你可以用 div 在表达式中,不必交错证明分母为非零。然后证明表达式是正确的 之后 它已经被定义了,而不是同时定义的。