------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of the `Reflects` construct ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Relation.Nullary.Reflects where open import Agda.Builtin.Equality open import Data.Bool.Base open import Data.Empty open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) open import Level using (Level) open import Function.Base using (_$_; _∘_; const) open import Relation.Nullary.Negation.Core private variable p q : Level P Q : Set p ------------------------------------------------------------------------ -- `Reflects` idiom. -- The truth value of P is reflected by a boolean value. -- `Reflects P b` is equivalent to `if b then P else ¬ P`. data Reflects {p} (P : Set p) : Bool → Set p where ofʸ : ( p : P) → Reflects P true ofⁿ : (¬p : ¬ P) → Reflects P false ------------------------------------------------------------------------ -- Constructors and destructors -- 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 ------------------------------------------------------------------------ -- Interaction with negation, product, sums etc. -- If we can decide P, then we can decide its negation. ¬-reflects : ∀ {b} → Reflects P b → Reflects (¬ P) (not b) ¬-reflects (ofʸ p) = ofⁿ (_$ p) ¬-reflects (ofⁿ ¬p) = ofʸ ¬p -- If we can decide P and Q then we can decide their product infixr 2 _×-reflects_ _×-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b → Reflects (P × Q) (a ∧ b) ofʸ p ×-reflects ofʸ q = ofʸ (p , q) ofʸ p ×-reflects ofⁿ ¬q = ofⁿ (¬q ∘ proj₂) ofⁿ ¬p ×-reflects _ = ofⁿ (¬p ∘ proj₁) infixr 1 _⊎-reflects_ _⊎-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b → Reflects (P ⊎ Q) (a ∨ b) ofʸ p ⊎-reflects _ = ofʸ (inj₁ p) ofⁿ ¬p ⊎-reflects ofʸ q = ofʸ (inj₂ q) ofⁿ ¬p ⊎-reflects ofⁿ ¬q = ofⁿ (¬p ¬-⊎ ¬q) infixr 2 _→-reflects_ _→-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b → Reflects (P → Q) (not a ∨ b) ofʸ p →-reflects ofʸ q = ofʸ (const q) ofʸ p →-reflects ofⁿ ¬q = ofⁿ (¬q ∘ (_$ p)) ofⁿ ¬p →-reflects _ = ofʸ (⊥-elim ∘ ¬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