{- 
  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  _≡_ -- \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