我试图解决常数不是通过COQ汇总
这是我迄今为止所做的工作。而我似乎被困在这里了。如果有人有任何想法，我将不胜感激。
Definition relation (X Y : Type) := X -> Y -> Prop.
Definition surjective {X Y : Type} (R: relation X Y) :=
forall y : Y, exists x : X, R x y.
Definition constant {X:Type} (c:X) := fun x y : X => y = c.
Definition injective {X Y : Type} (R: relation X Y) := forall x1 x2: X, forall y : Y, (R x1 y) -> (R x2 y) -> x1 = x2.
Theorem const_not_sur : forall c:nat, ~surjective (constant c).
Proof.
unfold not.
unfold surjective.
unfold constant.
intros.
destruct (H c) as [x H1].
destruct x.
据说这个问题可以使用n_Sn方法来解决。如果你觉得可以用这样的方法，会用在哪里呢？
This is the work I have so far. And I'm seemed to be stuck here. If anyone has any idea I would appreciate the help.
Definition relation (X Y : Type) := X -> Y -> Prop.
Definition surjective {X Y : Type} (R: relation X Y) :=
forall y : Y, exists x : X, R x y.
Definition constant {X:Type} (c:X) := fun x y : X => y = c.
Definition injective {X Y : Type} (R: relation X Y) := forall x1 x2: X, forall y : Y, (R x1 y) -> (R x2 y) -> x1 = x2.
Theorem const_not_sur : forall c:nat, ~surjective (constant c).
Proof.
unfold not.
unfold surjective.
unfold constant.
intros.
destruct (H c) as [x H1].
destruct x.
Supposedly this problem can be solved using n_Sn method. If you think such method can be used, where would it be?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
为了找到矛盾，您应该尝试解构
H (S c)而不是H c，给出假设S c = c。In order to find a contradiction, you should try to destruct
H (S c)instead ofH c, giving a hypothesisS c = c.正如 Pierre 所建议的，与
Sc的矛盾确实有效。但请注意，您不必使用n_Sn引理，因为归纳证明也可以。在 SSReflect 中，这将产生：请注意，
/eqP允许您移动到布尔域，从而可以直接使用归纳法（通过elim），这也是如何实现的n_Sn引理可以被证明。另外，在 SSReflect 中，Sc可以表示为c.+1。As suggested by Pierre, a contradiction with
S cindeed works. Note though that you don't have to use then_Snlemma, since a proof by induction would also work. In SSReflect, this would yield:Note that
/eqPallows you to move to the boolean domain, thus enabling a direct use of induction (viaelim), which is also how then_Snlemma could be proved. Also,S ccan be notatedc.+1, in SSReflect.