Compiling nested inductive types

Dealing with multiple nested applications of the same inductive type

Consider the following inductive type declaration:

inductive foo (A : Type) : nat → Type :=
| mk : Π (n : nat), prod (foo A 0) (foo A 1) → prod (foo A n) (foo A (n+1)) → foo A (n+2)

There are two separate occurrences of inductive type applications with foo inside:

prod (foo A 0) (foo A 1)
prod (foo A <n>) (foo A (<n> + 1))

There are at least two different options for how to encode this into a mutually inductive type.

Option 1: Abstract all indices

Since foo occurs twice in the first inductive type application, we can create a copy of prod that takes two indices (one for each foo occurrence), and which otherwise mimics prod:

foo_prod : ℕ → ℕ → Type
foo_prod.mk : Π (n₁ n₂ : ℕ), foo A n₁ → foo A n₂ → foo_prod n₁ n₂

We can then search for other occurrences in the declaration of foo that match the pattern prod (foo A ?M1) (foo A ?M2). The second occurrence matches this and so can be captured by foo_prod as well. The resulting mutually inductive type is as follows:

mutual_inductive foo, fprod (A : Type)
with foo : nat → Type :=
| mk : Π {n : nat}, fprod A 0 1 → fprod A n (n+1) → foo A (n+2)
with fprod : nat → nat → Type :=
| mk : Π {n₁ n₂}, foo A n₁ → foo A n₂ → fprod A n₁ n₂

definition real_foo.mk (A : Type)
                       (n : nat)
                       (p₁ : prod (foo A 0) (foo A 1))
                       (p₂ : prod (foo A n) (foo A (n+1)))
                         : foo A (n+2) :=
match p₁, p₂ with
| prod.mk f₁ f₂, prod.mk f₃ f₄ :=  foo.mk (fprod.mk f₁ f₂) (fprod.mk f₃ f₄)
end

Option 2: Only abstract non-parameter locals

The other option is to only generalize as much as is necessary to process each nested application in sequence. For prod (foo A 0) (foo A 1), we do not need our new inductive type to have any indices. However, since it does not syntactically match prod (foo A <n>) (foo A (<n> + 1)) (up to locals-renaming), we need to create a second copy of prod as well, and this second copy must take <n> as an index. Here is the result:

mutual_inductive foo, fprod₁, fprod₂ (A : Type)
with foo : nat → Type :=
| mk : Π {n : nat}, fprod₁ A → fprod₂ A n → foo A (n+2)
with fprod₁ : Type :=
| mk : foo A 0 → foo A 1 → fprod₁ A
with fprod₂ : nat → Type :=
| mk : Π {n : nat}, foo A n → foo A (n+1) → fprod₂ A n

definition real_foo.mk (A : Type)
                       (n : nat)
                       (p₁ : prod (foo A 0) (foo A 1))
                       (p₂ : prod (foo A n) (foo A (n+1)))
                         : foo A (n+2) :=
match p₁, p₂ with
| prod.mk f₁ f₂, prod.mk f₃ f₄ := foo.mk (fprod₁.mk f₁ f₂) (fprod₂.mk f₃ f₄)
end

Trade-offs

I don't think it matters much, and the second one is probably easier to implement. However, the first one may be preferable if we expect many nested applications that will unify semantically but not syntactically.

Conclusion

I will implement option #2.

Dealing with indices

Example 1: foo occurs inside a parameter argument to another inductive type.

Consider the following inductive declaration:

inductive foo (A : Type) : ℕ → Type :=
| mk : Π (n : nat), vector (foo A n) (n+1) → foo A (n+2)

The inductive type vector already has one index, and abstracting the local <n> adds an additional index. The fact that <n> appears in the position of vector's index is irrelevant, and the two indices of the copied vector type are "uncoupled":

