关于证明一些直觉逻辑语句的提示

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 ?

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

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

Answer 1

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

[您可能正在尝试将¬ A类型的值与()进行模式匹配，这是行不通的，因为¬ A扩展为A -> ⊥，即该函数只会返回一个[ C0]后再给它⊥。这是您的操作方式：

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