如何通过精益中的归纳简化证明？

Question

我想通过精益中的归纳来简化证明。

我在 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 行）。有没有其他方法可以得到更短的证明？

Answer 1

请注意，您的前两个公理实际上是定理，可以通过空模式匹配来证明。 （假定归纳类型的构造函数是满射的。）这些行末尾的句点表示声明已经结束，不需要正文。在内部，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。第二个和第三个构造函数分别相当于rel 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