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

chore: remove DecidableEq workaround

Browse source 
We have better indexing now.
This commit is contained in:
Leonardo de Moura 2019-11-26 17:30:18 -08:00
parent 9a160a197a
commit 2809cea147
10 changed files with 33 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/Init/Core.lean
View file

@ -294,19 +294,17 @@ class inductive Decidable (p : Prop)
| isFalse (h : ¬p) : Decidable
| isTrue (h : p) : Decidable
@[reducible] def DecidablePred {α : Sort u} (r : α → Prop) :=
abbrev DecidablePred {α : Sort u} (r : α → Prop) :=
∀ (a : α), Decidable (r a)
@[reducible] def DecidableRel {α : Sort u} (r : α → α → Prop) :=
abbrev DecidableRel {α : Sort u} (r : α → α → Prop) :=
∀ (a b : α), Decidable (r a b)
class DecidableEq (α : Sort u) :=
{decEq : ∀ (a b : α), Decidable (a = b)}
abbrev DecidableEq (α : Sort u) :=
∀ (a b : α), Decidable (a = b)
export DecidableEq (decEq)
@[inline] instance decidableOfDecidableEq {α : Sort u} (a b : α) [DecidableEq α] : Decidable (a = b) :=
decEq a b
def decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (a = b) :=
s a b
inductive Option (α : Type u)
| none {} : Option
@ -953,11 +951,11 @@ theorem Bool.falseNeTrue (h : false = true) : False :=
Bool.noConfusion h
instance : DecidableEq Bool :=
{decEq := fun a b => match a, b with
fun a b => match a, b with
| false, false => isTrue rfl
| false, true => isFalse Bool.falseNeTrue
| true, false => isFalse (Ne.symm Bool.falseNeTrue)
| true, true => isTrue rfl}
| true, true => isTrue rfl
/- if-then-else expression theorems -/
@ -1181,9 +1179,9 @@ instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p
⟨⟨a, h⟩⟩
instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
{decEq := fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
if h : a = b then isTrue (Subtype.eq h)
else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))}
else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))
end Subtype
/- Sum -/
@ -1198,7 +1196,7 @@ instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) :=
⟨Sum.inr (arbitrary β)⟩
instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) :=
{decEq := fun a b =>
fun a b =>
match a, b with
| (Sum.inl a), (Sum.inl b) =>
if h : a = b then isTrue (h ▸ rfl)
@ -1207,7 +1205,7 @@ instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : Decidab
if h : a = b then isTrue (h ▸ rfl)
else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h))
| (Sum.inr a), (Sum.inl b) => isFalse (fun h => Sum.noConfusion h)
| (Sum.inl a), (Sum.inr b) => isFalse (fun h => Sum.noConfusion h)}
| (Sum.inl a), (Sum.inr b) => isFalse (fun h => Sum.noConfusion h)
end
/- Product -/
@ -1219,13 +1217,13 @@ instance [Inhabited α] [Inhabited β] : Inhabited (Prod α β) :=
⟨(arbitrary α, arbitrary β)⟩
instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
{decEq := fun ⟨a, b⟩ ⟨a', b'⟩ =>
fun ⟨a, b⟩ ⟨a', b'⟩ =>
match (decEq a a') with
| (isTrue e₁) =>
match (decEq b b') with
| (isTrue e₂) => isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
| (isFalse n₂) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂))
| (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁))}
| (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁))
instance [HasBeq α] [HasBeq β] : HasBeq (α × β) :=
⟨fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂⟩
@ -1284,7 +1282,7 @@ instance : Inhabited PUnit :=
⟨⟨⟩⟩
instance : DecidableEq PUnit :=
{decEq := fun a b => isTrue (punitEq a b)}
fun a b => isTrue (punitEq a b)
/- Setoid -/
@ -1560,12 +1558,12 @@ EqvGen.recOn H
end
instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
{decEq := fun (q₁ q₂ : Quotient s) =>
fun (q₁ q₂ : Quotient s) =>
Quotient.recOnSubsingleton₂ q₁ q₂
(fun a₁ a₂ =>
match (d a₁ a₂) with
| (isTrue h₁) => isTrue (Quotient.sound h₁)
| (isFalse h₂) => isFalse (fun h => absurd (Quotient.exact h) h₂))}
| (isFalse h₂) => isFalse (fun h => absurd (Quotient.exact h) h₂))
/- Function extensionality -/
@ -1706,7 +1704,7 @@ noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) :=
⟨propDecidable a⟩
noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
{decEq := fun x y => propDecidable (x = y)}
fun x y => propDecidable (x = y)
noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
match (propDecidable (Nonempty α)) with

