πŸ“₯ Download raw
module Padova2025.ProvingBasics.Connectives.Disjunction where

Disjunction

In the previous couple sections, we have already stated and proved quite a few results. But we are still lacking the means to express other, quite basic, assertions, such as the following:

  1. Every natural number is even or odd.
    βˆ€(nβ€„βˆˆβ€„β„•).Β (Even(n)β€…βˆ¨β€…Odd(n))

  2. Every prime number greater than three is one more or one less than a multiple of six.
    βˆ€(pβ€„βˆˆβ€„β„™).Β (p > 3 ⇒ (6β€…βˆ£β€…pβ€…βˆ’β€…1β€…βˆ¨β€…6β€…βˆ£β€…pβ€…+β€…1))

  3. Beyond every natural number, there is a prime number.
    βˆ€(nβ€„βˆˆβ€„β„•).Β βˆƒ(pβ€„βˆˆβ€„β„•).Β (p > nβ€…βˆ§β€…pβ€„βˆˆβ€„β„™)

The purpose of this module and the next ones is to fill this gap, and introduce disjunction (∨), conjunction (∧) and existential quantification (βˆƒ). Following the propositions as types philosophy, we should for instance introduce a suitable type of witnesses that a given number n is even or odd. The first result above would then be formalized by a function which reads an arbitrary number n as input and outputs such a kind of witness.

Definition: Disjoint union

For expressing disjunction (∨), for given types A and B we introduce their disjoint union A ⊎ B:

infixr 1 _⊎_
data _⊎_ (A : Set) (B : Set) : Set where
  left  : A β†’ A ⊎ B
  right : B β†’ A ⊎ B
-- In Haskell, `A ⊎ B` is known as `Either A B`.

In other words, the elements of A ⊎ B are of the form left x for some x : A, or right y for some y : B. The computational reading is that left is a function which inputs an element of type A and outputs an element of type A ⊎ B, and similarly with right. The logical reading is that A implies A or B. The type of witnesses that a number n is even or odd is then Even n ⊎ Odd n.

Exercise: Tautologies involving disjunction

open import Padova2025.ProvingBasics.Negation

∨-comm : {A B : Set} β†’ A ⊎ B β†’ B ⊎ A
∨-comm = {!!}

∨-assoc : {A B C : Set} β†’ (A ⊎ B) ⊎ C β†’ A ⊎ (B ⊎ C)
∨-assoc = {!!}

∨-elim : {A B C : Set} β†’ (A β†’ C) β†’ (B β†’ C) β†’ A ⊎ B β†’ C
∨-elim = {!!}

∨-map : {A A' B B' : Set} β†’ (A β†’ A') β†’ (B β†’ B') β†’ A ⊎ B β†’ A' ⊎ B'
∨-map = {!!}

∨-codiag : {A : Set} β†’ A ⊎ A β†’ A
∨-codiag = {!!}

∨-not₁ : {A : Set} β†’ A ⊎ βŠ₯ β†’ A
∨-not₁ = {!!}

∨-notβ‚‚ : {A B : Set} β†’ A ⊎ B β†’ Β¬ B β†’ A
∨-notβ‚‚ = {!!}

Exercise: Even or odd

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProvingBasics.EvenOdd

even-or-odd : (x : β„•) β†’ Even x ⊎ Odd x
even-or-odd = {!!}

not-odd-implies-even : (x : β„•) β†’ Β¬ Odd x β†’ Even x
not-odd-implies-even = {!!}

Exercise: Successor of predecessor, revisited

open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProvingBasics.Equality.Base

We have already examined the equation succ(pred(a)) = a, which only holds for positive natural numbers. Let us now prove the following variant:

lemma-succ-pred'' : (a : β„•) β†’ succ (pred a) ≑ a ⊎ a ≑ zero
lemma-succ-pred'' = {!!}

Exercise: Decidability of equality

open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Equality.NaturalNumbers
open import Padova2025.ProgrammingBasics.HigherOrder

Every natural number is either zero, or not. This assertion is trivial in classical mathematics for general logical reasons, as it is just an instance of the law of excluded middle (Aβ€…βˆ¨β€…Β¬A). But there is also a direct proof, a proof which we can implement in Agda without having to postulate the law of excluded middle and thereby destroying Agda’s by-default constructive mode.

zero? : (x : β„•) β†’ (x ≑ zero) ⊎ Β¬ (x ≑ zero)
zero? = {!!}

Unlike a proof relying on the law of excluded middle, this proof can be runβ€”try it, within the Agda editing session, press C-c C-v and then input something like zero? four. The zero? function will then determine whether four is zero, and compute a corresponding witness.

This proof is a rare instance of an induction proof where the induction step does not use the induction hypothesis.

More generally, we have the result that any two numbers are equal or not:

eq? : (a b : β„•) β†’ (a ≑ b) ⊎ Β¬ (a ≑ b)
eq? = {!!}

Exercise: An oracle in the double negation monad

The following two tautologies are of supreme importance for the purpose of extracting constructive content from classical proofs, and also quite cryptic on first encounter.

¬¬-oracle : {A : Set} β†’ Β¬ Β¬ (A ⊎ Β¬ A)
¬¬-oracle = {!!}

¬¬-bind : {A B : Set} β†’ Β¬ Β¬ A β†’ (A β†’ Β¬ Β¬ B) β†’ Β¬ Β¬ B
¬¬-bind = {!!}

Exercise: Law of excluded middle and double negation elimination

LEMβ‡’DNE : ((A : Set) β†’ A ⊎ Β¬ A) β†’ ((B : Set) β†’ Β¬ Β¬ B β†’ B)
LEM⇒DNE = {!!}

DNEβ‡’LEM : ((B : Set) β†’ Β¬ Β¬ B β†’ B) β†’ ((A : Set) β†’ A ⊎ Β¬ A)
DNE⇒LEM = {!!}