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 of
pwith each constructor
val ghost function p'proof xs : p'witnessreturns, under precondition
p xs, a witness of its (minimal) proof.
val ghost function p'induction xs : intreturns a (decreasing) variant over the proof of
The post condition of
p'proof xs introduces, for each witness constructor
A ys the hypotheses
hs and the associated unifications of
xs, together with strictly decreasing variants of
p'induction for any sub-proofs of
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.