string.bend checks

raw source on the hub · import bend-mathlib@0.7.1.0/string.bend as MString

bend-mathlib/string.bend: String append, reverse and length, and comparison. Comparison descends String.eq -> String.cmp -> Char.cmp -> U32.cmp -> Word.cmp.

3 imports

import Base
import ./nat.bend as MNat
import ./bool.bend as MBool

Laws

law append_nil provedsource · line 20 · raw

@a:String -> {String.append(a, "") == a : String}

The empty string is a right identity for append: a ++ "" = a.

law nil_append provedsource · line 28 · raw

@-a:String -> {String.append("", a) == a : String}

The empty string is a left identity for append: "" ++ a = a.

law append_assoc provedsource · line 44 · raw

@a:String -> @-b:String -> @-c:String -> {String.append(String.append(a, b), c) == String.append(a, String.append(b, c)) : String}

Append is associative: (a ++ b) ++ c = a ++ (b ++ c).

law length_append provedsource · line 62 · raw

@a:String -> @-b:String -> {String.length(String.append(a, b)) == Nat.add(String.length(a), String.length(b)) : Nat}

The length of an append is the sum of the lengths.

law reverse_go_spec provedsource · line 81 · raw

@s:String -> @acc:String -> {String.reverse.go(s, acc) == String.append(String.reverse(s), acc) : String}

The reverse accumulator loop appends the reversed string to the accumulator.

law reverse_append provedsource · line 102 · raw

@a:String -> @b:String -> {String.reverse(String.append(a, b)) == String.append(String.reverse(b), String.reverse(a)) : String}

Reversing an append reverses and swaps the parts: reverse (a ++ b) = reverse b ++ reverse a.

law reverse_reverse provedsource · line 121 · raw

@a:String -> {String.reverse(String.reverse(a)) == a : String}

Reversing twice gives the string back.

law u32_cmp_refl provedsource · line 146 · raw

@x:U32 -> {U32.cmp(x, x) == EQ{} : Cmp}

Comparing a U32 with itself gives EQ.

law char_cmp_refl provedsource · line 160 · raw

@c:Char -> {Char.cmp(c, c) == ((c, c), EQ{}) : Pair(Pair(Char, Char), Cmp)}

Comparing a character with itself gives EQ and hands both back.

law cmp_refl provedsource · line 179 · raw

@s:String -> {String.cmp(s, s) == ((s, s), EQ{}) : Pair(Pair(String, String), Cmp)}

Comparing a string with itself gives EQ and hands both back.

law eq_refl provedsource · line 187 · raw

@s:String -> {String.eq(s, s) == True{} : Bool}

Every string is equal to itself under String.eq.

law u32_eq_of_is_eq provedsource · line 227 · raw

@a:U32 -> @b:U32 -> @h:{U32.is_eq(a, b) == True{} : Bool} -> {a == b : U32}

Two U32s that U32.is_eq calls equal are equal.

law char_eq_of_is_eq provedsource · line 240 · raw

@a:Char -> @b:Char -> @h:{Char.is_eq(a, b) == True{} : Bool} -> {a == b : Char}

Two characters that Char.is_eq calls equal are equal.

law eq_of_eq_true provedsource · line 273 · raw

@a:String -> @b:String -> @h:{String.eq(a, b) == True{} : Bool} -> {a == b : String}

Two strings that String.eq calls equal are equal.

law length_reverse provedsource · line 299 · raw

@s:String -> {String.length(String.reverse(s)) == String.length(s) : Nat}

Reversing preserves the length.

law reverse_nil provedsource · line 308 · raw

{String.reverse("") == "" : String}

Reversing the empty string gives the empty string.

law reverse_singleton provedsource · line 315 · raw

@-c:Char -> {String.reverse(SCon{c, ""}) == SCon{c, ""} : String}

Reversing a one-character string gives it back.

law is_empty_iff_length_eq_zero provedsource · line 323 · raw

