关于存在变量的提取问题

image
image
image
为什么这个存在变量提不出来呢?数理逻辑上明明说得通啊!
(PS:那会不会是Coq类型系统的问题?)

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

另:建议使用Markdown代码块,而非截图。

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

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.

你的ZZ对应等公设,均被Znat的结构归纳定义蕴含,故定义plus可直接分类讨论z1z2的正负。