需要有关证明一些直觉逻辑陈述的提示

Question

我是 Agda 的新手，我对依赖类型编程和一般证明助手也不熟悉。我决定从构建简单的直觉逻辑证明开始，使用我在Programming Language Foundations in Agda 中找到的定义，我取得了一些成功。但是，当我尝试写以下证明时，我感到困惑：

∨-identity-indirect : {A B : Set} → (¬ A) ∧ (A ∨ B) → B

在纸上证明这一点相当简单：扩展¬ A，我们有A → ⊥。所以这个语句就变成了等价于(⊥ ∨ B) → B，这显然是对的。

我能够成功证明后半部分，即(⊥ ∨ B) → B：

∨-identity : {A : Set} → (⊥ ∨ A) → A
∨-identity (∨-left ())
∨-identity (∨-right A) = A

然后，我可以写了：

∨-identity-indirect ⟨ ¬A , A∨B ⟩ = ∨-identity ?

建议我需要通过¬A 和A ∨ B 生成⊥ ∨ B。我想以某种方式将A ∨ B 中的A 替换为¬A A，但我认为没有办法这样做。 当尝试将∨-identity 案例分析模式应用于∨-identity-indirect 时，我收到一条错误消息，A 应该为空，但这对我来说并不明显 - 我认为我需要以某种方式使其明显通过使用¬A 发送给Agda。

我是在正确的轨道上，还是我完全错了？我应该如何编写这个∨-identity-indirect 函数？

Answer 1

建议我需要通过¬A 和A ∨ B 生成⊥ ∨ B。我想以某种方式将A ∨ B 中的A 替换为¬A A，但我认为没有办法这样做。 当尝试将∨-identity 案例分析模式应用于∨-identity-indirect 时，我收到一条错误消息，A 应该为空，但这对我来说并不明显 - 我认为我需要以某种方式使其明显通过使用 ¬A 发送给 Agda。

您可能正在尝试使用() 对¬ A 类型的值进行模式匹配，但这是行不通的，因为¬ A 扩展为A -> ⊥，即它是一个只会返回您的函数⊥ 在你给它一些 A 之后。这样做的方法如下：

replace-A : {A B : Set} → (¬ A) → (A ∨ B) → ⊥ ∨ B
replace-A f (v-left  x) = v-left (f x)
replace-A _ (v-right y) = v-right y

有了这个，∨-identity-indirect 就很简单了：

∨-identity-indirect : {A B : Set} → (¬ A) ∧ (A ∨ B) → B
∨-identity-indirect ⟨ ¬A , A∨B ⟩ = ∨-identity (replace-A ¬A A∨B)