Improved WD Support Clause Samples
Improved WD Support. To improve generated WD lemmas, the generating algorithm has not been changed (to ensure safety) but enhanced by a back-end that simplifies the generated lemma after the fact. The enhancement consists in removing all sub-predicates that are subsumed within the ▇▇ ▇▇▇▇▇. Also, as WD lemmas were changing between two releases of the platform, the automated proof replay mechanism needed to better tackle changes in proof obligations (when they get simpler). This allows user to retain their proof status, although proof obligations have changed. As concerns automated support, it has been chosen not to add new reasoners (to avoid expanding the trusted base of the sequent prover) but rather to work on the outside by adding new tactics that schedule the existing reasoners to discharge the WD subgoals. This approach also allowed to start introducing speculative reasoning within tactics (attempt proofs).
Improved WD Support. When the user enters an expression or predicate that is possibly ill-defined (such as applying a partial function), the Rodin platform insists that the user demonstrates that this formula is indeed well-defined (e.g., the partial function is applied to an element of its domain) before using it. This verification is implemented by generating a well-definedness (WD) predicate, based on the syntax of the input formula. In previous releases of the Rodin platform, the generation of WD predicates was implemented in a very simple manner, and the generated predicate was usually highly redundant. Moreover, the support by automated tactics for discharging such predicates was not always appropriate. Consequently, many well-definedness subproofs needed to be carried out interactively in a very cumbersome and repetitive manner.