{-# OPTIONS --without-K --safe #-}
module Relation.Nullary.Negation where
open import Effect.Monad
open import Data.Bool.Base using (Bool; false; true; if_then_else_; not)
open import Data.Empty
open import Data.Product as Prod
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Function
open import Level
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Unary
private
variable
a p q r w : Level
A : Set a
P : Set p
Q : Set q
R : Set r
Whatever : Set w
open import Relation.Nullary.Negation.Core public
decidable-stable : Dec P → Stable P
decidable-stable (yes p) ¬¬p = p
decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)
¬-drop-Dec : Dec (¬ ¬ P) → Dec (¬ P)
¬-drop-Dec ¬¬p? = map′ negated-stable contradiction (¬? ¬¬p?)
¬¬-Monad : RawMonad (λ (P : Set p) → ¬ ¬ P)
¬¬-Monad = record
{ return = contradiction
; _>>=_ = λ x f → negated-stable (¬¬-map f x)
}
¬¬-push : ∀ {P : Set p} {Q : P → Set q} →
¬ ¬ ((x : P) → Q x) → (x : P) → ¬ ¬ Q x
¬¬-push ¬¬P⟶Q P ¬Q = ¬¬P⟶Q (λ P⟶Q → ¬Q (P⟶Q P))
excluded-middle : ¬ ¬ Dec P
excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))
call/cc : ((P → Whatever) → ¬ ¬ P) → ¬ ¬ P
call/cc hyp ¬p = hyp (λ p → ⊥-elim (¬p p)) ¬p
independence-of-premise : ∀ {P : Set p} {Q : Set q} {R : Q → Set r} →
Q → (P → Σ Q R) → ¬ ¬ (Σ[ x ∈ Q ] (P → R x))
independence-of-premise {P = P} q f = ¬¬-map helper excluded-middle
where
helper : Dec P → _
helper (yes p) = Prod.map id const (f p)
helper (no ¬p) = (q , ⊥-elim ∘′ ¬p)
independence-of-premise-⊎ : (P → Q ⊎ R) → ¬ ¬ ((P → Q) ⊎ (P → R))
independence-of-premise-⊎ {P = P} f = ¬¬-map helper excluded-middle
where
helper : Dec P → _
helper (yes p) = Sum.map const const (f p)
helper (no ¬p) = inj₁ (⊥-elim ∘′ ¬p)
private
corollary : {P : Set p} {Q R : Set q} →
(P → Q ⊎ R) → ¬ ¬ ((P → Q) ⊎ (P → R))
corollary {P = P} {Q} {R} f =
¬¬-map helper (independence-of-premise
true ([ _,_ true , _,_ false ] ∘′ f))
where
helper : ∃ (λ b → P → if b then Q else R) → (P → Q) ⊎ (P → R)
helper (true , f) = inj₁ f
helper (false , f) = inj₂ f