lec18.lean

/-
Lecture 18:

Predicate logic
     ---
first steps in Lean


Contents:

1. Predicates in Lean
2. Quantifiers in Lean
3. Inference rules for quantifiers in Lean

-/


------------------------------
----PREDICATES IN LEAN--------
------------------------------

/-
In predicate logic, there is always a DOMAIN OF REASONING.
Predicates are propositions that depend on a parameter
from that domain.

In Lean:
- a domain is called a "Type"
- a predicate is a function from the domain to the type Prop

-/

section domain

variable U : Type
variable P : U → Prop
variable Q : U → U → Prop

variables x y : U

#check P x
--P x : Prop
#check Q x y
--Q x y : Prop

end domain

--Let's look at some examples of domains and predicates:

section examples

#check ℕ
--ℕ : Type
--type of natural numbers
-- to enter, type \ nat

variable is_even: ℕ → Prop

#check is_even 2   --is_even 2 : Prop
#check is_even 5   --is_even 5 : Prop

variable n : ℕ
#check is_even n   --is_even n : Prop

variable is_greater_than : ℕ → ℕ → Prop

#check is_greater_than 2 3   --is_greater_than 2 3 : Prop

#check is_greater_than n   --is_greater_than n : ℕ → Prop

--Another example of domain

#check list ℕ   --list ℕ : Type

variable is_empty : list ℕ → Prop
variable has_length : list ℕ → ℕ → Prop

#check [7,5,3]   --[7, 5, 3] : list ℕ

#check is_empty [7, 5, 3]   --is_empty [7, 5, 3] : Prop

#check has_length [7, 5, 3] 6   --has_length [7, 5, 3] 6 : Prop

end examples

/-
Remark:
The arrow "→" in "U → Prop" is the same as the one we use for implication.

Also, the application of a predicate to an element x : U,
denoted by juxtaposition "P x",
is the same concept as implication-elimination.

This will be made precise in a later lecture.
-/



------------------------------
----QUANTIFIERS IN LEAN-------
------------------------------

--We start with some examples:

section quantifiers

variable is_even : ℕ → Prop

#check ∃ x : ℕ, is_even x   --∃ (x : ℕ), is_even x : Prop
#check ∃ x, is_even x    --∃ (x : ℕ), is_even x : Prop
-- written \ exists

/-
Observation: in Lean, the domain a quantifier ranges over is
always recorded, even if we leave it implicit
-/

#check ∀ x : ℕ, is_even x  --∀ (x : ℕ), is_even x : Prop
-- written \ forall

variable is_greater_than : ℕ → ℕ → Prop

#check ∀ x, ∃ y, is_greater_than x y
--∀ (x : ℕ), ∃ (y : ℕ), is_greater_than x y : Prop

end quantifiers


--How to put parentheses
--in a formula?

section parsing

variable U : Type
variable P : U → Prop
variable Q : U → Prop
variable A : Prop

#check (∀ x, P x) → A
#check ∀ x, (P x → A)
#check ∀ x, P x → A
--The last two are synonymous

#check ∀ x, P x → Q x
--#check (∀ x, P x) → Q x
--This last one does not work, because the "x" in "Q x" is unknown to Lean:
--It is not in the scope of the quantifier ∀.

#check ∃ x, (P x → A)
#check ∃ x, P x → A
--The above two are synonymous

#check ∃ x, P x → Q x
--#check (∃ x, P x) → Q x


--General rule: anything after "∃ x" or "∀ x" can use "x", unless the scope of ∃ or ∀ is restricted by parentheses.

end parsing



section politicians

variable people : Type
variable trusts : people → people → Prop
variable politician : people → Prop
variable crazy : people → Prop
variable knows : people → people → Prop
variable related_to : people → people → Prop
variable rich : people → Prop

--Nobody trusts a politician
#check ¬ ∃ x : people, ∃ y : people, politician y ∧ trusts x y

--Anyone who trusts a politician is crazy.

--Everyone knows someone who is related to a politician.

--Everyone who is rich is either a politician or knows a politician.


end politicians

--Scroll down for the answers






































--#check ∀ x : people, (∃ y, politician y ∧ trusts x y) → crazy x
--#check ∀ x : people, ∃ y : people, knows x y ∧ (∃ z : people, politician z ∧ related_to y z)
--#check ∀ x, rich x → (politician x ∨ ∃ y, knows x y ∧ politician y)












