From 9b7d596e6bfe246f1b379887d175db7cf50e0711 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Dec 2013 20:33:31 -0800 Subject: [PATCH] chore(builtin/basic): simplify UnfoldExists2 proof Signed-off-by: Leonardo de Moura --- src/builtin/basic.lean | 8 ++++---- src/builtin/basic.olean | Bin 19869 -> 19907 bytes 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/builtin/basic.lean b/src/builtin/basic.lean index 27b042fda..28ca3f742 100644 --- a/src/builtin/basic.lean +++ b/src/builtin/basic.lean @@ -343,10 +343,10 @@ Theorem UnfoldExists1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) (λ Hne : w ≠ a, Disj2 (P a) (ExistsIntro w (Conj Hne H1)))). Theorem UnfoldExists2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x -:= DisjCases (EM (P a)) - (λ Hpos : P a, ExistsIntro a Hpos) - (λ Hneg : ¬ P a, - ExistsElim (Resolve1 H Hneg) +:= DisjCases H + (λ H1 : P a, ExistsIntro a H1) + (λ H2 : (∃ x : A, x ≠ a ∧ P x), + ExistsElim H2 (λ (w : A) (Hw : w ≠ a ∧ P w), ExistsIntro w (Conjunct2 Hw))). diff --git a/src/builtin/basic.olean b/src/builtin/basic.olean index a116994947ed3d32b213875c33f0101c898a0e86..9f1b6434fb932dea677e393e895c0564d52e87ce 100644 GIT binary patch delta 388 zcmbO`oAK~$#tr*CCwI8=*fB6LF#ZD)Tpv_`B!itQh^%G=5-dQ>bpga;QU;OCApR8) zaUaBGU}f?!ocz$!M$Cu-q?J<;tcaDV0wl@JF?o)wnw>fmkj-ep0Fq*11rkgk0d5g= zyFgOhTwnvhc7g2X=9^sLCCVcM7vQ=xd8gMGMxV)!KKhKIlM8*+Y{5pdffT!gnd~5@ z7nsQjVtT8A>|@A6av>AUg=t`O@`2{qOjht^m8u3?1a@BrNN*L;gCNb^^^?!|gjn%{ snEl8O2MH8_h(eIV84=n`L4w&Z?b9bm`I_>9+{DP}nwR31nUl%@05cXawEzGB delta 387 zcmX>+n{n=J#tr*Cm6aKQ07P)T2NCy`nLq-aAcE^XE0ae-e(_`uFPr+j)O4^i24!VN zpd1s3U{nVwX0%`caadSE?0-Oln@t5sGT5nt$ZC)rNQ&zMh{X)n%>v?I0jc5?MCknw zk*yX8IuP)HW26{M00q6wsu4MgyQ1Q{pa_xi%JdY~;B?!X;qKLAG)yf{0>Z003zQ?uyBud_t^v sK+Fzg&w&IoK|~hV9SH4tAi)%v_6d_4d`Vc044)4BLDyZ