{-# 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 = {!!}

Exercise: Double negation

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

Exercise: Commutativity of logical AND

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

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₁ = {!!}

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
γ = {!!}

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