Closing bounds on encoded lengths

enc_len expands encoded lengths into the lengths of their fields, then counts with omega.

The expansion is simp only with a fixed list of lemmas for the standard encodings (including nil and cons of encList), followed by the lemmas given at the call. Local encodings stay visible there: enc_len [eFoo_apply]. The location works as for simp, so hypotheses are expanded only when requested, as in enc_len at h ⊢.

omega treats a product of two lengths as an atom, which it can match only when both sides expanded to the same term. Bound a product by a fact in its own step, and bound each component by one context length in its own step, so that the last enc_len only adds. Expanding everything at once costs more: omega slows sharply with the number of atoms and facts.

The tactic fails when nothing expands, naming the plain omega that is then the right call, and when omega cannot close the expanded goal, showing that goal.

Main definitions

• enc_len: expand encoded lengths into their fields and close the bound with omega.

def Cslib.Tactic.EncLen.encLen : Lean.ParserDescr

enc_len closes a linear bound on encoded lengths: it expands standard encodings (pairs, frames, unary numbers, raw bit lists, Booleans, options, sums, and nil/cons of framed lists) into the lengths of their fields with simp only, then runs omega.

• enc_len [eFoo_apply] also unfolds the local encoding eFoo.
• enc_len at h ⊢ also expands the hypothesis h; without a location only the goal is expanded.

Products of lengths are atoms for omega. Bound them by facts in context first.