lean2/examples/lean/ex5.lean
Leonardo de Moura 7222a2d1a9 feat(builtin/kernel): use the same notation for mp, eq::mp and forall::elim
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 21:39:31 -08:00

50 lines
No EOL
1.5 KiB
Text

import macros
scope
theorem ReflIf (A : Type)
(R : A → A → Bool)
(Symm : Π x y, R x y → R y x)
(Trans : Π x y z, R x y → R y z → R x z)
(Linked : Π x, ∃ y, R x y)
:
Π x, R x x :=
λ x, obtain (w : A) (H : R x w), from (Linked x),
let L1 : R w x := Symm x w H
in Trans x w x H L1
pop::scope
scope
-- Same example but using ∀ instead of Π and ⇒ instead of →.
-- Remark: H ◂ x is syntax sugar for forall::elim H x,
-- and H1 ◂ H2 is syntax sugar for mp H1 H2
theorem ReflIf (A : Type)
(R : A → A → Bool)
(Symm : ∀ x y, R x y ⇒ R y x)
(Trans : ∀ x y z, R x y ⇒ R y z ⇒ R x z)
(Linked : ∀ x, ∃ y, R x y)
:
∀ x, R x x :=
take x, obtain (w : A) (H : R x w), from (Linked ◂ x),
let L1 : R w x := Symm ◂ x ◂ w ◂ H
in Trans ◂ x ◂ w ◂ x ◂ H ◂ L1
pop::scope
scope
-- Same example again.
variable A : Type
variable R : A → A → Bool
axiom Symm {x y : A} : R x y → R y x
axiom Trans {x y z : A} : R x y → R y z → R x z
axiom Linked (x : A) : ∃ y, R x y
theorem ReflIf (x : A) : R x x :=
obtain (w : A) (H : R x w), from (Linked x),
let L1 : R w x := Symm H
in Trans H L1
end
-- Display the last two theorems
print environment 2