From 5b29fd8d937fc5421b27f8d2916e2f0872a657c2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Dec 2013 15:43:09 -0800 Subject: [PATCH] test(tests/lean): add ExistsElim test Signed-off-by: Leonardo de Moura --- tests/lean/exists3.lean | 26 ++++++++++++++++++++++++++ tests/lean/exists3.lean.expected.out | 7 +++++++ 2 files changed, 33 insertions(+) create mode 100644 tests/lean/exists3.lean create mode 100644 tests/lean/exists3.lean.expected.out diff --git a/tests/lean/exists3.lean b/tests/lean/exists3.lean new file mode 100644 index 000000000..eedecb73a --- /dev/null +++ b/tests/lean/exists3.lean @@ -0,0 +1,26 @@ +Variable P : Int -> Int -> Bool + +Theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) := + ForallIntro (fun a, + ForallIntro (fun b, + ForallElim (DoubleNegElim (ForallElim (DoubleNegElim R1) a)) b)) + +Axiom Ax : forall x, exists y, P x y + +Theorem T2 : exists x y, P x y := + Refute (fun R : not (exists x y, P x y), + let L1 : forall x y, not (P x y) := ForallIntro (fun a, + ForallIntro (fun b, + ForallElim (DoubleNegElim (ForallElim (DoubleNegElim R) a)) b)), + L2 : exists y, P 0 y := ForallElim Ax 0 + in ExistsElim L2 (fun (w : Int) (H : P 0 w), + Absurd H (ForallElim (ForallElim L1 0) w))). + +Theorem T3 (A : Type U) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y := + Refute (fun R : not (exists x y, P x y), + let L1 : forall x y, not (P x y) := ForallIntro (fun a, + ForallIntro (fun b, + ForallElim (DoubleNegElim (ForallElim (DoubleNegElim R) a)) b)), + L2 : exists y, P a y := ForallElim H1 a + in ExistsElim L2 (fun (w : A) (H : P a w), + Absurd H (ForallElim (ForallElim L1 a) w))). diff --git a/tests/lean/exists3.lean.expected.out b/tests/lean/exists3.lean.expected.out new file mode 100644 index 000000000..85637a8ab --- /dev/null +++ b/tests/lean/exists3.lean.expected.out @@ -0,0 +1,7 @@ + Set: pp::colors + Set: pp::unicode + Assumed: P + Proved: T1 + Assumed: Ax + Proved: T2 + Proved: T3