feat: move and add theorems on `String` std4#124

Stream: std4

[Bulhwi Cha]

• Move helper simp theorems on String.Pos from Mathlib4 to Std4.
• Move String.utf8GetAux.inductionOn from Mathlib4 to Std4.
• Add new helper simp theorems on String.Pos.

[Bulhwi Cha]

!4#3712 deletes the theorems and the definition.

[Bulhwi Cha]

I've created two new files: Data.String.Basic and Data.String.Lemmas. Now Data.String imports them.

[Bulhwi Cha]

I deleted an obsolete theorem. I think !4#3712 is now ready to merge.

[Bulhwi Cha]

@Mario Carneiro Is it a good idea to change the name of the theorem String.addString_eq to String.addString_byteIdx and add the following theorems to Data.String.Lemmas?

theorem addString_eq (p : Pos) (s : String) : p + s = ⟨p.byteIdx + s.utf8ByteSize⟩ := rfl

theorem zero_addString_eq (s : String) : (0 : Pos) + s = ⟨s.utf8ByteSize⟩ := by
  rw [← zero_addString_byteIdx]

[Mario Carneiro]

@Bulhwi Cha LGTM

[Bulhwi Cha]

import Mathlib.Data.Nat.Order.Basic

example (a b c : Nat) (h : a = b) : a + c = b + c := by
  simp -- simp only [add_left_inj]
  exact h

Is there a way to make the above proof work in Std? I want simp to change a + c = b + c to a = b. If so, I can move more lemmas from Mathilb.Data.String.Basic to here. But I think this would be hard to do.

[Bulhwi Cha]

@Mario Carneiro, will you merge std4#128? I don't know any other way to prove drop_empty than using induction on the natural numbers. drop_eq's proof already uses drop_empty, so I can't use drop_eq to prove drop_empty.

[Kevin Buzzard]

Bulhwi Cha said:

import Mathlib.Data.Nat.Order.Basic

example (a b c : Nat) (h : a = b) : a + c = b + c := by
  simp -- simp only [add_left_inj]
  exact h

Is there a way to make the above proof work in Std? I want simp to change a + c = b + c to a = b. If so, I can move more lemmas from Mathilb.Data.String.Basic to here. But I think this would be hard to do.

If you want simp to do that then there needs to be a simp lemma saying a + c = b + c <-> a = b.

[Mario Carneiro]

it's not a simp lemma, that theorem is add_left_cancel which relies on AddLeftCancelSemigroup in mathlib

[Mario Carneiro]

just use simp [Nat.add_left_cancel]

[Bulhwi Cha]

Mario Carneiro said:

just use simp [Nat.add_left_cancel]

import Std.Data.String.Lemmas

namespace String

theorem utf8GetAux_add_right_cancel (s : List Char) (i p n : Nat) :
    utf8GetAux s ⟨i + n⟩ ⟨p + n⟩ = utf8GetAux s ⟨i⟩ ⟨p⟩ := by
  apply utf8InductionOn s ⟨i⟩ ⟨p⟩ (motive := fun s i ↦
    utf8GetAux s ⟨i.byteIdx + n⟩ ⟨p + n⟩ = utf8GetAux s i ⟨p⟩) <;>
  simp [utf8GetAux]
  intro c cs ⟨i⟩ h ih
  simp [Pos.ext_iff, Pos.addChar_eq] at *
  simp [Nat.add_left_cancel] -- this doesn't simplify `i + n = p + n` on the lhs of the goal
  sorry

[Bulhwi Cha]

Is there a way to simplify i + n = p + n on the left if-then-else statement of the goal?

[Mario Carneiro]

  simp [h, mt Nat.add_right_cancel h]
  rw [Nat.add_right_comm]; exact ih

works

[Mario Carneiro]

Nat.add_right_cancel isn't an iff statement so it doesn't really work well in the way you are trying to use it. I think there is an iff version called something like add_left_inj

[Bulhwi Cha]

There's Nat.add_left_cancel_iff. I've added Nat.add_right_cancel_iff to my PR: https://github.com/leanprover/std4/blob/bb3f17dc3cac77b7f15c4941acd20f3ca7a84ba8/Std/Data/Nat/Lemmas.lean#L64-L65

[Bulhwi Cha]

I moved more lemmas from Mathlib to Std, including drop_eq.