1

对于一个通过 LEAN 文档工作的新手来说，当更困难的问题显然已经解决时，看到一些简单的问题变成真正的瓶颈有时会非常令人沮丧。这是一个简单的自制练习，结果变成了几个小时的挫败感（当然，没有其他方法可以学习）：

theorem prByCont : ∀ P : Prop, ( P → false ) → ¬ P :=
    λ (P : Prop) (prf : P → false), prf
#check prByCont

example ( a b : ℕ ) (p: a = 2) (q: b=3) : ¬ (a ≥ b) :=
begin
    apply prByCont,
    assume h : a ≥ b,
    have order : 2 < 3 := dec_trivial,
    contradiction
end

问题似乎是order有类型2<3，但需要的是a<b，虽然在我看来应该很清楚a=2and b=3，但 LEAN 不这么认为。请帮我看看我在这里缺少什么！

4

0 回答 0