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 subproofs 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 Why3 reference implementation (without inductives) for all the generated symbols of the example.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information