lec23.lean

/-
Lecture 23:

Predicate logic
     ---
  ∃ in Lean


Contents:

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

-/


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

We usually use this rule
*from bottom to top*
(backwards reasoning),
choosing a suitable t : U
for which we can prove P(t).

In Lean, this looks like this:

-/

section exists_introduction

variable U : Type
variable P : U → Prop

variable t : U
variable p : P t
include t p

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 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 := _

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)
:= _
/-

                 ------q
                   Q t
               ---------
               P t ∨ Q t
-------h    --------------∃-intro(t,q)
∃ x, Q x    ∃ x, P x ∨ Q x
-----------------------------∃-elim(h)
        ∃ x, P x ∨ Q x
-----------------------------asm h
(∃ 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)
-/


example (h1 : ∀ x, P x → Q x)
        (h2 : ∃ x, P x) :
        ∃ x, Q x := _
/-
exists.elim h2
  (assume y : U,
   assume p : P y,
   have q : Q y, from h1 y p,
   exists.intro y q)
-/
end examples