lec9.lean

------------------------------
----REMINDER------------------
------------------------------

/-
Last week we saw
1. intro and elim rules in Lean
2. first proofs in Lean

In particular, we saw how
implication introduction works

Today, we learn more features
of Lean.
Having understood the previous
lecture is crucial - watch it
again if necessary, and type
the code yourself.
-/


------------------------------
----DOING WITHOUT VARIABLES---
------------------------------

/-
Instead of assuming "global"
variables for the propositions
we discuss, using

variables A B C D : Prop

, we can turn these
propositions into parameters
of each example:
-/

example (A : Prop) : A → A :=
sorry
--assume a : A, a

------------------------------
--SAVING PROOFS FOR REUSE-----
------------------------------

/-
We can give names to proofs
of propositions, and refer
to these proofs later on.
-/

theorem and_commute (A B : Prop) :
  A ∧ B → B ∧ A :=
sorry
--assume h : A ∧ B,
--  and.intro 
--   (and.elim_right h)
--   (and.elim_left h)

/-
The above proposition is
also the first example where
the antecedent of an implication
is not atomic.
Have you understood how we use
the hypothesis
"h : A ∧ B"
?
-/


/-
We now use "and_commute"
in the proof of another
result.
-/

section use_theorem
variables C D E : Prop
variable h1 : C ∧ ¬ D
variable h2 : ¬ D ∧ C → E
include h1 h2
example : E := sorry
--h2
--  (and_commute C (¬ D) h1)
end use_theorem


/-
In the example above,
Lean can *guess* the parameters
C and ¬ D of "and_commute".
Test:
replace them with underscores!

If we put the parameters of a
theorem in braces instead of
parentheses, we do not need
to specify them later
-/

theorem and_commute_var {A B : Prop} :
  A ∧ B → B ∧ A :=
assume h,
and.intro 
  (and.right h) 
  (and.left h)

section use_theorem
variables C D E : Prop
variable h1 : C ∧ ¬ D
variable h2 : ¬ D ∧ C → E
include h1 h2
example : E := sorry
--h2 (and_commute_var h1)
end use_theorem


------------------------------
--EXAMPLE WITH OR ELIMINATION-
------------------------------

/-
OR-elim looks a bit tricky at
first.
In Lean, it is actually quite
easy:
-/

#check or.elim
--this shows that or.elim
--takes 3 arguments:
--the first is a proof of
--P ∨ Q for some P, Q;
--the second and third
--are implications
--Lean calls these propositions
--by strange names.

--We simply start by
--using "or.elim h _ _"
--where h : P ∨ Q

example (A B C D : Prop) :
  A ∨ B → (A → C) →
   (B → D) → C ∨ D :=
sorry

/-
assume h : A ∨ B,
assume f : A → C,
assume g : B → D,
or.elim h
(assume a : A , or.intro_left D (f a))
(assume b : B, or.intro_right C (g b))
-/


------------------------------
----FORWARD REASONING IN LEAN-
------------------------------

--Example
section forward

example (A B C : Prop) : 
  (A → B) → (B → C) → (A → C) :=
sorry

/-
assume f : A → B,
assume g : B → C,
assume a : A,
have b : B, from f a,
show C, from g b
-/
end forward

/-

Writing a proof with
"have h : A, from P,
   ... h ... "
is the same as writing
"... P ...."

Advantages of "have":

1. more readable
2. can use "h" multiple times,
   hence avoid repetition
3. makes proofs more modular
   and results in readable 
   messages from Lean

Use of "have" is entirely
optional: any proposition that
can be proved with "have"
can also be proved without
using "have"

-/

example (A B : Prop) : 
  A ∧ B → B ∧ A :=
sorry

--assume h1 : A ∧ B,
--have a : A, from and.left h1,
--have b : B, from and.right h1,
--and.intro b a




------------------------------
--CLASSICAL REASONING IN LEAN-
------------------------------

/-
In Lean, access to the rule

 ¬ ¬ A
-------
   A

requires importing a special
library called "classical"
-/

--First we prove a result
--that we want to use later
theorem Not_Or {A B : Prop} :
  ¬ (A ∨ B) → (¬ A ∧ ¬ B) :=
sorry

/-
assume f : ¬ (A ∨ B),
 and.intro
  (assume a : A,
    f (or.intro_left _ a))
  (assume b : B,
    f (or.intro_right _ b))
-/

open classical

example (A : Prop) : ¬ ¬ A → A :=
 assume nna : ¬ ¬ A, 
  by_contradiction nna

theorem Not_And {A B : Prop} :
  ¬ (A ∧ B) → ¬ A ∨ ¬ B :=
sorry
/-
assume h : ¬ (A ∧ B),
 by_contradiction
  (assume w : ¬(¬A ∨ ¬B) ,
    have k : ¬ ¬ A ∧ ¬ ¬ B, from Not_Or w ,
      h (and.intro (by_contradiction k.left) 
                   (by_contradiction k.right))
)
-/

theorem Excluded_Middle (A : Prop) :
  A ∨ ¬ A :=
sorry
/-
by_contradiction 
 (assume nor : ¬ (A ∨ ¬ A),
  have foo : ¬ A ∧ ¬ ¬ A,
    from Not_Or (assume k : A ∨ ¬ A , nor k),
  foo.right foo.left
)
-/




------------------------------
--SHOWING MORE INFORMATION----
------------------------------

/-
Looking back at last example,
we might want to spell out the
result of some intermediate 
expressions, e.g.,
-/

example (A B : Prop) : 
  A ∧ B → B ∧ A :=
assume h1 : A ∧ B,
have h2 : A, from and.left h1,
have h3 : B, from and.right h1,
show B ∧ A, from and.intro h3 h2

/-
Schematically, we replaced
some expression "p" above,
where p : P,
by
"show P, from p"

Technically, these are
entirely equivalent.

Advantages of "show":
1. better error messages from
   Lean
2. better readability for us
-/

--We can be more extreme:
example (A B : Prop) : 
  A ∧ B → B ∧ A :=
assume h1 : A ∧ B,
have a : A, from and.left h1,
have b : B, from and.right h1,
show B ∧ A, from 
  and.intro
   (show B, from b)
   (show A, from a)




------------------------------
--BI-IMPLICATION--------------
------------------------------

/-
When A → B and B → A, then we
call A and B "equivalent".
Intuitively, they are equally
"strong" as propositions.

Bi-implication expresses this
concept. Bi-implication could
be *defined*, just like negation,
in terms of the other logical
connectives: 

A ↔ B = (A → B) ∧ (B → A)

In Lean, bi-implication is
however a primitive concept,
implemented through introduction
and elimination rules.

The introduction rule is

A → B   B → A
---------------
    A ↔ B

as one might expect. Similarly,
we get two elimination rules:

 A ↔ B
-------
 A → B

and 

 A ↔ B
-------
 B → A

See the Lean code below.
-/


section bi_impl

variables A B : Prop
variable f : A → B
variable g : B → A

#check iff.intro f g

variable h : A ↔ B

#check iff.elim_left h
#check iff.elim_right h

end bi_impl