{-# OPTIONS --cubical-compatible #-}
module Padova2025.VerifiedAlgorithms.PostHocVerification where

Post-hoc verification#

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.DecisionProcedures
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Equality.NaturalNumbers

Beware of bugs in the above code; I have only proved it correct, not tried it.
―Donald Knuth

In post-hoc verification, we leverage the expressivity and strength of Agda to verify the correctness of (separatedly) implemented algorithms.

For instance, the purpose of the eq? : ℕ → ℕ → Bool function is to decide whether its two inputs agree. But does our implementation really meet this challenge? In ordinary programming languages without dependent types, we might test the function with particular examples (perhaps randomly generated), or have a close look at the implementation, perhaps ask colleagues to share a review, … Thanks to the expressivity of Agda’s type system, in Agda we can instead formally prove the correctness.

Expand.

Exercise 1eq?-correct₁

eq?-correct₁ : (x y : ℕ) → eq? x y ≡ true → x ≡ y
eq?-correct₁ = {!!}

The reference solution uses: zero refl succ cong

Your solution

Reference solution

eq?-correct₁ : (x y : ℕ) → eq? x y ≡ true → x ≡ y
eq?-correct₁ zero     zero     p = refl
eq?-correct₁ (succ x) (succ y) p = cong succ (eq?-correct₁ x y p)

Exercise 2eq?-correct₂

eq?-correct₂ : (x y : ℕ) → x ≡ y → eq? x y ≡ true
eq?-correct₂ = {!!}

The reference solution uses: zero refl succ succ-injective

Your solution

Reference solution

eq?-correct₂ : (x y : ℕ) → x ≡ y → eq? x y ≡ true
eq?-correct₂ zero zero p = refl
eq?-correct₂ (succ x) (succ y) p = eq?-correct₂ x y (succ-injective p)

Exercise: Correctness of the decision procedure for inequality#

open import Padova2025.ProvingBasics.Termination.Ordering

Exercise 3≤?-correct₁

≤?-correct₁ : (x y : ℕ) → ≤? x y ≡ true → x ≤ y
≤?-correct₁ = {!!}

The reference solution uses: zero z≤n succ s≤s

Your solution

Reference solution

≤?-correct₁ : (x y : ℕ) → ≤? x y ≡ true → x ≤ y
≤?-correct₁ zero     y        p = z≤n
≤?-correct₁ (succ x) (succ y) p = s≤s (≤?-correct₁ x y p)

Exercise 4≤?-correct₂

≤?-correct₂ : (x y : ℕ) → x ≤ y → ≤? x y ≡ true
≤?-correct₂ = {!!}

The reference solution uses: z≤n refl succ s≤s

Your solution

Reference solution

≤?-correct₂ : (x y : ℕ) → x ≤ y → ≤? x y ≡ true
≤?-correct₂ x        y        z≤n     = refl
≤?-correct₂ (succ x) (succ y) (s≤s p) = ≤?-correct₂ x y p

Exercise: Correctness of the decision procedure for evenness#

open import Padova2025.ProvingBasics.EvenOdd

Exercise 5even?-correct₁

even?-correct₁ : (x : ℕ) → even? x ≡ true → Even x
even?-correct₁ = {!!}

The reference solution uses: zero base-even succ step-even

Your solution

Reference solution

even?-correct₁ : (x : ℕ) → even? x ≡ true → Even x
even?-correct₁ zero            p = base-even
even?-correct₁ (succ (succ x)) p = step-even (even?-correct₁ x p)

Exercise 6even?-correct₂

even?-correct₂ : {x : ℕ} → Even x → even? x ≡ true
even?-correct₂ = {!!}

The reference solution uses: base-even refl step-even

Your solution

Reference solution

even?-correct₂ : {x : ℕ} → Even x → even? x ≡ true
even?-correct₂ base-even     = refl
even?-correct₂ (step-even p) = even?-correct₂ p

Exercise: Correctness of the subtraction function#

open import Padova2025.ProgrammingBasics.Naturals.Arithmetic

Exercise 7∸-correct

∸-correct : (x y : ℕ) → x ≥ y → y + (x ∸ y) ≡ x
∸-correct = {!!}

The reference solution uses: zero refl succ s≤s cong

Your solution

Reference solution

∸-correct : (x y : ℕ) → x ≥ y → y + (x ∸ y) ≡ x
∸-correct x        zero     x≥y       = refl
∸-correct (succ x) (succ y) (s≤s x≥y) = cong succ (∸-correct x y x≥y)