lec18-short-lines.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.
-/


/-
Exercise:
formulate a predicate
likes(x,y,z)
where 
x is a person,
y is an activity,
z is a place

Scroll down for one solution.
-/



section likes

variable people : Type
variable activity : Type
variable place : Type

variable likes : 
  people → activity → place → Prop

end likes


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

Hygiene: 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;

Lean takes care of hygiene.
It 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.

Lean takes care of variable
hygiene.

In Lean, this inference rule
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 choose a 
suitable t and prove P(t).

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 of A ∨ B).
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.
-/

variable is_even : ℕ → Prop

example : ∃ n, is_even n :=
exists.intro 3 _

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
---------------------- ∃ - elim
          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