## Stream: general

### Topic: string_lt doesn't match its spec

#### Mario Carneiro (Jun 20 2018 at 22:14):

@Gabriel Ebner @Sebastian Ullrich I started trying to prove that string.lt is a total order, and then I discovered it's not true:

#eval to_bool ([1, 2] < [2, 1]) -- tt
#eval to_bool ([2, 1] < [1, 2]) -- tt


Surely this is a bug?

#### Mario Carneiro (Jun 20 2018 at 22:16):

Even worse, it behaves differently (correctly) on actual strings:

#eval to_bool ("ab" < "ba") -- tt
#eval to_bool ("ba" < "ab") -- ff
#reduce to_bool ("ba" < "ab") -- tt
example : "ba" < "ab" := dec_trivial


oops

#### Mario Carneiro (Jun 21 2018 at 01:13):

I'm using this in mathlib:

inductive lex (r : α → α → Prop) : list α → list α → Prop
| nil {} {a l} : lex [] (a :: l)
| cons {a l₁ l₂} (h : lex l₁ l₂) : lex (a :: l₁) (a :: l₂)
| rel {a₁ l₁ a₂ l₂} (h : r a₁ a₂) : lex (a₁ :: l₁) (a₂ :: l₂)


Feel free to poach

#### Sebastian Ullrich (Jun 21 2018 at 01:15):

Right, an inductive definition is certainly nicer here

#### Mario Carneiro (Jun 21 2018 at 01:16):

here's the decidability proof, although it needs rejiggering for core:

instance decidable_rel [decidable_eq α] (r : α → α → Prop)
[decidable_rel r] : decidable_rel (lex r)
| l₁ [] := is_false \$ λ h, by cases h
| [] (b::l₂) := is_true lex.nil
| (a::l₁) (b::l₂) := begin
haveI := decidable_rel l₁ l₂,
refine decidable_of_iff (r a b ∨ a = b ∧ lex r l₁ l₂) ⟨λ h, _, λ h, _⟩,
{ rcases h with h | ⟨rfl, h⟩,
{ exact lex.rel h },
{ exact lex.cons h } },
{ rcases h with _|⟨_,_,_,h⟩|⟨_,_,_,_,h⟩,
{ exact or.inr ⟨rfl, h⟩ },
{ exact or.inl h } }
end


Last updated: May 14 2021 at 22:15 UTC