------------------------------------------------------------------------ -- The Agda standard library -- -- Operations on and properties of decidable relations -- -- This file contains some core definitions which are re-exported by -- Relation.Nullary.Decidable ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Relation.Nullary.Decidable.Core where -- decToMaybe was deprecated in v2.1 #2330/#2336 -- this can go through `Data.Maybe.Base` once that deprecation is fully done. open import Agda.Builtin.Equality using (_≡_) open import Agda.Builtin.Maybe using (Maybe; just; nothing) open import Level using (Level) open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_) open import Data.Unit.Polymorphic.Base using (⊤) open import Data.Empty.Polymorphic using (⊥) open import Data.Product.Base using (_×_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base using (_∘_; const; _$_; flip) open import Relation.Nullary.Irrelevant using (Irrelevant) open import Relation.Nullary.Recomputable.Core as Recomputable using (Recomputable) open import Relation.Nullary.Reflects as Reflects hiding (recompute; recompute-constant) open import Relation.Nullary.Negation.Core using (¬_; Stable; negated-stable; contradiction; DoubleNegation) private variable a b : Level A B : Set a ------------------------------------------------------------------------ -- Definition. -- Decidability proofs have two parts: the `does` term which contains -- the boolean result and the `proof` term which contains a proof that -- reflects the boolean result. This definition allows the boolean -- part of the decision procedure to compute independently from the -- proof. This leads to better computational behaviour when we only care -- about the result and not the proof. See README.Design.Decidability -- for further details. infix 2 _because_ record Dec (A : Set a) : Set a where constructor _because_ field does : Bool proof : Reflects A does open Dec public pattern yes a = true because ofʸ a pattern no ¬a = false because ofⁿ ¬a ------------------------------------------------------------------------ -- Flattening module _ {A : Set a} where From-yes : Dec A → Set a From-yes (true because _) = A From-yes (false because _) = ⊤ From-no : Dec A → Set a From-no (false because _) = ¬ A From-no (true because _) = ⊤ ------------------------------------------------------------------------ -- Recompute -- Given an irrelevant proof of a decidable type, a proof can -- be recomputed and subsequently used in relevant contexts. recompute : Dec A → Recomputable A recompute = Reflects.recompute ∘ proof recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q recompute-constant = Recomputable.recompute-constant ∘ recompute recompute-irrelevant-id : (a? : Dec A) → Irrelevant A → (a : A) → recompute a? a ≡ a recompute-irrelevant-id = Recomputable.recompute-irrelevant-id ∘ recompute ------------------------------------------------------------------------ -- Interaction with negation, sum, product etc. infixr 1 _⊎-dec_ infixr 2 _×-dec_ _→-dec_ T? : ∀ x → Dec (T x) T? x = x because T-reflects x ¬? : Dec A → Dec (¬ A) does (¬? a?) = not (does a?) proof (¬? a?) = ¬-reflects (proof a?) ⊤-dec : Dec {a} ⊤ does ⊤-dec = true proof ⊤-dec = ⊤-reflects _×-dec_ : Dec A → Dec B → Dec (A × B) does (a? ×-dec b?) = does a? ∧ does b? proof (a? ×-dec b?) = proof a? ×-reflects proof b? ⊥-dec : Dec {a} ⊥ does ⊥-dec = false proof ⊥-dec = ⊥-reflects _⊎-dec_ : Dec A → Dec B → Dec (A ⊎ B) does (a? ⊎-dec b?) = does a? ∨ does b? proof (a? ⊎-dec b?) = proof a? ⊎-reflects proof b? _→-dec_ : Dec A → Dec B → Dec (A → B) does (a? →-dec b?) = not (does a?) ∨ does b? proof (a? →-dec b?) = proof a? →-reflects proof b? ------------------------------------------------------------------------ -- Relationship with Maybe dec⇒maybe : Dec A → Maybe A dec⇒maybe ( true because [a]) = just (invert [a]) dec⇒maybe (false because _ ) = nothing ------------------------------------------------------------------------ -- Relationship with Sum toSum : Dec A → A ⊎ ¬ A toSum ( true because [p]) = inj₁ (invert [p]) toSum (false because [¬p]) = inj₂ (invert [¬p]) fromSum : A ⊎ ¬ A → Dec A fromSum (inj₁ p) = yes p fromSum (inj₂ ¬p) = no ¬p ------------------------------------------------------------------------ -- Relationship with booleans -- `isYes` is a stricter version of `does`. The lack of computation -- means that we can recover the proposition `P` from `isYes a?` by -- unification. This is useful when we are using the decision procedure -- for proof automation. isYes : Dec A → Bool isYes (true because _) = true isYes (false because _) = false isNo : Dec A → Bool isNo = not ∘ isYes True : Dec A → Set True = T ∘ isYes False : Dec A → Set False = T ∘ isNo -- The traditional name for isYes is ⌊_⌋, indicating the stripping of evidence. ⌊_⌋ = isYes ------------------------------------------------------------------------ -- Witnesses -- Gives a witness to the "truth". toWitness : {a? : Dec A} → True a? → A toWitness {a? = true because [a]} _ = invert [a] toWitness {a? = false because _ } () -- Establishes a "truth", given a witness. fromWitness : {a? : Dec A} → A → True a? fromWitness {a? = true because _ } = const _ fromWitness {a? = false because [¬a]} = invert [¬a] -- Variants for False. toWitnessFalse : {a? : Dec A} → False a? → ¬ A toWitnessFalse {a? = true because _ } () toWitnessFalse {a? = false because [¬a]} _ = invert [¬a] fromWitnessFalse : {a? : Dec A} → ¬ A → False a? fromWitnessFalse {a? = true because [a]} = flip _$_ (invert [a]) fromWitnessFalse {a? = false because _ } = const _ -- If a decision procedure returns "yes", then we can extract the -- proof using from-yes. from-yes : (a? : Dec A) → From-yes a? from-yes (true because [a]) = invert [a] from-yes (false because _ ) = _ -- If a decision procedure returns "no", then we can extract the proof -- using from-no. from-no : (a? : Dec A) → From-no a? from-no (false because [¬a]) = invert [¬a] from-no (true because _ ) = _ ------------------------------------------------------------------------ -- Maps map′ : (A → B) → (B → A) → Dec A → Dec B does (map′ A→B B→A a?) = does a? proof (map′ A→B B→A (true because [a])) = of (A→B (invert [a])) proof (map′ A→B B→A (false because [¬a])) = of (invert [¬a] ∘ B→A) ------------------------------------------------------------------------ -- Relationship with double-negation -- Decidable predicates are stable. decidable-stable : Dec A → Stable A decidable-stable (true because [a]) ¬¬a = invert [a] decidable-stable (false because [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A) ¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?) -- A double-negation-translated variant of excluded middle (or: every -- nullary relation is decidable in the double-negation monad). ¬¬-excluded-middle : DoubleNegation (Dec A) ¬¬-excluded-middle ¬?a = ¬?a (no (λ a → ¬?a (yes a))) ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ -- Please use the new names as continuing support for the old names is -- not guaranteed. -- Version 2.0 excluded-middle = ¬¬-excluded-middle {-# WARNING_ON_USAGE excluded-middle "Warning: excluded-middle was deprecated in v2.0. Please use ¬¬-excluded-middle instead." #-} -- Version 2.1 decToMaybe = dec⇒maybe {-# WARNING_ON_USAGE decToMaybe "Warning: decToMaybe was deprecated in v2.1. Please use Relation.Nullary.Decidable.Core.dec⇒maybe instead." #-} fromDec = toSum {-# WARNING_ON_USAGE fromDec "Warning: fromDec was deprecated in v2.1. Please use Relation.Nullary.Decidable.Core.toSum instead." #-} toDec = fromSum {-# WARNING_ON_USAGE toDec "Warning: toDec was deprecated in v2.1. Please use Relation.Nullary.Decidable.Core.fromSum instead." #-}