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

Results on Booleans#

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Operators
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General

Exercise: False is not true#

false≢true : false ≢ true
false≢true = {!!}

false≢true : false ≢ true
false≢true ()

Exercise: Double negation#

not² : (x : Bool) → not (not x) ≡ x
not² = {!!}

not² : (x : Bool) → not (not x) ≡ x
not² false = refl
not² true  = refl

Exercise: Commutativity of logical AND#

&&-comm : (x y : Bool) → (x && y) ≡ (y && x)
&&-comm = {!!}

&&-comm : (x y : Bool) → (x && y) ≡ (y && x)
&&-comm false false = refl
&&-comm false true  = refl
&&-comm true  false = refl
&&-comm true  true  = refl

Tautologies#

Before we have discussed a function is-tautology₁ : (Bool → Bool) → Bool with the purpose of returning true if and only if the first argument is constantly true. A straightforward implementation is the following:

is-tautology₁ : (Bool → Bool) → Bool
is-tautology₁ f = f false && f true

However, a more cryptic implementation is also possible.

is-tautology₁' : (Bool → Bool) → Bool
is-tautology₁' f = f (f false)

Let us verify that this alternatively works correctly. To this end, we first formalize what it means for a function to be constantly true:

ConstantlyTrue : (Bool → Bool) → Set
ConstantlyTrue f = (x : Bool) → f x ≡ true

In other words, an element of the type ConstantlyTrue f is a function which maps every input x : Bool to a witness that f x ≡ true. We are then ready to state and prove that is-tautology₁' f correctly returns true if f is constantly true:

part₁ : (f : Bool → Bool) → ConstantlyTrue f → is-tautology₁' f ≡ true
part₁ = {!!}

part₁ : (f : Bool → Bool) → ConstantlyTrue f → is-tautology₁' f ≡ true
part₁ f p = p (f false)

The converse direction is more involved. One way to structure the argument is to first verify an auxiliary lemma.

γ : (f : Bool → Bool) → (a : Bool) → f false ≡ a → f a ≡ true → ConstantlyTrue f
γ = {!!}

γ : (f : Bool → Bool) → (a : Bool) → f false ≡ a → f a ≡ true → ConstantlyTrue f
γ f false p q false = q
γ f false p q true  with trans (sym p) q
... | ()
γ f true  p q false = p
γ f true  p q true  = q

part₂ : (f : Bool → Bool) → is-tautology₁' f ≡ true → ConstantlyTrue f
part₂ f = {!!}

part₂ : (f : Bool → Bool) → is-tautology₁' f ≡ true → ConstantlyTrue f
part₂ f = γ f (f false) refl