代码之家 › 专栏 › 技术社区 › Waiting for Dev...

COQ:处理不等式(<>)

coq-tactic theorem-proving proof coq

2

Waiting for Dev... · 技术社区 · 6 年前

我试图理解在coq中处理不平等的逻辑。

什么时候? <> 在目标中,做 intros contra. 将目标更改为 False 把目标转移到一个假设,但是 <> 切换到 = . 我想我明白这是怎么回事。如果我有目标 a <> b 然后 a = b 因为假设会产生矛盾。

但是,我不能在coq做相反的事情。如果我有目标 A=B 我不能 介绍相反。 为了拥有 假 作为目标和 和; 作为假设。 会这样吗? intros 合乎逻辑吗?仅仅因为不需要完成证明就不支持它吗?
什么时候? <> 在一个假设中 H 做 destruct H. 会消除假设(我做不到 destruct (H) eqn:H. )它会把任何目标转换成 H 但与 <> 切换为 = . 我不懂这里的逻辑 . 如果我有一个假设,这是一个不平等,我不明白没有它是如何等同于有平等作为目标。

一个不等式如何归纳为 destruct ?

如果我有一个矛盾的假设 0 <> 0 ,为了完成证明并说明这是一个矛盾,我需要 destruct G. (* now the goal is 0 = 0 *). reflexivity. 为什么不可以做一些 inversion G. ,就像你假设的那样 S n = 0 ?.

所以我有四个相关的问题 用粗体 .

1 回复 | 直到 6 年前

1

4

Arthur Azevedo De Amorim 6 年前

会这样吗? intros [在目标上] a = b ]合乎逻辑吗?

如果我理解你的问题,你想知道是否有可能有一个目标 A=B ,呼叫 intros contra ,并将其转换为目标 H : a <> b |- False . 这是合理的,但不能在coq的基本构造逻辑中推导出来。 a 和 b 任意类型:它断言 A=B 支持双重否定消除( ~ (~ a = b) -> a = b )coq不支持这一点,因为它意味着在不同的逻辑形式中工作。

一个不等式如何归纳为 destruct ?

正如耶普顿所说, a <> b 定义为 a = b -> False ,而falsity被归纳定义为没有构造函数的命题;因此,破坏某种类型的东西 False 简单地完成证明。此外,打电话 破坏 关于某种类型的东西 A -> B 大致上产生了 A ,将该证据输入到暗示中以获取 B ,然后打电话 破坏 关于那个证据 乙 . 在你的情况下,这意味着做你所描述的事情。

为什么不可以做一些 inversion G. ,就像你假设的那样 S n = 0 ?

我猜是的 inversion 不是那么宽大 破坏 ,不扩展到我前面解释过的含义。