module logic where -- conjunction data _∧_ (A B : Set) : Set where ∧-intro : A → B → A ∧ B infixr 2 _∧_ -- case-split ∧-elim₀ : ∀ {A B : Set} → A ∧ B → A ∧-elim₀ = {!!} -- with pattern lambda ∧-elim₀′ : ∀ {A B : Set} → A ∧ B → A ∧-elim₀′ = {!!} ∧-elim₁ : ∀ {A B : Set} → A ∧ B → B ∧-elim₁ = {!!} record _∧′_ (A B : Set) : Set where constructor ∧′-intro field ∧′-elim₀ : A ∧′-elim₁ : B and-example : ∀ {A B : Set} → A ∧ B → B ∧ A and-example = {!!} -- exercises ex2-1 : ∀ {A B C : Set} → (A ∧ B → C) → (A → B → C) ex2-1 = {!!} ex2-2 : ∀ {A B C : Set} → (A → B → C) → (A ∧ B → C) ex2-2 = {!!} ex2-3 : ∀ {A B C : Set} → (A → B) → (A ∧ C) → (B ∧ C) ex2-3 = {!!} ex2-4 : ∀ {A B C D : Set} → (A → B) ∧ (C → D) → (A ∧ C) → (B ∧ D) ex2-4 = {!!} -- disjunction data _∨_ (A B : Set) : Set where ∨-intro₀ : A → A ∨ B ∨-intro₁ : B → A ∨ B infixr 1 _∨_ or-example1 : ∀ {A : Set} → A ∨ A → A or-example1 = {!!} -- with pattern lambda or-example1′ : ∀ {A : Set} → A ∨ A → A or-example1′ = {!!} or-example2 : ∀ {A B : Set} → A ∨ B → B ∨ A or-example2 = {!!} -- with local helper function or-example3 : ∀ {A B C D : Set} → (A → B ∨ C) → (B → D) → (C → D) → (A → D) or-example3 = {!!} -- with 'with' or-example3′ : ∀ {A B C D : Set} → (A → B ∨ C) → (B → D) → (C → D) → (A → D) or-example3′ = {!!} ex4-1 : ∀ {A B C : Set} → (A → B) → (A ∨ C) → (B ∨ C) ex4-1 = {!!} ex4-2 : ∀ {A B C : Set} → (A ∨ B) ∨ C → A ∨ (B ∨ C) ex4-2 = {!!} ex4-3 : ∀ {A B C : Set} → A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) ex4-3 = {!!} -- top, the unit type data ⊤ : Set where tt : ⊤ -- bottom, the empty type data ⊥ : Set where -- the "absurd" or "empty" pattern ⊥-elim : {A : Set} → ⊥ → A ⊥-elim = {!!} -- negation ¬ : Set → Set ¬ A = A → ⊥ bot-example : ∀ {A : Set} → ⊥ ∨ A → A bot-example = {!!} neg-example : ∀ {A B : Set} → A ∧ ¬ A → B neg-example = {!!} -- exercises ex6-1 : ∀ {A B : Set} → (A → B) → (¬ B → ¬ A) ex6-1 = {!!} ex6-2 : ∀ {A B : Set} → ¬ (A ∨ B) → (A → B) ex6-2 = {!!} ex6-3 : ∀ {A B C : Set} → (A → (B ∨ C)) → ¬ B → ¬ C → ¬ A ex6-3 = {!!} ex6-4 : ∀ {A B : Set} → ¬ (A ∨ B) → ¬ A ∧ ¬ B ex6-4 = {!!} -- universal quantification ∀-dist-∧ : ∀ (A : Set) (B C : A → Set) → (∀ (a : A) → B a ∧ C a) → (∀ (a : A) → B a) ∧ (∀ (a : A) → C a) ∀-dist-∧ A B C f = {!!} -- existential quantification data Σ (A : Set) (B : A → Set) : Set where _,_ : (x : A) → B x → Σ A B Σ-syntax = Σ infix 2 Σ-syntax syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B ∃ : ∀ {A : Set} (B : A → Set) → Set ∃ {A} B = Σ A B ∃-syntax = ∃ syntax ∃-syntax (λ x → B) = ∃[ x ] B -- exercises ∃¬∀¬ : ∀ {A : Set} {B : A → Set} → ∃[ x ] B x → ¬ ∀ x → ¬ (B x) ∃¬∀¬ = {!!} ¬∃∀¬ : ∀ {A : Set} {B : A → Set} → ¬ (∃[ x ] B x) → ∀ x → ¬ (B x) ¬∃∀¬ = {!!} ∃¬¬∀ : ∀ {A : Set} {B : A → Set} → ∃[ x ] ¬ (B x) → ¬ ∀ x → B x ∃¬¬∀ = {!!} ∃-distr-∨ : ∀ {A : Set} {B C : A → Set} → ∃[ x ] (B x ∨ C x) → (∃[ x ] B x) ∨ (∃[ x ] C x) ∃-distr-∨ = {!!} -- Excluded middle cannot be proved in intuitionistic logic, but -- adding it is consistent, and gives classical logic. Here are four -- other classical theorems with the same property. The task is to -- show that each of them is logically equivalent to all the others. -- You do not need to prove twenty implications, since implication is -- transitive. But there is a lot of choice as to how to proceed! -- Excluded Middle em = ∀ {A : Set} → A ∨ ¬ A -- Double Negation Elimination dne = ∀ {A : Set} → ¬ (¬ A) → A -- Peirce’s Law peirce = ∀ {A B : Set} → ((A → B) → A) → A -- Implication as disjunction iad = ∀ {A B : Set} → (A → B) → ¬ A ∨ B -- De Morgan: dem = ∀ {A B : Set} → ¬ (¬ A ∧ ¬ B) → A ∨ B