在Coq中定义整数加法

如何解决在Coq中定义整数加法

我遵循this question的答案来定义Coq中的整数，但是当尝试在其上定义加法时，总是出现错误“无法猜测递减的参数”。我尝试了多种不同的定义，但它似乎总是会发生。有什么方法可以证明Coq的论点在减少吗？也许我错过了一些定义加法的明显方法。

Inductive nat : Type := (*Natural numbers*)
| O
| S (n : nat).

Fixpoint plus (n:nat) (m:nat) : nat := (*Addition of natural numbers*)
match n with
| O => m
| S(n') => S(plus n' m) 
end.

Notation "x + y" := (plus x y).

Inductive Z := (*Integers*)
  | Positive : nat -> Z   
  | Negative : nat -> Z.  

Fixpoint plus (n:Z) (m:Z) : Z := (*Addition of integers*)
match n,m with
| Positive O,_ => m
| _,Positive O => n
| Negative O,Negative O => n
| Positive (S n'),Positive (S m') => Positive (n' + m')
| Positive (S n'),Negative (S m') => plus (Positive n') (Negative m')
| Negative (S n'),Positive (S m') => plus (Positive n') (Negative m') 
| Negative (S n'),Negative (S m') => Negative (n'+ m') 
end.

解决方法

在Coq中，您可以定义的唯一递归函数是对参数的子项执行递归调用的函数。尽管Positive n'小于Positive (S n')（这可以确保您的递归调用是安全的），但它不是Positive (S n')的一个子项（实际上并不会发生里面）。因此，Coq无法识别您的函数总是终止并拒绝它。

解决方案是定义加法而不递归：

Definition plusZ (n1 n2 : Z) : Z :=
  match n1,n2 with
  | Positive n1,Positive n2 => Positive (n1 + n2)
  | Negative n1,Negative n2 => Negative (n1 + n2)
  | Positive n1,Negative n2 =>
    if n2 <=? n1 then Positive (n1 - n2)
    else Negative (n2 - n1)
  | Negative n1,Positive n2 => (* Analogous to the previous case *)
  end.

在这里，<=?指nat上的布尔比较运算符，而n1 - n2指的是截断减法，当n1 <= n2时得出0。 （要注意这种编码的一件事是它包含两种表示形式的0：Positive 0和Negative 0。您可能需要调整plusZ的定义，以便Negative n代表-(n+1)而不是-n，这解决了这个问题。）