关于存在变量的提取问题

[zh] Coq 中文
1

image
image
image
为什么这个存在变量提不出来呢？数理逻辑上明明说得通啊！
（PS：那会不会是Coq类型系统的问题？）

2

虽然没看懂你的数理逻辑意图，但就Coq而言，想在当前定义下得到类型为Z的表达式，有X和X0两个现成的实例，也可把负或正作用在自然数上来构造。

另：建议使用Markdown代码块，而非截图。

3

再另：用自然数定义整数，不考虑负零与正零重复的话，应使用结构归纳定义：

Variant Znat :=
  Znatpos : nat -> Znat
| Znatneg : nat -> Znat.

而非Axiom。

至于整数加法，因为是运算而非证明，建议用Definition而非Proof来定义：

Definition plus (z1 z2: Znat) : Znat :=
  match z1, z2 with
  | Znatpos n1, Znatpos n2 => Znatpos (n1 + n2)
  | Znatneg n1, Znatneg n2 => Znatneg (n1 + n2)
  | Znatpos n1, Znatneg n2 => if (n1 <? n2) then Znatneg (n2 - n1) else Znatpos (n1 - n2)
  | Znatneg n1, Znatpos n2 => if (n1 <? n2) then Znatpos (n2 - n1) else Znatneg (n1 - n2)
  end.

你的Z、正、负、Z对应等公设，均被Znat的结构归纳定义蕴含，故定义plus可直接分类讨论z1和z2的正负。