证明常数不是满射的 Coq

Question

有一个函数定义常量 {X:Type} (c:X) := fun xy : X => y = c。 证明：定理 const_not_sur ：forall c:nat, ~surjective (constant c)。 我做到了：

unfold not.
unfold surjective.
unfold constant.
intros.
destruct (H 1) as [x H1].
destruct x.
induction c.
symmetry in H1.
discriminate.

我还需要使用 n_Sn 定理来证明上面的问题。然而，我花了一个小时却无法让它发挥作用。 有什么建议吗？

Answer 1

我认为问题出在你的destruct (H 1)上。如果您的关系constant c 是满射的，那么您可能会通过考虑S c 而不是1 来发现矛盾。

Answer 2

与您的常数兼容的满射性定义可能是

Definition surj {X:Type} (R: X -> X -> Prop) := forall y, exists x, R x y.

对的？ （或更通用的变量，带有类型变量 X 和 Y）。

您还可以考虑以下一对定义：

Definition const X {Y:Type} (k: Y) := fun (x:X)  =>  k.
Definition surj {X Y : Type} (f : X -> Y) := forall y, exists x, f x = y.

Goal forall n: nat,  ~ surj(const nat n).

一般来说，在您的代码片段中包含足够的必要定义（或库的使用）可能会很有用，以便我们能够重播您谈论的脚本。

Answer 3

正如 HTNW 在您之前的一篇文章中已经提到的，问题可能来自于您对 constant 函数的定义。

如果我尝试使用 mathcomp 证明你的定理，我会得到以下观点（我不知道你使用的是哪个版本的 Surjective，所以我复制了一个）：

From mathcomp Require Import all_ssreflect.

Lemma equal_f: forall {A B : Type} {f g : A -> B}, f = g -> forall x, f x = g x.
Proof. by move=> A B f g -> y. Qed.

Definition Surjective {A B} (f : A->B) := forall y, exists x, f x = y.

Definition constant {X:Type} (c:X) := fun x y : X => y = c.

Theorem const_not_sur : forall c:nat, ~Surjective (constant c). 
Proof.
move=> c /(_ (fun y => true)) [x] /equal_f /(_ c.+1). 
rewrite /constant.
elim: c => [|c].

在那里我必须证明两个命题相等（它们漂亮地打印为 1 = 0 和 true），这是一个复杂的问题（注意：相等，而不是等价）。

但是，如果您将自己限制为常量定义中具有相等性的类型，并返回布尔值而不是命题，那么您可以完成类似的证明：

Definition constant' {X:eqType} (c:X) := fun x y : X => y == c.

Theorem const_not_sur' : forall c:nat, ~Surjective (constant' c). 
Proof.
move=> c /(_ (fun y => true)) [x] /equal_f /(_ c.+1). 
elim: c => [//|c].
by rewrite /constant' eqSS.
Qed.

我仍然相信问题可能是在于constant的初始定义。