lean2/tests/lean/tactic14.lean
Leonardo de Moura 08718e33dc refactor(builtin): only load the kernel and natural numbers by default
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 13:35:37 -08:00

13 lines
393 B
Text

Import int.
(**
-- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions
congr_tac = Try(unfold_tac("eq")) .. Repeat(OrElse(apply_tac("Refl"), apply_tac("Congr"), assumption_tac()))
**)
Theorem T1 (a b : Int) (f : Int -> Int) : a = b -> (f (f a)) = (f (f b)) :=
fun assumption : a = b,
show (f (f a)) = (f (f b)) by congr_tac
Show Environment 1.