From a8bc9fb4e0d3c87ab5bc03bfb9d587b2254a017c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Jan 2014 11:00:32 -0800
Subject: [PATCH] refactor(builtin/kernel): mark exists as opaque after proving
 key theorems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/kernel.lean              |   4 +++-
 src/builtin/obj/kernel.olean         | Bin 20029 -> 20042 bytes
 tests/lean/exists3.lean              |   2 ++
 tests/lean/exists4.lean.expected.out |   2 +-
 4 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index ca95b1bb8..903ecea16 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -361,4 +361,6 @@ Theorem UnfoldExists2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x :
 
 Theorem UnfoldExists {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x))
 := ImpAntisym (assume H : (∃ x : A, P x), UnfoldExists1 a H)
-              (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), UnfoldExists2 a H).
\ No newline at end of file
+              (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), UnfoldExists2 a H).
+
+SetOpaque exists true.
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 41d411e4424e9e0bb3e691a446fd490f51a027ac..cbad4b0e0054511ebd359dec457cec5667a8e8e5 100644
GIT binary patch
delta 31
mcmdlxhw;=L#to)^qW%Sm3{0sNnZ+f=42-UMDQ=lLsSE(MehOp&

delta 18
ZcmX>#hjH&5#to)^9IkmOZkai$3;;&Q29y8*

diff --git a/tests/lean/exists3.lean b/tests/lean/exists3.lean
index 6c68ab015..50c4cbd52 100644
--- a/tests/lean/exists3.lean
+++ b/tests/lean/exists3.lean
@@ -1,6 +1,8 @@
 Import int.
 Variable P : Int -> Int -> Bool
 
+SetOpaque exists false.
+
 Theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) :=
          ForallIntro (fun a,
              ForallIntro (fun b,
diff --git a/tests/lean/exists4.lean.expected.out b/tests/lean/exists4.lean.expected.out
index b75fda078..582b65c90 100644
--- a/tests/lean/exists4.lean.expected.out
+++ b/tests/lean/exists4.lean.expected.out
@@ -15,7 +15,7 @@ Theorem T1 : ∃ x y z : N, P x y z :=
         N
         (λ x : N, ∃ y z : N, P x y z)
         a
-        (@ExistsIntro N (λ x : N, ¬ (∀ x::1 : N, ¬ P a x x::1)) b (@ExistsIntro N (λ z : N, P a b z) c H3))
+        (@ExistsIntro N (λ y : N, ∃ z : N, P a y z) b (@ExistsIntro N (λ z : N, P a b z) c H3))
 Theorem T2 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
 Theorem T3 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
 Theorem T4 (H : P a a b) : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro a (ExistsIntro b H))