@s:String -> {String.is_empty(s) == Nat.is_eq(String.length(s), 0n) : Bool}

A string is empty exactly when its length is zero.

law is_empty_append provedsource · line 335 · raw

@a:String -> @-b:String -> {String.is_empty(String.append(a, b)) == Bool.and(String.is_empty(a), String.is_empty(b)) : Bool}

An append is empty exactly when both parts are.

law is_empty_reverse provedsource · line 355 · raw

@s:String -> {String.is_empty(String.reverse(s)) == String.is_empty(s) : Bool}

The reverse is empty exactly when the string is.

law take_append_drop provedsource · line 367 · raw

@s:String -> @n:Nat -> {String.append(String.take(s, n), String.drop(s, n)) == s : String}

Taking n characters and appending the rest after dropping n gives the string back.

law length_take provedsource · line 383 · raw

@s:String -> @n:Nat -> {String.length(String.take(s, n)) == Nat.min(n, String.length(s)) : Nat}

Taking n characters leaves min(n, length) of them.

law length_drop provedsource · line 399 · raw

@s:String -> @n:Nat -> {String.length(String.drop(s, n)) == Nat.sub(String.length(s), n) : Nat}

Dropping n characters leaves length - n of them.

law to_list_from_list provedsource · line 414 · raw

@cs:List<&2, Char> -> {String.to_list(String.from_list(cs)) == cs : List<&2, Char>}

Converting a character list to a string and back gives the list.

law from_list_to_list provedsource · line 427 · raw

@s:String -> {String.from_list(String.to_list(s)) == s : String}

Converting a string to a character list and back gives the string.

law to_list_append provedsource · line 440 · raw

@a:String -> @-b:String -> {String.to_list(String.append(a, b)) == List.append(&2, Char, String.to_list(a), String.to_list(b)) : List<&2, Char>}

The characters of an append are the characters of each part, appended.

law length_to_list provedsource · line 454 · raw

@s:String -> {List.length(&2, Char, String.to_list(s)) == String.length(s) : Nat}

A string has as many characters as its character list.

law append_nil_sym provedsource · line 469 · raw

@a:String -> {a == String.append(a, "") : String}

The empty string is a right identity for append: a ++ "" = a, reversed to rewrite toward the simple side.

law nil_append_sym provedsource · line 477 · raw

@-a:String -> {a == String.append("", a) : String}

The empty string is a left identity for append: "" ++ a = a, reversed to rewrite toward the simple side.

law append_assoc_sym provedsource · line 485 · raw

@a:String -> @-b:String -> @-c:String -> {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}

Append is associative: (a ++ b) ++ c = a ++ (b ++ c), reversed to rewrite toward the simple side.

law length_append_sym provedsource · line 495 · raw

@a:String -> @-b:String -> {Nat.add(String.length(a), String.length(b)) == String.length(String.append(a, b)) : Nat}

The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.

law reverse_go_spec_sym provedsource · line 504 · raw

@s:String -> @acc:String -> {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}

The reverse accumulator loop appends the reversed string to the accumulator, reversed to rewrite toward the simple side.

law reverse_append_sym provedsource · line 513 · raw

@a:String -> @b:String -> {String.append(String.reverse(b), String.reverse(a)) == String.reverse(String.append(a, b)) : String}

Reversing an append reverses and swaps the parts: reverse (a ++ b) = reverse b ++ reverse a, reversed to rewrite toward the simple side.

law reverse_reverse_sym provedsource · line 522 · raw

@a:String -> {a == String.reverse(String.reverse(a)) : String}

Reversing twice gives the string back, reversed to rewrite toward the simple side.

law u32_cmp_refl_sym provedsource · line 530 · raw

@x:U32 -> {EQ{} == U32.cmp(x, x) : Cmp}

Comparing a U32 with itself gives EQ, reversed to rewrite toward the simple side.

law char_cmp_refl_sym provedsource · line 538 · raw

