Porting Data.String.Basic

Stream: mathlib4

[Richard Osborn]

I had a quick look at Data.String.Basic, and it seems that Data.String.Defs was only partially ported. Is the plan to finish porting the missing definitions in that file? I have also noticed that Control.Monad.Writer was partially ported as Control.Writer. Should Control.Monad.Writer now import Control.Writer?

[Scott Morrison]

When Control.Monad.Writer is fully ported, we should just delete Control.Writer (I'm presuming there is no control.writer in mathlib3).

[Arien Malec]

I suspect that a good chunk of Data.String.Basic is going to be #alignd away to Std

[Jakob von Raumer]

I've started to work on Data.String.Basic. There's the issue that the new implementation of Iterator looks completely different under the hood and it seems harder to prove anything about it

[Jakob von Raumer]

Also, I'm not really sure why the file adds an additional instance of LT String

[Jakob von Raumer]

The same goes for properties of evyerthing that's built on top of String.extract which now uses an external function and UTF8 byte indices. So to prove anything meaningful about these String operations would require a whole stack of helper lemmas

[Mario Carneiro]

Those helper lemmas sound like something to be added to std

[Jakob von Raumer]

The only place where the stuff in Data.String.Basic is needed, is Data.Buffer.Parser.Basic of which I'm not sure if it's well-portable either

[Arien Malec]

Scott Morrison said:

When Control.Monad.Writer is fully ported, we should just delete Control.Writer (I'm presuming there is no control.writer in mathlib3).

I'm looking at Control.Monad.Writer -- do I want to move code from Control.Writer here?

[Arien Malec]

i.e., as part of the single PR?

[Scott Morrison]

I think that would be fine.

[Jakob von Raumer]

Made a new PR for this: mathlib4#1054

[Jakob von Raumer]

Some stuff involving Iterator, String.popn and String.head still missing

[Arien Malec]

This reminds me that I keep going back to the proofs in Control.Monad.Writer and getting stuck.

Happy to unwind the PR here.

[Jakob von Raumer]

So the one thing I'm stuck at is to prove that Iterator.hasNext { s := { data := hd :: tl }, i := 0 } holds

[Bulhwi Cha]

I'm trying to rewrite the proof of String.lt_iff_toList_lt from the beginning, but I'm stuck on the following goal:

case cons.cons.inl
c₁ : Char
cs₁ : List Char
ih : ∀ (l₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := l₂ }, i := 0 } = true ↔ cs₁ < l₂
cs₂ : List Char
⊢ ltb { s := { data := c₁ :: cs₁ }, i := { byteIdx := csize c₁ } }
    { s := { data := c₁ :: cs₂ }, i := { byteIdx := csize c₁ } } =
  ltb { s := { data := cs₁ }, i := 0 } { s := { data := cs₂ }, i := 0 }

The above goal is the tactic state of the sorry in my proof:

String.lt_iff_toList_lt

/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.string.basic
! leanprover-community/mathlib commit d13b3a4a392ea7273dfa4727dbd1892e26cfd518
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.Lex
import Mathlib.Data.Char

/-!
# Strings

Supplementary theorems about the `String` type.
-/

namespace String

@[simp]
theorem Pos.zero_byteIdx : (0 : Pos).byteIdx = 0 :=
  rfl

@[simp]
theorem Pos.zero_add (i : Pos) : 0 + i = i := by
  show ⟨0 + i.byteIdx⟩ = i
  rw [Nat.zero_add]

@[simp]
theorem Pos.zero_add_char (c : Char) : (0 : Pos) + c = ⟨csize c⟩ := by
  show ⟨0 + csize c⟩ = (⟨csize c⟩ : Pos)
  rw [Nat.zero_add]

@[simp]
theorem Pos.zero_add_string (s : String) : (0 : Pos) + s = ⟨s.utf8ByteSize⟩ := by
  show ⟨0 + s.utf8ByteSize⟩ = (⟨s.utf8ByteSize⟩ : Pos)
  rw [Nat.zero_add]

/-- `<` on string iterators. This coincides with `<` on strings as lists. -/
def ltb (s₁ s₂ : Iterator) : Bool :=
  if s₂.hasNext then
    if s₁.hasNext then
      if s₁.curr = s₂.curr then
        have : s₁.i < s₁.next.i :=
          match s₁ with
          | ⟨s, i⟩ => show i.byteIdx < i.byteIdx + csize (get s i) from
            Nat.lt_add_of_pos_right (csize_pos (get s i))
        ltb s₁.next s₂.next
      else s₁.curr < s₂.curr
    else true
  else false
#align string.ltb String.ltb

theorem ltb.inductionOn.{u} {motive : Iterator → Iterator → Sort u} (s₁ s₂ : Iterator)
    (ind : ∀ s₁ s₂ i₁ i₂, Iterator.hasNext ⟨s₂, i₂⟩ → Iterator.hasNext ⟨s₁, i₁⟩ →
      get s₁ i₁ = get s₂ i₂ → motive (Iterator.next ⟨s₁, i₁⟩) (Iterator.next ⟨s₂, i₂⟩) →
      motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩)
    (base_eq : ∀ s₁ s₂ i₁ i₂, Iterator.hasNext ⟨s₂, i₂⟩ → Iterator.hasNext ⟨s₁, i₁⟩ →
      ¬ get s₁ i₁ = get s₂ i₂ → motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩)
    (base₁ : ∀ s₁ s₂ i₁ i₂, ¬ Iterator.hasNext ⟨s₁, i₁⟩ → motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩)
    (base₂ : ∀ s₁ s₂ i₁ i₂, ¬ Iterator.hasNext ⟨s₂, i₂⟩ → motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩) :
    motive s₁ s₂ :=
  if h₂ : s₂.hasNext then
    if h₁ : s₁.hasNext then
      if eq : s₁.curr = s₂.curr then
        ind s₁.s s₂.s s₁.i s₂.i h₂ h₁ eq (inductionOn s₁.next s₂.next ind base_eq base₁ base₂)
      else base_eq s₁.s s₂.s s₁.i s₂.i h₂ h₁ eq
    else base₁ s₁.s s₂.s s₁.i s₂.i h₁
  else base₂ s₁.s s₂.s s₁.i s₂.i h₂

instance LT' : LT String :=
  ⟨fun s₁ s₂ => ltb s₁.mkIterator s₂.mkIterator⟩
#align string.has_lt' String.LT'

instance decidableLT : @DecidableRel String (· < ·) := by
  simp only [LT']
  infer_instance
#align string.decidable_lt String.decidableLT

-- short-circuit type class inference
@[simp]
theorem lt_iff_toList_lt : ∀ {s₁ s₂ : String}, s₁ < s₂ ↔ s₁.toList < s₂.toList
  | ⟨l₁⟩, ⟨l₂⟩ => show ltb ⟨⟨l₁⟩, 0⟩ ⟨⟨l₂⟩, 0⟩ ↔ l₁ < l₂ by
    induction l₁ generalizing l₂ <;> cases l₂
    . simp
    . rename_i c₂ cs₂; apply iff_of_true
      . rw [ltb]; simp; apply ne_false_of_eq_true; apply decide_eq_true
        apply Nat.add_pos_right (utf8ByteSize.go cs₂) (csize_pos c₂)
      . apply List.nil_lt_cons
    . rename_i c₁ cs₁ ih; apply iff_of_false
      . rw [ltb]; simp
      . apply not_lt_of_lt; apply List.nil_lt_cons
    . rename_i c₁ cs₁ ih c₂ cs₂; rw [ltb]
      simp [Iterator.hasNext, Iterator.curr, Iterator.next, next, endPos, utf8ByteSize,
            utf8ByteSize.go, csize_pos]; rw [decide_eq_true_iff]
      show (if c₁ = c₂ then
              ltb ⟨⟨c₁ :: cs₁⟩, ⟨csize c₁⟩⟩ ⟨⟨c₂ :: cs₂⟩, ⟨csize c₂⟩⟩ = true
            else c₁ < c₂) ↔ c₁ :: cs₁ < c₂ :: cs₂
      split_ifs with h
      . subst c₂
        suffices ltb ⟨⟨c₁ :: cs₁⟩, ⟨csize c₁⟩⟩ ⟨⟨c₁ :: cs₂⟩, ⟨csize c₁⟩⟩ = ltb ⟨⟨cs₁⟩, 0⟩ ⟨⟨cs₂⟩, 0⟩
          by rw [this]; exact (ih cs₂).trans List.Lex.cons_iff.symm
        sorry
      . refine ⟨List.Lex.rel, fun e => ?_⟩
        cases e <;> rename_i h'
        . contradiction
        . assumption
#align string.lt_iff_to_list_lt String.lt_iff_toList_lt

Jakob von Raumer said:

The same goes for properties of evyerthing that's built on top of String.extract which now uses an external function and UTF8 byte indices. So to prove anything meaningful about these String operations would require a whole stack of helper lemmas

I don't know whether I should create a new git branch because I'm attempting not to use these helper lemmas to prove String.lt_iff_toList_lt.

[Bulhwi Cha]

I've managed to prove String.lt_iff_toList_lt. This theorem took me over 30 hours to prove. I'll soon push my commit to the git branch.

It's my first time porting a Mathlib file, and I think I picked the wrong one for a novice. :smiling_face_with_tear:

String.lt_iff_toList_lt

/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.string.basic
! leanprover-community/mathlib commit d13b3a4a392ea7273dfa4727dbd1892e26cfd518
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.Lex
import Mathlib.Data.Char

/-!
# Strings

Supplementary theorems about the `String` type.
-/

namespace String

@[simp]
theorem Pos.eq_iff {i₁ i₂ : Pos} : i₁ = i₂ ↔ i₁.byteIdx = i₂.byteIdx :=
  ⟨fun h ↦ h ▸ rfl, fun h ↦ show ⟨i₁.byteIdx⟩ = (⟨i₂.byteIdx⟩ : Pos) from h ▸ rfl⟩

@[simp]
theorem Pos.zero_add_char (c : Char) : (0 : Pos) + c = ⟨csize c⟩ :=
  show ⟨0 + csize c⟩ = (⟨csize c⟩ : Pos) by rw [Nat.zero_add]

@[simp]
theorem Pos.zero_add_string (s : String) : (0 : Pos) + s = ⟨s.utf8ByteSize⟩ :=
  show ⟨0 + s.utf8ByteSize⟩ = (⟨s.utf8ByteSize⟩ : Pos) by rw [Nat.zero_add]

/-- Induction on `String.utf8GetAux`. -/
def utf8GetAux.inductionOn.{u} {motive : List Char → Pos → Pos → Sort u}
    (s : List Char) (i p : Pos)
    (nil : ∀ i p, motive [] i p)
    (eq  : ∀ c cs i p, i = p → motive (c :: cs) i p)
    (ind : ∀ c cs i p, i ≠ p → motive cs ⟨i.byteIdx + csize c⟩ p → motive (c :: cs) i p) :
    motive s i p :=
  match s with
  | [] => nil i p
  | c::cs =>
    if h : i = p then
      eq c cs i p h
    else ind c cs i p h (inductionOn cs ⟨i.byteIdx + csize c⟩ p nil eq ind)

lemma utf8GetAux.add_right_cancel (i p n : ℕ) (s : List Char) :
    utf8GetAux s ⟨i + n⟩ ⟨p + n⟩ = utf8GetAux s ⟨i⟩ ⟨p⟩ := by
  apply utf8GetAux.inductionOn s ⟨i⟩ ⟨p⟩ (motive := fun s i p ↦
    utf8GetAux s ⟨i.byteIdx + n⟩ ⟨p.byteIdx + n⟩ = utf8GetAux s i p) <;>
  simp [utf8GetAux]
  · intro c cs ⟨i⟩ ⟨p⟩ h
    simp at h
    subst i
    simp
  · intro c cs ⟨i⟩ ⟨p⟩ h ih
    simp at h
    simp [h]
    show utf8GetAux cs ⟨i + n + csize c⟩ ⟨p + n⟩ = utf8GetAux cs ⟨i + csize c⟩ ⟨p⟩
    rw [Nat.add_right_comm]
    exact ih

lemma get.cons_add_csize (c : Char) (cs : List Char) (i : ℕ) :
    get ⟨c :: cs⟩ ⟨i + csize c⟩ = get ⟨cs⟩ ⟨i⟩ := by
  have : 0 ≠ i + csize c := Nat.ne_of_lt (Nat.add_pos_right i (csize_pos c))
  simp [get, utf8GetAux, this]
  rw [← Pos.zero_add_char]
  apply utf8GetAux.add_right_cancel

lemma Iterator.hasNext.cons_add_csize (c : Char) (cs : List Char) (i : ℕ) :
    hasNext ⟨⟨c :: cs⟩, ⟨i + csize c⟩⟩ = hasNext ⟨⟨cs⟩, ⟨i⟩⟩ := by
  simp [hasNext, endPos, utf8ByteSize, utf8ByteSize.go]

/-- `<` on string iterators. This coincides with `<` on strings as lists. -/
def ltb (s₁ s₂ : Iterator) : Bool :=
  if s₂.hasNext then
    if s₁.hasNext then
      if s₁.curr = s₂.curr then
        ltb s₁.next s₂.next
      else s₁.curr < s₂.curr
    else true
  else false
#align string.ltb String.ltb

instance LT' : LT String :=
  ⟨fun s₁ s₂ ↦ ltb s₁.iter s₂.iter⟩
#align string.has_lt' String.LT'

instance decidableLT : @DecidableRel String (· < ·) := by
  simp only [LT']
  infer_instance
#align string.decidable_lt String.decidableLT

/-- Induction on `String.ltb`. -/
def ltb.inductionOn.{u} {motive : Iterator → Iterator → Sort u} (it₁ it₂ : Iterator)
    (ind : ∀ s₁ s₂ i₁ i₂, Iterator.hasNext ⟨s₂, i₂⟩ → Iterator.hasNext ⟨s₁, i₁⟩ →
      get s₁ i₁ = get s₂ i₂ → motive (Iterator.next ⟨s₁, i₁⟩) (Iterator.next ⟨s₂, i₂⟩) →
      motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩)
    (eq : ∀ s₁ s₂ i₁ i₂, Iterator.hasNext ⟨s₂, i₂⟩ → Iterator.hasNext ⟨s₁, i₁⟩ →
      ¬ get s₁ i₁ = get s₂ i₂ → motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩)
    (base₁ : ∀ s₁ s₂ i₁ i₂, Iterator.hasNext ⟨s₂, i₂⟩ → ¬ Iterator.hasNext ⟨s₁, i₁⟩ →
      motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩)
    (base₂ : ∀ s₁ s₂ i₁ i₂, ¬ Iterator.hasNext ⟨s₂, i₂⟩ → motive ⟨s₁, i₁⟩ ⟨s₂, i₂⟩) :
    motive it₁ it₂ :=
if h₂ : it₂.hasNext then
    if h₁ : it₁.hasNext then
      if heq : it₁.curr = it₂.curr then
        ind it₁.s it₂.s it₁.i it₂.i h₂ h₁ heq (inductionOn it₁.next it₂.next ind eq base₁ base₂)
      else eq it₁.s it₂.s it₁.i it₂.i h₂ h₁ heq
    else base₁ it₁.s it₂.s it₁.i it₂.i h₂ h₁
  else base₂ it₁.s it₂.s it₁.i it₂.i h₂

lemma ltb.cons_add_csize (c : Char) (cs₁ cs₂ : List Char) (i₁ i₂ : ℕ) :
    ltb ⟨⟨c :: cs₁⟩, ⟨i₁ + csize c⟩⟩ ⟨⟨c :: cs₂⟩, ⟨i₂ + csize c⟩⟩ =
    ltb ⟨⟨cs₁⟩, ⟨i₁⟩⟩ ⟨⟨cs₂⟩, ⟨i₂⟩⟩ := by
  apply ltb.inductionOn ⟨⟨cs₁⟩, ⟨i₁⟩⟩ ⟨⟨cs₂⟩, ⟨i₂⟩⟩ (motive := fun ⟨⟨cs₁⟩, ⟨i₁⟩⟩ ⟨⟨cs₂⟩, ⟨i₂⟩⟩ ↦
    ltb ⟨⟨c :: cs₁⟩, ⟨i₁ + csize c⟩⟩ ⟨⟨c :: cs₂⟩, ⟨i₂ + csize c⟩⟩ =
    ltb ⟨⟨cs₁⟩, ⟨i₁⟩⟩ ⟨⟨cs₂⟩, ⟨i₂⟩⟩) <;> simp <;>
  intro ⟨cs₁⟩ ⟨cs₂⟩ ⟨i₁⟩ ⟨i₂⟩ <;>
  intros <;>
  (conv => lhs; rw [ltb]) <;> (conv => rhs; rw [ltb]) <;>
  simp [Iterator.hasNext.cons_add_csize, *]
  · rename_i h₂ h₁ heq ih
    simp [Iterator.curr, Iterator.next, next, Iterator.hasNext.cons_add_csize,
          get.cons_add_csize, *] at *
    show ltb ⟨⟨c :: cs₁⟩, ⟨i₁ + csize c + csize (get ⟨cs₂⟩ ⟨i₂⟩)⟩⟩
             ⟨⟨c :: cs₂⟩, ⟨i₂ + csize c + csize (get ⟨cs₂⟩ ⟨i₂⟩)⟩⟩ =
         ltb ⟨⟨cs₁⟩, ⟨i₁ + csize (get ⟨cs₂⟩ ⟨i₂⟩)⟩⟩ ⟨⟨cs₂⟩, ⟨i₂ + csize (get ⟨cs₂⟩ ⟨i₂⟩)⟩⟩
    repeat rw [Nat.add_right_comm _ (csize c)]
    exact ih
  · rename_i h₂ h₁ hne
    simp [Iterator.curr, Iterator.hasNext.cons_add_csize, get.cons_add_csize, *] at *

-- short-circuit type class inference
@[simp]
theorem lt_iff_toList_lt : ∀ {s₁ s₂ : String}, s₁ < s₂ ↔ s₁.toList < s₂.toList
| ⟨s₁⟩, ⟨s₂⟩ => show ltb ⟨⟨s₁⟩, 0⟩ ⟨⟨s₂⟩, 0⟩ ↔ s₁ < s₂ by
  induction s₁ generalizing s₂ <;> cases s₂
  · simp
  · rename_i c₂ cs₂; apply iff_of_true
    · rw [ltb]; simp; apply ne_false_of_eq_true; apply decide_eq_true
      simp [endPos, utf8ByteSize, utf8ByteSize.go, csize_pos]
    · apply List.nil_lt_cons
  · rename_i c₁ cs₁ ih; apply iff_of_false
    · rw [ltb]; simp
    · apply not_lt_of_lt; apply List.nil_lt_cons
  · rename_i c₁ cs₁ ih c₂ cs₂; rw [ltb]
    simp [Iterator.hasNext, Iterator.curr, Iterator.next, next, endPos, utf8ByteSize,
          utf8ByteSize.go, csize_pos]; rw [decide_eq_true_iff]
    show (if c₁ = c₂ then
            ltb ⟨⟨c₁ :: cs₁⟩, ⟨csize c₁⟩⟩ ⟨⟨c₂ :: cs₂⟩, ⟨csize c₂⟩⟩ = true
          else c₁ < c₂) ↔ c₁ :: cs₁ < c₂ :: cs₂
    split_ifs with h
    · subst c₂
      suffices ltb ⟨⟨c₁ :: cs₁⟩, ⟨csize c₁⟩⟩ ⟨⟨c₁ :: cs₂⟩, ⟨csize c₁⟩⟩ = ltb ⟨⟨cs₁⟩, 0⟩ ⟨⟨cs₂⟩, 0⟩
        by rw [this]; exact (ih cs₂).trans List.Lex.cons_iff.symm
      rw [← Pos.zero_add_char]
      apply ltb.cons_add_csize
    · refine ⟨List.Lex.rel, fun e ↦ ?_⟩
      cases e <;> rename_i h'
      · contradiction
      · assumption
#align string.lt_iff_to_list_lt String.lt_iff_toList_lt

[Eric Wieser]

Why did you choose to rewrite it from scratch?

[Bulhwi Cha]

The previous proof didn't work, and its comment said, "TODO This proof probably has to be completely redone."

[Bulhwi Cha]

Jakob von Raumer said:

I've started to work on Data.String.Basic. There's the issue that the new implementation of Iterator looks completely different under the hood and it seems harder to prove anything about it

I had to prove several new theorems and lemmas because the definition of String.Iterator in Mathlib4 was different from that of Mathlib3.

[Eric Wieser]

docs4#String.Iterator, docs#string.iterator

[Eric Wieser]

Does it help to define String.Iterator.fst as it.extract it.toEnd and String.Iterator.snd as it.string.iter.extract it, and then use those two properties as before?

[Bulhwi Cha]

I'm not sure, but I assume it'll help only when you change the definition of String.Iterator back into the Mathlib3 one.

[Bulhwi Cha]

Richard Osborn said:

I had a quick look at Data.String.Basic, and it seems that Data.String.Defs was only partially ported. Is the plan to finish porting the missing definitions in that file?

I'll port data.string.defs before I push my commit to the port-data-string-basic-2 branch.

I first pushed my commits to the port-data-string-basic-2 branch, since porting data.string.defs would take more time than I expected.

[Bulhwi Cha]

I think !4#1054 is now ready to merge. :smile:

[Jakob von Raumer]

That's really cool! I felt bad about letting it sit for so long

[Bulhwi Cha]

instance : LinearOrder String where
  le_refl a := le_iff_toList_le.mpr le_rfl
  le_trans a b c := by
    simp only [le_iff_toList_le]
    apply le_trans
  lt_iff_le_not_le a b := by
    simp only [le_iff_toList_le, lt_iff_toList_lt, lt_iff_le_not_le]
  le_antisymm a b := by
    simp only [le_iff_toList_le, ← toList_inj]
    apply le_antisymm
  le_total a b := by
    simp only [le_iff_toList_le]
    apply le_total
  decidable_le := String.decidableLE

The above code has the following error, which didn't occur before. Can anyone tell me how to solve this goal?

unsolved goals
case mk.mk
data✝¹ data✝: List Char
⊢ compare { data := data✝¹ } { data := data✝ } = compareOfLessAndEq { data := data✝¹ } { data := data✝ }

GitHub PR discussion: https://github.com/leanprover-community/mathlib4/pull/1054#discussion_r1158533762

[Ruben Van de Velde]

Maybe related to !4#2858

[Bulhwi Cha]

Solution: add the line compare a b := compareOfLessAndEq a b to the instance declaration.

[Notification Bot]

Jeremy Tan has marked this topic as resolved.

[Eric Wieser]

That's the wrong solution

[Eric Wieser]

It discards the optimized string comparison function and replaces it with the naive one

[Yaël Dillies]

@Jeremy Tan, please don't resolve topics you're not involved in.

[Yaël Dillies]

Or simply don't resolve topics. It's noisy and broken.

[Eric Wieser]

(re "broken": if you resolve a topic, anyone who shared a link to that topic will find that the link they shared no longer works)

[Notification Bot]

Jeremy Tan has marked this topic as unresolved.

[Bulhwi Cha]

Eric Wieser said:

It discards the optimized string comparison function and replaces it with the naive one

Hmm, I'm not sure what I should do to solve the error correctly. Can you help me?

[Eric Wieser]

You need to provide a manual compare_eq field, I think

[Eric Wieser]

The error is coming from the default value for a proof field which no longer works; you need to provide that proof field explicitly, rather than replacing the data field with something that creates a diamond.

[Eric Wieser]

I'm afraid I don't know the name of the field; does the error message not tell you?

[Bulhwi Cha]

Eric Wieser said:

I'm afraid I don't know the name of the field; does the error message not tell you?

No, I don't think it does:

unsolved goals
case mk.mk
data✝¹ data✝: List Char
⊢ compare { data := data✝¹ } { data := data✝ } = compareOfLessAndEq { data := data✝¹ } { data := data✝ }

Is the field you mentioned compare_eq_compareOfLessAndEq?

[Ruben Van de Velde]

instance : LinearOrder String where
  le_refl a := le_iff_toList_le.mpr le_rfl
  le_trans a b c := by
    simp only [le_iff_toList_le]
    apply le_trans
  lt_iff_le_not_le a b := by
    simp only [le_iff_toList_le, lt_iff_toList_lt, lt_iff_le_not_le]
  le_antisymm a b := by
    simp only [le_iff_toList_le, ← toList_inj]
    apply le_antisymm
  le_total a b := by
    simp only [le_iff_toList_le]
    apply le_total
  decidable_le := String.decidableLE
  compare_eq_compareOfLessAndEq := sorry

[Bulhwi Cha]

Eric Wieser said:

The error is coming from the default value for a proof field which no longer works; you need to provide that proof field explicitly, rather than replacing the data field with something that creates a diamond.

Right now, I'm clueless about how to prove compare_eq_compareOfLessAndEq. I'll try it again later.

[Ruben Van de Velde]

I'm confused - the PR seems to be closed already?

[Bulhwi Cha]

Yes. :worried:

[Bulhwi Cha]

Eric Wieser said:

It discards the optimized string comparison function and replaces it with the naive one

Can you elaborate on "the optimized string comparison function"?

[Bulhwi Cha]

Here is my attempt to prove compare_eq_compareOfLessAndEq:

import Mathlib.Data.String.Basic

namespace String

instance : LinearOrder String where
  le_refl a := le_iff_toList_le.mpr le_rfl
  le_trans a b c := by
    simp only [le_iff_toList_le]
    apply le_trans
  lt_iff_le_not_le a b := by
    simp only [le_iff_toList_le, lt_iff_toList_lt, lt_iff_le_not_le]
  le_antisymm a b := by
    simp only [le_iff_toList_le, ← toList_inj]
    apply le_antisymm
  le_total a b := by
    simp only [le_iff_toList_le]
    apply le_total
  decidable_le := String.decidableLE
  compare_eq_compareOfLessAndEq a b := by
    simp [compare, compareOfLessAndEq]
    split_ifs <;>
    rw [← lt_iff_toList_lt] at * <;>
    sorry

end String

[Ruben Van de Velde]

So where is the code that doesn't work? Or can you make a #mwe including imports?

[Bulhwi Cha]

I edited the above message.

[Bulhwi Cha]

Data.String.Basic has the instance String.LT', which overrides the default instance of LT String.

[Bulhwi Cha]

So, how do you close the following goal?

a b : String
h1: @LT.lt String instLTString a b
h2: ¬ @LT.lt String LT' a b
h3: ¬ a = b
⊢ False

[Bulhwi Cha]

Bulhwi Cha said:

Solution: add the line compare a b := compareOfLessAndEq a b to the instance declaration.

I don't know. Perhaps my naive solution isn't wrong?

[Eric Wieser]

It is wrong, because there is already a docs4#instOrdString and your fix creates a second instance that is not defeq

[Bulhwi Cha]

"404 Not Found"

[Eric Wieser]

The sorry you're stuck on is proving that the instance you wanted to provide is defeq to the existing one. The proof is probably not completely trivial.

[Eric Wieser]

Although now I'm questioning whether it's actually not already defeq

[Eric Wieser]

Although now I'm questioning whether it's actually not already defeq

[Eric Wieser]

@thorimur can probably advise here, I'm not at lean so can't really help.

[Bulhwi Cha]

This might be relevant: https://github.com/leanprover-community/mathlib4/blob/a897757abcb0bffa1dc96f46017f1d65e0fd1f9b/Mathlib/Data/List/Lex.lean#L178-L181

It's 3:12 a.m. here in KR, so I'll get into bed now. :in_bed:

[Eric Wieser]

I don't think it's urgent to fix this

[Eric Wieser]

Feel free to open an issue, assign it to me/ thorimur, and abandon it entirely if you're not that interested in this.

[Bulhwi Cha]

import Mathlib.Data.String.Basic

open String

theorem List.lt_iff_lex_char_lt (l l' : List Char) : List.lt l l' ↔ List.Lex Char.lt l l' := by
  constructor
  · intro h
    induction h with
    | nil b bs => exact Lex.nil
    | @head a as b bs hab => apply Lex.rel; assumption
    | @tail a as b bs hab hba _ ih =>
      have heq : a = b := _root_.le_antisymm (le_of_not_lt hba) (le_of_not_lt hab)
      subst b; apply Lex.cons; assumption
  · intro h
    induction h with
    | @nil a as => apply List.lt.nil
    | @cons a as bs _ ih => apply List.lt.tail <;> simp [ih]
    | @rel a as b bs h => apply List.lt.head; assumption

namespace String

instance : LinearOrder String where
  le_refl a := le_iff_toList_le.mpr le_rfl
  le_trans a b c := by
    simp only [le_iff_toList_le]
    apply le_trans
  lt_iff_le_not_le a b := by
    simp only [le_iff_toList_le, lt_iff_toList_lt, lt_iff_le_not_le]
  le_antisymm a b := by
    simp only [le_iff_toList_le, ← toList_inj]
    apply le_antisymm
  le_total a b := by
    simp only [le_iff_toList_le]
    apply le_total
  decidable_le := String.decidableLE
  compare_eq_compareOfLessAndEq a b := by
    simp [compare, compareOfLessAndEq, toList, instLTString, List.instLTList, List.LT']
    split_ifs <;>
    simp [List.lt_iff_lex_char_lt] at * <;>
    contradiction

end String

Eric Wieser said:

The sorry you're stuck on is proving that the instance you wanted to provide is defeq to the existing one. The proof is probably not completely trivial.

It took me over an hour to prove compare_eq_compareOfLessAndEq. Thank you so much for your guidance!

[Bulhwi Cha]

GitHub PR: !4#3339

[Alex J. Best]

Eric Wieser said:

(re "broken": if you resolve a topic, anyone who shared a link to that topic will find that the link they shared no longer works)

Is that still true? I thought zulip fixed that long ago https://github.com/zulip/zulip/issues/19651. If not we should report it of course