------------------------------------------------------------------------
-- The Agda standard library
--
-- Core properties related to negation
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Relation.Nullary.Negation.Core where

open import Data.Bool.Base using (not)
open import Data.Empty
open import Data.Product
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function.Base using (flip; _$_; _∘_; const)
open import Level
open import Relation.Nullary
open import Relation.Unary using (Pred)

private
  variable
    a p q w : Level
    A : Set a
    P : Set p
    Q : Set q
    Whatever : Set w

------------------------------------------------------------------------
-- Uses of negation

contradiction : P  ¬ P  Whatever
contradiction p ¬p = ⊥-elim (¬p p)

contradiction₂ : P  Q  ¬ P  ¬ Q  Whatever
contradiction₂ (inj₁ p) ¬p ¬q = contradiction p ¬p
contradiction₂ (inj₂ q) ¬p ¬q = contradiction q ¬q

contraposition : (P  Q)  ¬ Q  ¬ P
contraposition f ¬q p = contradiction (f p) ¬q

-- Note also the following use of flip:

private
  note : (P  ¬ Q)  Q  ¬ P
  note = flip

-- 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

¬? : Dec P  Dec (¬ P)
does  (¬? p?) = not (does p?)
proof (¬? p?) = ¬-reflects (proof p?)

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

module _ {P : Pred A p} where

  ∃⟶¬∀¬ :  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

¬¬-map : (P  Q)  ¬ ¬ P  ¬ ¬ Q
¬¬-map f = contraposition (contraposition f)

-- Stability under double-negation.

Stable : Set p  Set p
Stable P = ¬ ¬ P  P

-- Everything is stable in the double-negation monad.

stable : ¬ ¬ Stable P
stable ¬[¬¬p→p] = ¬[¬¬p→p]  ¬¬p  ⊥-elim (¬¬p (¬[¬¬p→p]  const)))

-- Negated predicates are stable.

negated-stable : Stable (¬ P)
negated-stable ¬¬¬P P = ¬¬¬P  ¬P  ¬P P)