diff --git a/library/data/sum.lean b/library/data/sum.lean index 50892cbcb8..ed6e2d4d79 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -36,18 +36,4 @@ namespace sum protected definition is_inhabited_right [instance] [h : inhabited B] : inhabited (A + B) := inhabited.mk (inr (default B)) - - protected definition has_decidable_eq [instance] [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ s₁ s₂ : A + B, decidable (s₁ = s₂) - | has_decidable_eq (inl a₁) (inl a₂) := - match h₁ a₁ a₂ with - | decidable.tt hp := decidable.tt sorry -- by left; congruence; assumption - | decidable.ff hn := decidable.ff sorry -- by right; intro h; injection h; contradiction - end - | has_decidable_eq (inl a₁) (inr b₂) := decidable.ff sorry -- by right; contradiction - | has_decidable_eq (inr b₁) (inl a₂) := decidable.ff sorry -- by right; contradiction - | has_decidable_eq (inr b₁) (inr b₂) := - match h₂ b₁ b₂ with - | decidable.tt hp := decidable.tt sorry -- by left; congruence; assumption - | decidable.ff hn := decidable.ff sorry -- by right; intro h; injection h; contradiction - end end sum diff --git a/library/init/default.lean b/library/init/default.lean index d62d78c510..5e0c2eb5f1 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -10,5 +10,5 @@ import init.bool init.unit init.num init.sigma init.measurable init.setoid init. import init.funext init.function init.subtype init.classical init.simplifier import init.monad init.option init.fin init.list init.char init.string init.to_string import init.timeit init.trace init.unsigned init.ordering init.list_classes -import init.meta +import init.meta init.instances import init.wf init.wf_k init.sigma_lex diff --git a/library/init/instances.lean b/library/init/instances.lean new file mode 100644 index 0000000000..530562a742 --- /dev/null +++ b/library/init/instances.lean @@ -0,0 +1,24 @@ +/- +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Leonardo de Moura +-/ +prelude +import init.meta.mk_dec_eq_instance init.subtype init.meta.occurrences + +open tactic subtype + +definition subtype_decidable_eq [instance] {A : Type} {P : A → Prop} [decidable_eq A] : decidable_eq {x | P x} := +by mk_dec_eq_instance + +definition list_decidable_eq [instance] {A : Type} [decidable_eq A] : decidable_eq (list A) := +by mk_dec_eq_instance + +definition occurrences_decidable_eq [instance] : decidable_eq occurrences := +by mk_dec_eq_instance + +definition unit_decidable_eq [instance] : decidable_eq unit := +by mk_dec_eq_instance + +definition sum_decidable [instance] {A : Type} {B : Type} [decidable_eq A] [decidable_eq B] : decidable_eq (sum A B) := +by mk_dec_eq_instance diff --git a/library/init/list.lean b/library/init/list.lean index 7b0b8ed069..9faa1ef673 100644 --- a/library/init/list.lean +++ b/library/init/list.lean @@ -10,21 +10,6 @@ open decidable list protected definition list.is_inhabited [instance] (A : Type) : inhabited (list A) := inhabited.mk list.nil -definition list.has_decidable_eq [instance] {A : Type} [H : decidable_eq A] (l₁ : list A) : ∀ l₂ : list A, decidable (l₁ = l₂) := -list.rec_on l₁ - (λ l₂, list.cases_on l₂ - (tt rfl) - (λ b l₂, ff (λ H, list.no_confusion H))) - (λ a l₁ ih l₂, list.cases_on l₂ - (ff (λ H, list.no_confusion H)) - (λ b l₂, - decidable.cases_on (H a b) - (λ Hnab : a ≠ b, ff (λ H, list.no_confusion H (λ Hab Hl₁l₂, absurd Hab Hnab))) - (λ Hab : a = b, - decidable.cases_on (ih l₂) - (λ Hne : l₁ ≠ l₂, ff (λ H, list.no_confusion H (λ Hab Hl₁l₂, absurd Hl₁l₂ Hne))) - (λ He : l₁ = l₂, tt (congr (congr_arg cons Hab) He))))) - notation h :: t := cons h t notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l diff --git a/library/init/meta/occurrences.lean b/library/init/meta/occurrences.lean index 6ef489b50f..71d237e3a9 100644 --- a/library/init/meta/occurrences.lean +++ b/library/init/meta/occurrences.lean @@ -45,18 +45,3 @@ meta_definition occurrences_has_to_format [instance] : has_to_format occurrences has_to_format.mk occurrences_to_format open decidable tactic - -definition occurrences_has_decidable_eq [instance] : ∀ a b : occurrences, decidable (a = b) -| all all := tt rfl -| all (pos l) := by left >> intron 1 >> contradiction -| all (neg l) := by left >> intron 1 >> contradiction -| (pos l) all := by left >> intron 1 >> contradiction -| (pos l₁) (pos l₂) := if H : l₁ = l₂ - then by right >> get_local "H" >>= subst >> reflexivity - else by left >> intro "_" >>= injection >> contradiction -| (pos l₁) (neg l₂) := by left >> intron 1 >> contradiction -| (neg l₁) all := by left >> intron 1 >> contradiction -| (neg l₁) (pos l₂) := by left >> intron 1 >> contradiction -| (neg l₁) (neg l₂) := if H : l₁ = l₂ - then by right >> get_local "H" >>= subst >> reflexivity - else by left >> intro "_" >>= injection >> contradiction diff --git a/library/init/subtype.lean b/library/init/subtype.lean index a94c4afe4a..78817181a0 100644 --- a/library/init/subtype.lean +++ b/library/init/subtype.lean @@ -35,8 +35,3 @@ open subtype variables {A : Type} {P : A → Prop} protected definition subtype.is_inhabited [instance] {a : A} (H : P a) : inhabited {x | P x} := inhabited.mk (tag a H) - -protected definition subtype.has_decidable_eq [instance] [H : decidable_eq A] : ∀ s₁ s₂ : {x | P x}, decidable (s₁ = s₂) -| (tag v₁ p₁) (tag v₂ p₂) := - decidable_of_decidable_of_iff (H v₁ v₂) - (iff.intro tag_eq (λh, subtype.no_confusion h (λa b, a))) diff --git a/library/init/unit.lean b/library/init/unit.lean index a82d31b314..dcad625a6e 100644 --- a/library/init/unit.lean +++ b/library/init/unit.lean @@ -17,6 +17,3 @@ subsingleton.intro unit_eq definition unit_is_inhabited [instance] : inhabited unit := inhabited.mk () - -definition unit_has_decidable_eq [instance] : decidable_eq unit := -take (a b : unit), decidable.tt (unit_eq a b)