Need hints about proving some intuitionistic logic statements

user_13518784 0
Viewed 68

I'm new to Agda, and I'm new to dependently typed programming and proof assistants in general. I decided to get myself started by constructing simple intuitionistic logic proofs, using the definitions I found in Programming Language Foundations in Agda, and I had some success. However, I got confused when I tried to write the following proof:

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

Proving this on paper would be fairly simple: expanding ¬ A, we have A → ⊥. So this statement becomes equivalent to (⊥ ∨ B) → B, which is obviously true.

I was able to successfully prove the latter part, that is, (⊥ ∨ B) → B:

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

Then, I was able to write:

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

Suggesting me that I need to produce ⊥ ∨ B by having ¬A and A ∨ B. I'd like to somehow replace A in A ∨ B with ¬A A, but I don't think there's a way of doing so. When trying to apply the ∨-identity case analysis pattern to ∨-identity-indirect, I get an error message that A should be empty, but that's not obvious to me - I assume I need to somehow make this obvious to Agda, by making use of ¬A.

Am I on the right track, or am I getting this wrong completely? How should I go about writing this ∨-identity-indirect function?

dependent-type agda functional-programming
1 Answers

Suggesting me that I need to produce ⊥ ∨ B by having ¬A and A ∨ B. I'd like to somehow replace A in A ∨ B with ¬A A, but I don't think there's a way of doing so. When trying to apply the ∨-identity case analysis pattern to ∨-identity-indirect, I get an error message that A should be empty, but that's not obvious to me - I assume I need to somehow make this obvious to Agda, by making use of ¬A.

You're probably trying to pattern match on a value of type ¬ A with (), which doesn't work, because ¬ A expands to A -> ⊥, i.e. it's a function that will only return you a ⊥ after you give it some A. Here is how you do that:

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

Having that, ∨-identity-indirect is straightforward:

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