string.bend checks

raw source on the hub · import 0x89df026edd2acf2673b5e469e037eaf1/string.bend as MString

String.append and String.reverse — the lemmas Base does not ship.

Base has 40 String functions and zero facts about any of them; every proof that touches strings writes these by hand. First written for the Life proofs of bend2-from-zero, extracted here so the next proof can import them. The rewrite rule that fixes each statement's orientation: %lem(args) : P P is the goal AFTER the rewrite, with _ at the position the lemma's LEFT side was put in; the right side is the form being eliminated.

append_nil2 {a == append(a, "")} eliminates append(a, "") append_assoc2 {append(a, append(b,c)) == append(append(a,b), c)} reverse_go_spec {append(reverse(s), acc) == reverse.go(s, acc)} reverse_append2 {append(reverse(b), reverse(a)) == reverse(append(a, b))} reverse_reverse {a == reverse(reverse(a))} eliminates reverse(reverse(a))

1 import

import Base

Definitions

def append_nil2 source · line 19 · raw

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

def append_assoc2 source · line 27 · raw

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

def reverse_go_spec source · line 36 · raw

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

def reverse_append2 source · line 47 · raw

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

def reverse_reverse source · line 60 · raw

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