Let's play Agda 
{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.ProvingBasics.Connectives.Conjunction where

合取#

open import Agda.Primitive
open import Padova2025-zh-TW.ProvingBasics.Connectives.Existential

合取 A and B 的見證，應該由一個型別 A 的見證與一個型別 B 的見證組成，也就是說，合取的見證就是一對見證。 這只是前面介紹過的依值序對構造的特例。因此，對任意型別 A 與 B，我們引進笛卡兒積型別 A × B：

infixr 2 _×_
_×_ : {ℓ ℓ' : Level} → Set ℓ → Set ℓ' → Set (ℓ ⊔ ℓ')
A × B = Σ A (λ _ → B)

特別是，fst 與 snd 這兩個函數，對這些非依值的積也同樣適用。讓我們把這些函數匯出，供匯入本模組的使用者使用。

open Padova2025-zh-TW.ProvingBasics.Connectives.Existential using (fst; snd; _,_) public

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

open import Padova2025-zh-TW.ProvingBasics.Negation
習題 1∧-comm
∧-comm : {A B : Set} → A × B → B × A
∧-comm = {!!}
參考解答用到： _,_
參考解答
∧-comm : {A B : Set} → A × B → B × A
∧-comm (x , y) = (y , x)
習題 2∧-assoc
∧-assoc : {A B C : Set} → (A × B) × C → A × (B × C)
∧-assoc = {!!}
參考解答用到： _,_
參考解答
∧-assoc : {A B C : Set} → (A × B) × C → A × (B × C)
∧-assoc ((x , y) , z) = (x , (y , z))
習題 3curry
curry : {A B C : Set} → (A × B → C) → (A → (B → C))
curry = {!!}
參考解答用到： _,_
參考解答
curry : {A B C : Set} → (A × B → C) → (A → (B → C))
curry f x y = f (x , y)
-- 或者：curry f = λx → λy → f (x , y)
習題 4uncurry
uncurry : {A B C : Set} → (A → (B → C)) → (A × B → C)
uncurry = {!!}
參考解答用到： _,_
參考解答
uncurry : {A B C : Set} → (A → (B → C)) → (A × B → C)
uncurry f (x , y) = f x y
習題 5∧-map
∧-map : {A A' B B' : Set} → (A → A') → (B → B') → A × B → A' × B'
∧-map = {!!}
參考解答用到： _,_
參考解答
∧-map : {A A' B B' : Set} → (A → A') → (B → B') → A × B → A' × B'
∧-map f g (x , y) = (f x , g y)
習題 6∧-diag
∧-diag : {A : Set} → A → A × A
∧-diag = {!!}
參考解答用到： _,_
參考解答
∧-diag : {A : Set} → A → A × A
∧-diag x = (x , x)
習題 7∧-not
∧-not : {A : Set} → A × ⊥ → ⊥
∧-not = {!!}
參考解答用到： snd
參考解答
∧-not : {A : Set} → A × ⊥ → ⊥
∧-not = snd
習題 8frobenius
frobenius : {A B : Set} {P : A → Set} → ∃[ x ] (P x × B) → (∃[ x ] P x) × B
frobenius = {!!}
參考解答用到： _,_
參考解答
frobenius : {A B : Set} {P : A → Set} → ∃[ x ] (P x × B) → (∃[ x ] P x) × B
frobenius (x , (p , b)) = (x , p) , b

習題：De Morgan 定律#

open import Padova2025-zh-TW.ProvingBasics.Connectives.Disjunction

驗證四條 De Morgan 定律中的下列三條。

習題 9de-morgan₁
de-morgan₁ : {A B : Set} → ¬ A × ¬ B → ¬ (A ⊎ B)
de-morgan₁ = {!!}
參考解答用到： _,_ left right
參考解答
de-morgan₁ : {A B : Set} → ¬ A × ¬ B → ¬ (A ⊎ B)
de-morgan₁ (f , g) (left  x) = f x
de-morgan₁ (f , g) (right y) = g y
習題 10de-morgan₂
de-morgan₂ : {A B : Set} → ¬ (A ⊎ B) → ¬ A × ¬ B
de-morgan₂ = {!!}
參考解答用到： left _,_ right
參考解答
de-morgan₂ : {A B : Set} → ¬ (A ⊎ B) → ¬ A × ¬ B
de-morgan₂ f = (λ x → f (left x)), (λ y → f (right y))
習題 11de-morgan₃
de-morgan₃ : {A B : Set} → ¬ A ⊎ ¬ B → ¬ (A × B)
de-morgan₃ = {!!}
參考解答用到： left right
參考解答
de-morgan₃ : {A B : Set} → ¬ A ⊎ ¬ B → ¬ (A × B)
de-morgan₃ (left  f) = λ (x , y) → f x
de-morgan₃ (right g) = λ (x , y) → g y

第四條 ¬ (A × B) → ¬ A ⊎ ¬ B 會破壞建構性數學區分否定性斷言與肯定性斷言的細緻能力。由於 Agda 預設是建構性的系統， 第四條定律在 Agda 中無法證明。

習題：零和#

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

證明如果兩個自然數的和為零，則兩個加數都是零。

習題 12sum-zero
sum-zero : (a b : ℕ) → a + b ≡ zero → a ≡ zero × b ≡ zero
sum-zero = {!!}
參考解答用到： refl _,_ succ
參考解答
sum-zero : (a b : ℕ) → a + b ≡ zero → a ≡ zero × b ≡ zero
sum-zero zero     b p = refl , p
sum-zero (succ a) b ()