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

test(tests/lean): ExistsElim test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-23 12:47:16 -08:00
parent 2cdd06b182
commit 2c30b87f30
2 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/exists6.lean Normal file
View file

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

6
tests/lean/exists6.lean.expected.out Normal file
View file

@ -0,0 +1,6 @@
Set: pp::colors
Set: pp::unicode
Assumed: P
Assumed: Ax1
Assumed: Ax2
Proved: T