mutual_inductive foo, fvector
with foo : ℕ → Type :=
| mk : Π (n : ℕ), fvector n (n+1) → foo (n+2)
with fvector : nat → nat → Type :=
| vnil  : Π (n₁ : ℕ), fvector n₁ 0
| vcons : Π (n₁ : ℕ) (n₂ : ℕ), foo n₁ → fvector n₁ n₂ → fvector n₁ (n₂+1)

definition fvector_to_vector : Π (n₁ n₂ : ℕ), fvector n₁ n₂ → vector (foo n₁) n₂
| n₁    0     (fvector.vnil n₁)         := @vector.vnil (foo n₁)
| n₁    (k+1) (fvector.vcons n₁ k f v)  := @vector.vcons (foo n₁) f k (fvector_to_vector n₁ k v)

Example 2: foo occurs inside an index argument to another inductive type

Consider the following inductive declarations:

inductive bar : Type → Type :=
| mk : bar ℕ

inductive foo (A : Type.{1}) : A → Type.{1} :=
| mk : Π (a : A), bar (foo A a) → foo A a

Note that (foo A a) is an index argument to bar. I do not see any reasonable way to handle this case. Suppose we try the following:

mutual_inductive foo, foo_bar (A : Type.{1})
with foo: A → Type.{1} :=
| mk : Π (a : A), foo_bar A a → foo A a
with foo_bar : A → Type.{1} :=
| mk : Π (a : A), foo_bar A ℕ -- does not type-check

This does not type-check, because we no longer have the arbitrary Type index. On the other hand, if we keep both indices, we have nothing reasonable to pass for the second index:

mutual_inductive foo, foo_bar (A : Type.{1}) 
with foo : A → Type.{1} :=
| mk : Π (a : A), foo_bar A a _ → foo A a       -- We have nothing reasonable to put for the _
with foo_bar : A → Type.{1} -> Type.{1} :=
| mk : Π (a : A), foo_bar A a ℕ

Conclusion

When foo appears inside a parameter argument, we add new indices for every local that appears in the parameter arguments, and keep the old indices completely unconstrained. When foo appears inside an index argument, it is an error.

Pseudocode for the construction itself

• Input: a "generalized" inductive declaration (ginductive_decl) with at least one nested occurrence
• Output: a ginductive_decl with one additional mutually inductive declaration and a least one fewer nested occurrences.

1. For each inductive declaration, for each introduction rule, if the type of any of the arguments to that introduction include an occurrence of one of the inductive types being defined in either an application of a function that is not an inductive type, or as an index argument to an inductive type, fail. If there is an occurrence ind _ ... (<foo> _ ... _) ... _ inside a parameter argument of an inductive type, select that occurrence to factor out.

2. Find all other occurrences that structurally match the pre-index prefix. We will be extra strict here, and force all parameter arguments of ind to be fixed by the selected occurrence, rather than lift that parameter to an index.

3. Add a new inductive_decl to the ginductive_decl with type Pi <non-param-locals-in-occurrence>, old_indices -> Type.

4. Copy the introduction rules for ind to the new inductive_decl, instantiate the types with the parameters which have all been fixed already, and then abstract the locals.

5. Traverse all other inductive_decls in the ginductive_decl, and replace the selected occurrences of ind _ ... (<foo> _ ... _) ... _ with foo.ind <locals> <original_indices>.

Dealing with iterated nesting

Suppose we have

inductive foo :=
| mk : list (prod foo bool) -> foo

The first un-nesting gives:

mutual_inductive foo, foo_prod
with foo :=
| mk : list foo_prod -> foo
with foo_prod :=
| mk : foo -> bool -> foo_prod

and the second gives:

mutual_inductive foo, foo_prod, foo_prod_list
with foo :=
| mk : foo_prod_list -> foo
with foo_prod :=
| mk : foo -> bool -> foo_prod
with foo_prod_list :=
| nil : foo_prod_list
| cons : foo_prod -> foo_prod_list -> foo_prod_list

