import macros
using Nat

-- In this example, we prove two simple theorems about even/odd numbers.
-- First, we define the predicates even and odd.
definition even (a : Nat) := ∃ b, a = 2*b
definition odd  (a : Nat) := ∃ b, a = 2*b + 1

-- Prove that the sum of two even numbers is even.
--
--   Notes: we use the macro
--      obtain [bindings] ',' 'from' [expr]_1 ',' [expr]_2
--
--   It is syntax sugar for existential elimination.
--   It expands to
--
--     exists::elim [expr]_1 (fun [binding], [expr]_2)
--
--   It is defined in the file macros.lua.
--
--   We also use the calculational proof style.
--   See doc/lean/calc.md for more information.
--
--  We use the first two obtain-expressions to extract the
--  witnesses w1 and w2 s.t. a = 2*w1 and b = 2*w2.
--  We can do that because H1 and H2 are evidence/proof for the
--  fact that 'a' and 'b' are even.
--
--  We use a calculational proof 'calc' expression to derive
--  the witness w1+w2 for the fact that a+b is also even.
--  That is, we provide a derivation showing that a+b = 2*(w1 + w2)
theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b)
:= obtain (w1 : Nat) (Hw1 : a = 2*w1), from H1,
   obtain (w2 : Nat) (Hw2 : b = 2*w2), from H2,
     exists::intro (w1 + w2)
        (calc a + b  =  2*w1 + b      : { Hw1 }
                ...  =  2*w1 + 2*w2   : { Hw2 }
                ...  =  2*(w1 + w2)   : symm (distribute 2 w1 w2))

-- In the following example, we omit the arguments for Nat::PlusAssoc, Refl and Nat::Distribute.
-- Lean can infer them automatically.
--
-- Refl is the reflexivity proof. (Refl a) is a proof that two
-- definitionally equal terms are indeed equal.
-- "definitionally equal" means that they have the same normal form.
-- We can also view it as "Proof by computation".
-- The normal form of (1+1), and 2*1 is 2.
--
-- Another remark: '2*w + 1 + 1' is not definitionally equal to '2*w + 2*1'.
-- The gotcha is that '2*w + 1 + 1' is actually '(2*w + 1) + 1' since +
-- is left associative. Moreover, Lean normalizer does not use
-- any theorems such as + associativity.
theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1)
:= obtain (w : Nat) (Hw : a = 2*w + 1), from H,
   exists::intro (w + 1)
        (calc a + 1 = 2*w + 1 + 1   : { Hw }
                ... = 2*w + (1 + 1) : symm (plus::assoc _ _ _)
                ... = 2*w + 2*1     : refl _
                ... = 2*(w + 1)     : symm (distribute _ _ _))

-- The following command displays the proof object produced by Lean after
-- expanding macros, and infering implicit/missing arguments.
print environment 2

-- By default, Lean does not display implicit arguments.
-- The following command will force it to display them.
set::option pp::implicit true

print environment 2

-- As an exercise, prove that the sum of two odd numbers is even,
-- and other similar theorems.