------------------------------------------------------------------------ -- 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.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) open import Data.Unit.Polymorphic.Base using (⊤) open import Data.Empty.Polymorphic using (⊥) open import Level using (Level) open import Function.Base using (_$_; _∘_; const; id) open import Relation.Nullary.Negation.Core using (¬_; contradiction-irr; contradiction; _¬-⊎_) open import Relation.Nullary.Recomputable as Recomputable using (Recomputable) private variable a : Level A B : Set a ------------------------------------------------------------------------ -- `Reflects` idiom. -- The truth value of A is reflected by a boolean value. -- `Reflects A b` is equivalent to `if b then A else ¬ A`. data Reflects (A : Set a) : Bool → Set a where ofʸ : ( a : A) → Reflects A true ofⁿ : (¬a : ¬ A) → Reflects A 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 `A` or the proof of `¬ A`. of : ∀ {b} → if b then A else ¬ A → Reflects A b of {b = false} ¬a = ofⁿ ¬a of {b = true } a = ofʸ a invert : ∀ {b} → Reflects A b → if b then A else ¬ A invert (ofʸ a) = a invert (ofⁿ ¬a) = ¬a ------------------------------------------------------------------------ -- recompute -- Given an irrelevant proof of a reflected type, a proof can -- be recomputed and subsequently used in relevant contexts. recompute : ∀ {b} → Reflects A b → Recomputable A recompute (ofʸ a) _ = a recompute (ofⁿ ¬a) a = contradiction-irr a ¬a recompute-constant : ∀ {b} (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q recompute-constant = Recomputable.recompute-constant ∘ recompute ------------------------------------------------------------------------ -- Interaction with true, false, negation, product, sums etc. infixr 1 _⊎-reflects_ infixr 2 _×-reflects_ _→-reflects_ ⊥-reflects : Reflects (⊥ {a}) false ⊥-reflects = of λ() ⊤-reflects : Reflects (⊤ {a}) true ⊤-reflects = of _ T-reflects : ∀ b → Reflects (T b) b T-reflects true = of _ T-reflects false = of id ¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b) ¬-reflects (ofʸ a) = of (_$ a) ¬-reflects (ofⁿ ¬a) = of ¬a _×-reflects_ : ∀ {a b} → Reflects A a → Reflects B b → Reflects (A × B) (a ∧ b) ofʸ a ×-reflects ofʸ b = of (a , b) ofʸ a ×-reflects ofⁿ ¬b = of (¬b ∘ proj₂) ofⁿ ¬a ×-reflects _ = of (¬a ∘ proj₁) _⊎-reflects_ : ∀ {a b} → Reflects A a → Reflects B b → Reflects (A ⊎ B) (a ∨ b) ofʸ a ⊎-reflects _ = of (inj₁ a) ofⁿ ¬a ⊎-reflects ofʸ b = of (inj₂ b) ofⁿ ¬a ⊎-reflects ofⁿ ¬b = of (¬a ¬-⊎ ¬b) _→-reflects_ : ∀ {a b} → Reflects A a → Reflects B b → Reflects (A → B) (not a ∨ b) ofʸ a →-reflects ofʸ b = of (const b) ofʸ a →-reflects ofⁿ ¬b = of (¬b ∘ (_$ a)) ofⁿ ¬a →-reflects _ = of (λ a → contradiction a ¬a) ------------------------------------------------------------------------ -- Other lemmas fromEquivalence : ∀ {b} → (T b → A) → (A → T b) → Reflects A b fromEquivalence {b = true} sound complete = of (sound _) fromEquivalence {b = false} sound complete = of complete -- `Reflects` is deterministic. det : ∀ {b b′} → Reflects A b → Reflects A b′ → b ≡ b′ det (ofʸ a) (ofʸ _) = refl det (ofʸ a) (ofⁿ ¬a) = contradiction a ¬a det (ofⁿ ¬a) (ofʸ a) = contradiction a ¬a det (ofⁿ ¬a) (ofⁿ _) = refl T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a T-reflects-elim {a} r = det r (T-reflects a)