In order to define the constructors of the outermost foo in terms of the middle one, we need to convert back and forth between list (prod foo bool) and list foo_prod. In general, we need to unpack all nested applications to get to the innermost one that is being eliminated. Although I was planning to write these functions in C++, this may be much easier to do in Lean.

Pseudocode for defining the constructors

1. Traverse the types of the arguments to the introduction rules for the original foo. For every argument that contains a selected occurrence, create customized unpack and pack functions using tactics, and then define the introduction rule for the real foo to unpack and pack those arguments that contain selected occurrences and pass the other arguments through unchanged. We will want to cache these unpack and pack functions because other constructions will require them as well, such as cases_on.

Generating the cases_on

Let's consider a simple example to start:

inductive foo :=
| mk : list foo -> foo

This yields the following boilerplate:

inductive foo₁ :=
| mk : foo_list → foo₁
with foo_list :=
| nil : foo_list
| cons : foo₁ → foo_list → foo_list

definition foo := foo₁

definition pack_foo_list : list foo → foo_list
| []     := foo_list.nil
| (list.cons x xs) := foo_list.cons x (pack_foo_list xs)

definition unpack_foo_list : foo_list → list foo
| foo_list.nil     := []
| (foo_list.cons x xs) := list.cons x (unpack_foo_list xs)

definition foo.mk (xs : list foo) : foo := foo₁.mk (pack_foo_list xs)

lemma foo_list_pack_unpack (ys : foo_list) : pack_foo_list (unpack_foo_list ys) = ys := sorry
lemma foo_list_unpack_pack (xs : list foo) : unpack_foo_list (pack_foo_list xs) = xs := sorry

The cases_on is complicated by the fact that we need to rewrite with our pack_unpack lemma in order to make it type-correct:

lemma foo.cases_on
                        (C : foo → Type)
                        (f : foo)
                        (mp : Π (xs : list foo), C (foo.mk xs))
                          : C f :=
@foo₁.cases_on C
               f
               (λ (ys : foo_list),
                   eq.rec_on (foo_list_pack_unpack ys) (mp (unpack_foo_list ys)))

As a result, foo.cases_on will not compute unless foo_list_pack_unpack ys is a proof of ys = ys instead of its stated type pack_foo_list (unpack_foo_list ys) = ys, and this will only hold definitionally when ys is fully concrete. Thus the desired computational property of the cases_on does not hold in general:

lemma foo.mk.cases_on_spec (C : foo → Type)
                           (mp : Π (xs : list foo), C (foo.mk xs))
                           (xs : list foo)
      : foo.cases_on C (foo.mk xs) mp = mp xs :=

Worked example of compilation

Preliminaries:

inductive vector (A : Type) : nat -> Type
| vnil : vector 0
| vcons : Pi (n : nat), A -> vector n -> vector (n+1)

inductive lvector (A : Type) : nat -> Type
| lnil : lvector 0
| lcons : Pi (n : nat), A -> lvector n -> lvector (n+1)

constants (f g h j : nat -> nat)

Suppose we want to do define:

-- Level 3
inductive foo (A : Type) : ℕ -> Type
| mk : Pi (n : nat), lvector (vector (foo (f n)) (g n)) (h n) -> foo (j n)

This leads to the following intermediate steps:

-- Level 2
mutual_inductive foo, fvector
with foo : ℕ -> Type
| mk : Pi (n : ℕ), lvector (fvector n (g n)) (h n) -> foo (j n)
with fvector : nat -> nat -> Type :=
| vnil  : Pi (n₁ : ℕ), fvector n₁ 0
| vcons : Pi (n₁ : ℕ) (n₂ : ℕ), foo (f n₁) -> fvector n₁ n₂ -> fvector n₁ (n₂+1)

