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.
eq?-correct₁ : (x y : ℕ) → eq? x y ≡ true → x ≡ y
eq?-correct₁ = {!!}
eq?-correct₂ : (x y : ℕ) → x ≡ y → eq? x y ≡ true
eq?-correct₂ = {!!}
Exercise: Correctness of the decision procedure for inequality
open import Padova2025.ProvingBasics.Termination.Ordering
≤?-correct₁ : (x y : ℕ) → ≤? x y ≡ true → x ≤ y
≤?-correct₁ = {!!}
≤?-correct₂ : (x y : ℕ) → x ≤ y → ≤? x y ≡ true
≤?-correct₂ = {!!}
Exercise: Correctness of the decision procedure for evenness
open import Padova2025.ProvingBasics.EvenOdd
even?-correct₁ : (x : ℕ) → even? x ≡ true → Even x
even?-correct₁ = {!!}
even?-correct₂ : {x : ℕ} → Even x → even? x ≡ true
even?-correct₂ = {!!}
Exercise: Correctness of the subtraction function
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
∸-correct : (x y : ℕ) → x ≥ y → y + (x ∸ y) ≡ x
∸-correct = {!!}