From 640ebcc0407017a30dacb66af273b5aaa4cf60c5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Feb 2014 11:35:40 -0800 Subject: [PATCH] test(tests/lean/exp): add example for Steve Signed-off-by: Leonardo de Moura --- tests/lean/exp/arith.lean | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/lean/exp/arith.lean diff --git a/tests/lean/exp/arith.lean b/tests/lean/exp/arith.lean new file mode 100644 index 000000000..e15b6fdd9 --- /dev/null +++ b/tests/lean/exp/arith.lean @@ -0,0 +1,24 @@ +import tactic +using Nat + +-- Manual proof using symmetry, transitivity, distributivity and 1*x=x. +theorem T1 (a b c : Nat) + (H1 : a = b + c) -- First hypothesis + (H2 : b = c) -- Second hypothesis + : a = 2*c -- Conclusion +:= calc a = b + c : H1 + ... = c + c : { H2 } + ... = 1*c + 1*c : { symm (mul_onel c) } + ... = (1 + 1)*c : symm (distributel 1 1 c) + ... = 2*c : refl (2*c) + +add_rewrite mul_onel + +-- The simplifier can already compress the proof above. +theorem T2 (a b c : Nat) + (H1 : a = b + c) -- first hypothesis + (H2 : b = c) -- second hypothesis + : a = 2*c +:= calc a = 1*c + 1*c : by simp + ... = (1 + 1)*c : symm (distributel 1 1 c) + ... = 2*c : refl (2*c)