------------------------------
----INFERENCE RULES IN LEAN---
------------------------------


------------------------------
----∀ introduction------------
------------------------------


/-
How to prove a formula starting with a ∀ ?

As always, use the corresponding INTRODUCTION rule!

On paper, that inference rule looks like this:


  P (t)
--------- ∀ - introduction
∀ x, P (x)

Here, the variable t must be *general*.

We usually use this rule *from bottom to top* (backwards reasoning).
When doing so, we simply choose a variable of our liking.

In Lean, this looks like this:

-/

section forall_introduction

variable U : Type
variable P : U → Prop

example : ∀ x, P x := assume t : U, _

--Read "assume t : U" as "fix an arbitrary value t of U".
--Instead of t, we could call it anything else, e.g.,

example : ∀ x, P x := assume y : U, _

--Of course, we cannot finish this proof without further assumptions.

--Note that forall-introduction is similar to implication-introduction in Lean.

end forall_introduction








------------------------------
----∀ elimination-------------
------------------------------

/-
How to use a formula starting with a ∀ ?

As always, use the corresponding ELIMINATION rule!

On paper, that inference rule looks like this:

∀ x, P (x)
--------- ∀ - elimination
 P (t)

We usually use this rule *from top to bottom* (forwards reasoning).
When doing so, we simply replace all the *free* occurrences of x in P(x) by t.

In Lean, this looks like this:

-/

section forall_elimination

variable U : Type
variable P : U → Type

variable h : ∀ x, P x
variable a : U

example : P a := h a

--Note that forall-elimination is similar to implication-elimination in Lean.

end forall_elimination






------------------------------
----∃ introduction------------
------------------------------


/-

How to prove a formula starting with a ∃ ?

As always, use the corresponding INTRODUCTION rule!

On paper, that inference rule looks like this:


  P (t)
--------- ∃ - introduction
∃ x, P (x)

We usually use this rule *from bottom to top* (backwards reasoning).
When doing so, we simply choose a variable of our liking.

In Lean, this looks like this:

-/

section exists_introduction

variable U : Type
variable P : U → Prop

variable y : U
variable p : P y

example : ∃ x, P x := exists.intro y p

--That is, to prove ∃ x, P x, we have to provide a specific y : U and a proof of P y

/-
∃ introduction is similar to ∨ introduction:
we have to pick a y : U (analogous to picking left or right) and then
prove P y (analogous to proving the left or right side).
If we make the wrong choice, we might end up with an unprovable goal!

Example: when proving
∃ n : nat, is_even n
picking n to be 3 is an unwise choice, since
is_even 3
will be impossible to prove.
-/

end exists_introduction




------------------------------
----∃ elimination-------------
------------------------------

/-
How to use a formula starting with a ∃ ?

As always, use the corresponding ELIMINATION rule!

On paper, that inference rule looks like this:


               P(t)
               ---
                .
                .
               ---
∃ x, P (x)      C
---------------------- ∃ - elimination
          C

Intuition: when using a proof ∃ x : U, P x, we can assume having some
t : U and a proof of P(t).
But t must be *general*: we do not know anything about t except that
it satisfies P, i.e., that we have proof of P(t).

In Lean, this looks like this:

-/

section exists_elimination

variable U : Type
variable P : U → Prop
variable C : Prop

example (h1 : ∃ x, P x) : C := 
exists.elim h1 
  (assume t : U,
   assume p : P t,
   _)

/-

At this stage, the situation looks very much like the top-right
side of the inference rule above:

       P(t)
       ---
        .
        .
       ---
        C

-/

end exists_elimination




------------------------------
----EXAMPLE PROOFS------------
------------------------------


section examples

variable U : Type
variables P Q : U → Prop

example :
 (∀ x, P x) → (∀ x, P x ∨ Q x) :=
  _

/-
assume h : ∀ x, P x,
assume t : U,
or.intro_left (Q t)
              (h t)
-/

example :
(∃ x, P x ∧ Q x) → (∃ x, Q x) :=
_

/-
assume h : ∃ x, P x ∧ Q x,
exists.elim h 
 (assume t : U,
  assume k : P t ∧ Q t,
  exists.intro t (and.elim_right k))
-/
end examples