/usr/share/agda-stdlib/Relation/Nullary/Negation.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to negation
------------------------------------------------------------------------
module Relation.Nullary.Negation where
open import Relation.Nullary
open import Relation.Unary
open import Data.Bool
open import Data.Empty
open import Function
open import Data.Product as Prod
open import Data.Fin using (Fin)
open import Data.Fin.Dec
open import Data.Sum as Sum
open import Category.Monad
open import Level
contradiction : ∀ {p w} {P : Set p} {Whatever : Set w} →
P → ¬ P → Whatever
contradiction p ¬p = ⊥-elim (¬p p)
contraposition : ∀ {p q} {P : Set p} {Q : Set q} →
(P → Q) → ¬ Q → ¬ P
contraposition f ¬q p = contradiction (f p) ¬q
-- Note also the following use of flip:
private
note : ∀ {p q} {P : Set p} {Q : Set q} →
(P → ¬ Q) → Q → ¬ P
note = flip
-- If we can decide P, then we can decide its negation.
¬? : ∀ {p} {P : Set p} → Dec P → Dec (¬ P)
¬? (yes p) = no (λ ¬p → ¬p p)
¬? (no ¬p) = yes ¬p
------------------------------------------------------------------------
-- Quantifier juggling
∃⟶¬∀¬ : ∀ {a p} {A : Set a} {P : A → Set p} →
∃ P → ¬ (∀ x → ¬ P x)
∃⟶¬∀¬ = flip uncurry
∀⟶¬∃¬ : ∀ {a p} {A : Set a} {P : A → Set p} →
(∀ x → P x) → ¬ ∃ λ x → ¬ P x
∀⟶¬∃¬ ∀xPx (x , ¬Px) = ¬Px (∀xPx x)
¬∃⟶∀¬ : ∀ {a p} {A : Set a} {P : A → Set p} →
¬ ∃ (λ x → P x) → ∀ x → ¬ P x
¬∃⟶∀¬ = curry
∀¬⟶¬∃ : ∀ {a p} {A : Set a} {P : A → Set p} →
(∀ x → ¬ P x) → ¬ ∃ (λ x → P x)
∀¬⟶¬∃ = uncurry
∃¬⟶¬∀ : ∀ {a p} {A : Set a} {P : A → Set p} →
∃ (λ x → ¬ P x) → ¬ (∀ x → P x)
∃¬⟶¬∀ = flip ∀⟶¬∃¬
-- When P is a decidable predicate over a finite set the following
-- lemma can be proved.
¬∀⟶∃¬ : ∀ n {p} (P : Fin n → Set p) → Decidable P →
¬ (∀ i → P i) → ∃ λ i → ¬ P i
¬∀⟶∃¬ n P dec ¬P = Prod.map id proj₁ $ ¬∀⟶∃¬-smallest n P dec ¬P
------------------------------------------------------------------------
-- Double-negation
¬¬-map : ∀ {p q} {P : Set p} {Q : Set q} →
(P → Q) → ¬ ¬ P → ¬ ¬ Q
¬¬-map f = contraposition (contraposition f)
-- Stability under double-negation.
Stable : ∀ {ℓ} → Set ℓ → Set ℓ
Stable P = ¬ ¬ P → P
-- Everything is stable in the double-negation monad.
stable : ∀ {p} {P : Set p} → ¬ ¬ Stable P
stable ¬[¬¬p→p] = ¬[¬¬p→p] (λ ¬¬p → ⊥-elim (¬¬p (¬[¬¬p→p] ∘ const)))
-- Negated predicates are stable.
negated-stable : ∀ {p} {P : Set p} → Stable (¬ P)
negated-stable ¬¬¬P P = ¬¬¬P (λ ¬P → ¬P P)
-- Decidable predicates are stable.
decidable-stable : ∀ {p} {P : Set p} → Dec P → Stable P
decidable-stable (yes p) ¬¬p = p
decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)
¬-drop-Dec : ∀ {p} {P : Set p} → Dec (¬ ¬ P) → Dec (¬ P)
¬-drop-Dec (yes ¬¬p) = no ¬¬p
¬-drop-Dec (no ¬¬¬p) = yes (negated-stable ¬¬¬p)
-- Double-negation is a monad (if we assume that all elements of ¬ ¬ P
-- are equal).
¬¬-Monad : ∀ {p} → RawMonad (λ (P : Set p) → ¬ ¬ P)
¬¬-Monad = record
{ return = contradiction
; _>>=_ = λ x f → negated-stable (¬¬-map f x)
}
¬¬-push : ∀ {p q} {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))
-- A double-negation-translated variant of excluded middle (or: every
-- nullary relation is decidable in the double-negation monad).
excluded-middle : ∀ {p} {P : Set p} → ¬ ¬ Dec P
excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))
-- 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 : ∀ {w p} {Whatever : Set w} {P : Set p} →
((P → Whatever) → ¬ ¬ P) → ¬ ¬ P
call/cc hyp ¬p = hyp (λ p → ⊥-elim (¬p p)) ¬p
-- The "independence of premise" rule, in the double-negation monad.
-- It is assumed that the index set (Q) is inhabited.
independence-of-premise
: ∀ {p q r} {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)
-- The independence of premise rule for binary sums.
independence-of-premise-⊎
: ∀ {p q r} {P : Set p} {Q : Set q} {R : Set r} →
(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
-- 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 : ∀ {p ℓ} {P : Set p} {Q R : Set ℓ} →
(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
-- The classical statements of excluded middle and double-negation
-- elimination.
Excluded-Middle : (ℓ : Level) → Set (suc ℓ)
Excluded-Middle p = {P : Set p} → Dec P
Double-Negation-Elimination : (ℓ : Level) → Set (suc ℓ)
Double-Negation-Elimination p = {P : Set p} → Stable P
private
-- The two statements above are equivalent. The proofs are so
-- simple, given the definitions above, that they are not exported.
em⇒dne : ∀ {ℓ} → Excluded-Middle ℓ → Double-Negation-Elimination ℓ
em⇒dne em = decidable-stable em
dne⇒em : ∀ {ℓ} → Double-Negation-Elimination ℓ → Excluded-Middle ℓ
dne⇒em dne = dne excluded-middle
|