------------------------------------------------------------------------ -- 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 --without-K --safe #-} module Relation.Nullary.Decidable.Core where open import Level using (Level; Lift) open import Data.Bool.Base using (Bool; false; true; not; T) open import Data.Unit.Base using () open import Data.Empty open import Data.Product open import Function.Base open import Agda.Builtin.Equality open import Relation.Nullary.Reflects open import Relation.Nullary private variable p q : Level P : Set p Q : Set q -- `isYes` is a stricter version of `does`. The lack of computation means that -- we can recover the proposition `P` from `isYes P?` by unification. This is -- useful when we are using the decision procedure for proof automation. isYes : Dec P Bool isYes ( true because _) = true isYes (false because _) = false isYes≗does : (P? : Dec P) isYes P? does P? isYes≗does ( true because _) = refl isYes≗does (false because _) = refl -- The traditional name for isYes is ⌊_⌋, indicating the stripping of evidence. ⌊_⌋ = isYes isNo : Dec P Bool isNo = not isYes True : Dec P Set True Q = T (isYes Q) False : Dec P Set False Q = T (isNo Q) -- Gives a witness to the "truth". toWitness : {Q : Dec P} True Q P toWitness {Q = true because [p]} _ = invert [p] toWitness {Q = false because _ } () -- Establishes a "truth", given a witness. fromWitness : {Q : Dec P} P True Q fromWitness {Q = true because _ } = const _ fromWitness {Q = false because [¬p]} = invert [¬p] -- Variants for False. toWitnessFalse : {Q : Dec P} False Q ¬ P toWitnessFalse {Q = true because _ } () toWitnessFalse {Q = false because [¬p]} _ = invert [¬p] fromWitnessFalse : {Q : Dec P} ¬ P False Q fromWitnessFalse {Q = true because [p]} = flip _\$_ (invert [p]) fromWitnessFalse {Q = false because _ } = const _ -- If a decision procedure returns "yes", then we can extract the -- proof using from-yes. module _ {p} {P : Set p} where From-yes : Dec P Set p From-yes (true because _) = P From-yes (false because _) = Lift p from-yes : (p : Dec P) From-yes p from-yes (true because [p]) = invert [p] from-yes (false because _ ) = _ -- If a decision procedure returns "no", then we can extract the proof -- using from-no. From-no : Dec P Set p From-no (false because _) = ¬ P From-no (true because _) = Lift p from-no : (p : Dec P) From-no p from-no (false because [¬p]) = invert [¬p] from-no (true because _ ) = _ ------------------------------------------------------------------------ -- Result of decidability dec-true : (p? : Dec P) P does p? true dec-true (true because _ ) p = refl dec-true (false because [¬p]) p = ⊥-elim (invert [¬p] p) dec-false : (p? : Dec P) ¬ P does p? false dec-false (false because _ ) ¬p = refl dec-false (true because [p]) ¬p = ⊥-elim (¬p (invert [p])) dec-yes : (p? : Dec P) P λ p′ p? yes p′ dec-yes p? p with dec-true p? p dec-yes (yes p′) p | refl = p′ , refl dec-no : (p? : Dec P) ¬ P λ ¬p′ p? no ¬p′ dec-no p? ¬p with dec-false p? ¬p dec-no (no ¬p′) ¬p | refl = ¬p′ , refl dec-yes-irr : (p? : Dec P) Irrelevant P (p : P) p? yes p dec-yes-irr p? irr p with dec-yes p? p ... | p′ , eq rewrite irr p p′ = eq ------------------------------------------------------------------------ -- Maps map′ : (P Q) (Q P) Dec P Dec Q does (map′ P→Q Q→P p?) = does p? proof (map′ P→Q Q→P (true because [p])) = ofʸ (P→Q (invert [p])) proof (map′ P→Q Q→P (false because [¬p])) = ofⁿ (invert [¬p] Q→P)