@c:Char -> {((c, c), EQ{}) == Char.cmp(c, c) : Pair(Pair(Char, Char), Cmp)}

Comparing a character with itself gives EQ and hands both back, reversed to rewrite toward the simple side.

law cmp_refl_sym provedsource · line 546 · raw

@s:String -> {((s, s), EQ{}) == String.cmp(s, s) : Pair(Pair(String, String), Cmp)}

Comparing a string with itself gives EQ and hands both back, reversed to rewrite toward the simple side.

law eq_refl_sym provedsource · line 554 · raw

@s:String -> {True{} == String.eq(s, s) : Bool}

Every string is equal to itself under String.eq, reversed to rewrite toward the simple side.

law length_reverse_sym provedsource · line 562 · raw

@s:String -> {String.length(s) == String.length(String.reverse(s)) : Nat}

Reversing preserves the length, reversed to rewrite toward the simple side.

law reverse_nil_sym provedsource · line 570 · raw

{"" == String.reverse("") : String}

Reversing the empty string gives the empty string, reversed to rewrite toward the simple side.

law reverse_singleton_sym provedsource · line 577 · raw

@-c:Char -> {SCon{c, ""} == String.reverse(SCon{c, ""}) : String}

Reversing a one-character string gives it back, reversed to rewrite toward the simple side.

law is_empty_iff_length_eq_zero_sym provedsource · line 585 · raw

@s:String -> {Nat.is_eq(String.length(s), 0n) == String.is_empty(s) : Bool}

A string is empty exactly when its length is zero, reversed to rewrite toward the simple side.

law is_empty_append_sym provedsource · line 593 · raw

@a:String -> @-b:String -> {Bool.and(String.is_empty(a), String.is_empty(b)) == String.is_empty(String.append(a, b)) : Bool}

An append is empty exactly when both parts are, reversed to rewrite toward the simple side.

law is_empty_reverse_sym provedsource · line 602 · raw

@s:String -> {String.is_empty(s) == String.is_empty(String.reverse(s)) : Bool}

The reverse is empty exactly when the string is, reversed to rewrite toward the simple side.

law take_append_drop_sym provedsource · line 610 · raw

@s:String -> @n:Nat -> {s == String.append(String.take(s, n), String.drop(s, n)) : String}

Taking n characters and appending the rest after dropping n gives the string back, reversed to rewrite toward the simple side.

law length_take_sym provedsource · line 619 · raw

@s:String -> @n:Nat -> {Nat.min(n, String.length(s)) == String.length(String.take(s, n)) : Nat}

Taking n characters leaves min(n, length) of them, reversed to rewrite toward the simple side.

law length_drop_sym provedsource · line 628 · raw

@s:String -> @n:Nat -> {Nat.sub(String.length(s), n) == String.length(String.drop(s, n)) : Nat}

Dropping n characters leaves length - n of them, reversed to rewrite toward the simple side.

law to_list_from_list_sym provedsource · line 637 · raw

@cs:List<&2, Char> -> {cs == String.to_list(String.from_list(cs)) : List<&2, Char>}

Converting a character list to a string and back gives the list, reversed to rewrite toward the simple side.

law from_list_to_list_sym provedsource · line 645 · raw

@s:String -> {s == String.from_list(String.to_list(s)) : String}

Converting a string to a character list and back gives the string, reversed to rewrite toward the simple side.

law to_list_append_sym provedsource · line 653 · raw

@a:String -> @-b:String -> {List.append(&2, Char, String.to_list(a), String.to_list(b)) == String.to_list(String.append(a, b)) : List<&2, Char>}

The characters of an append are the characters of each part, appended, reversed to rewrite toward the simple side.

law length_to_list_sym provedsource · line 662 · raw

@s:String -> {String.length(s) == List.length(&2, Char, String.to_list(s)) : Nat}

A string has as many characters as its character list, reversed to rewrite toward the simple side.

Definitions

def internal_false_ne_true source · line 7 · raw

