theorem-proving - 如何通过精益中的归纳简化证明?
问题描述
我想通过精益中的归纳来简化证明。
我在 Lean 中定义了一个具有 3 个构造函数的归纳类型,并在此类型上定义了一个二元关系。我已经包含了这些公理,因为 Lean 不允许我将它们作为 rel 的构造函数。
inductive Fintype : Type
| a : Fintype
| b : Fintype
| c : Fintype
inductive rel : Fintype → Fintype → Prop
| r1 : rel Fintype.a Fintype.b
| r2 : ∀ p : Prop, (p → rel Fintype.a Fintype.c )
| r3 : ∀ p : Prop, (¬ p → rel Fintype.c Fintype.b)
axiom asymmetry_for_Fintype : ∀ x y : Fintype, rel x y → ¬ rel y x
axiom trivial1 : ¬ rel Fintype.c Fintype.a
axiom trivial2 : ¬ rel Fintype.b Fintype.c
axiom trivial3 : ∀ p : Prop, rel Fintype.a Fintype.c → p
axiom trivial4 : ∀ p : Prop, rel Fintype.c Fintype.b → ¬ p
一个目标是证明以下定理:
def nw_o_2 (X : Type) (binrel : X → X → Prop) (x y : X) : Prop := ¬ binrel y x
def pw_o_2 (X : Type) (binrel : X → X → Prop )(x y : X) : Prop := ∀ z : X, (binrel z x → binrel z y) ∧ (binrel y z → binrel x z)
theorem simple17: ∀ x y : Fintype, nw_o_2 Fintype rel x y → pw_o_2 Fintype rel x y :=
我已经通过对 x、y 和 z 的归纳证明了这一点;“z”来自上面 pw_o_2 的定义。但是证明很长(约 136 行)。还有另一种方法可以得到更短的证明吗?
解决方案
请注意,您的前两个公理实际上是定理,可以通过空模式匹配来证明。(假定归纳类型的构造函数是满射的。)这些行末尾的句点表示声明已经结束,不需要正文。在内部,Lean 递归地证明rel Fintype.c Fintype.a
并表明每个案例在结构上都是不可能的。
lemma trivial1 : ¬ rel Fintype.c Fintype.a.
lemma trivial2 : ¬ rel Fintype.b Fintype.c.
你的后两个公理是不一致的,这使得你的定理的证明容易但无趣。
theorem simple17: ∀ x y : Fintype, nw_o_2 Fintype rel x y → pw_o_2 Fintype rel x y :=
false.elim (trivial3 _ (rel.r2 _ trivial))
我不确定您是否rel
按照您的意图进行了定义。第二个和第三个构造函数分别等价于justrel Fintype.a Fintype.c
和rel Fintype.c Fintype.b
。
lemma rel_a_c : rel Fintype.a Fintype.c :=
rel.r2 true trivial
lemma rel_c_b : rel Fintype.c Fintype.b :=
rel.r3 false not_false
推荐阅读
- javascript - 如何将编辑器添加到特定选项卡的整个工作表保护?
- qt - QT QVulkanWindow 覆盖小部件
- android - 如何在命令行中为服务应用程序从 C++ 源代码构建 apk 包
- git - 默认情况下 git 跟踪分支
- python - 使用 Pyqt Print 支持但出现错误“对象不可调用”
- java - 为什么我不能从泛型参数访问属性?
- angular - 如何验证 Angular 2 表单
- android - 从 Firebase 检索数据时的应用加载程序文本
- neo4j - 具有 2 种节点类型的 neo4j 社区检测
- centos7 - 从 PHP 使用 OpenLDAP 进行身份验证