{-
Computer Aided Formal Reasoning (G53CFR, G54CFR)
Thorsten Altenkirch

Lecture 7: Basic Predicate Logic

In this lecture we extend the Curry-Howard correspondence to
predicate logic. To do this we need to use dependent types which we
have already seen in programming, e.g. Vec and Fin.

-}
module l07 where

open import l05 -- we are going to use the definitions for propositional logic

{-
What are predicates and relations?

Given A : Set a predicate is an element of A → Prp
a relation over A is an element of A → A → Prp

Examples:
Odd : ℕ → Prp
Prime : ℕ → Prp
_≡_ : ℕ → ℕ → Prp ( being equal, we use ≡ not to confuse equality
with definitions (=)).
_≡_ : {A : Set} → A → A → Prp (polymorphic equality)
_<_ : ℕ → ℕ → Prp
_≡_mod2 : ℕ → ℕ → Prp (equality modulo 2, both are even or both are
odd. )
_∈_ : {A : Set} → A → List A → Prp (occurs relation, a ∈ as means a
occurs in the list as.)
-}

{- Universal quantification: given a set A, and a predicate P : A → Prp
∀' A P : Prop means that P a is true (inhabited) for all a:A.
A proof of this is a (depndent) function which assigns to any a:A
an element of P a.
We have seen dependent functions before, e.g.
max : (n : ℕ) → Fin (suc n)
-}
∀' : (A : Set) → (A → Prp) → Prp
∀' A P = (a : A) → P a

{- Note: we use ∀' because ∀ is a reserved word in Agda. -}

{- Existential quantification: given a set A, and a predicate P : A → Prp
∀' A P : Prop means that P a is true (inhabited) for some a:A.
A proof of this is a (depndent) pair (a , p) where a : A and
p : P a is a proof that P a is true (inhabited).
-}
data ∃ (A : Set)(P : A → Prp) : Prp where
_,_ : (a : A) → P a → ∃ A P

{- for convenience we are going to use fst and snd. -}

fst : {P Q : Prp} → P ∧ Q ⇒ P
fst (p , q) = p

snd : {P Q : Prp} → P ∧ Q ⇒ Q
snd (p , q) = q

{- As an example we show that ∀ commutes with ∧
"Everybody has glasses and a watch is equivalent to
everybody has glasses and everybody has a watch."
-}

∀∧-lem-1 : {A : Set}{P Q : A → Prp} →
(∀' A λ a → P a ∧ Q a) ⇒ (∀' A λ a → P a) ∧ (∀' A λ a → Q a)
∀∧-lem-1 pq = (λ a → fst (pq a)) , (λ a → snd (pq a))

∀∧-lem-2 : {A : Set}{P Q : A → Prp} →
(∀' A λ a → P a) ∧ (∀' A λ a → Q a) ⇒ (∀' A λ a → P a ∧ Q a)
∀∧-lem-2 (p , q) = λ a → (p a) , (q a)

∀∧-lem : {A : Set}{P Q : A → Prp} →
(∀' A λ a → P a ∧ Q a) ⇔ (∀' A λ a → P a) ∧ (∀' A λ a → Q a)
∀∧-lem = ∀∧-lem-1 , ∀∧-lem-2

{- We noticed that ∀ does not commute with ∨. The following direction
fails:
-}

{-
∀∨-lem-1 : {A : Set}{P Q : A → Prp} →
(∀' A λ a → P a ∨ Q a) ⇒ (∀' A λ a → P a) ∨ (∀' A λ a → Q a)
∀∨-lem-1 pq = left (λ a → {!!})
-}

{- Intuitively: If everybody has a watch or glasses, it is not
necesserially true that everybody has a watch or everybody has
glasses. There may be somebody who has only got a watch and
somebody else who only has got glasses.
-}

{- However, ∃ does commute with ∨.
I leave the proof as an exercise.
Can you come up with an intuitive explanation?

∃∨-lem : {A : Set}{P Q : A → Prp} → (∃ A λ a → P a ∨ Q a) ⇔ (∃ A λ a → P a) ∨ (∃ A λ a → Q a)
∃∨-lem = {!!}
-}

{- Next we are going to show a lemma which relates ∀ and ∃.
Intuitively: If anybody understands the course then I am happy
is equivelent to If there exists somebody who understands the
course then I am happy.
-}

∀∃-lem-1 : {A : Set}{P : A → Prp}{Q : Prp} →
(∀' A λ a → P a ⇒ Q) ⇒ (∃ A λ a → P a) ⇒ Q
∀∃-lem-1 pq (a , p) = pq a p

∀∃-lem-2 : {A : Set}{P : A → Prp}{Q : Prp} →
((∃ A λ a → P a) ⇒ Q) ⇒ (∀' A λ a → P a ⇒ Q)
∀∃-lem-2 pq = λ a p → pq (a , p)

∀∃-lem : {A : Set}{P : A → Prp}{Q : Prp} →
(∀' A λ a → P a ⇒ Q) ⇔ (∃ A λ a → P a) ⇒ Q
∀∃-lem = ∀∃-lem-1 , ∀∃-lem-2

{- Note that the proofs look identical to one of the exercises on
propositional logic:

P ⇒ Q => R  ⇔ P ∧ Q ⇒ R
-}

{- Equality: We are going to define polymorphic equality using CH.

In future we use
open import Relation.Binary.PropositionalEquality
-}

infix 4 _≡_ -- \equiv

{- We define a dependent type where the only proof of equality is
reflexivity, which for any element a:A proves that a ≡ a. -}

data _≡_ {A : Set} : A → A → Prp where
refl : {a : A} → a ≡ a

{- Using pattern matching we can prove that ≡ is symmetric & transitive
and hence an equivalence relation (because refl proves reflexivity)/ -}

sym : {A : Set} → {a b : A} → a ≡ b ⇒ b ≡ a
sym refl = refl

trans : {A : Set}{a b c : A} → a ≡ b ⇒ b ≡ c ⇒ a ≡ c
trans p refl = p

{- Any function respects equality: -}

resp : {A B : Set}{f : A → B}{a b : A} → a ≡ b ⇒ f a ≡ f b
resp refl = refl

{- But not every function is injective. -}

{-
resp' : {A B : Set}{f : A → B}{a b : A} →  f a ≡ f b ⇒ a ≡ b
resp' p = {!p!}
-}

{- Agda rejects the attempt to pattern match on f a ≡ f b.
While it is correct that refl is the only proof of this
type, we cannot conclude that a ≡ b. -}

{- We prove a very general property: substitutivity.
The other properties we have mentioned are derivable
from this one. -}

subst : {A : Set}{P : A → Prp} → {a b : A} → a ≡ b ⇒ P a ⇒ P b
subst refl p = p