max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init): use mk_dec_eq_instance in the init folder

Browse source 
We cannot mk_dec_eq_instance everywhere in the init folder because some
dec_eq instances are used to define the tactic mk_dec_eq_instance.
This commit is contained in:
Leonardo de Moura 2016-07-20 20:17:27 -04:00
parent 40b3410ede
commit 0163c1aa5b
7 changed files with 25 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
library/data/sum.lean
View file

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

2
library/init/default.lean
View file

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

24
library/init/instances.lean Normal file
View file

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

15
library/init/list.lean
View file

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

15
library/init/meta/occurrences.lean
View file

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

5
library/init/subtype.lean
View file

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

3
library/init/unit.lean
View file

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