refactor(init/data/string/*): implement decidable equality for string…

…s without using tactics (#204)
leanprover-community · Apr 28, 2020 · f1fc405 · f1fc405
1 parent 2259a2c
commit f1fc405
Show file tree

Hide file tree

Showing 6 changed files with 11 additions and 15 deletions.
diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean
@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.data.list.lemmas
-import init.meta.mk_dec_eq_instance init.control.lawful
+
 open list
 
 universes u v

diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean
@@ -21,13 +21,20 @@ def list.as_string (s : list char) : string :=
 ⟨s⟩
 
 namespace string
+
 instance : has_lt string :=
 ⟨λ s₁ s₂, s₁.data < s₂.data⟩
 
 /- Remark: this function has a VM builtin efficient implementation. -/
 instance has_decidable_lt (s₁ s₂ : string) : decidable (s₁ < s₂) :=
 list.has_decidable_lt s₁.data s₂.data
 
+instance has_decidable_eq : decidable_eq string := λ ⟨x⟩ ⟨y⟩,
+match list.has_dec_eq x y with
+| is_true p := is_true (congr_arg string_imp.mk p)
+| is_false p := is_false (λ q, p (string_imp.mk.inj q))
+end
+
 def empty : string :=
 ⟨[]⟩
 

diff --git a/library/init/data/string/default.lean b/library/init/data/string/default.lean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.string.basic init.data.string.instances init.data.string.ops
+import init.data.string.basic init.data.string.ops
diff --git a/library/init/data/string/instances.lean b/library/init/data/string/instances.lean
diff --git a/library/init/meta/name.lean b/library/init/meta/name.lean
@@ -51,8 +51,7 @@ def name.update_prefix : name → name → name
 | (mk_string s p)  new_p := mk_string s new_p
 | (mk_numeral s p) new_p := mk_numeral s new_p
 
-/- The (decidable_eq string) has not been defined yet.
-   So, we disable the use of if-then-else when compiling the following definitions. -/
+-- Without this option, we get errors when defining the following definitions.
 set_option eqn_compiler.ite false
 
 def name.to_string_with_sep (sep : string) : name → string

diff --git a/library/init/meta/well_founded_tactics.lean b/library/init/meta/well_founded_tactics.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.meta init.data.sigma.lex init.data.nat.lemmas init.data.list.instances
-import init.data.list.qsort init.data.string.instances
+import init.data.list.qsort
 
 /- TODO(Leo): move this lemma, or delete it after we add algebraic normalizer. -/
 lemma nat.lt_add_of_zero_lt_left (a b : nat) (h : 0 < b) : a < a + b :=