Inductive proofs on inductives
This is a proposal feature allowing inductive proofs over inductive predicates in why3.
Consider an inductive predicate P
as follows:
inductive p xs = A: forall ys. hs -> p es | ...
The idea is to automatically generate the following items:
-
type p'witness = A ys | ...
witnessing the universally quantified variables obtained to build a proof ofp
with each constructor -
val ghost function p'proof xs : p'witness
returns, under preconditionp xs
, a witness of its (minimal) proof. -
val ghost function p'induction xs : int
returns a (decreasing) variant over the proof ofp xs
.
The post condition of p'proof xs
introduces, for each witness constructor A ys
the hypotheses hs
and the associated unifications of es
and xs
, together with strictly decreasing variants of p'induction
for any sub-proofs of p
in hs
.
A complete example of how this can be used in practice is provided here:
- ind.mlw: full example of use of the generated symbols (including also #547 although it is not necessary…).
- ind_gen.mlw: the full exemple together with the (axiomatized) generated symbols, that makes the lemma proof automatically discharged easily.
-
ind.v: a Coq realization of the generated symbols of the example using destruction of the inductive predicate in
Type
(we can not realize modules... yet, although it shall look like this). - ind_fol.mlw: a fully proven Why-3 reference implementation (without inductives) for all the generated symbols of the example.