module PLFA.Decidable where import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) open Eq.≡-Reasoning open import Data.Nat using (ℕ; zero; suc) open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Relation.Nullary using (¬_) open import Relation.Nullary.Negation using () renaming (contradiction to ¬¬-intro) open import Data.Unit using (⊤; tt) open import Data.Empty using (⊥; ⊥-elim) open import PLFA.Relations using (_≤_; z≤n; s≤s) -- we skipped this: infix 4 _<_ data _<_ : ℕ → ℕ → Set where z booleans -- mapping a decidable to bool: -- forget about the evidence, just extract the single bit ⌊_⌋ : ∀ {A : Set} → Dec A → Bool ⌊ yes x ⌋ = true ⌊ no x ⌋ = false -- may be used to recover _≤ᵇ_ _≤ᵇ′_ : ∀ (m n : ℕ) → Bool m ≤ᵇ′ n = ⌊ m ≤? n ⌋ -- may also obtain the witness from a decidable toWitness : ∀ {A : Set}{d : Dec A} → T ⌊ d ⌋ → A toWitness {d = yes a} td = a -- optional: -- toWitness {d = no ¬a} () fromWitness : {A : Set} {d : Dec A} → A → T ⌊ d ⌋ fromWitness {d = yes x} a = tt fromWitness {d = no ¬a} a = ¬a a -- subsequent excursion from Lambda Calculus chapter -- * -- proof by reflection {- remember the definition of truncated subtraction, _∸_ "monus" ... -} minus : (m n : ℕ) → (n≤m : n ≤ m) → ℕ minus m zero n≤m = m minus zero (suc n) () minus (suc m) (suc n) (s≤s n≤m) = minus m n n≤m _ : minus 4 2 (s≤s (s≤s z≤n)) ≡ 2 _ = refl -- bothersome! need to constrcut the proof even though it's obvious! -- why can't Agda calculate the proof for us? -- proof by reflection: let Agda calculate the result/proof during type checking -- works as long as the arguments are sufficiently known -- in this case: ask for a value of type Dec (n ≤ m) -- next: map the result to Bool using ⌊_⌋ -- next: map the bool to a type using T -- result: if n ≤ m , then the resulting type is inhabited -- otherwise, the resulting type is empty -- we are going to ask for an implicit argument of type T ⌊ n ≤? m ⌋ _-_ : (m n : ℕ) → {n≤m : T ⌊ n ≤? m ⌋} → ℕ _-_ m n {n≤m} = minus m n (toWitness n≤m) _ : 4 - 2 ≡ 2 _ = refl try : ∀ m → m - 0 ≡ m try m = refl True : ∀ {Q} → Dec Q → Set True q = T ⌊ q ⌋