------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to negation
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Relation.Nullary.Negation where

open import Effect.Monad using (RawMonad; mkRawMonad)
open import Data.Bool.Base using (Bool; false; true; if_then_else_; not)
open import Data.Empty using (⊥-elim)
open import Data.Product.Base as Prod using (_,_; Σ; Σ-syntax; ; curry; uncurry)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Function.Base using (flip; _∘_; const; _∘′_)
open import Level using (Level)
open import Relation.Nullary.Decidable.Core using (Dec; yes; no; ¬¬-excluded-middle)
open import Relation.Unary using (Universal; Pred)

private
  variable
    a b c d p w : Level
    A B C D : Set a
    P : Pred A p
    Whatever : Set w

------------------------------------------------------------------------
-- Re-export public definitions

open import Relation.Nullary.Negation.Core public

------------------------------------------------------------------------
-- Quantifier juggling

∃⟶¬∀¬ :  P  ¬ (∀ x  ¬ P x)
∃⟶¬∀¬ = flip uncurry

∀⟶¬∃¬ : (∀ x  P x)  ¬  λ x  ¬ P x
∀⟶¬∃¬ ∀xPx (x , ¬Px) = ¬Px (∀xPx x)

¬∃⟶∀¬ : ¬   x  P x)   x  ¬ P x
¬∃⟶∀¬ = curry

∀¬⟶¬∃ : (∀ x  ¬ P x)  ¬   x  P x)
∀¬⟶¬∃ = uncurry

∃¬⟶¬∀ :   x  ¬ P x)  ¬ (∀ x  P x)
∃¬⟶¬∀ = flip ∀⟶¬∃¬

------------------------------------------------------------------------
-- Double Negation

-- Double-negation is a monad (if we assume that all elements of ¬ ¬ P
-- are equal).

¬¬-Monad : RawMonad {a} DoubleNegation
¬¬-Monad = mkRawMonad
  DoubleNegation
  contradiction
   x f  negated-stable (¬¬-map f x))

¬¬-push : DoubleNegation Π[ P ]  Π[ DoubleNegation  P ]
¬¬-push ¬¬∀P a ¬Pa = ¬¬∀P  ∀P  ¬Pa (∀P a))

-- If Whatever is instantiated with ¬ ¬ something, then this function
-- is call with current continuation in the double-negation monad, or,
-- if you will, a double-negation translation of Peirce's law.
--
-- In order to prove ¬ ¬ P one can assume ¬ P and prove ⊥. However,
-- sometimes it is nice to avoid leaving the double-negation monad; in
-- that case this function can be used (with Whatever instantiated to
-- ⊥).

call/cc : ((A  Whatever)  DoubleNegation A)  DoubleNegation A
call/cc hyp ¬a = hyp  a  ⊥-elim (¬a a)) ¬a

-- The "independence of premise" rule, in the double-negation monad.
-- It is assumed that the index set (A) is inhabited.

independence-of-premise : A  (B  Σ A P)  DoubleNegation (Σ[ x  A ] (B  P x))
independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-excluded-middle
  where
  helper : Dec B  Σ[ x  A ] (B  P x)
  helper (yes p) = Prod.map₂ const (f p)
  helper (no ¬p) = (q , ⊥-elim ∘′ ¬p)

-- The independence of premise rule for binary sums.

independence-of-premise-⊎ : (A  B  C)  DoubleNegation ((A  B)  (A  C))
independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-excluded-middle
  where
  helper : Dec A  (A  B)  (A  C)
  helper (yes p) = Sum.map const const (f p)
  helper (no ¬p) = inj₁ (⊥-elim ∘′ ¬p)

private

  -- Note that independence-of-premise-⊎ is a consequence of
  -- independence-of-premise (for simplicity it is assumed that Q and
  -- R have the same type here):

  corollary : {B C : Set b}  (A  B  C)  DoubleNegation ((A  B)  (A  C))
  corollary {A = A} {B = B} {C = C} f =
    ¬¬-map helper (independence-of-premise true ([ _,_ true , _,_ false ] ∘′ f))
    where
    helper :   b  A  if b then B else C)  (A  B)  (A  C)
    helper (true  , f) = inj₁ f
    helper (false , f) = inj₂ f