Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-16 19:18 81dabdaf

View on Github →

feat(data/buffer/parser/*): expand parser properties (#6339) Add several new properties to parsers: static err_static step prog bounded unfailing conditionally_unfailing. Most of these properties hold cleanly for existing core parsers, and are provided as classes. This allows nice derivation for any parsers that are made using parser combinators. This PR is towards proving that the nat parser provides the maximal possible natural. Other API lemmas are introduced for string, buffer, char, and array.

Estimated changes

Modified src/data/buffer/basic.lean

added theorem buffer.ext_iff

added theorem buffer.nth_le_to_list'

added theorem buffer.nth_le_to_list

added theorem buffer.read_eq_nth_le_to_list

added theorem buffer.size_eq_zero_iff

added theorem buffer.size_nil

added theorem buffer.to_list_nil

added theorem buffer.to_list_to_array

Modified src/data/buffer/parser/basic.lean

modified theorem parser.any_char_eq_done

added theorem parser.any_char_eq_fail

added theorem parser.bounded.char_buf_iff

added theorem parser.bounded.decorate_error_iff

added theorem parser.bounded.decorate_errors_iff

added theorem parser.bounded.done_of_unbounded

added theorem parser.bounded.eof

added theorem parser.bounded.eps

added theorem parser.bounded.exists

added theorem parser.bounded.fix

added theorem parser.bounded.fix_core

added theorem parser.bounded.foldl

added theorem parser.bounded.foldl_core

added theorem parser.bounded.foldr

added theorem parser.bounded.foldr_core

added theorem parser.bounded.guard_iff

added theorem parser.bounded.many'

added theorem parser.bounded.many

added theorem parser.bounded.many_char

added theorem parser.bounded.of_done

added theorem parser.bounded.pure

added theorem parser.bounded.remaining

added theorem parser.bounded.str_iff

modified theorem parser.ch_eq_done

added theorem parser.char_buf_eq_done

added theorem parser.conditionally_unfailing.of_fail

modified theorem parser.digit_eq_done

added theorem parser.digit_eq_fail

modified theorem parser.eof_eq_done

modified theorem parser.eps_eq_done

added theorem parser.err_static.fix

added theorem parser.err_static.fix_core

added theorem parser.err_static.not_of_ne

added theorem parser.exists_done

added theorem parser.exists_done_in_bounds

modified theorem parser.guard_eq_done

modified theorem parser.many'_eq_done

added theorem parser.many1_bounded_of_done

added theorem parser.many1_eq_done_iff_many_eq_done

added theorem parser.many1_length_of_done

added theorem parser.many_eq_nil_of_done

added theorem parser.many_eq_nil_of_out_of_bound

added theorem parser.many_sublist_of_done

modified theorem parser.one_of'_eq_done

added theorem parser.prog.char_buf_iff

added theorem parser.prog.decorate_error_iff

added theorem parser.prog.decorate_errors_iff

added theorem parser.prog.eof

added theorem parser.prog.eps

added theorem parser.prog.fix

added theorem parser.prog.fix_core

added theorem parser.prog.guard_true

added theorem parser.prog.pure

added theorem parser.prog.remaining

added theorem parser.prog.str_iff

added theorem parser.remaining_ne_fail

added theorem parser.sat_eq_fail

added theorem parser.static.any_char

added theorem parser.static.ch

added theorem parser.static.char_buf_iff

added theorem parser.static.digit

added theorem parser.static.fix

added theorem parser.static.fix_core

added theorem parser.static.iff

added theorem parser.static.nat

added theorem parser.static.not_of_ne

added theorem parser.static.one_of'_iff

added theorem parser.static.one_of_iff

added theorem parser.static.sat_iff

added theorem parser.static.str_iff

added theorem parser.step.char_buf_iff

added theorem parser.step.decorate_error_iff

added theorem parser.step.decorate_errors_iff

added theorem parser.step.eof

added theorem parser.step.eps

added theorem parser.step.fix

added theorem parser.step.fix_core

added theorem parser.step.guard_true

added theorem parser.step.not_step_of_static_done

added theorem parser.step.pure

added theorem parser.step.remaining

added theorem parser.step.str_iff

added theorem parser.str_eq_char_buf

added theorem parser.str_eq_done

added theorem parser.unfailing.digit

added theorem parser.unfailing.failure

added theorem parser.unfailing.foldr_core_zero

added theorem parser.unfailing.guard

added theorem parser.unfailing.nat

added theorem parser.unfailing.of_bounded

added theorem parser.unfailing.of_fail

added theorem parser.unfailing.sat

Modified src/data/buffer/parser/numeral.lean

modified def parser.numeral.char.of_fintype

modified def parser.numeral.char

modified def parser.numeral.from_one.of_fintype

modified def parser.numeral.from_one

modified def parser.numeral.of_fintype

modified def parser.numeral

Modified src/data/char.lean

added theorem char.of_nat_to_nat

Modified src/data/string/basic.lean

added theorem list.length_as_string

added theorem string.length_to_list