@e:{False{} == True{} : Bool} -> Empty

def internal_append_nil source · line 11 · raw

@a:String -> {a == String.append(a, "") : String}

def internal_append_assoc source · line 35 · raw

@a:String -> @-b:String -> @-c:String -> {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}

def internal_length_append source · line 53 · raw

@a:String -> @-b:String -> {Nat.add(String.length(a), String.length(b)) == String.length(String.append(a, b)) : Nat}

def internal_reverse_go_spec source · line 70 · raw

@s:String -> @+acc:String -> {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}

def internal_reverse_append source · line 89 · raw

@a:String -> @+b:String -> {String.append(String.reverse(b), String.reverse(a)) == String.reverse(String.append(a, b)) : String}

def internal_reverse_reverse source · line 110 · raw

@a:String -> {a == String.reverse(String.reverse(a)) : String}

def internal_word_cmp_refl source · line 128 · raw

@n:Nat -> @w:Word(n) -> {EQ{} == Word.cmp(n, w, w) : Cmp}

def internal_u32_cmp_refl source · line 139 · raw

@x:U32 -> {EQ{} == U32.cmp(x, x) : Cmp}

def internal_char_cmp_refl source · line 153 · raw

@c:Char -> {((c, c), EQ{}) == Char.cmp(c, c) : Pair(Pair(Char, Char), Cmp)}

def internal_cmp_refl source · line 167 · raw

@s:String -> {((s, s), EQ{}) == String.cmp(s, s) : Pair(Pair(String, String), Cmp)}

def internal_fin_head source · line 195 · raw

@ab:Bool -> @bb:Bool -> @c:Cmp -> @h:{Cmp.is_eq(Word.cmp.fin(ab, bb, c)) == True{} : Bool} -> {ab == bb : Bool}

def internal_fin_tail source · line 204 · raw

@ab:Bool -> @bb:Bool -> @c:Cmp -> @h:{Cmp.is_eq(Word.cmp.fin(ab, bb, c)) == True{} : Bool} -> {Cmp.is_eq(c) == True{} : Bool}

def internal_word_eq source · line 213 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @+h:{Cmp.is_eq(Word.cmp(n, a, b)) == True{} : Bool} -> {a == b : Word(n)}

def internal_rec_is_eq source · line 252 · raw

@h1:Char -> @h2:Char -> @rr:Pair(Pair(String, String), Cmp) -> {Cmp.is_eq(Pair.snd(Pair(String, String), Cmp, String.cmp.rec(h1, h2, rr))) == Cmp.is_eq(Pair.snd(Pair(String, String), Cmp, rr)) : Bool}

def internal_is_eq_of source · line 257 · raw

@c:Cmp -> @+d:Cmp -> @e:{c == d : Cmp} -> @h:{Cmp.is_eq(c) == True{} : Bool} -> {Cmp.is_eq(d) == True{} : Bool}

def internal_step source · line 261 · raw

@+x:U32 -> @+y:U32 -> @+t1:String -> @+t2:String -> @c:Cmp -> @ec:{c == U32.cmp(x, y) : Cmp} -> @h:{Cmp.is_eq(Pair.snd(Pair(String, String), Cmp, String.cmp.fin(t1, t2, ((Chr{x}, Chr{y}), c)))) == True{} : Bool} -> @ih:(@_:{String.eq(t1, t2) == True{} : Bool} -> {t1 == t2 : String}) -> {SCon{Chr{x}, t1} == SCon{Chr{y}, t2} : String}

def internal_length_reverse_go source · line 290 · raw

@s:String -> @-acc:String -> {Nat.add(String.length(s), String.length(acc)) == String.length(String.reverse.go(s, acc)) : Nat}

def internal_is_empty_reverse_go source · line 347 · raw

@s:String -> @-c:Char -> @-acc:String -> {String.is_empty(String.reverse.go(s, SCon{c, acc})) == False{} : Bool}