如何从明显矛盾的假设中证明错误 [英] How to prove False from obviously contradictory assumptions

查看:58
本文介绍了如何从明显矛盾的假设中证明错误的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

假设我要证明以下定理:

Suppose I want to prove following Theorem:

Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.

这很简单,因为 m 不能假定为后继和零。但是我发现要证明它非常棘手,而且我不知道如何在没有辅助引理的情况下做到这一点:

This one is trivial since m cannot be both successor and zero, as assumed. However I found it quite tricky to prove it, and I don't know how to make it without an auxiliary lemma:

Lemma succ_neq_zero_lemma : forall n : nat, O = S n -> False.
Proof.
  intros.
  inversion H.
Qed.

Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
Proof.
  intros.
  symmetry in H.
  apply (succ_neq_zero_lemma n).
  transitivity m.
  assumption.
  assumption.
Qed.

我很确定有更好的方法来证明这一点。最好的方法是什么?

I am pretty sure there is a better way to prove this. What is the best way to do it?

推荐答案

您只需要在第一个方程式中替换 m

You just need to substitute for m in the first equation:

Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
Proof.
intros n m H1 H2; rewrite <- H2 in H1; inversion H1.
Qed.

这篇关于如何从明显矛盾的假设中证明错误的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!

查看全文
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