如何解决用 Isabelle 证明谓词逻辑
我试图证明以下引理:
lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"
我试图从消除 forall 量词开始,所以这是我尝试的:
lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"
apply(rule iffI)
apply ( erule_tac x="x" in allE)
apply (rule allE)
(*goal Now: get rid of conj on both sides and the quantifiers on right*)
apply (erule conjE) (*isn't conjE supposed to be used with elim/erule?*)
apply (rule allI)
apply (assumption)
apply ( rule conjI) (*at this point,the following starts to make no sense... *)
apply (rule conjE) (*should be erule?*)
apply ( rule conjI)
apply ( rule conjI)
...
最后我才开始根据上次申请的结果采取行动,但在我看来是错误的,可能是因为一开始有一些错误......有人可以向我解释我的错误以及如何完成这个证明正确吗?
提前致谢
解决方法
在这个早期阶段消除全称量词并不是一个好主意,因为你甚至没有任何可以在那个时候插入的值(你给出的 x
在那个时候不在范围内,这就是为什么它在 Isabelle/jEdit 中以橙色背景打印)。
执行 iffI
后,您有两个目标:
goal (2 subgoals):
1. ∀x. A x ∧ B x ⟹ (∀x. A x) ∧ (∀x. B x)
2. (∀x. A x) ∧ (∀x. B x) ⟹ ∀x. A x ∧ B x
现在让我们专注于第一个。您应该首先应用右侧的介绍规则,即 conjI
和 allI
。这让你有
goal (3 subgoals):
1. ⋀x. ∀x. A x ∧ B x ⟹ A x
2. ⋀x. ∀x. A x ∧ B x ⟹ B x
3. (∀x. A x) ∧ (∀x. B x) ⟹ ∀x. A x ∧ B x
现在您可以应用使用 allE
实例化的 x
,第一个目标变为 ⋀x. A x ∧ B x ⟹ A x
,然后您可以使用 erule conjE
和 assumption
求解。第二个目标类似。
对于最后一个目标,再次类似:先应用介绍规则,然后应用消除规则和assumption
,您就完成了。
当然,Isabelle 的所有标准证明器,例如 auto
、force
、blast
甚至是简单的证明器,例如 metis
、meson
、{ {1}} 可以轻松地自动解决这个问题,但这可能不是您在这里想要的。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。