From 2c30b87f301adbf4e788bea79a021cfc2870b1df Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Dec 2013 12:47:16 -0800 Subject: [PATCH] test(tests/lean): ExistsElim test Signed-off-by: Leonardo de Moura --- tests/lean/exists6.lean | 7 +++++++ tests/lean/exists6.lean.expected.out | 6 ++++++ 2 files changed, 13 insertions(+) create mode 100644 tests/lean/exists6.lean create mode 100644 tests/lean/exists6.lean.expected.out diff --git a/tests/lean/exists6.lean b/tests/lean/exists6.lean new file mode 100644 index 000000000..35fe6579a --- /dev/null +++ b/tests/lean/exists6.lean @@ -0,0 +1,7 @@ +Variable P : Int -> Int -> Int -> Bool +Axiom Ax1 : exists x y z, P x y z +Axiom Ax2 : forall x y z, not (P x y z) +Theorem T : false := + ExistsElim Ax1 (fun a H1, ExistsElim H1 (fun b H2, ExistsElim H2 (fun (c : Int) (H3 : P a b c), + let notH3 : not (P a b c) := ForallElim (ForallElim (ForallElim Ax2 a) b) c + in Absurd H3 notH3))) diff --git a/tests/lean/exists6.lean.expected.out b/tests/lean/exists6.lean.expected.out new file mode 100644 index 000000000..6055c3fff --- /dev/null +++ b/tests/lean/exists6.lean.expected.out @@ -0,0 +1,6 @@ + Set: pp::colors + Set: pp::unicode + Assumed: P + Assumed: Ax1 + Assumed: Ax2 + Proved: T