{-# OPTIONS --type-in-type #-}
open import NeilPrelude
open import Data.Bool
open import Properties
module Logic where
record True : Set where
absurd : {A : Set} → False → A
absurd ()
ProveTruth : {P : Set} → (True → P) → P
ProveTruth p = p _
↔-refl : Reflexive _↔_
↔-refl = id , id
↔-trans : Transitive _↔_
↔-trans = ×-map2 _⋙_ _∘_
↔-sym : Symmetric _↔_
↔-sym = swap
↔-≡ : {A : Set} → {a b c d : A} → (a ≡ c) → (b ≡ d) → (a ≡ b) ↔ (c ≡ d)
↔-≡ refl refl = id , id
infixr 1 _↔⟨_⟩_ _→⟨_⟩_ _←⟨_⟩_ _→⟨_⟩↔_ _←⟨_⟩↔_
infix 2 _qed _Qed _←⟨_⟩TRUE
_↔⟨_⟩_ : {B C : Set} → (A : Set) → A ↔ B → B ↔ C → A ↔ C
_↔⟨_⟩_ _ = ↔-trans
_→⟨_⟩_ : {B C : Set} → (A : Set) → (A → B) → (B → C) → (A → C)
_→⟨_⟩_ _ = _⋙_
_←⟨_⟩_ : {B C : Set} → (A : Set) → (B → A) → (C → B) → (C → A)
_←⟨_⟩_ _ = _∘_
_→⟨_⟩↔_ : {B C : Set} → (A : Set) → (A ↔ B) → (B → C) → (A → C)
_→⟨_⟩↔_ _ = λ ab bc → bc ∘ fst ab
_←⟨_⟩↔_ : {B C : Set} → (A : Set) → (B ↔ A) → (C → B) → (C → A)
_←⟨_⟩↔_ _ = λ ab cb → fst ab ∘ cb
_←⟨_⟩TRUE : (A : Set) → A → (True → A)
_←⟨_⟩TRUE _ a _ = a
_qed : (A : Set) → (A ↔ A)
_ qed = ↔-refl
_Qed : (A : Set) → (A → A)
_ Qed = id
≡→↔ : {A B : Set} → A ≡ B → A ↔ B
≡→↔ refl = ↔-refl
isTrue : Bool → Set
isTrue true = True
isTrue false = False
magic : {A : Set} → (True → False) → A
magic p = absurd (p _)
Sat : {A : Set} → (A → Bool) → A → Set
Sat p = isTrue ∘ p
isFalse : Bool → Set
isFalse = Sat not
trueIsTrue : {b : Bool} → b ≡ true → isTrue b
trueIsTrue refl = _
falseIsFalse : {b : Bool} → b ≡ false → isFalse b
falseIsFalse refl = _
isJust : {A : Set} → Maybe A → Bool
isJust nothing = false
isJust (just _) = true
isNothing : {A : Set} → Maybe A → Bool
isNothing nothing = true
isNothing (just _) = false
IsJust : {A : Set} → Maybe A → Set
IsJust = Sat isJust
IsNothing : {A : Set} → Maybe A → Set
IsNothing = Not ∘ IsJust
lem-isNothing : {A : Set} → {ma : Maybe A} → IsNothing ma → ma ≡ nothing
lem-isNothing {_} {nothing} _ = refl
lem-isNothing {_} {just _} p = magic p
lem-isNothingEq : {A : Set} → {ma mb : Maybe A} → IsNothing ma → IsNothing mb → ma ≡ mb
lem-isNothingEq p q = trans (lem-isNothing p) (sym (lem-isNothing q))
lem-just≠nothing : {A : Set} → {a : A} → just a ≢ nothing
lem-just≠nothing ()
implDist : {P Q R : Set} → (P ⊎ Q → R) → (P → R) × (Q → R)
implDist = λ f → f ∘ inl , f ∘ inr
implDistR : {P Q R : Set} → (P → R) × (Q → R) → (P ⊎ Q → R)
implDistR = λ pq → case (fst pq) (snd pq)
NotNot : {P : Set} → P → Not (Not P)
NotNot = applyTo
contpos : {P Q : Set} → (P → Q) → (Not Q → Not P)
contpos = _⋙_
nn-antecedent : {P Q : Set} → (Not (Not P) → Q) → (P → Q)
nn-antecedent = argument applyTo
nn-consequent : {P Q : Set} → (P → Q) → (P → Not (Not Q))
nn-consequent f = applyTo ∘ f
impl-contr : {P Q : Set} → (P → Q) → P → Not Q → False
impl-contr f p nq = nq (f p)
ProofIrrelevence : Set → Set
ProofIrrelevence P = (p q : P) → p ≡ q
proofIrrelevence : {A : Set} → {a b : A} → ProofIrrelevence (a ≡ b)
proofIrrelevence refl refl = refl
EM : Set
EM = ∀ {P} → P ⊎ Not P
Decidable : Set → Set
Decidable P = P ⊎ Not P
em-isTrue : {b : Bool} → isTrue b ⊎ Not (isTrue b)
em-isTrue {false} = inr id
em-isTrue {true} = inl _
contradiction : {P : Set} → Decidable P → Not (Not P) → P
contradiction (inl p) nnp = p
contradiction (inr np) nnp = absurd (nnp np)
contpos-em : {P Q : Set} → Decidable P → (Not P → Not Q) → (Q → P)
contpos-em em f q = contradiction em (flip f q)
nn-antecedent-em : {P Q : Set} → Decidable P → (P → Q) → (Not (Not P) → Q)
nn-antecedent-em (inl p) f nnp = f p
nn-antecedent-em (inr np) f nnp = absurd (nnp np)
nn-consequent-em : {P Q : Set} → Decidable Q → (P → Not (Not Q)) → (P → Q)
nn-consequent-em em f p = contradiction em (f p)
notBoth : {P Q : Set} → Decidable P ⊎ Decidable Q → Not (P × Q) → Not P ⊎ Not Q
notBoth (inl (inl p)) nb = inr (λ q → nb (p , q))
notBoth (inl (inr np)) nb = inl np
notBoth (inr (inl q)) nb = inl (λ p → nb (p , q))
notBoth (inr (inr nq)) nb = inr nq
must-always-cur : {A : Set} → {P : A → Set} → EM → Π A (Not ∘ Not ∘ P) → Π A P
must-always-cur em npa a = contradiction em (npa a)
must-always : {A : Set} → {P : A → Set} → EM → Not (Σ A (Not ∘ P)) → Π A P
must-always em = must-always-cur em ∘ curry
must-exist : {A : Set} → {P : A → Set} → EM → Not (Π A (Not ∘ P)) → Σ A P
must-exist em nn = contradiction em (nn ∘ curry)
must-exist-not : {A : Set} → {P : A → Set} → EM → Not (Π A P) → Σ A (Not ∘ P)
must-exist-not em nap = must-exist em (λ f → nap (must-always-cur em f))
must-exist-not2 : {A : Set} → {B : A → Set} → {P : (a : A) → B a → Set} → EM → Not (Π₂ A B P) → Σ A (λ a → Σ (B a) (Not ∘ P a))
must-exist-not2 em = second' (must-exist-not em) ∘ must-exist-not em