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

Question

例如,如果我定义一个从nat到nat的函数,那就是

Definition plusfive(a:nat): nat := a + 5.

但是,我想定义一个函数,其参数是使用"S"构造函数(即非零)构造的nat,是否可以直接指定为类型？就像是

Definition plusfive(a: nat.S): nat := a + 5.

(我知道在这种情况下我也可以添加一个a非零的证明的参数,但我想知道是否可以根据'S'构造函数直接命名类型).

Answer 1

函数必须完整,因此您必须使用某个子类型代替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直接在表达式中使用,而不必交错分母非零的证明.在定义表达式之后,证明表达式是正确的,而不是同时进行.