Improved WD Lemma Generation

This page describes work in progress for optimising well-definedness lemmas generated by the Core Rodin platform.

Motivating examples

With Rodin 1.3, the well-definedness lemma generated for predicate $f(x) = f(y)$ is

$f\in S\pfun T\land x\in\dom(f)\land f\in S\pfun T\land y\in\dom(f)$

This predicate is sub-optimal as it contains twice the same sub-predicate ($f\in S\pfun T$). Consequently, when the prover is fed with the generated lemma, it will have to prove twice the same goal.

The well-definedness lemma generated for predicate $x \div y=5 \land \lnot x \div y=3$ is

$\lnot y=0 \land (x\div y=5 \limp \lnot y=0)$