{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProvingBasics.Negation where

Negation#

In mathematical logic, the negation ¬ P of a proposition P is defined as “assuming P implies a contradiction”, that is as the implication (P ⇒ ↯).

To adopt this definition in Agda, we introduce a type ⊥ which does not have any inhabitants:

data ⊥ : Set where   -- enter `⊥` by `\bot`
-- no constructors, so the type `⊥` is manifestly empty

Hence proving a negation ¬ P in Agda means to construct a function which maps witnesses of P to witnesses of ↯, i.e. to values of type ⊥.

We can also introduce the negation symbol in Agda:

infix 3 ¬_
¬_ : Set → Set  -- enter `¬` as `\neg`
¬ P = (P → ⊥)

Exercise: One is not even#

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

An immediate consequence from the definition of Even, but nevertheless quite instructive at this point, is the result that the number one is not even.

Exercise 1one-not-even

one-not-even : Even one → ⊥
one-not-even = {!!}

Your solution

Reference solution

one-not-even : Even one → ⊥
one-not-even ()

As usual, introduce a variable on the left of the = sign: one-not-even p = {!!}
Then, also as usual, press C-c C-c to ask Agda to do a case split on p.
Agda will then notice that there are no possible cases and indicate this observation with the empty pattern ().

Exercise: No simultaneously even and odd numbers#

Exercise 2even-and-odd

even-and-odd : {a : ℕ} → Even a → Odd a → ⊥
even-and-odd = {!!}

The reference solution uses: step-even step-odd

Your solution

Reference solution

even-and-odd : {a : ℕ} → Even a → Odd a → ⊥
even-and-odd (step-even p) (step-odd q) = even-and-odd p q

Exercise: An inductive type without a base case#

Let us consider the following variant of the definition of the natural numbers:

data Weird : Set where
  succ : Weird → Weird

How many values of type Weird are there?

Given an inhabitant x of type Weird, its sole constructor succ could be used to obtain the further inhabitant succ x. Applying succ again would result in yet another inhabitant, and so on. But we do not have any inhabitants to start with; the constructor succ is of no use; the type Weird is empty.

What about the infinite expression succ (succ (succ (...)))? Does this expression not denote a value of type Weird?

No – non-terminating expressions like these are not allowed for datatypes. Try it:

loop : Weird
loop = succ loop

Specific kinds of non-terminating expressions are possible for so-called co-datatypes, but we will not discuss those here.

We can formalize this observation in Agda as follows, expressing the following implication: If there would be an inhabitant of Weird, then a contradiction would ensue.

Exercise 3Weird-is-empty

Weird-is-empty : Weird → ⊥
Weird-is-empty = {!!}

The reference solution uses: succ

Your solution

Reference solution

Weird-is-empty : Weird → ⊥
Weird-is-empty (succ x) = Weird-is-empty x

Exercise: Ex falso quodlibet#

In (both classical and intutionistic, but not minimal) logic, from a contradiction any statement follows. In Agda, we have the parallel fact we have a function ⊥ → A for any type A:

Exercise 4⊥-elim

⊥-elim : {A : Set} → ⊥ → A
⊥-elim = {!!}

Your solution

Reference solution

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

Exercise: Law of non-contradiction#

From A and ¬ A we can deduce a contradiction:

Exercise 5contradiction

contradiction : {A : Set} → A → ¬ A → ⊥
contradiction = {!!}

Your solution

Reference solution

contradiction : {A : Set} → A → ¬ A → ⊥
contradiction p f = f p

Exercise: Double negation#

In classical mathematics, the double negation ¬ ¬ A of a statement is equivalent to A again. Constructive mathematics, which is the default mode of Agda, allows us to see finer distinctions; in general, ¬ ¬ A is not equivalent to A. (We will explore the differences between these two statements in detail later.)

While we do not have, in Agda, that ¬ ¬ A ⇒ A (unless we add this principle as a postulate), we have the converse implication.

Exercise 6dni

dni : {A : Set} → A → ¬ ¬ A
dni = {!!}

Your solution

Reference solution

dni : {A : Set} → A → ¬ ¬ A
dni x = λ k → k x

As a corollary, triple negation implies (and is hence equivalent to) single negation.

Exercise 7triple-to-one

triple-to-one : {A : Set} → ¬ ¬ ¬ A → ¬ A
triple-to-one = {!!}

The reference solution uses: dni

Your solution

Reference solution

triple-to-one : {A : Set} → ¬ ¬ ¬ A → ¬ A
triple-to-one p = λ x → p (dni x)

Exercise: Contraposition#

Prove that if A implies B, then also ¬ B implies ¬ A:

Exercise 8contraposition

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

Your solution

Reference solution

contraposition : {A B : Set} → (A → B) → (¬ B → ¬ A)
contraposition f g p = g (f p)

The converse direction cannot be proven constructively and hence is not available in the default mode of Agda.