{- 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