michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/lean): add ExistsElim test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-16 15:43:09 -08:00
parent 7792561b20
commit 5b29fd8d93
2 changed files with 33 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
tests/lean/exists3.lean Normal file
View file

@ -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))).

7
tests/lean/exists3.lean.expected.out Normal file
View file

@ -0,0 +1,7 @@
Set: pp::colors
Set: pp::unicode
Assumed: P
Proved: T1
Assumed: Ax
Proved: T2
Proved: T3