1
$\begingroup$

This is a follow up to a question someone else previously posted: Expressivity of mutual/nested inductives vs. regular inductives.

pigworker answered that

Adopting Agda-ish notation, the basic strategy is to turn your bunch of mutually defined inductive types into a single inductively defined universe, indexed over its collection of sorts...

...

BEFORE

mutual
  data Even : Set where
    zero : Even
    suco : Odd -> Even

  data Odd  : Set where
    suce : Even -> Odd

AFTER

data Sort : Set where
  even odd : Sort

data Stuff : Sort -> Set where
  zero : Stuff even
  suco : Stuff odd -> Stuff even
  suce : Stuff even -> Stuff odd

Even = Stuff even
Odd  = Stuff odd

However, Twitter user @JulesJacobs5 offers a different approach:

In Coq you can sometimes parameterize one inductive with some T, and then use the parameterized one in the definition of the other one ...

For example, using the even-odd example, we could take this mutually-defined example:

Inductive odd : Set := suce (e : even)
with even : Set := zero | suco (o : odd).

...and turn it into this non-mutual version:

Inductive make_odd (even_placeholder : Set) : Set :=
  | suce (e : even_placeholder)
.

Inductive even : Set :=
  | zero
  | suco (o : make_odd even)
.

Definition odd := make_odd even.

My question: Can we take any mutually-defined inductive type, and "de-mutualize" it via this "Replace all mutual references with a parameter" technique?

If not, what is an example where this technique would fail? A concrete code example would be appreciated.

EDIT: I'm not interested in whether such a "de-mutualizing" technique would make proofs more or less tedious. I'm purely interested in whether or not this particular technique can always be applied.

$\endgroup$
3
  • $\begingroup$ This produces nested inductives though, which imo is worse than mutual inductives in both theory and application. $\endgroup$
    – Trebor
    Aug 15, 2023 at 10:56
  • $\begingroup$ @Trebor Do you think nested inductives are always worse, or only in certain contexts? I agree that in the above example, the mutual definition is nicer than the nested version. However, compare Ind tree := node : (list tree) -> tree to Mutual[tree,tlist] := node : tlist -> tree | tnil : tlist | tcons : tree -> tlist -> tlist. I'd argue that the first (nested) encoding is better than the second (mutual) encoding, since you can reuse all of list's functions and theorems, without having to reimplement them for tlist. $\endgroup$
    – Kyle Lin
    Aug 16, 2023 at 5:25
  • 1
    $\begingroup$ It is indeed the first thought that you can reuse functions, but turns out you can't in some of the cases! It poses difficulties for termination checking. Coq already had a rule to deal with this, it works well but doesn't cover more advanced cases. For other theorem proves that doesn't have the rule it's worse. $\endgroup$
    – Trebor
    Aug 16, 2023 at 6:45

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.