module Martes where
prop : Set₁
prop = Set
K : {P Q : prop} → P → Q → P
K x y = x
S : {P Q R : prop} → (P → Q → R) → (P → Q) → P → R
S pqr pq p = pqr p (pq p)
I : {P : prop} → P → P
I x = x
B : {P Q R : prop} → (P → Q) → (Q → R) → P → R
B = λ pq qr p → qr (pq p)
C : {P Q R : prop} → (P → Q → R) → Q → P → R
C = λ x x' x0 → x x0 x'
I' : {P : prop} → P → P
I' {P} = S K (K {Q = P})
CB' : {P Q R : prop} → (Q → R) → (P → Q) → P → R
CB' = S (K S) K
C' : {P Q R : prop} → (P → Q → R) → Q → P → R
C' = S (S (K S) (S (K K) S)) (K K)
B' : {P Q R : prop} → (P → Q) → (Q → R) → P → R
B' = C' CB'
data _∧_ (P Q : prop) : prop where
_,_ : P → Q → P ∧ Q
infixr 2 _∧_
∧-comm : {P Q : prop} → P ∧ Q → Q ∧ P
∧-comm (p , q) = q , p
data _∨_ (P Q : prop) : prop where
left : P → P ∨ Q
right : Q → P ∨ Q
distrib→ : {P Q R : prop} → P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)
distrib→ (p , left q) = left (p , q)
distrib→ (p , right r) = right (p , r)
distrib← : {P Q R : prop} → (P ∧ Q) ∨ (P ∧ R) → P ∧ (Q ∨ R)
distrib← (left (p , q)) = p , left q
distrib← (right (p , r)) = p , right r
_⇔_ : prop → prop → prop
P ⇔ Q = (P → Q) ∧ (Q → P)
infixr 0 _⇔_
distrib⇔ : {P Q R : prop} → P ∧ (Q ∨ R) ⇔ (P ∧ Q) ∨ (P ∧ R)
distrib⇔ = distrib→ , distrib←
curry→ : {P Q R : prop} → (P ∧ Q → R) → (P → Q → R)
curry→ pqr p q = pqr (p , q)
curry← : {P Q R : prop} → (P → Q → R) → (P ∧ Q → R)
curry← pqr (p , q) = pqr p q
curry⇔ : {P Q R : prop} → (P ∧ Q → R) ⇔ (P → Q → R)
curry⇔ = curry→ , curry←
∨∧→ : {P Q R : prop} → (P ∨ Q → R) → ((P → R) ∧ (Q → R))
∨∧→ pqr = (λ p → pqr (left p)) , λ q → pqr (right q)
∨∧← : {P Q R : prop} → ((P → R) ∧ (Q → R)) → (P ∨ Q → R)
∨∧← (pr , qr) (left p) = pr p
∨∧← (pr , qr) (right q) = qr q
∨∧ : {P Q R : prop} → (P ∨ Q → R) ⇔ ((P → R) ∧ (Q → R))
∨∧ = ∨∧→ , ∨∧←
fst : {A B : prop} → A ∧ B → A
fst (a , b) = a
snd : {A B : prop} → A ∧ B → B
snd (a , b) = b
case : {A B C : prop} → (A → C) → (B → C) → A ∨ B → C
case ac bc (left a) = ac a
case ac bc (right b) = bc b
or-com : {P Q : prop} → P ∨ Q → Q ∨ P
or-com = case right left
copy : {A : prop} → A ⇔ A ∧ A
copy = (λ x → (x , x)) , (λ x → fst x)
data ⊤ : prop where
tt : ⊤
data ⊥ : prop where
efq : {P : prop} → ⊥ → P
efq ()
¬ : prop → prop
¬ P = P → ⊥
contradict : {P : prop} → ¬ (P ∧ ¬ P)
contradict (p , np) = np p
contrapos : {P Q : prop} → (P → Q) → ¬ Q → ¬ P
contrapos pq nq p = nq (pq p)
paradox : {P : prop} → ¬ (P ⇔ ¬ P)
paradox (pnp , npp) = pnp (npp (λ x → pnp x x)) (npp (λ x → pnp x x))
deMorgan¬∨ : {P Q : prop} → ¬ (P ∨ Q) → ¬ P ∧ ¬ Q
deMorgan¬∨ npq = (λ p → npq (left p)) , λ q → npq (right q)
deMorgan¬∧¬ : {P Q : prop} → (¬ P) ∧ (¬ Q) → ¬ (P ∨ Q)
deMorgan¬∧¬ (np , nq) (left p) = np p
deMorgan¬∧¬ (np , nq) (right q) = nq q
deMorgan¬∨¬ : {P Q : prop} → (¬ P) ∨ (¬ Q) → ¬ (P ∧ Q)
deMorgan¬∨¬ (left np) (p , q) = np p
deMorgan¬∨¬ (right nq) (p , q) = nq q
¬¬ : prop → prop
¬¬ P = ¬ (¬ P)
pnnp : {P : prop} → P → ¬¬ P
pnnp p np = np p
¬¬tnd : {P : prop} → ¬¬ (P ∨ ¬ P)
¬¬tnd npnp = npnp (right (λ p → npnp (left p)))
TND : Set₁
TND = {P : prop} → P ∨ ¬ P
RAA : Set₁
RAA = {P : prop} → ¬¬ P → P
RAA→TND : RAA → TND
RAA→TND raa = raa ¬¬tnd
TND→RND : TND → RAA
TND→RND tnd {P} nnp with tnd {P}
TND→RND tnd nnp | left p = p
TND→RND tnd nnp | right np = efq (nnp np)
ret¬¬ : {P : prop} → P → ¬¬ P
ret¬¬ p np = np p
bind¬¬ : {P Q : prop} → ¬¬ P → (P → ¬¬ Q) → ¬¬ Q
bind¬¬ nnp pnnq nq = nnp (λ p → pnnq p nq)
map¬¬ : {P Q : prop} → ¬¬ P → (P → Q) → ¬¬ Q
map¬¬ np pq = bind¬¬ np (λ p → ret¬¬ (pq p))
app¬¬ : {P Q : prop} → ¬¬ (P → Q) → ¬¬ P → ¬¬ Q
app¬¬ nnpq nnp = bind¬¬ nnpq (λ pq → bind¬¬ nnp (λ p → ret¬¬ (pq p)))
∧¬¬-1 : {P Q : prop} → ¬¬ (P ∧ Q) → ¬¬ P ∧ ¬¬ Q
∧¬¬-1 nnpq = map¬¬ nnpq fst , map¬¬ nnpq snd
∧¬¬-2 : {P Q : prop} → ¬¬ P ∧ ¬¬ Q → ¬¬ (P ∧ Q)
∧¬¬-2 (nnp , nnq) = bind¬¬ nnp (λ p → map¬¬ nnq (λ q → p , q))
∧¬¬ : {P Q : prop} → ¬¬ (P ∧ Q) ⇔ ¬¬ P ∧ ¬¬ Q
∧¬¬ = ∧¬¬-1 , ∧¬¬-2
∨¬¬-2 : {P Q : prop} → ¬¬ P ∨ ¬¬ Q → ¬¬ (P ∨ Q)
∨¬¬-2 (left np) = map¬¬ np left
∨¬¬-2 (right nq) = map¬¬ nq right
¬¬deMorgan¬∧ : {P Q : prop} → ¬ (P ∧ Q) → ¬¬ ((¬ P) ∨ (¬ Q))
¬¬deMorgan¬∧ npq = λ x → x (left (λ x' → x (right (λ x0 → npq (x' , x0)))))
∀∧ : {A : Set}{P Q : A → prop} →
((a : A) → P a ∧ Q a) → ((a : A) → P a) ∧ ((a : A) → Q a)
∀∧ pq = (λ a → fst (pq a)) , (λ a → snd (pq a))
∧∀ : {A : Set}{P Q : A → prop} →
((a : A) → P a) ∧ ((a : A) → Q a) → ((a : A) → P a ∧ Q a)
∧∀ (ap , aq) = λ a → (ap a , aq a)
∨∀ : {A : Set}{P Q : A → prop} →
((a : A) → P a) ∨ ((a : A) → Q a) → ((a : A) → P a ∨ Q a)
∨∀ (left ap) = λ a → left (ap a)
∨∀ (right aq) = λ a → right (aq a)
data ∃ (A : Set)(P : A → prop) : prop where
_,_ : (a : A) → P a → ∃ A P
∃∧ : {A : Set}{P Q : A → prop} →
(∃ A (λ a → P a ∧ Q a)) → (∃ A P) ∧ (∃ A Q)
∃∧ (a , (p , q)) = (a , p) , (a , q)
∃∨ : {A : Set}{P Q : A → prop} →
(∃ A (λ a → P a ∨ Q a)) → (∃ A P) ∨ (∃ A Q)
∃∨ (a , left p) = left (a , p)
∃∨ (a , right q) = right (a , q)
∨∃ : {A : Set}{P Q : A → prop} →
(∃ A P) ∨ (∃ A Q) → (∃ A (λ a → P a ∨ Q a))
∨∃ (left (a , p)) = a , left p
∨∃ (right (a , q)) = a , right q
deMorgan¬∃ : {A : Set}{P : A → prop} →
¬ (∃ A (λ x → P x)) → ((x : A) → ¬ (P x))
deMorgan¬∃ = λ x x' x0 → x (x' , x0)
deMorgan∀¬ : {A : Set}{P : A → prop} →
((x : A) → ¬ (P x)) → ¬ (∃ A (λ x → P x))
deMorgan∀¬ x (a , y) = x a y
deMorgan∃¬ : {A : Set}{P : A → prop} →
∃ A (λ x → ¬ (P x)) → ¬ ((x : A) → P x)
deMorgan∃¬ (a , y) = λ x → y (x a)
curry∀→ : {A : Set}{P : A → Set}{Q : prop}
→ ((∃ A P) → Q) → (a : A) → P a → Q
curry∀→ x = λ a x' → x (a , x')
curry∀← : {A : Set}{P : A → Set}{Q : prop}
→ ((a : A) → P a → Q) → ((∃ A P) → Q)
curry∀← x (a , y) = x a y
fst' : {A : Set}{P : A → prop} → ∃ A P → A
fst' (a , p) = a
snd' : {A : Set}{P : A → prop} → (p : ∃ A P) → P (fst' p)
snd' (a , p) = p
ac : {A B : Set}{R : A → B → prop} →
((a : A) → ∃ B λ b → R a b)
→ ∃ (A → B) λ f → (a : A) → R a (f a)
ac f = (λ a → fst' (f a)) , λ a → snd' (f a)
dac : {A : Set}{B : A → Set}{R : (a : A) → B a → Set}
→ ((a : A) → ∃ (B a) (λ b → R a b))
→ ∃ ((a : A) → B a) (λ f → (a : A) → R a (f a))
dac f = (λ a → fst' (f a)) , λ a → snd' (f a)