-- Level 1
mutual_inductive foo, fvector, flvector (A : Type)
with foo : nat -> Type
| mk : Pi (n : nat), flvector n (h n) -> foo (j n)
with fvector : nat -> nat -> Type
| vnil : Pi (n1 : nat), fvector n1 0
| vcons : Pi (n1 n2 : nat), foo (f n1) -> fvector n1 n2 -> fvector n1 (n2+1)
with flvector : nat -> nat -> Type
| lnil : Pi (n : nat), flvector n 0
| lcons : Pi (n1 n2 : nat), fvector n1 (g n1) -> flvector n1 n2 -> flvector n1 (n2+1)

We can then define level 2:

definition foo₂ : Pi (A : Type), nat -> Type.{1} := @foo
definition fvector₂ : Pi (A : Type), nat -> nat -> Type.{1} := @fvector

definition lvector_to_flvector (A : Type) (n₁ : nat) 
  : Pi (n₂ : nat), lvector (fvector₂ A n₁ (g n₁)) n₂ -> flvector A n₁ n₂ :=
@lvector.rec (fvector₂ A n₁ (g n₁))
             (λ (n₂ : nat) (v : lvector (fvector₂ A n₁ (g n₁)) n₂), flvector A n₁ n₂)
             (@flvector.lnil A n₁)
             (λ (n₂ : nat)
                (x : fvector₂ A n₁ (g n₁))
                (vs : lvector (fvector₂ A n₁ (g n₁)) n₂)
                (fvs : flvector A n₁ n₂),
                  @flvector.lcons A n₁ n₂ x fvs)

definition foo₂.mk 
  : Pi (A : Type) (n : nat) (fvs : lvector (fvector A n (g n)) (h n)), foo₂ A (j n) :=
    assume A n fvs, foo.mk n (lvector_to_flvector A n (h n) fvs)

definition fvector₂.vnil 
  : Pi (A : Type) (n : nat), fvector₂ A n 0 := 
    @fvector.vnil
definition fvector₂.vcons 
  : Pi (A : Type) (n1 n2 : nat), foo₂ A (f n1) -> fvector₂ A n1 n2 -> fvector₂ A n1 (n2+1) := 
    @fvector.vcons

and finally level 3:

definition foo₃ : Pi (A : Type), nat -> Type.{1} := @foo₂

definition vector_to_fvector (A : Type) (n₁ : nat) 
  : Π (n₂ : nat), vector (foo₃ A (f n₁)) n₂ -> fvector₂ A n₁ n₂ :=
@vector.rec (foo₃ A (f n₁))
            (λ (n₂ : nat) (v : vector (foo₃ A (f n₁)) n₂), fvector₂ A n₁ n₂)
            (@fvector₂.vnil A n₁)
            (λ (n₂ : nat)
               (x : foo₃ A (f n₁))
               (vs : vector (foo₃ A (f n₁)) n₂)
               (fvs : fvector₂ A n₁ n₂),
                 @fvector.vcons A n₁ n₂ x fvs)

definition lvector_vector_to_lvector_fvector (A : Type) (n₁ : nat) 
  : Pi (n₂ : nat), lvector (vector (foo A (f n₁)) (g n₁)) n₂ -> lvector (fvector A n₁ (g n₁)) n₂ :=
@lvector.rec (vector (foo A (f n₁)) (g n₁))
             (λ (n₂ : nat) (lv : lvector _ n₂), lvector (fvector A n₁ (g n₁)) n₂)
             (@lvector.lnil _)
             (λ (n₂ : nat)
                (x : vector (foo A (f n₁)) (g n₁))
                (lv : lvector _ n₂)
                (lv' : lvector (fvector A n₁ (g n₁)) n₂),
                (@lvector.lcons _ n₂ (vector_to_fvector A n₁ (g n₁) x) lv'))

definition foo₃.mk : Pi (A : Type) (n : nat), lvector (vector (foo A (f n)) (g n)) (h n) -> foo₃ A (j n) :=
  assume A n lv,
  @foo₂.mk A n (@lvector_vector_to_lvector_fvector A n (h n) lv)