3
src/Init/Data/Char/Basic.lean
View file

@ -63,8 +63,7 @@ theorem vneOfNe {c d : Char} (h : c ≠ d) : c.val ≠ d.val :=
fun h' => absurd (eqOfVeq h') h
instance : DecidableEq Char :=
{decEq := fun i j => decidableOfDecidableOfIff
(decEq i.val j.val) ⟨Char.eqOfVeq, Char.veqOfEq⟩}
fun i j => decidableOfDecidableOfIff (decEq i.val j.val) ⟨Char.eqOfVeq, Char.veqOfEq⟩
instance : Inhabited Char :=
⟨'A'⟩

3
src/Init/Data/Fin/Basic.lean
View file

@ -103,5 +103,4 @@ end Fin
open Fin
instance (n : Nat) : DecidableEq (Fin n) :=
{decEq := fun i j => decidableOfDecidableOfIff
(decEq i.val j.val) ⟨eqOfVeq, veqOfEq⟩}
fun i j => decidableOfDecidableOfIff (decEq i.val j.val) ⟨eqOfVeq, veqOfEq⟩

2
src/Init/Data/Int/Basic.lean
View file

@ -96,7 +96,7 @@ match a, b with
| negSucc a, ofNat b => isFalse $ fun h => Int.noConfusion h
instance Int.DecidableEq : DecidableEq Int :=
{decEq := Int.decEq}
Int.decEq
@[extern "lean_int_dec_nonneg"]
private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=

2
src/Init/Data/List/Basic.lean
View file

@ -30,7 +30,7 @@ protected def hasDecEq [DecidableEq α] : ∀ (a b : List α), Decidable (a = b)
| isFalse nab => isFalse (fun h => List.noConfusion h (fun hab _ => absurd hab nab))
instance [DecidableEq α] : DecidableEq (List α) :=
{decEq := List.hasDecEq}
List.hasDecEq
def reverseAux : List α → List α → List α
| [], r => r

2
src/Init/Data/Nat/Basic.lean
View file

@ -40,7 +40,7 @@ if h : beq n m = true then isTrue (eqOfBeqEqTt h)
else isFalse (neOfBeqEqFf (eqFalseOfNeTrue h))
@[inline] instance : DecidableEq Nat :=
{decEq := Nat.decEq}
Nat.decEq
@[extern "lean_nat_dec_le"]
def ble : Nat → Nat → Bool

4
src/Init/Data/Option/Basic.lean
View file

@ -75,14 +75,14 @@ instance (α : Type u) : Inhabited (Option α) :=
⟨none⟩
instance {α : Type u} [DecidableEq α] : DecidableEq (Option α) :=
{decEq := fun a b => match a, b with
fun a b => match a, b with
| none, none => isTrue rfl
| none, (some v₂) => isFalse (fun h => Option.noConfusion h)
| (some v₁), none => isFalse (fun h => Option.noConfusion h)
| (some v₁), (some v₂) =>
match decEq v₁ v₂ with
| (isTrue e) => isTrue (congrArg (@some α) e)
| (isFalse n) => isFalse (fun h => Option.noConfusion h (fun e => absurd e n))}
| (isFalse n) => isFalse (fun h => Option.noConfusion h (fun e => absurd e n))
instance {α : Type u} [HasBeq α] : HasBeq (Option α) :=
⟨fun a b => match a, b with

