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

feat(library/data/subtype): cleanup proof

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-02 19:51:28 -07:00
parent 70d0dea02d
commit 228a99af7e
1 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/data/subtype.lean
View file

@ -3,7 +3,6 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE. Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura, Jeremy Avigad Author: Leonardo de Moura, Jeremy Avigad
-/ -/
open decidable open decidable
set_option structure.proj_mk_thm true set_option structure.proj_mk_thm true
@ -30,9 +29,8 @@ namespace subtype
protected definition has_decidable_eq [instance] [H : decidable_eq A] : ∀ s₁ s₂ : {x | P x}, decidable (s₁ = s₂) protected definition has_decidable_eq [instance] [H : decidable_eq A] : ∀ s₁ s₂ : {x | P x}, decidable (s₁ = s₂)
| (tag v₁ p₁) (tag v₂ p₂) := | (tag v₁ p₁) (tag v₂ p₂) :=
begin match H v₁ v₂ with
apply (@by_cases (v₁ = v₂)), | inl veq := begin left, substvars end
{intro e, revert p₁, rewrite e, intro p₁, left, congruence}, | inr vne := begin right, intro h, injection h, contradiction end
{intro n, right, intro h, injection h, contradiction}
end end
end subtype end subtype