Let's play Agda 
{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.VerifiedAlgorithms.PostHocVerification where

事後驗證#

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

Beware of bugs in the above code; I have only proved it correct, not tried it.（小心上面程式碼中的錯誤；我只證明了它是正確的，並沒有試過它。）
―Donald Knuth

在事後驗證中，我們運用 Agda 的表達力與強度，來驗證（另外實作的）演算法的正確性。

例如，函數 eq? : ℕ → ℕ → Bool 的目的是判斷它的兩個輸入是否一致。但我們的實作真的達成這個目標了嗎？在沒有依值型別的一般程式語言中，我們可能會用特定的例子 （也許是隨機產生的）來測試這個函數，或是仔細檢視實作， 也許請同事一起審查，……由於 Agda 型別系統的表達力，在 Agda 中我們可以改為形式化地證明其正確性。

待補：擴充。

習題 1eq?-correct₁
eq?-correct₁ : (x y : ℕ) → eq? x y ≡ true → x ≡ y
eq?-correct₁ = {!!}
參考解答用到： zero refl succ cong
參考解答
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)
習題 2eq?-correct₂
eq?-correct₂ : (x y : ℕ) → x ≡ y → eq? x y ≡ true
eq?-correct₂ = {!!}
參考解答用到： zero refl succ succ-injective
參考解答
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)

習題：不等的決策程序之正確性#

open import Padova2025-zh-TW.ProvingBasics.Termination.Ordering
習題 3≤?-correct₁
≤?-correct₁ : (x y : ℕ) → ≤? x y ≡ true → x ≤ y
≤?-correct₁ = {!!}
參考解答用到： zero z≤n succ s≤s
參考解答
≤?-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)
習題 4≤?-correct₂
≤?-correct₂ : (x y : ℕ) → x ≤ y → ≤? x y ≡ true
≤?-correct₂ = {!!}
參考解答用到： z≤n refl succ s≤s
參考解答
≤?-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

習題：判定偶數的決策程序之正確性#

open import Padova2025-zh-TW.ProvingBasics.EvenOdd
習題 5even?-correct₁
even?-correct₁ : (x : ℕ) → even? x ≡ true → Even x
even?-correct₁ = {!!}
參考解答用到： zero base-even succ step-even
參考解答
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)
習題 6even?-correct₂
even?-correct₂ : {x : ℕ} → Even x → even? x ≡ true
even?-correct₂ = {!!}
參考解答用到： base-even refl step-even
參考解答
even?-correct₂ : {x : ℕ} → Even x → even? x ≡ true
even?-correct₂ base-even     = refl
even?-correct₂ (step-even p) = even?-correct₂ p

習題：減法函數之正確性#

open import Padova2025-zh-TW.ProgrammingBasics.Naturals.Arithmetic
習題 7∸-correct
∸-correct : (x y : ℕ) → x ≥ y → y + (x ∸ y) ≡ x
∸-correct = {!!}
參考解答用到： zero refl succ s≤s cong
參考解答
∸-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)