mathlib documentation

data.string.basic

Strings #

Supplementary theorems about the string type.

def string.ltb :

string.iterator → string.iterator → bool

< on string iterators. This coincides with < on strings as lists.

Equations

string.ltb s₁ s₂ = s₂.has_next.cases_on ff ((λ (_x : bool) (h₁ : s₁.has_next = _x), _x.cases_on (λ (h₁ : s₁.has_next = ff), tt) (λ (h₁ : s₁.has_next = tt), ite (s₁.curr = s₂.curr) (string.ltb s₁.next s₂.next) (to_bool (s₁.curr < s₂.curr))) h₁) s₁.has_next _)

@[protected, instance]

def string.has_lt' :

Equations

string.has_lt' = {lt := λ (s₁ s₂ : string), ↥(string.ltb s₁.mk_iterator s₂.mk_iterator)}

@[protected, instance]

def string.decidable_lt :

decidable_rel has_lt.lt

Equations

string.decidable_lt = λ (a b : string), bool.decidable_eq (string.ltb a.mk_iterator b.mk_iterator) tt

@[simp]

theorem string.lt_iff_to_list_lt {s₁ s₂ : string} :

s₁ < s₂ ↔ s₁.to_list < s₂.to_list

@[protected, instance]

def string.has_le :

Equations

string.has_le = {le := λ (s₁ s₂ : string), ¬s₂ < s₁}

@[protected, instance]

def string.decidable_le :

decidable_rel has_le.le

Equations

string.decidable_le = λ (a b : string), ne.decidable (string.ltb b.mk_iterator a.mk_iterator) tt

@[simp]

theorem string.le_iff_to_list_le {s₁ s₂ : string} :

s₁ ≤ s₂ ↔ s₁.to_list ≤ s₂.to_list

theorem string.to_list_inj {s₁ s₂ : string} :

s₁.to_list = s₂.to_list ↔ s₁ = s₂

theorem string.nil_as_string_eq_empty :

list.nil.as_string = ""

@[simp]

theorem string.to_list_empty :

"".to_list = list.nil

theorem string.as_string_inv_to_list (s : string) :

s.to_list.as_string = s

@[simp]

theorem string.to_list_singleton (c : char) :

(string.singleton c).to_list = [c]

theorem string.to_list_nonempty {s : string} :

s ≠ "" → s.to_list = s.head :: (s.popn 1).to_list

@[simp]

theorem string.head_empty :

"".head = default

@[simp]

theorem string.popn_empty {n : ℕ} :

"".popn n = ""

@[protected, instance]

def string.linear_order :

linear_order string

Equations

string.linear_order = {le := has_le.le string.has_le, lt := has_lt.lt string.has_lt', le_refl := string.linear_order._proof_1, le_trans := string.linear_order._proof_2, lt_iff_le_not_le := string.linear_order._proof_3, le_antisymm := string.linear_order._proof_4, le_total := string.linear_order._proof_5, decidable_le := string.decidable_le, decidable_eq := λ (a b : string), string.has_decidable_eq a b, decidable_lt := λ (a b : string), string.decidable_lt a b, max := max_default (λ (a b : string), string.decidable_le a b), max_def := string.linear_order._proof_10, min := min_default (λ (a b : string), string.decidable_le a b), min_def := string.linear_order._proof_11}

theorem list.to_list_inv_as_string (l : list char) :

l.as_string.to_list = l

@[simp]

theorem list.length_as_string (l : list char) :

l.as_string.length = l.length

@[simp]

theorem list.as_string_inj {l l' : list char} :

l.as_string = l'.as_string ↔ l = l'

@[simp]

theorem string.length_to_list (s : string) :

s.to_list.length = s.length

theorem list.as_string_eq {l : list char} {s : string} :

l.as_string = s ↔ l = s.to_list