------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of the `Reflects` construct ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Relation.Nullary.Reflects where open import Agda.Builtin.Equality open import Data.Bool.Base open import Data.Empty open import Level open import Relation.Nullary private variable p : Level P : Set p ------------------------------------------------------------------------ -- `Reflects P b` is equivalent to `if b then P else ¬ P`. -- These lemmas are intended to be used mostly when `b` is a value, so -- that the `if` expressions have already been evaluated away. -- In this case, `of` works like the relevant constructor (`ofⁿ` or -- `ofʸ`), and `invert` strips off the constructor to just give either -- the proof of `P` or the proof of `¬ P`. of : {b} if b then P else ¬ P Reflects P b of {b = false} ¬p = ofⁿ ¬p of {b = true } p = ofʸ p invert : {b} Reflects P b if b then P else ¬ P invert (ofʸ p) = p invert (ofⁿ ¬p) = ¬p ------------------------------------------------------------------------ -- Other lemmas fromEquivalence : {b} (T b P) (P T b) Reflects P b fromEquivalence {b = true} sound complete = ofʸ (sound _) fromEquivalence {b = false} sound complete = ofⁿ complete -- `Reflects` is deterministic. det : {b b′} Reflects P b Reflects P b′ b b′ det (ofʸ p) (ofʸ p′) = refl det (ofʸ p) (ofⁿ ¬p′) = ⊥-elim (¬p′ p) det (ofⁿ ¬p) (ofʸ p′) = ⊥-elim (¬p p′) det (ofⁿ ¬p) (ofⁿ ¬p′) = refl