lec21.lean

/-
Lecture 21:

Predicate logic
     ---
first proofs in Lean


Contents:

1. Inference rules for quantifiers
2. Proofs of formulas with quantifiers

-/


------------------------------
----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, _

/-
We cannot finish this proof
without further assumptions.

Note:
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




-----------------------------
----EXAMPLE PROOF-------------
------------------------------


section forall_example

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)


          --------h
          ∀ x, P x
         ---------∀-elim
            P t
       ------------or-i-left
         P t ∨ Q t
    ------------------asm t (∀-i)
      ∀ x, P x ∨ Q x
-----------------------------asm h
(∀ x, P x) → (∀ x, P x ∨ Q x)


-/

end forall_example


--Next: an exercise...

















section exercise

variable U : Type
variables P Q : U → Prop

example :
 (∀ x, P x ∧ Q x) → (∀ x, Q x) :=
 assume h : ∀ x, P x ∧ Q x,
 assume t : U,
 and.elim_right (h t)
/-
assume h : ∀ x, P x ∧ Q x,
assume t : U,
and.elim_right (h t)


        --------------h
        ∀ x, P x ∧ Q x
       ----------------∀-elim
           P t ∧ Q t
           ---------and-elim-right
             Q t
          ----------asm t
           ∀ x, Q x
-----------------------------asm h
(∀ x, P x ∧ Q x) → (∀ x, Q x)
-/

end exercise


------------------------------
----INTERLUDE: HAVE-----------
------------------------------

section exercise_again

variable U : Type
variables P Q : U → Prop

example :
 (∀ x, P x ∧ Q x) → (∀ x, Q x) :=
 assume h : ∀ x, P x ∧ Q x,
 assume t : U,
 have r : P t ∧ Q t, from h t,
 and.elim_right r

/-
        --------------h
        ∀ x, P x ∧ Q x
       ----------------∀-elim
           P t ∧ Q t
           ---------and-elim-right
             Q t
          ----------asm t
           ∀ x, Q x
-----------------------------asm h
(∀ x, P x ∧ Q x) → (∀ x, Q x)


Note:
A "have" does not show up
in the proof tree.


General rule:

have x : A, from long-expression,
   foo(x)

is the same as replacing
x
by
long-expression
everywhere in foo(x)

-/

end exercise_again


section another_example

variable U : Type
variables P Q : U → Prop

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

end another_example



------------------------------
----∃ 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 t : U
variable p : P t

example : ∃ x, P x := _

/-

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


∃ introduction is similar
to ∨ introduction:
we have to pick a t : U 
(analogous to picking left 
or right) 
and then
prove P t 
(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.
-/

variable is_even : ℕ → Prop

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

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, Q x) →
 (∃ x, P x ∨ Q x)
:= _

/-
assume h : ∃ x, Q x,
exists.elim h
(assume t : U,
 assume q : Q t,
 exists.intro
 t
 (or.intro_right (P t) q))
-/




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


                 ∃ x, P x ∧ Q x
                  -----------
                    P t ∧ Q t
                    --------
                      Q t
---------------h   ----------
∃ x, P x ∧ Q x      ∃ x, Q x
 ----------------------------
          (∃ x, Q x)
-----------------------------
(∃ x, P x ∧ Q x) → (∃ x, Q x)
-/




end examples