坚持建造一个非常简单的功能

Question

我正在学习Coq.我陷入了一个非常愚蠢的问题(没有动力,真的很傻).我想构建一个从2,+ oo]到映射x到x-3的整数集的函数.这应该很简单...... 我知道,任何语言都很简单.但不是在Coq.首先,我写(我解释了很多细节,以便有人可以解释我在Coq的行为中不理解的东西)

Definition f : forall n : nat, n > 2 -> nat.

我得到了一个子目标

  ============================
   forall n : nat, n > 2 -> nat

这意味着Coq想要一个从n> 2的证明到整数集的映射.精细.所以我想告诉它n = 3 + p对于某个整数p,然后返回整数p.我写 :

intros n H.

我得到了上下文/子目标

  n : nat
  H : n > 2
  ============================
   nat

然后我想我已经证明n = 3 + p对于某个整数p by

cut(exists p, 3 + p = n).

我得到了上下文/子目标

  n : nat
  H : n > 2
  ============================
   (exists p : nat, 3 + p = n) -> nat

subgoal 2 (ID 6) is:
 exists p : nat, 3 + p = n

我在上下文中提出了假设

intro K.

我获得:

  n : nat
  H : n > 2
  K : exists p : nat, 3 + p = n
  ============================
   nat

subgoal 2 (ID 6) is:
 exists p : nat, 3 + p = n

我稍后会证明p的存在.现在我想通过精确的p完成证明.所以我需要先做一个

destruct K as (p,K).

我收到错误信息

错误:排序集的案例分析不允许用于归纳定义ex.

而且我被困住了.

Answer 1

你是绝对正确的!在任何合理的编程语言中编写这个函数应该很容易,幸运的是,Coq也不例外.

在您的情况下,通过简单地忽略您提供的证明参数来定义函数要容易得多:

Definition f (n : nat) : nat := n - 3.

然后你可能想知道"但等一下,自然数字在减法下不会关闭,所以这有什么意义呢？".好吧,在Coq中,对自然数的减法并不是真正的减法:它实际上是截断的.如果你试图从2减去,比如说3,你会得到0作为答案:

Goal 2 - 3 = 0. reflexivity. Qed.

这在实践中意味着你总是被允许"减去"两个自然数并得到一个自然数,但为了使这个减法有意义,第一个参数需要大于第二个参数.然后我们得到以下的lemmas(在标准库中可用):

le_plus_minus_r : forall n m, n <= m -> n + (m - n) = m

在大多数情况下,使用部分正确的函数(例如此减法定义)就足够了.但是,如果您愿意,可以限制域f以使其属性更加舒适.我冒昧地使用ssreflect库执行以下脚本,这使得编写此类函数更容易:

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.eqtype.

Definition f (n : {n | 2 < n}) : nat :=
  val n - 3.

Definition finv (m : nat) : {n | 2 < n} :=
  Sub (3 + m) erefl.

Lemma fK : cancel f finv.
Proof.
move=> [n Pn] /=; apply/val_inj=> /=.
by rewrite /f /= addnC subnK.
Qed.

Lemma finvK : cancel finv f.
Proof.
by move=> n; rewrite /finv /f /= addnC addnK.
Qed.

现在,f将一个n大于的自然数作为参数2({x : T | P x}形式是sig标准库中类型的语法糖,用于形成类似子集的类型).通过限制参数类型,我们可以编写一个反函数finv,它接受一个任意的nat并返回另一个大于的数2.然后,我们可以证明引理fK和finvK,其断言fK和finvK互为逆.

在定义上f,我们使用val,这是ssreflect的习惯用法,用于从类型的成员中提取元素{n | 2 < n}.在Sub上功能finv则正好相反,包装的自然数n与证明2 < n和返回的元素{n | 2 < n}.在这里,我们主要依赖于<在ssreflect中表示为布尔运算的事实,因此Coq可以使用其计算规则来检查erefl,证明true = true,也是有效的证据2 < 3 + m.

总而言之,你最终得到的神秘错误信息与Coq控制计算类型的规则有关,包括生活Type和命题类型Prop.Coq的规则禁止您使用命题证明来构建具有计算内容(例如自然数)的元素,除非在非常特殊的情况下.如果你愿意,你仍然可以通过使用{p | 3 + p = n}代替来完成你的定义exists p, 3 + p = n- 两者意味着相同的事情,除了前者生活在Type后者生活中Prop.