我该如何用coq荒谬的证明？

发布于 2025-01-28 00:55:28 字数 440 浏览 3 评论 0原文

我正在阅读软件基础系列中的逻辑基础，并且看到plus_id_example也就是说：

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.

Proof.
  intros n m.
  intros H.
  rewrite H.
  reflexivity.  Qed.

我可以理解解决方案，所以我尝试使用荒谬来解决它，我想做的是：

让我们考虑荒谬的考虑。，n+n＆lt;＆gt; m+m，所以我们有2n＆lt;＆gt; 2M，n＆lt;＆gt; m，这是一个矛盾，因为我们将n = m作为假设。

如何使用COQ策略写这件？

原文

I am reading Logical Foundations from Software Foundations series and i saw the plus_id_example that is:

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.

Proof.
  intros n m.
  intros H.
  rewrite H.
  reflexivity.  Qed.

I could understand the solution, so i tried to solve it using absurd, what i want to do is:

Lets consider by absurd, that n+n <> m+m, so we have 2n <> 2m, n <> m, which is a contradiction since we have n=m as our hypothesis.

How could i write this using Coq tactics?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

素年丶 2025-02-04 00:55:28

您可以在COQ中使用许多基于对比的引理之一：您可以通过使用搜索“ Contra”。在Coq中看到它们。

使用SSSREFLECT策略语言，可以根据以下方式获得基于此想法的证据（我敢肯定必须有更短的证明）：

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.
Proof.
  move=> n m.
  apply: contra_eq.
  have twice : forall p, p + p = p * 2.
    move=> p.
    by rewrite -iter_addn_0 /= addn0.
  by rewrite !twice eqn_mul2r.
Qed.

You can use one of the many contraposition-based lemmas in Coq: you can see them by using, for instance, Search "contra". in Coq.

Using the ssreflect tactic language, a proof based on this idea can be obtained as follows (I'm sure there must be shorter proofs):

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.
Proof.
  move=> n m.
  apply: contra_eq.
  have twice : forall p, p + p = p * 2.
    move=> p.
    by rewrite -iter_addn_0 /= addn0.
  by rewrite !twice eqn_mul2r.
Qed.

回复收藏 0 原文

~没有更多了~