From 9888e50ce40326ccc5c412da396548cf418bfcb0 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Mon, 22 Jun 2026 13:53:03 +0100 Subject: [PATCH 1/4] [ draft ] Refactor Dec to use constructive negation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Now that v3.0 is being worked on, I think it is the right time for me to push us to rethink our approach to Dec. Historically Dec was just a datatype with yes/no constructors choosing between A and (¬ A). In #929 we entered the era of Reflects and the idea that we could separately compute the Bool telling us the outcome of the decision procedure from the actual proof that comes from its correctness. In this draft, I'd like to shed the commitment to ¬_ in favour of a solution offering constructive notions of negation. This is based on @bobatkey's work: * https://bentnib.org/posts/2023-01-15-datatypes-with-negation.html * https://bentnib.org/posts/2023-11-02-more-data-types-with-negation.html and @jfdm has been porting some of these ideas to Idris. --- The core of the design behind this specific incarnation is that we start by describing what it means for two types to be orthogonal with respect to a (vocabulary influenced by realisability) "pole" P. We say these types are P-orthogonal. A type is always P-orthogonal to its literal negation but there may be more constructive notions of negation e.g. _≤_ is orthogonal to _>_, (A × B) is orthogonal to (¬A ⊎ ¬B), or even (¬A ⊎ (A × ¬B)) if we record the left-biased nature of the decision procedure in the type. The pole idea gives us the ability to decide how strict the orthogonality should be. ⊥-orthogonality is the usual "not both at the same time" whereas ⊤-orthogonality is always trivially true of any pair of types. The orthogonality combinators allow us to build a type of constructive orthogonals to types built out of the standard type constructors. Once we have our orthogonal types, we introduce Choice as the generalisation of Reflects. Choice is a Boolean-indexed decision between two orthogonal types. This covers: 1. the usual strong decidability Dec by having a choice between a type and its negation 2. a variant with constructive negation by simply demanding two ⊥-orthogonal types 3. weak decidability by letting the pole be ⊤ and writing a choice function between A and ⊤ --- src/Relation/Nullary/Choice.agda | 213 +++++++++++++++++++++++++++ src/Relation/Nullary/Orthogonal.agda | 128 ++++++++++++++++ 2 files changed, 341 insertions(+) create mode 100644 src/Relation/Nullary/Choice.agda create mode 100644 src/Relation/Nullary/Orthogonal.agda diff --git a/src/Relation/Nullary/Choice.agda b/src/Relation/Nullary/Choice.agda new file mode 100644 index 0000000000..b75aba5f3b --- /dev/null +++ b/src/Relation/Nullary/Choice.agda @@ -0,0 +1,213 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of the `Choice` construct +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Relation.Nullary.Choice where + +open import Agda.Builtin.Equality + +open import Data.Bool.Base using (Bool; T; true; false; not; if_then_else_; _∧_) + +open import Data.Empty using (⊥; ⊥-elim-irr) +open import Data.Empty.Polymorphic using () renaming (⊥ to ⊥ˡ) +open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) +open import Data.Unit.Base using (⊤) +open import Data.Unit.Polymorphic.Base using () renaming (⊤ to ⊤ˡ) + +open import Level using (Level; _⊔_) + +open import Function.Base using (_$_; _∘′_; _∘_; const; id) + +open import Relation.Nullary.Negation.Core + using (¬_; contraposition; contradiction-irr; contradiction; _¬-⊎_; ¬¬-η) +open import Relation.Nullary.Recomputable as Recomputable using (Recomputable) + + +open import Relation.Nullary.Orthogonal + using (_⫫[_]_; negation; orthogonal; ∁; _∩_; _!∩_) + +private + variable + ℓa ℓaⁿ ℓb ℓbⁿ p : Level + A : Set ℓa + ¬A : Set ℓaⁿ + B : Set ℓb + ¬B : Set ℓbⁿ + P : Set p + oA : A ⫫[ P ] ¬A + oB : B ⫫[ P ] ¬B + a b : Bool + +------------------------------------------------------------------------ +-- `Choice` idiom. + +-- The choice between A and B is reflected by a boolean value. +-- `Choice A B b` is equivalent to `if b then A else B`. +-- `Choice A (¬ A) b` is equivalent to `Reflects A b` + +data Choice + (A : Set ℓa) (P : Set p) (B : Set ℓb) + (oA : A ⫫[ P ] B) : Bool → Set (ℓa ⊔ p ⊔ ℓb) where + ofʸ : (a : A) → Choice A P B oA true + ofⁿ : (a : B) → Choice A P B oA false + +Reflects : Set ℓa → Bool → Set ℓa +Reflects A = Choice A ⊥ (¬ A) (negation A) + +------------------------------------------------------------------------ +-- 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 `B`. + +of : ∀ {b} → if b then A else B → Choice A P B oA b +of {b = true } a = ofʸ a +of {b = false} b = ofⁿ b + +invert : ∀ {b} → Choice A P B oA b → if b then A else B +invert (ofʸ a) = a +invert (ofⁿ b) = b + +------------------------------------------------------------------------ +-- Transformation + +map : (A → B) → (¬A → ¬B) → + Choice A P ¬A oA b → Choice B P ¬B oB b +map f g (ofʸ a) = ofʸ (f a) +map f g (ofⁿ b) = ofⁿ (g b) + +map₁ : (A → B) → Choice A P ¬A oA b → Choice B P ¬A oB b +map₁ f = map f id + +map₂ : (¬A → ¬B) → Choice A P ¬A oA b → Choice A P ¬B oB b +map₂ = map id + +------------------------------------------------------------------------ +-- recompute + +-- Given an irrelevant proof of a reflected type, a proof can +-- be recomputed and subsequently used in relevant contexts. + +recompute : ∀ {b} → Choice A ⊥ B oA b → Recomputable A +recompute (ofʸ a) _ = a +recompute {oA = oA} (ofⁿ b) a = ⊥-elim-irr (oA .orthogonal a b) + +recompute-constant : ∀ {b} (r : Choice A ⊥ B oA b) (p q : A) → + recompute r p ≡ recompute r q +recompute-constant = Recomputable.recompute-constant ∘ recompute + +------------------------------------------------------------------------ +-- Interaction with true, false, negation, product, sums etc. + +⊥ˡ-choice : Choice A P (¬ ⊥ˡ) oA false +⊥ˡ-choice = ofⁿ λ () + +⊥ˡ-reflects : Reflects (⊥ˡ {ℓa}) false +⊥ˡ-reflects = ⊥ˡ-choice + +⊤ˡ-choice : Choice ⊤ˡ P B oA true +⊤ˡ-choice = ofʸ _ + +⊤ˡ-reflects : Reflects (⊤ˡ {ℓa}) true +⊤ˡ-reflects = ⊤ˡ-choice + +⊥-choice : Choice A P (¬ ⊥) oA false +⊥-choice = ofⁿ λ () + +⊥-reflects : Reflects ⊥ false +⊥-reflects = ⊥-choice + +⊤-choice : Choice ⊤ P B oA true +⊤-choice = ofʸ _ + +⊤-reflects : Reflects ⊤ true +⊤-reflects = ⊤-choice + +∁-choice : ∀ {b} → Choice A P B oA b → Choice B P A (∁ oA) (not b) +∁-choice (ofʸ a) = ofⁿ a +∁-choice (ofⁿ b) = ofʸ b + +¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b) +¬-reflects = map id ¬¬-η ∘′ ∁-choice + +Truth-choice : ∀ b {oA} → Choice (T b) P (T (not b)) oA b +Truth-choice true = ⊤-choice +Truth-choice false = ∁-choice ⊤-choice + +-- This could also be implemented using map over Truth-choice +-- if only we had a conveniently accessible proof of +-- T (not b) → ¬ T b +T-reflects : ∀ b → Reflects (T b) b +T-reflects true = ⊤-choice +T-reflects false = ⊥-choice + +infixr 2 _×-choice_ _!×-choice_ + +_×-choice_ : Choice A P ¬A oA a → Choice B P ¬B oB b → + Choice (A × B) P (¬A ⊎ ¬B) (oA ∩ oB) (a ∧ b) +ofʸ a ×-choice ofʸ b = ofʸ (a , b) +ofʸ a ×-choice ofⁿ ¬b = ofⁿ (inj₂ ¬b) +ofⁿ ¬a ×-choice _ = ofⁿ (inj₁ ¬a) + +_×-reflects_ : Reflects A a → Reflects B b → Reflects (A × B) (a ∧ b) +ra ×-reflects rb = map₂ + [ contraposition proj₁ + , contraposition proj₂ + ]′ (ra ×-choice rb) + +_!×-choice_ : Choice A P ¬A oA a → Choice B P ¬B oB b → + Choice (A × B) P (¬A ⊎ (A × ¬B)) (oA !∩ oB) (a ∧ b) +ofʸ a !×-choice ofʸ b = ofʸ (a , b) +ofʸ a !×-choice ofⁿ ¬b = ofⁿ (inj₂ (a , ¬b)) +ofⁿ ¬a !×-choice _ = ofⁿ (inj₁ ¬a) + + +{- +infixr 1 _⊎-choice_ +infixr 2 _×-choice_ _→-choice_ + +_×-choice_ : ∀ {a b} → Choice A a → Choice B b → + Choice (A × B) (a ∧ b) +ofʸ a ×-choice ofʸ b = of (a , b) +ofʸ a ×-choice ofⁿ ¬b = of (¬b ∘ proj₂) +ofⁿ ¬a ×-choice _ = of (¬a ∘ proj₁) + +_⊎-choice_ : ∀ {a b} → Choice A a → Choice B b → + Choice (A ⊎ B) (a ∨ b) +ofʸ a ⊎-choice _ = of (inj₁ a) +ofⁿ ¬a ⊎-choice ofʸ b = of (inj₂ b) +ofⁿ ¬a ⊎-choice ofⁿ ¬b = of (¬a ¬-⊎ ¬b) + +_→-choice_ : ∀ {a b} → Choice A a → Choice B b → + Choice (A → B) (not a ∨ b) +ofʸ a →-choice ofʸ b = of (const b) +ofʸ a →-choice ofⁿ ¬b = of (¬b ∘ (_$ a)) +ofⁿ ¬a →-choice _ = 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 + +{- +-- `Choice` is deterministic. +det : ∀ {b b′} → Choice A b → Choice 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-choice-elim : ∀ {a b} → Choice (T a) b → b ≡ a +T-choice-elim {a} r = det r (T-choice a) +-} diff --git a/src/Relation/Nullary/Orthogonal.agda b/src/Relation/Nullary/Orthogonal.agda new file mode 100644 index 0000000000..36ca8ffcdc --- /dev/null +++ b/src/Relation/Nullary/Orthogonal.agda @@ -0,0 +1,128 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Orthogonality for types +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Relation.Nullary.Orthogonal where + +open import Data.Bool.Base as Bool using (T; true; false; not) +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Empty.Polymorphic renaming (⊥ to ⊥ˡ; ⊥-elim to ⊥ˡ-elim) +open import Data.Product.Base using (_×_; Σ-syntax; _,_; proj₁; proj₂) +open import Data.Sum.Base using (_⊎_; [_,_]′) +open import Data.Unit.Base using (⊤) + +open import Function.Base using (const; flip; _∘′_; _$′_) + +open import Level using (Level; _⊔_) + +open import Relation.Nullary.Negation.Core using (¬_; contradiction) + +private + variable + a aⁿ b bⁿ p q : Level + A : Set a + ¬A : Set aⁿ + B : Set b + ¬B : Set bⁿ + P : Set p + Q : Set q + +------------------------------------------------------------------------ +-- Basic definitions + +-- Two types are orthogonal with respect to a pole P when assuming +-- that both are inhabited leads to a proof of P. +-- In particular, when the pole is the empty set this amounts to +-- saying that one is a (more or less constructive) notiong of +-- negation for the other. + +infix 1 _⫫[_]_ +record _⫫[_]_ (A : Set a) (P : Set p) (B : Set b) : Set (p ⊔ a ⊔ b) where + field orthogonal : A → B → P + + co-orthogonal : B → A → P + co-orthogonal = flip orthogonal +open _⫫[_]_ public + +------------------------------------------------------------------------ +-- Base cases + +-- The empty type is orthogonal with everything +∅ : ⊥ ⫫[ P ] A +∅ .orthogonal = ⊥-elim + +⊘ˡ : ⊥ˡ {a} ⫫[ P ] A +⊘ˡ .orthogonal = ⊥ˡ-elim + +-- Truth of a boolean is orthogonal to truth of its negation +Truth : ∀ b → Bool.T b ⫫[ P ] Bool.T (not b) +Truth false .orthogonal = ⊥-elim +Truth true .orthogonal = flip ⊥-elim + +-- A type is always orthogonal to its negation +negation : (A : Set a) → A ⫫[ P ] ¬ A +negation A .orthogonal = contradiction + +-- If our notion of orthogonality is with respect to ⊤ then any +-- two things are related +universal : A ⫫[ ⊤ ] B +universal .orthogonal = _ + +------------------------------------------------------------------------ +-- Closure principles + +-- The relation is a contravariant bifunctor +map : (B → A) → (P → Q) → (¬B → ¬A) → A ⫫[ P ] ¬A → B ⫫[ Q ] ¬B +map f g ¬f oA .orthogonal b ¬b = g (oA .orthogonal (f b) (¬f ¬b)) + +-- Being ⊥-orthogonal to the unit type is being uninhabited +uninhabited : ⊤ ⫫[ ⊥ ] A → ¬ A +uninhabited oA = oA .orthogonal _ + +------------------------------------------------------------------------ +-- Type constructors building constructive negations + +-- Constructive negation just swaps the two parameters. +-- It is involutive! +∁ : A ⫫[ P ] ¬A → ¬A ⫫[ P ] A +∁ oA .orthogonal a ¬a = oA .orthogonal ¬a a + +-- The negation of a function is a proof the domain is inhabited +-- together with a negation of the codomain +_⇒_ : (A : Set a) → B ⫫[ P ] ¬B → (A → B) ⫫[ P ] (A × ¬B) +(oA ⇒ oB) .orthogonal f (a , ¬b) = oB .orthogonal (f a) ¬b + +Π : (A : Set a) {B : A → Set b} {¬B : A → Set bⁿ} + → ((a : A) → B a ⫫[ P ] ¬B a) → ((a : A) → B a) ⫫[ P ] (Σ[ a ∈ A ] ¬B a) +Π A oB .orthogonal f (a , ¬b) = oB a .orthogonal (f a) ¬b + +-- The negation of a conjunction is a disjunction of negations +_∩_ : A ⫫[ P ] ¬A → B ⫫[ P ] ¬B → (A × B) ⫫[ P ] (¬A ⊎ ¬B) +(oA ∩ oB) .orthogonal (a , b) = + [ oA .orthogonal a + , oB .orthogonal b ]′ + +Σ : A ⫫[ P ] ¬A → {B : A → Set b} {¬B : A → Set bⁿ} → ((a : A) → B a ⫫[ P ] ¬B a) + → (Σ[ a ∈ A ] B a) ⫫[ P ] (¬A ⊎ ((a : A) → ¬B a)) +Σ oA oB .orthogonal (a , b) = + [ oA .orthogonal a + , (λ f → oB a .orthogonal b (f a)) ]′ + +-- The negation of a strict left-to-right conjunction is defined +-- by either finding a way to disprove A or, a way to disprove B +-- given the knowledge that A is provable +_!∩_ : A ⫫[ P ] ¬A → B ⫫[ P ] ¬B → (A × B) ⫫[ P ] (¬A ⊎ (A × ¬B)) +(oA !∩ oB) .orthogonal (a , b) = + [ oA .orthogonal a + , oB .orthogonal b ∘′ proj₂ ]′ + + +-- The negation of a disjunction is a conjunction of negations +-- This is defined using de Morgan's law + +_∪_ : A ⫫[ P ] ¬A → B ⫫[ P ] ¬B → (A ⊎ B) ⫫[ P ] (¬A × ¬B) +oA ∪ oB = ∁ (∁ oA ∩ ∁ oB) From d724f8e1fbf059d6ca7eb572bcb3542701032712 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Mon, 22 Jun 2026 13:53:03 +0100 Subject: [PATCH 2/4] [ draft ] Refactor Dec to use constructive negation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Now that v3.0 is being worked on, I think it is the right time for me to push us to rethink our approach to Dec. Historically Dec was just a datatype with yes/no constructors choosing between A and (¬ A). In #929 we entered the era of Reflects and the idea that we could separately compute the Bool telling us the outcome of the decision procedure from the actual proof that comes from its correctness. In this draft, I'd like to shed the commitment to ¬_ in favour of a solution offering constructive notions of negation. This is based on @bobatkey's work: * https://bentnib.org/posts/2023-01-15-datatypes-with-negation.html * https://bentnib.org/posts/2023-11-02-more-data-types-with-negation.html and @jfdm has been porting some of these ideas to Idris. --- The core of the design behind this specific incarnation is that we start by describing what it means for two types to be orthogonal with respect to a (vocabulary influenced by realisability) "pole" P. We say these types are P-orthogonal. A type is always P-orthogonal to its literal negation but there may be more constructive notions of negation e.g. _≤_ is orthogonal to _>_, (A × B) is orthogonal to (¬A ⊎ ¬B), or even (¬A ⊎ (A × ¬B)) if we record the left-biased nature of the decision procedure in the type. The pole idea gives us the ability to decide how strict the orthogonality should be. ⊥-orthogonality is the usual "not both at the same time" whereas ⊤-orthogonality is always trivially true of any pair of types. The orthogonality combinators allow us to build a type of constructive orthogonals to types built out of the standard type constructors. Once we have our orthogonal types, we introduce Choice as the generalisation of Reflects. Choice is a Boolean-indexed decision between two orthogonal types. This covers: 1. the usual strong decidability Dec by having a choice between a type and its negation 2. a variant with constructive negation by simply demanding two ⊥-orthogonal types 3. weak decidability by letting the pole be ⊤ and writing a choice function between A and ⊤ --- src/Relation/Nullary/Choice.agda | 213 +++++++++++++++++++++++++++ src/Relation/Nullary/Orthogonal.agda | 128 ++++++++++++++++ 2 files changed, 341 insertions(+) create mode 100644 src/Relation/Nullary/Choice.agda create mode 100644 src/Relation/Nullary/Orthogonal.agda diff --git a/src/Relation/Nullary/Choice.agda b/src/Relation/Nullary/Choice.agda new file mode 100644 index 0000000000..b75aba5f3b --- /dev/null +++ b/src/Relation/Nullary/Choice.agda @@ -0,0 +1,213 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of the `Choice` construct +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Relation.Nullary.Choice where + +open import Agda.Builtin.Equality + +open import Data.Bool.Base using (Bool; T; true; false; not; if_then_else_; _∧_) + +open import Data.Empty using (⊥; ⊥-elim-irr) +open import Data.Empty.Polymorphic using () renaming (⊥ to ⊥ˡ) +open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) +open import Data.Unit.Base using (⊤) +open import Data.Unit.Polymorphic.Base using () renaming (⊤ to ⊤ˡ) + +open import Level using (Level; _⊔_) + +open import Function.Base using (_$_; _∘′_; _∘_; const; id) + +open import Relation.Nullary.Negation.Core + using (¬_; contraposition; contradiction-irr; contradiction; _¬-⊎_; ¬¬-η) +open import Relation.Nullary.Recomputable as Recomputable using (Recomputable) + + +open import Relation.Nullary.Orthogonal + using (_⫫[_]_; negation; orthogonal; ∁; _∩_; _!∩_) + +private + variable + ℓa ℓaⁿ ℓb ℓbⁿ p : Level + A : Set ℓa + ¬A : Set ℓaⁿ + B : Set ℓb + ¬B : Set ℓbⁿ + P : Set p + oA : A ⫫[ P ] ¬A + oB : B ⫫[ P ] ¬B + a b : Bool + +------------------------------------------------------------------------ +-- `Choice` idiom. + +-- The choice between A and B is reflected by a boolean value. +-- `Choice A B b` is equivalent to `if b then A else B`. +-- `Choice A (¬ A) b` is equivalent to `Reflects A b` + +data Choice + (A : Set ℓa) (P : Set p) (B : Set ℓb) + (oA : A ⫫[ P ] B) : Bool → Set (ℓa ⊔ p ⊔ ℓb) where + ofʸ : (a : A) → Choice A P B oA true + ofⁿ : (a : B) → Choice A P B oA false + +Reflects : Set ℓa → Bool → Set ℓa +Reflects A = Choice A ⊥ (¬ A) (negation A) + +------------------------------------------------------------------------ +-- 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 `B`. + +of : ∀ {b} → if b then A else B → Choice A P B oA b +of {b = true } a = ofʸ a +of {b = false} b = ofⁿ b + +invert : ∀ {b} → Choice A P B oA b → if b then A else B +invert (ofʸ a) = a +invert (ofⁿ b) = b + +------------------------------------------------------------------------ +-- Transformation + +map : (A → B) → (¬A → ¬B) → + Choice A P ¬A oA b → Choice B P ¬B oB b +map f g (ofʸ a) = ofʸ (f a) +map f g (ofⁿ b) = ofⁿ (g b) + +map₁ : (A → B) → Choice A P ¬A oA b → Choice B P ¬A oB b +map₁ f = map f id + +map₂ : (¬A → ¬B) → Choice A P ¬A oA b → Choice A P ¬B oB b +map₂ = map id + +------------------------------------------------------------------------ +-- recompute + +-- Given an irrelevant proof of a reflected type, a proof can +-- be recomputed and subsequently used in relevant contexts. + +recompute : ∀ {b} → Choice A ⊥ B oA b → Recomputable A +recompute (ofʸ a) _ = a +recompute {oA = oA} (ofⁿ b) a = ⊥-elim-irr (oA .orthogonal a b) + +recompute-constant : ∀ {b} (r : Choice A ⊥ B oA b) (p q : A) → + recompute r p ≡ recompute r q +recompute-constant = Recomputable.recompute-constant ∘ recompute + +------------------------------------------------------------------------ +-- Interaction with true, false, negation, product, sums etc. + +⊥ˡ-choice : Choice A P (¬ ⊥ˡ) oA false +⊥ˡ-choice = ofⁿ λ () + +⊥ˡ-reflects : Reflects (⊥ˡ {ℓa}) false +⊥ˡ-reflects = ⊥ˡ-choice + +⊤ˡ-choice : Choice ⊤ˡ P B oA true +⊤ˡ-choice = ofʸ _ + +⊤ˡ-reflects : Reflects (⊤ˡ {ℓa}) true +⊤ˡ-reflects = ⊤ˡ-choice + +⊥-choice : Choice A P (¬ ⊥) oA false +⊥-choice = ofⁿ λ () + +⊥-reflects : Reflects ⊥ false +⊥-reflects = ⊥-choice + +⊤-choice : Choice ⊤ P B oA true +⊤-choice = ofʸ _ + +⊤-reflects : Reflects ⊤ true +⊤-reflects = ⊤-choice + +∁-choice : ∀ {b} → Choice A P B oA b → Choice B P A (∁ oA) (not b) +∁-choice (ofʸ a) = ofⁿ a +∁-choice (ofⁿ b) = ofʸ b + +¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b) +¬-reflects = map id ¬¬-η ∘′ ∁-choice + +Truth-choice : ∀ b {oA} → Choice (T b) P (T (not b)) oA b +Truth-choice true = ⊤-choice +Truth-choice false = ∁-choice ⊤-choice + +-- This could also be implemented using map over Truth-choice +-- if only we had a conveniently accessible proof of +-- T (not b) → ¬ T b +T-reflects : ∀ b → Reflects (T b) b +T-reflects true = ⊤-choice +T-reflects false = ⊥-choice + +infixr 2 _×-choice_ _!×-choice_ + +_×-choice_ : Choice A P ¬A oA a → Choice B P ¬B oB b → + Choice (A × B) P (¬A ⊎ ¬B) (oA ∩ oB) (a ∧ b) +ofʸ a ×-choice ofʸ b = ofʸ (a , b) +ofʸ a ×-choice ofⁿ ¬b = ofⁿ (inj₂ ¬b) +ofⁿ ¬a ×-choice _ = ofⁿ (inj₁ ¬a) + +_×-reflects_ : Reflects A a → Reflects B b → Reflects (A × B) (a ∧ b) +ra ×-reflects rb = map₂ + [ contraposition proj₁ + , contraposition proj₂ + ]′ (ra ×-choice rb) + +_!×-choice_ : Choice A P ¬A oA a → Choice B P ¬B oB b → + Choice (A × B) P (¬A ⊎ (A × ¬B)) (oA !∩ oB) (a ∧ b) +ofʸ a !×-choice ofʸ b = ofʸ (a , b) +ofʸ a !×-choice ofⁿ ¬b = ofⁿ (inj₂ (a , ¬b)) +ofⁿ ¬a !×-choice _ = ofⁿ (inj₁ ¬a) + + +{- +infixr 1 _⊎-choice_ +infixr 2 _×-choice_ _→-choice_ + +_×-choice_ : ∀ {a b} → Choice A a → Choice B b → + Choice (A × B) (a ∧ b) +ofʸ a ×-choice ofʸ b = of (a , b) +ofʸ a ×-choice ofⁿ ¬b = of (¬b ∘ proj₂) +ofⁿ ¬a ×-choice _ = of (¬a ∘ proj₁) + +_⊎-choice_ : ∀ {a b} → Choice A a → Choice B b → + Choice (A ⊎ B) (a ∨ b) +ofʸ a ⊎-choice _ = of (inj₁ a) +ofⁿ ¬a ⊎-choice ofʸ b = of (inj₂ b) +ofⁿ ¬a ⊎-choice ofⁿ ¬b = of (¬a ¬-⊎ ¬b) + +_→-choice_ : ∀ {a b} → Choice A a → Choice B b → + Choice (A → B) (not a ∨ b) +ofʸ a →-choice ofʸ b = of (const b) +ofʸ a →-choice ofⁿ ¬b = of (¬b ∘ (_$ a)) +ofⁿ ¬a →-choice _ = 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 + +{- +-- `Choice` is deterministic. +det : ∀ {b b′} → Choice A b → Choice 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-choice-elim : ∀ {a b} → Choice (T a) b → b ≡ a +T-choice-elim {a} r = det r (T-choice a) +-} diff --git a/src/Relation/Nullary/Orthogonal.agda b/src/Relation/Nullary/Orthogonal.agda new file mode 100644 index 0000000000..36ca8ffcdc --- /dev/null +++ b/src/Relation/Nullary/Orthogonal.agda @@ -0,0 +1,128 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Orthogonality for types +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Relation.Nullary.Orthogonal where + +open import Data.Bool.Base as Bool using (T; true; false; not) +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Empty.Polymorphic renaming (⊥ to ⊥ˡ; ⊥-elim to ⊥ˡ-elim) +open import Data.Product.Base using (_×_; Σ-syntax; _,_; proj₁; proj₂) +open import Data.Sum.Base using (_⊎_; [_,_]′) +open import Data.Unit.Base using (⊤) + +open import Function.Base using (const; flip; _∘′_; _$′_) + +open import Level using (Level; _⊔_) + +open import Relation.Nullary.Negation.Core using (¬_; contradiction) + +private + variable + a aⁿ b bⁿ p q : Level + A : Set a + ¬A : Set aⁿ + B : Set b + ¬B : Set bⁿ + P : Set p + Q : Set q + +------------------------------------------------------------------------ +-- Basic definitions + +-- Two types are orthogonal with respect to a pole P when assuming +-- that both are inhabited leads to a proof of P. +-- In particular, when the pole is the empty set this amounts to +-- saying that one is a (more or less constructive) notiong of +-- negation for the other. + +infix 1 _⫫[_]_ +record _⫫[_]_ (A : Set a) (P : Set p) (B : Set b) : Set (p ⊔ a ⊔ b) where + field orthogonal : A → B → P + + co-orthogonal : B → A → P + co-orthogonal = flip orthogonal +open _⫫[_]_ public + +------------------------------------------------------------------------ +-- Base cases + +-- The empty type is orthogonal with everything +∅ : ⊥ ⫫[ P ] A +∅ .orthogonal = ⊥-elim + +⊘ˡ : ⊥ˡ {a} ⫫[ P ] A +⊘ˡ .orthogonal = ⊥ˡ-elim + +-- Truth of a boolean is orthogonal to truth of its negation +Truth : ∀ b → Bool.T b ⫫[ P ] Bool.T (not b) +Truth false .orthogonal = ⊥-elim +Truth true .orthogonal = flip ⊥-elim + +-- A type is always orthogonal to its negation +negation : (A : Set a) → A ⫫[ P ] ¬ A +negation A .orthogonal = contradiction + +-- If our notion of orthogonality is with respect to ⊤ then any +-- two things are related +universal : A ⫫[ ⊤ ] B +universal .orthogonal = _ + +------------------------------------------------------------------------ +-- Closure principles + +-- The relation is a contravariant bifunctor +map : (B → A) → (P → Q) → (¬B → ¬A) → A ⫫[ P ] ¬A → B ⫫[ Q ] ¬B +map f g ¬f oA .orthogonal b ¬b = g (oA .orthogonal (f b) (¬f ¬b)) + +-- Being ⊥-orthogonal to the unit type is being uninhabited +uninhabited : ⊤ ⫫[ ⊥ ] A → ¬ A +uninhabited oA = oA .orthogonal _ + +------------------------------------------------------------------------ +-- Type constructors building constructive negations + +-- Constructive negation just swaps the two parameters. +-- It is involutive! +∁ : A ⫫[ P ] ¬A → ¬A ⫫[ P ] A +∁ oA .orthogonal a ¬a = oA .orthogonal ¬a a + +-- The negation of a function is a proof the domain is inhabited +-- together with a negation of the codomain +_⇒_ : (A : Set a) → B ⫫[ P ] ¬B → (A → B) ⫫[ P ] (A × ¬B) +(oA ⇒ oB) .orthogonal f (a , ¬b) = oB .orthogonal (f a) ¬b + +Π : (A : Set a) {B : A → Set b} {¬B : A → Set bⁿ} + → ((a : A) → B a ⫫[ P ] ¬B a) → ((a : A) → B a) ⫫[ P ] (Σ[ a ∈ A ] ¬B a) +Π A oB .orthogonal f (a , ¬b) = oB a .orthogonal (f a) ¬b + +-- The negation of a conjunction is a disjunction of negations +_∩_ : A ⫫[ P ] ¬A → B ⫫[ P ] ¬B → (A × B) ⫫[ P ] (¬A ⊎ ¬B) +(oA ∩ oB) .orthogonal (a , b) = + [ oA .orthogonal a + , oB .orthogonal b ]′ + +Σ : A ⫫[ P ] ¬A → {B : A → Set b} {¬B : A → Set bⁿ} → ((a : A) → B a ⫫[ P ] ¬B a) + → (Σ[ a ∈ A ] B a) ⫫[ P ] (¬A ⊎ ((a : A) → ¬B a)) +Σ oA oB .orthogonal (a , b) = + [ oA .orthogonal a + , (λ f → oB a .orthogonal b (f a)) ]′ + +-- The negation of a strict left-to-right conjunction is defined +-- by either finding a way to disprove A or, a way to disprove B +-- given the knowledge that A is provable +_!∩_ : A ⫫[ P ] ¬A → B ⫫[ P ] ¬B → (A × B) ⫫[ P ] (¬A ⊎ (A × ¬B)) +(oA !∩ oB) .orthogonal (a , b) = + [ oA .orthogonal a + , oB .orthogonal b ∘′ proj₂ ]′ + + +-- The negation of a disjunction is a conjunction of negations +-- This is defined using de Morgan's law + +_∪_ : A ⫫[ P ] ¬A → B ⫫[ P ] ¬B → (A ⊎ B) ⫫[ P ] (¬A × ¬B) +oA ∪ oB = ∁ (∁ oA ∩ ∁ oB) From 43cba51c12b0462056f556be79ac85003ffb83ee Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 14 Aug 2026 16:17:30 +0100 Subject: [PATCH 3/4] [ more ] choices --- src/Relation/Nullary/Choice.agda | 61 +++++++++++++------------------- 1 file changed, 24 insertions(+), 37 deletions(-) diff --git a/src/Relation/Nullary/Choice.agda b/src/Relation/Nullary/Choice.agda index b75aba5f3b..e489b79052 100644 --- a/src/Relation/Nullary/Choice.agda +++ b/src/Relation/Nullary/Choice.agda @@ -10,9 +10,9 @@ module Relation.Nullary.Choice where open import Agda.Builtin.Equality -open import Data.Bool.Base using (Bool; T; true; false; not; if_then_else_; _∧_) +open import Data.Bool.Base using (Bool; T; true; false; not; if_then_else_; _∧_; _∨_) -open import Data.Empty using (⊥; ⊥-elim-irr) +open import Data.Empty using (⊥; ⊥-elim; ⊥-elim-irr) open import Data.Empty.Polymorphic using () renaming (⊥ to ⊥ˡ) open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) @@ -29,16 +29,17 @@ open import Relation.Nullary.Recomputable as Recomputable using (Recomputable) open import Relation.Nullary.Orthogonal - using (_⫫[_]_; negation; orthogonal; ∁; _∩_; _!∩_) + using (_⫫[_]_; negation; orthogonal; ∁; _∩_; _!∩_; _∪_; _⇒_) private variable - ℓa ℓaⁿ ℓb ℓbⁿ p : Level + ℓa ℓaⁿ ℓb ℓbⁿ p q : Level A : Set ℓa ¬A : Set ℓaⁿ B : Set ℓb ¬B : Set ℓbⁿ P : Set p + Q : Set q oA : A ⫫[ P ] ¬A oB : B ⫫[ P ] ¬B a b : Bool @@ -80,14 +81,14 @@ invert (ofⁿ b) = b -- Transformation map : (A → B) → (¬A → ¬B) → - Choice A P ¬A oA b → Choice B P ¬B oB b + Choice A P ¬A oA b → Choice B Q ¬B oB b map f g (ofʸ a) = ofʸ (f a) map f g (ofⁿ b) = ofⁿ (g b) -map₁ : (A → B) → Choice A P ¬A oA b → Choice B P ¬A oB b +map₁ : (A → B) → Choice A P ¬A oA b → Choice B Q ¬A oB b map₁ f = map f id -map₂ : (¬A → ¬B) → Choice A P ¬A oA b → Choice A P ¬B oB b +map₂ : (¬A → ¬B) → Choice A P ¬A oA b → Choice A Q ¬B oB b map₂ = map id ------------------------------------------------------------------------ @@ -169,29 +170,17 @@ ofʸ a !×-choice ofʸ b = ofʸ (a , b) ofʸ a !×-choice ofⁿ ¬b = ofⁿ (inj₂ (a , ¬b)) ofⁿ ¬a !×-choice _ = ofⁿ (inj₁ ¬a) +_⊎-choice_ : Choice A P ¬A oA a → Choice B P ¬B oB b → + Choice (A ⊎ B) P (¬A × ¬B) (oA ∪ oB) (a ∨ b) +ofʸ a ⊎-choice _ = ofʸ (inj₁ a) +ofⁿ ¬a ⊎-choice ofʸ b = ofʸ (inj₂ b) +ofⁿ ¬a ⊎-choice ofⁿ ¬b = ofⁿ (¬a , ¬b) -{- -infixr 1 _⊎-choice_ -infixr 2 _×-choice_ _→-choice_ - -_×-choice_ : ∀ {a b} → Choice A a → Choice B b → - Choice (A × B) (a ∧ b) -ofʸ a ×-choice ofʸ b = of (a , b) -ofʸ a ×-choice ofⁿ ¬b = of (¬b ∘ proj₂) -ofⁿ ¬a ×-choice _ = of (¬a ∘ proj₁) - -_⊎-choice_ : ∀ {a b} → Choice A a → Choice B b → - Choice (A ⊎ B) (a ∨ b) -ofʸ a ⊎-choice _ = of (inj₁ a) -ofⁿ ¬a ⊎-choice ofʸ b = of (inj₂ b) -ofⁿ ¬a ⊎-choice ofⁿ ¬b = of (¬a ¬-⊎ ¬b) - -_→-choice_ : ∀ {a b} → Choice A a → Choice B b → - Choice (A → B) (not a ∨ b) -ofʸ a →-choice ofʸ b = of (const b) -ofʸ a →-choice ofⁿ ¬b = of (¬b ∘ (_$ a)) -ofⁿ ¬a →-choice _ = of (λ a → contradiction a ¬a) --} +_→-choice_ : Choice A B ¬A oA a → Choice B P ¬B oB b → + Choice (A → B) P (A × ¬B) (A ⇒ oB) (not a ∨ b) +ofʸ a →-choice ofʸ b = ofʸ (const b) +ofʸ a →-choice ofⁿ ¬b = ofⁿ (a , ¬b) +_→-choice_ {oA = oA} (ofⁿ ¬a) _ = ofʸ (λ a → oA .orthogonal a ¬a) ------------------------------------------------------------------------ -- Other lemmas @@ -200,14 +189,12 @@ 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 -{- --- `Choice` is deterministic. -det : ∀ {b b′} → Choice A b → Choice A b′ → b ≡ b′ +-- `Choice` is deterministic on orthogonal types. +det : ∀ {b b′} → Choice A ⊥ ¬A oA b → Choice A ⊥ ¬A oA 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 {oA = oA} (ofʸ a) (ofⁿ ¬a) = ⊥-elim (oA .orthogonal a ¬a) +det {oA = oA} (ofⁿ ¬a) (ofʸ a) = ⊥-elim (oA .orthogonal a ¬a) det (ofⁿ ¬a) (ofⁿ _) = refl -T-choice-elim : ∀ {a b} → Choice (T a) b → b ≡ a -T-choice-elim {a} r = det r (T-choice a) --} +T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a +T-reflects-elim {a} r = det r (T-reflects a) From e4da7fbda5273702d35d8bbe96906f0b73ecc1f9 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 14 Aug 2026 16:45:39 +0100 Subject: [PATCH 4/4] [ new ] alternative design A lot of the times the orthogonality constraints are under-constrained so why not simply get rid of them on the Choice/Choose and only require them when orthogonality is needed for a proof. --- src/Relation/Nullary/Choice.agda | 2 +- src/Relation/Nullary/Choice2.agda | 196 +++++++++++++++++++++ src/Relation/Nullary/Choose/Core.agda | 238 ++++++++++++++++++++++++++ src/Relation/Nullary/Orthogonal.agda | 9 +- 4 files changed, 442 insertions(+), 3 deletions(-) create mode 100644 src/Relation/Nullary/Choice2.agda create mode 100644 src/Relation/Nullary/Choose/Core.agda diff --git a/src/Relation/Nullary/Choice.agda b/src/Relation/Nullary/Choice.agda index e489b79052..f24fb3d392 100644 --- a/src/Relation/Nullary/Choice.agda +++ b/src/Relation/Nullary/Choice.agda @@ -58,7 +58,7 @@ data Choice ofⁿ : (a : B) → Choice A P B oA false Reflects : Set ℓa → Bool → Set ℓa -Reflects A = Choice A ⊥ (¬ A) (negation A) +Reflects A = Choice A ⊥ (¬ A) (negation {A = A}) ------------------------------------------------------------------------ -- Constructors and destructors diff --git a/src/Relation/Nullary/Choice2.agda b/src/Relation/Nullary/Choice2.agda new file mode 100644 index 0000000000..a56bd9b603 --- /dev/null +++ b/src/Relation/Nullary/Choice2.agda @@ -0,0 +1,196 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of the `Choice` construct +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Relation.Nullary.Choice2 where + +open import Agda.Builtin.Equality + +open import Data.Bool.Base using (Bool; T; true; false; not; if_then_else_; _∧_; _∨_) + +open import Data.Empty using (⊥; ⊥-elim; ⊥-elim-irr) +open import Data.Empty.Polymorphic using () renaming (⊥ to ⊥ˡ) +open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) +open import Data.Unit.Base using (⊤) +open import Data.Unit.Polymorphic.Base using () renaming (⊤ to ⊤ˡ) + +open import Level using (Level; _⊔_) + +open import Function.Base using (_$_; _∘′_; _∘_; const; id) + +open import Relation.Nullary.Negation.Core + using (¬_; contraposition; contradiction-irr; contradiction; _¬-⊎_; ¬¬-η) +open import Relation.Nullary.Recomputable as Recomputable using (Recomputable; ⊥-recompute) + + +open import Relation.Nullary.Orthogonal + using (_⫫[_]_; byOrthogonality) + +private + variable + ℓa ℓaⁿ ℓb ℓbⁿ : Level + A : Set ℓa + ¬A : Set ℓaⁿ + B : Set ℓb + ¬B : Set ℓbⁿ + a b : Bool + +------------------------------------------------------------------------ +-- `Choice` idiom. + +-- The choice between A and B is reflected by a boolean value. +-- `Choice A B b` is equivalent to `if b then A else B`. +-- `Choice A (¬ A) b` is equivalent to `Reflects A b` + +data Choice (A : Set ℓa) (B : Set ℓb) : Bool → Set (ℓa ⊔ ℓb) where + ofʸ : (a : A) → Choice A B true + ofⁿ : (a : B) → Choice A B false + +Reflects : Set ℓa → Bool → Set ℓa +Reflects A = Choice A (¬ A) + +------------------------------------------------------------------------ +-- 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 `B`. + +of : ∀ {b} → if b then A else B → Choice A B b +of {b = true } a = ofʸ a +of {b = false} b = ofⁿ b + +invert : ∀ {b} → Choice A B b → if b then A else B +invert (ofʸ a) = a +invert (ofⁿ b) = b + +------------------------------------------------------------------------ +-- Transformation + +map : (A → B) → (¬A → ¬B) → Choice A ¬A b → Choice B ¬B b +map f g (ofʸ a) = ofʸ (f a) +map f g (ofⁿ b) = ofⁿ (g b) + +map₁ : (A → B) → Choice A ¬A b → Choice B ¬A b +map₁ f = map f id + +map₂ : (¬A → ¬B) → Choice A ¬A b → Choice A ¬B b +map₂ = map id + +------------------------------------------------------------------------ +-- recompute + +-- Given an irrelevant proof of a reflected type, a proof can +-- be recomputed and subsequently used in relevant contexts. + +recompute : {{oA : A ⫫[ ⊥ ] B}} → Choice A B b → Recomputable A +recompute (ofʸ a) _ = a +recompute (ofⁿ b) a = ⊥-elim-irr (byOrthogonality a b) + +recompute-constant : + {{oA : A ⫫[ ⊥ ] B}} (r : Choice A B b) (p q : A) → + recompute r p ≡ recompute r q +recompute-constant = Recomputable.recompute-constant ∘ recompute + +------------------------------------------------------------------------ +-- Interaction with true, false, negation, product, sums etc. + +⊥ˡ-choice : Choice A (¬ (⊥ˡ {ℓb})) false +⊥ˡ-choice = ofⁿ λ () + +⊥ˡ-reflects : Reflects (⊥ˡ {ℓa}) false +⊥ˡ-reflects = ⊥ˡ-choice + +⊤ˡ-choice : Choice (⊤ˡ {ℓa}) B true +⊤ˡ-choice = ofʸ _ + +⊤ˡ-reflects : Reflects (⊤ˡ {ℓa}) true +⊤ˡ-reflects = ⊤ˡ-choice + +⊥-choice : Choice A (¬ ⊥) false +⊥-choice = ofⁿ λ () + +⊥-reflects : Reflects ⊥ false +⊥-reflects = ⊥-choice + +⊤-choice : Choice ⊤ B true +⊤-choice = ofʸ _ + +⊤-reflects : Reflects ⊤ true +⊤-reflects = ⊤-choice + +∁-choice : Choice A B b → Choice B A (not b) +∁-choice (ofʸ a) = ofⁿ a +∁-choice (ofⁿ b) = ofʸ b + +¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b) +¬-reflects = map id ¬¬-η ∘′ ∁-choice + +T-choice : (b : Bool) → Choice (T b) (T (not b)) b +T-choice true = ⊤-choice +T-choice false = ∁-choice ⊤-choice + +-- This could also be implemented using map over T-choice +-- if only we had a conveniently accessible proof of +-- T (not b) → ¬ T b +T-reflects : ∀ b → Reflects (T b) b +T-reflects true = ⊤-choice +T-reflects false = ⊥-choice + +infixr 2 _×-choice_ _!×-choice_ + +_×-choice_ : Choice A ¬A a → Choice B ¬B b → + Choice (A × B) (¬A ⊎ ¬B) (a ∧ b) +ofʸ a ×-choice ofʸ b = ofʸ (a , b) +ofʸ a ×-choice ofⁿ ¬b = ofⁿ (inj₂ ¬b) +ofⁿ ¬a ×-choice _ = ofⁿ (inj₁ ¬a) + +_×-reflects_ : Reflects A a → Reflects B b → Reflects (A × B) (a ∧ b) +ra ×-reflects rb = map₂ + [ contraposition proj₁ + , contraposition proj₂ + ]′ (ra ×-choice rb) + +_!×-choice_ : Choice A ¬A a → Choice B ¬B b → + Choice (A × B) (¬A ⊎ (A × ¬B)) (a ∧ b) +ofʸ a !×-choice ofʸ b = ofʸ (a , b) +ofʸ a !×-choice ofⁿ ¬b = ofⁿ (inj₂ (a , ¬b)) +ofⁿ ¬a !×-choice _ = ofⁿ (inj₁ ¬a) + +_⊎-choice_ : Choice A ¬A a → Choice B ¬B b → + Choice (A ⊎ B) (¬A × ¬B) (a ∨ b) +ofʸ a ⊎-choice _ = ofʸ (inj₁ a) +ofⁿ ¬a ⊎-choice ofʸ b = ofʸ (inj₂ b) +ofⁿ ¬a ⊎-choice ofⁿ ¬b = ofⁿ (¬a , ¬b) + +_→-choice_ : + {{oA : A ⫫[ ⊥ ] ¬A}} → + Choice A ¬A a → Choice B ¬B b → + Choice (A → B) (A × ¬B) (not a ∨ b) +ofʸ a →-choice ofʸ b = ofʸ (const b) +ofʸ a →-choice ofⁿ ¬b = ofⁿ (a , ¬b) +ofⁿ ¬a →-choice _ = ofʸ (λ a → byOrthogonality 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 + +-- `Choice` is deterministic on orthogonal types. +det : {{oA : A ⫫[ ⊥ ] ¬A}} → Choice A ¬A a → Choice A ¬A b → a ≡ b +det (ofʸ a) (ofʸ _) = refl +det (ofʸ a) (ofⁿ ¬a) = byOrthogonality a ¬a +det (ofⁿ ¬a) (ofʸ a) = byOrthogonality a ¬a +det (ofⁿ ¬a) (ofⁿ _) = refl + +T-reflects-elim : Reflects (T a) b → b ≡ a +T-reflects-elim {a} r = det r (T-reflects a) diff --git a/src/Relation/Nullary/Choose/Core.agda b/src/Relation/Nullary/Choose/Core.agda new file mode 100644 index 0000000000..8f39b61a87 --- /dev/null +++ b/src/Relation/Nullary/Choose/Core.agda @@ -0,0 +1,238 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Operations on and properties of decidable relations +-- +-- This file contains some core definitions which are re-exported by +-- Relation.Nullary.Choose +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Relation.Nullary.Choose.Core where + +{- +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) +-} + +open import Data.Bool.Base using (Bool; true; false) + +open import Relation.Nullary.Orthogonal using (_⫫[_]_) +open import Relation.Nullary.Choice2 as Choice + +open import Level using (Level; _⊔_) + +private + variable + ℓa ℓaⁿ ℓb ℓbⁿ p q : Level + A : Set ℓa + ¬A : Set ℓaⁿ + B : Set ℓb + ¬B : Set ℓbⁿ + a b : Bool + +------------------------------------------------------------------------ +-- 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 Choose (A : Set ℓa) (¬A : Set ℓaⁿ) : Set (ℓa ⊔ ℓaⁿ) where + constructor _because_ + field + does : Bool + proof : Choice A ¬A does + +open Choose public + +pattern yes a = true because ofʸ a +pattern no ¬a = false because ofⁿ ¬a + +{- +------------------------------------------------------------------------ +-- Flattening + +module _ {A : Set ℓa} {P : Set p} {¬A : Set ℓaⁿ} {oA : A ⫫[ P ] ¬A} where + + From-yes : Choose A P ¬A oA → Set a + From-yes (true because _) = A + From-yes (false because _) = ⊤ + + From-no : Choose A P ¬A oA → 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 _⊎?_ +infixr 2 _×?_ _→?_ + +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 {a} ⊤ +does ⊤? = true +proof ⊤? = ⊤-reflects + +_×?_ : Dec A → Dec B → Dec (A × B) +does (a? ×? b?) = does a? ∧ does b? +proof (a? ×? b?) = proof a? ×-reflects proof b? + +⊥? : Dec {a} ⊥ +does ⊥? = false +proof ⊥? = ⊥-reflects + +_⊎?_ : Dec A → Dec B → Dec (A ⊎ B) +does (a? ⊎? b?) = does a? ∨ does b? +proof (a? ⊎? b?) = proof a? ⊎-reflects proof b? + +_→?_ : Dec A → Dec B → Dec (A → B) +does (a? →? b?) = not (does a?) ∨ does b? +proof (a? →? 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 ¬¬-η (¬? ¬¬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))) + + +-} diff --git a/src/Relation/Nullary/Orthogonal.agda b/src/Relation/Nullary/Orthogonal.agda index 36ca8ffcdc..725a51a1cf 100644 --- a/src/Relation/Nullary/Orthogonal.agda +++ b/src/Relation/Nullary/Orthogonal.agda @@ -48,6 +48,9 @@ record _⫫[_]_ (A : Set a) (P : Set p) (B : Set b) : Set (p ⊔ a ⊔ b) where co-orthogonal = flip orthogonal open _⫫[_]_ public +byOrthogonality : {{A ⫫[ ⊥ ] ¬A}} → A → ¬A → B +byOrthogonality {{oA}} a ¬a = ⊥-elim (oA .orthogonal a ¬a) + ------------------------------------------------------------------------ -- Base cases @@ -64,8 +67,10 @@ Truth false .orthogonal = ⊥-elim Truth true .orthogonal = flip ⊥-elim -- A type is always orthogonal to its negation -negation : (A : Set a) → A ⫫[ P ] ¬ A -negation A .orthogonal = contradiction +instance + + negation : A ⫫[ P ] ¬ A + negation .orthogonal = contradiction -- If our notion of orthogonality is with respect to ⊤ then any -- two things are related