The simplification of the verification conditions

The contracts of the components with a loop are proved by vcgen, whose verification conditions encode the weakest preconditions in the order of Prop: meets, propositions of the order, the measures that end the loops and the applied invariants of the while loops. The tactic vc_simp rewrites these encodings into plain propositions in all the hypotheses and the goal, with further lemmas of each contract (the invariants to unfold and propositional clean-up), before the dispatch of the conditions.

Implementation notes

The file uses Lean core and Std only, as the contracts that use the tactic do.

def vcSimp : Lean.ParserDescr

vc_simp [l₁, …] rewrites, in all the hypotheses and the goal, the encodings of the weakest preconditions that the verification conditions of vcgen contain into plain propositions: meets and propositions of the order (Lean.Order.meet_prop_eq_and, Lean.Order.ofProp_prop_eq), the measures that end the loops (Std.WP.Variant.evalsTo_ofMeasure, Std.WP.Variant.evalsBelow_ofMeasure_nat, Std.WP.Assertion.NondetFun.evalsTo_pure) and the applied invariants of while loops (Std.WP.WhileInvariant.mk_apply), with the further simp lemmas l₁, …. It is simp only [these lemmas, l₁, …] at *.

Equations

• One or more equations did not get rendered due to their size.