Closing word-size bounds

Cslib.WordRAM.Fits w v states v < 2 ^ w, and word-RAM proofs need many such side conditions, one per value an instruction writes. fits proves them by linear arithmetic: it unfolds Fits in the goal and in every hypothesis that mentions it, then runs omega. The hypotheses are found by their statements, not by their names, so a bound follows from whichever word-size facts are in context, without first choosing the fact to weaken with Fits.of_le.

Only hypotheses whose statements contain Fits are unfolded: they are added to the context in unfolded form, and the others are left to omega as they are. Each power of two 2 ^ e among them is added as positive, which omega does not know by itself. fits [h₁, h₂] also adds the statements of the given terms, such as a product bound that omega cannot derive.

The tactic fails on a goal that is not a word-size bound, naming the plain omega that is then the right call, and when omega cannot close the unfolded goal, showing that goal and saying whether any hypothesis Fits w v was found.

The simplification procedure Cslib.WordRAM.reduceFits rewrites Fits w v to True when omega proves it from the hypotheses that mention Fits alone, so that a simp call deciding whether written values fit a word, as in ram_eval, needs no named Fits facts. It leaves the other hypotheses out to keep its cost independent of the length of the context.

Main definitions

• fits: prove Fits w v, or v < 2 ^ w, by omega from the word-size facts in context.
• Cslib.WordRAM.reduceFits: the same proof, from the Fits hypotheses, as a simp procedure.

def Cslib.Tactic.Fits.prove? (target : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

A proof of the word-size bound target by omega from the hypotheses that mention Fits, unfolded, or none. Unlike fits it uses no other hypotheses and adds no positivity facts, so that its cost does not grow with a long context; it runs inside simp (reduceFits), possibly on every value a program writes.

def Cslib.Tactic.Fits.fits : Lean.ParserDescr

fits proves a word-size bound Fits w v, or v < 2 ^ w, by linear arithmetic. It unfolds Fits in the goal and in each hypothesis that mentions it, and runs omega; hypotheses are found by their statements, whatever their names.

• fits [h₁, h₂] also uses the statements of the terms h₁ and h₂, unfolded likewise, for facts omega cannot derive, such as bounds on products.

It fails on a goal that is not a word-size bound, for which plain omega is the right call.

def Cslib.WordRAM.reduceFits : Lean.Meta.Simp.Simproc

simp procedure that rewrites a word-size bound Fits w v to True when omega proves it from the hypotheses Fits w' v' in context. ram_eval and ram_exact_eval use it to decide which written values fit a word.