2
src/Init/Data/String/Basic.lean
View file

@ -28,7 +28,7 @@ match s₁, s₂ with
else isFalse (fun h' => String.noConfusion h' (fun h' => absurd h' h))
instance : DecidableEq String :=
{decEq := String.decEq}
String.decEq
def List.asString (s : List Char) : String :=
⟨s⟩

10
src/Init/Data/UInt.lean
View file

@ -64,7 +64,7 @@ def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
UInt8.casesOn a $ fun n => UInt8.casesOn b $ fun m =>
inferInstanceAs (Decidable (n <= m))
instance : DecidableEq UInt8 := {decEq := UInt8.decEq}
instance : DecidableEq UInt8 := UInt8.decEq
instance UInt8.hasDecidableLt (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
instance UInt8.hasDecidableLe (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
@ -123,7 +123,7 @@ def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
UInt16.casesOn a $ fun n => UInt16.casesOn b $ fun m =>
inferInstanceAs (Decidable (n <= m))
instance : DecidableEq UInt16 := {decEq := UInt16.decEq}
instance : DecidableEq UInt16 := UInt16.decEq
instance UInt16.hasDecidableLt (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
instance UInt16.hasDecidableLe (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
@ -182,7 +182,7 @@ def UInt32.decLe (a b : UInt32) : Decidable (a ≤ b) :=
UInt32.casesOn a $ fun n => UInt32.casesOn b $ fun m =>
inferInstanceAs (Decidable (n <= m))
instance : DecidableEq UInt32 := {decEq := UInt32.decEq}
instance : DecidableEq UInt32 := UInt32.decEq
instance UInt32.hasDecidableLt (a b : UInt32) : Decidable (a < b) := UInt32.decLt a b
instance UInt32.hasDecidableLe (a b : UInt32) : Decidable (a ≤ b) := UInt32.decLe a b
@ -258,7 +258,7 @@ def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
UInt64.casesOn a $ fun n => UInt64.casesOn b $ fun m =>
inferInstanceAs (Decidable (n <= m))
instance : DecidableEq UInt64 := {decEq := UInt64.decEq}
instance : DecidableEq UInt64 := UInt64.decEq
instance UInt64.hasDecidableLt (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
instance UInt64.hasDecidableLe (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
@ -332,7 +332,7 @@ def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
USize.casesOn a $ fun n => USize.casesOn b $ fun m =>
inferInstanceAs (Decidable (n <= m))
instance : DecidableEq USize := {decEq := USize.decEq}
instance : DecidableEq USize := USize.decEq
instance USize.hasDecidableLt (a b : USize) : Decidable (a < b) := USize.decLt a b
instance USize.hasDecidableLe (a b : USize) : Decidable (a ≤ b) := USize.decLe a b

4
src/Init/Lean/Position.lean
View file

@ -16,11 +16,11 @@ structure Position :=
namespace Position
instance : DecidableEq Position :=
{decEq := fun ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ =>
fun ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ =>
if h₁ : l₁ = l₂ then
if h₂ : c₁ = c₂ then isTrue (Eq.recOn h₁ (Eq.recOn h₂ rfl))
else isFalse (fun contra => Position.noConfusion contra (fun e₁ e₂ => absurd e₂ h₂))
else isFalse (fun contra => Position.noConfusion contra (fun e₁ e₂ => absurd e₁ h₁))}
else isFalse (fun contra => Position.noConfusion contra (fun e₁ e₂ => absurd e₁ h₁))
protected def lt : Position → Position → Bool
| ⟨l₁, c₁⟩, ⟨l₂, c₂⟩ => (l₁, c₁) < (l₂, c₂)