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

chore(builtin/basic): simplify UnfoldExists2 proof

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-29 20:33:31 -08:00
parent a7654cfdbe
commit 9b7d596e6b
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/builtin/basic.lean
View file

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

BIN
src/builtin/basic.olean
View file

Binary file not shown.