{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.ProvingBasics.Connectives.Disjunction where

析取#

在前面幾節裡，我們已經陳述並證明了不少結果。但我們仍然缺少表達其他一些相當基本的斷言所需的工具，例如下列這些：

每個自然數不是偶數就是奇數。
∀(n ∈ ℕ). (Even(n) ∨ Odd(n))
每個大於三的質數，都比六的某個倍數大一或小一。
∀(p ∈ ℙ). (p > 3 ⇒ (6 ∣ p-1 ∨ 6 ∣ p+1))
每個自然數之後都還有質數。
∀(n ∈ ℕ). ∃(p ∈ ℕ). (p > n ∧ p ∈ ℙ)

這個模組以及接下來幾個模組的目的，就是補上這個缺口，並引進析取（∨）、合取（∧）與存在量詞（∃）。依照命題即型別（propositions as types）的哲學，我們應該引進一個適當的見證型別，例如給定數字 n 是偶數或奇數的見證。上面第一個結果就可以用一個函數來形式化：這個函數讀入任意的數字 n 作為輸入，並輸出這種見證。

定義：不交聯集#

為了表達析取（∨），對給定的型別 A 與 B，我們引進它們的不交聯集 A ⊎ B：

infixr 1 _⊎_
data _⊎_ (A : Set) (B : Set) : Set where
  left  : A → A ⊎ B
  right : B → A ⊎ B
-- 在 Haskell 中，`A ⊎ B` 稱為 `Either A B`。

換句話說，A ⊎ B 的元素有兩種形式：對某個 x : A 的 left x，或對某個 y : B 的 right y。從計算的角度來看，left 是一個函數，輸入型別 A 的元素，輸出型別 A ⊎ B 的元素，right 也類似。從邏輯的角度來看，A 蘊涵 A or B。數字 n 是偶數或奇數的見證所成的型別，就是 Even n ⊎ Odd n。

習題：涉及析取的重言式#

open import Padova2025-zh-TW.ProvingBasics.Negation

習題 1∨-comm

∨-comm : {A B : Set} → A ⊎ B → B ⊎ A
∨-comm = {!!}

參考解答用到： left right

你的解答

參考解答

∨-comm : {A B : Set} → A ⊎ B → B ⊎ A
∨-comm (left  x) = right x
∨-comm (right y) = left  y

習題 2∨-assoc

∨-assoc : {A B C : Set} → (A ⊎ B) ⊎ C → A ⊎ (B ⊎ C)
∨-assoc = {!!}

參考解答用到： left right

你的解答

參考解答

∨-assoc : {A B C : Set} → (A ⊎ B) ⊎ C → A ⊎ (B ⊎ C)
∨-assoc (left  (left  x)) = left  x
∨-assoc (left  (right y)) = right (left  y)
∨-assoc (right z)         = right (right z)

習題 3∨-elim

∨-elim : {A B C : Set} → (A → C) → (B → C) → A ⊎ B → C
∨-elim = {!!}

參考解答用到： left right

你的解答

參考解答

∨-elim : {A B C : Set} → (A → C) → (B → C) → A ⊎ B → C
∨-elim f g (left  x) = f x
∨-elim f g (right y) = g y

習題 4∨-map

∨-map : {A A' B B' : Set} → (A → A') → (B → B') → A ⊎ B → A' ⊎ B'
∨-map = {!!}

參考解答用到： left right

你的解答

參考解答

∨-map : {A A' B B' : Set} → (A → A') → (B → B') → A ⊎ B → A' ⊎ B'
∨-map f g (left  x) = left  (f x)
∨-map f g (right y) = right (g y)

習題 5∨-codiag

∨-codiag : {A : Set} → A ⊎ A → A
∨-codiag = {!!}

參考解答用到： left right

你的解答

參考解答

∨-codiag : {A : Set} → A ⊎ A → A
∨-codiag (left  x) = x
∨-codiag (right y) = y

習題 6∨-not₁

∨-not₁ : {A : Set} → A ⊎ ⊥ → A
∨-not₁ = {!!}

參考解答用到： left right

你的解答

參考解答

∨-not₁ : {A : Set} → A ⊎ ⊥ → A
∨-not₁ (left  x)  = x
∨-not₁ (right ())

習題 7∨-not₂

∨-not₂ : {A B : Set} → A ⊎ B → ¬ B → A
∨-not₂ = {!!}

參考解答用到： left right ⊥-elim

你的解答

參考解答

∨-not₂ : {A B : Set} → A ⊎ B → ¬ B → A
∨-not₂ (left  x) f = x
∨-not₂ (right y) f = ⊥-elim (f y)
-- 或者，第二個子句可以寫成下面這樣。
-- ∨-not₂ (right y) f with f y
-- ... | ()

習題：偶數或奇數#

open import Padova2025-zh-TW.ProgrammingBasics.Naturals.Base
open import Padova2025-zh-TW.ProvingBasics.EvenOdd

習題 8even-or-odd

even-or-odd : (x : ℕ) → Even x ⊎ Odd x
even-or-odd = {!!}

參考解答用到： zero left base-even succ right base-odd step-even step-odd

你的解答

參考解答

even-or-odd : (x : ℕ) → Even x ⊎ Odd x
even-or-odd zero            = left base-even
even-or-odd (succ zero)     = right base-odd
even-or-odd (succ (succ x)) with even-or-odd x
... | left  p = left  (step-even p)
... | right p = right (step-odd p)

習題 9not-odd-implies-even

not-odd-implies-even : (x : ℕ) → ¬ Odd x → Even x
not-odd-implies-even = {!!}

參考解答用到： ∨-not₂ even-or-odd

你的解答

參考解答

not-odd-implies-even : (x : ℕ) → ¬ Odd x → Even x
not-odd-implies-even x p = ∨-not₂ (even-or-odd x) p

習題：後繼的前驅，再訪#

open import Padova2025-zh-TW.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025-zh-TW.ProvingBasics.Equality.Base

我們已經檢視過等式 succ(pred(a)) = a，它只對正的自然數成立。現在讓我們證明下面這個變體：

習題 10lemma-succ-pred''

lemma-succ-pred'' : (a : ℕ) → succ (pred a) ≡ a ⊎ a ≡ zero
lemma-succ-pred'' = {!!}

參考解答用到： right refl left

你的解答

參考解答

lemma-succ-pred'' : (a : ℕ) → succ (pred a) ≡ a ⊎ a ≡ zero
lemma-succ-pred'' zero     = right refl
lemma-succ-pred'' (succ a) = left  refl

習題：相等的可判定性#

open import Padova2025-zh-TW.ProvingBasics.Equality.General
open import Padova2025-zh-TW.ProvingBasics.Equality.NaturalNumbers
open import Padova2025-zh-TW.ProgrammingBasics.HigherOrder

每個自然數要嘛是零，要嘛不是。在古典數學中，這個斷言基於一般的邏輯理由是顯然的，因為它只是排中律（law of excluded middle）（A ∨ ¬A）的一個實例。但它也有直接的證明，一個我們可以在 Agda 中實作、而不必假設排中律（從而破壞 Agda 預設的建構性模式）的證明。

習題 11zero?

zero? : (x : ℕ) → (x ≡ zero) ⊎ ¬ (x ≡ zero)
zero? = {!!}

參考解答用到： left refl succ right

你的解答

參考解答

zero? : (x : ℕ) → (x ≡ zero) ⊎ ¬ (x ≡ zero)
zero? zero     = left  refl
zero? (succ x) = right λ ()

與依賴排中律的證明不同，這個證明可以被執行——試試看，在 Agda 的編輯過程中按 C-c C-v，然後輸入像 zero? four 這樣的東西。zero? 函數就會判斷 four 是不是零，並計算出對應的見證。

這個證明是歸納證明中少見的例子：歸納步驟並沒有用到歸納假設。

更一般地，我們有這個結果：任意兩個數字要嘛相等，要嘛不相等：

習題 12eq?

eq? : (a b : ℕ) → (a ≡ b) ⊎ ¬ (a ≡ b)
eq? = {!!}

參考解答用到： zero left refl succ right ∨-map cong _∘_ succ-injective

你的解答

參考解答

eq? : (a b : ℕ) → (a ≡ b) ⊎ ¬ (a ≡ b)
eq? zero     zero     = left refl
eq? zero     (succ b) = right λ ()
eq? (succ a) zero     = right λ ()
eq? (succ a) (succ b) = ∨-map (cong succ) (λ f → f ∘ succ-injective) (eq? a b)
-- 或者：
-- eq? (succ a) (succ b) with eq? a b
-- ... | left  a≡b = left (cong succ a≡b)
-- ... | right a≢b = right λ p → a≢b (succ-injective p)

習題：雙重否定單子中的神諭#

下面兩個重言式，對於從古典證明中萃取出建構性內容這個目的來說極為重要，初次見到時也相當費解。

習題 13¬¬-oracle

¬¬-oracle : {A : Set} → ¬ ¬ (A ⊎ ¬ A)
¬¬-oracle = {!!}

參考解答用到： right left

你的解答

參考解答

¬¬-oracle : {A : Set} → ¬ ¬ (A ⊎ ¬ A)
¬¬-oracle f = f (right (λ x → f (left x)))

習題 14¬¬-bind

¬¬-bind : {A B : Set} → ¬ ¬ A → (A → ¬ ¬ B) → ¬ ¬ B
¬¬-bind = {!!}

你的解答

參考解答

¬¬-bind : {A B : Set} → ¬ ¬ A → (A → ¬ ¬ B) → ¬ ¬ B
¬¬-bind m f = λ k → m (λ x → f x k)

習題：排中律與雙重否定消去#

習題 15LEM⇒DNE

LEM⇒DNE : ((A : Set) → A ⊎ ¬ A) → ((B : Set) → ¬ ¬ B → B)
LEM⇒DNE = {!!}

參考解答用到： left right ⊥-elim

你的解答

參考解答

LEM⇒DNE : ((A : Set) → A ⊎ ¬ A) → ((B : Set) → ¬ ¬ B → B)
LEM⇒DNE p B m with p B
... | left   a = a
... | right ¬a = ⊥-elim (m ¬a)

習題 16DNE⇒LEM

DNE⇒LEM : ((B : Set) → ¬ ¬ B → B) → ((A : Set) → A ⊎ ¬ A)
DNE⇒LEM = {!!}

參考解答用到： ¬¬-oracle

你的解答

參考解答

DNE⇒LEM : ((B : Set) → ¬ ¬ B → B) → ((A : Set) → A ⊎ ¬ A)
DNE⇒LEM p A = p (A ⊎ ¬ A) ¬¬-oracle