1

精益定理证明的第 4.4 节显示以下内容：

(∃ x, p x) ↔ ¬ (∀ x, ¬ p x) := sorry

在这里，我将重点介绍从右到左的情况：

¬ (∀ x, ¬ p x) → (∃ x, p x)

我们知道我们将有一个类型的参数，¬ (∀ x, ¬ p x)所以让我们从它开始：

example : ¬ (∀ x, ¬ p x) → (∃ x, p x) := 
    (assume hnAxnpx : ¬ (∀ x, ¬ p x),
        _ 
    )

此时，如果我们尝试使用exists.introwith x：

example : ¬ (∀ x, ¬ p x) → (∃ x, p x) := 
    (assume hnAxnpx : ¬ (∀ x, ¬ p x),
        exists.intro x _)

我们会得到一个错误，因为x它是一个未知的标识符。

然而，作为这组练习的一部分，我们得到：

variables a : α

所以让我们尝试使用exists.intro它：

example : ¬ (∀ x, ¬ p x) → (∃ x, p x) := 
    (assume hnAxnpx : ¬ (∀ x, ¬ p x),
        exists.intro a _)

我们没有，p a所以让我们尝试通过以下方式使用经典逻辑em：

的第一个子句or.elim以简单的方式处理：

example : ¬ (∀ x, ¬ p x) → (∃ x, p x) := 
    (assume hnAxnpx : ¬ (∀ x, ¬ p x),
        or.elim (em (p a))
            (λ hpa : p a, exists.intro a hpa)
            (λ hnpa : ¬ p a, _))

由于我们有一个从(∀ x, ¬ p x)to false(ie hnAxnpx) 的函数，让我们尝试构建一个 type 的值(∀ x, ¬ p x)。然后我们可以调用hnAxnpx它并使用false.elim.

example : ¬ (∀ x, ¬ p x) → (∃ x, p x) := 
    (assume hnAxnpx : ¬ (∀ x, ¬ p x),    
        or.elim (em (p a))        
            (λ hpa : p a, exists.intro a hpa)    
            (λ hnpa : ¬ p a, false.elim (hnAxnpx (λ a, _))))

在这一点上，我们似乎如此接近！我们被告知我们需要一个¬p a下划线所在的位置。似乎这hnpa就是这样一个价值。所以让我们试试：

example : ¬ (∀ x, ¬ p x) → (∃ x, p x) :=     
    (assume hnAxnpx : ¬ (∀ x, ¬ p x),    
        or.elim (em (p a))        
            (λ hpa : p a, exists.intro a hpa)    
            (λ hnpa : ¬ p a, false.elim (hnAxnpx (λ a, hnpa))))

但是，我们得到以下错误：

type mismatch at application
  hnAxnpx (λ (a : α), hnpa)
term
  λ (a : α), hnpa
has type
  α → ¬p a
but is expected to have type
  ∀ (x : α), ¬p x

我应该继续使用上面说明的方法吗？还是应该考虑完全不同的方法？

更新

这是另一种方法：

example : ¬ (∀ x, ¬ p x) → (∃ x, p x) := 
    (assume hnAxnpx : ¬ (∀ x, ¬ p x),
        false.elim (hnAxnpx
            (λ x,
                (λ hpx : p x, _)))) -- Here we'll need a false.

但是，那时，我不清楚如何false在下划线处获得值。

更新

关于最后一种方法，leanprover zulip 小组的 Mario Carneiro提供了以下非常有用的提示：

不要false.elim在你做过的地方使用；这会丢弃我们试图证明的信息(∃ x, p x)并导致无法解决的状态

改用 by_contradiction ，这也给了你一个假设¬ (∃ x, p x)

根据这个建议，我们得到：

example : ¬ (∀ x, ¬ p x) → (∃ x, p x) := 
    (assume hnAxnpx : ¬ (∀ x, ¬ p x),
        by_contradiction
            (λ hnExpx : ¬ (∃ x, p x), 
                (hnAxnpx
                    (λ x, (λ hpx, 
                        hnExpx (exists.intro x hpx))))))

这似乎有效。

4

0 回答 0