The Coq mailing list

[Ralph Matthes <Ralph.Matthes AT irit.fr>]

Le 14/07/2015 10:16, Gabriel Scherer a écrit :
> I think the main reason why nobody has experimented with 
> induction-{recursion,induction} in Coq yet is that implementing it 
> requires an important amount of non-trivial work.

Dear all,

My answer may appear to be a bit late, but the status of these questions 
does not change so rapidly. I do not speak about induction-induction but 
about induction-recursion, as did Jason Gross when starting this thread 
(and was taken up by Gabriel Scherer, Fredrik Nordvall Forsberg and Eddy 
Westbrook).

In fact, based on Venzio Capretta's notes mentioned by Jason Gross, I 
gave an implementation in Coq of a module type for inductive Set-indexed 
families (nested datatypes). This type features Mendler iteration and 
comes with a genuine map operation (not derived from the iterator). The 
details are in my JFP paper of 2009. The crucial element in Figure 1 in 
the paper (p.450) is that the mapping operation map_muF appears in the 
type of the constructor In of the datatype (family) muF and that the 
rewrite rule for map_muF is by pattern-matching on its inductive 
argument (in the family muF). To be honest, this is rather 
induction-inversion than induction-recursion. Thanks to Venanzio 
Capretta's idea, this scheme could be fully implemented in the CIC with 
impredicative Set. Section 5 of the paper shows the construction - for 
the proof of a corresponding induction principle, proof irrelevance (for 
naturality proofs and for discarding the proofs in a strong sigma type) 
had to be assumed.

So, the disclaimer is: this is not about a framework for playing with 
induction-recursion, but only one instance of it. And the simultaneous 
recursive part is shallow in being only inversion of the datatype 
constructor. However, the constructed datatype additionally features an 
iterator, and it models an arbitrary nested datatype (in the tradition 
of categorical datatypes given by just some "functor").

Have a nice weekend,     Ralph