Mutual inductive rec

Stream: lean4

[Marcus Rossel]

Why are recursors for mutual inductive types the way they are? And how are they to be used?

I've had a previous discussion about some mutual inductive types. Fundamentally, all of the types I had to define were structures. But since it isn't possible to directly declare structures in a mutual block, I'm trying to add the niceties of structures manually.
My problem now is that I have to use the recursors of those types, which (e.g.) look like this:

Component.MutationOutput.rec : ((prtVals : Ports ?m.534 ?m.535) →
    (state : StateVars ?m.534 ?m.535) →
      (newCns delCns : List (?m.534 × ?m.534)) →
        (newRtrs : List (Component.Reactor ?m.534 ?m.535)) →
          (delRtrs : Finset ?m.534) →
            ?m.540 newRtrs → ?m.536 (Component.MutationOutput.mk prtVals state newCns delCns newRtrs delRtrs)) →
  ((deps : Ports.Role → Finset ?m.534) →
      (triggers : Finset ?m.534) →
        (body : Ports ?m.534 ?m.535 → StateVars ?m.534 ?m.535 → Component.MutationOutput ?m.534 ?m.535) →
          (tsSubInDeps : triggers ⊆ deps Ports.Role.in) →
            ((a : Ports ?m.534 ?m.535) → (a_1 : StateVars ?m.534 ?m.535) → ?m.536 (body a a_1)) →
              ?m.537 (Component.Mutation.mk deps triggers body tsSubInDeps)) →
    ((ports : Ports.Role → Ports ?m.534 ?m.535) →
        (state : StateVars ?m.534 ?m.535) →
          (rcns muts : Finmap ?m.534 (Component.Mutation ?m.534 ?m.535)) →
            (nest : Component.Network ?m.534 ?m.535) →
              ?m.541 rcns → ?m.541 muts → ?m.539 nest → ?m.538 (Component.Reactor.mk ports state rcns muts nest)) →
      ([l : LGraph.Edge (NetworkEdge ?m.534) ?m.534] →
          (nodes : Finmap ?m.534 (Component.Reactor ?m.534 ?m.535)) →
            (edges : Finset (NetworkEdge ?m.534)) → ?m.542 nodes → ?m.539 (Component.Network.mk nodes edges)) →
        ?m.540 [] →
          ((head : Component.Reactor ?m.534 ?m.535) →
              (tail : List (Component.Reactor ?m.534 ?m.535)) → ?m.538 head → ?m.540 tail → ?m.540 (head :: tail)) →
            ((map : ?m.534 → Option (Component.Mutation ?m.534 ?m.535)) →
                (finite : Set.finite (Set.image map Set.univ)) →
                  ((a : ?m.534) → ?m.543 (map a)) → ?m.541 { map := map, finite := finite }) →
              ((map : ?m.534 → Option (Component.Reactor ?m.534 ?m.535)) →
                  (finite : Set.finite (Set.image map Set.univ)) →
                    ((a : ?m.534) → ?m.544 (map a)) → ?m.542 { map := map, finite := finite }) →
                ?m.543 none →
                  ((val : Component.Mutation ?m.534 ?m.535) → ?m.537 val → ?m.543 (some val)) →
                    ?m.544 Option.none →
                      ((val : Component.Reactor ?m.534 ?m.535) → ?m.538 val → ?m.544 (Option.some val)) →
                        (t : Component.MutationOutput ?m.534 ?m.535) → ?m.536 t

This is the recursor for the following type (without showing the related mutual inductives):

inductive MutationOutput (ι υ)
  | mk
    (prtVals : Ports ι υ)
    (state   : StateVars ι υ)
    (newCns  : List (ι × ι))
    (delCns  : List (ι × ι))
    (newRtrs : List (Reactor ι υ))
    (delRtrs : Finset ι)

I was trying to write a simple accessor for prtVals:

def MutationOutput.prtVals (o : MutationOutput ι υ) : Ports ι υ := ...

But I don't know how to apply that wall of a recursor here.

[Marcus Rossel]

Jannis Limperg said:

Note that termination checking for mutually recursive functions is not implemented yet, and neither is well-founded recursion. So you can only use the equation compiler for partial functions. If you want a function about which you can prove things, you need to use the recursor for now, and even then the function will be noncomputable (since the recursor is currently noncomputable). So my advice would be to avoid mutual inductives at all cost.

Hmm, I don't really understand what you're saying yet. What's different about using the recursor vs. the equation compiler?

[Marcus Rossel]

And can't I do well-founded recursion manually?

[Notification Bot]

Marcus Rossel has marked this topic as unresolved.

[Jannis Limperg]

Take a look at this example:

mutual
  inductive A
    | base : A
    | mk : B → A

  inductive B
    | mk : A → B
end

mutual
  def constructorCountA : A → Nat
    | A.base => 1
    | A.mk b => constructorCountB b + 1

  def constructorCountB : B → Nat
    | B.mk a => constructorCountA a + 1
end

noncomputable def constructorCountA₂ : A → Nat :=
  A.rec (motive_1 := λ _ => Nat) (motive_2 := λ _ => Nat)
    1
    (λ _ rec => rec + 1)
    (λ _ rec => rec + 1)

The mutual block does not compile. constructorCountA₂ does not compile unless marked noncomputable (and I guess if marked noncomputable, it doesn't compile in a different sense). If you try to use wfrec, you'll notice (a) that all the definitions in Init/WF.lean are noncomputable and (b) that whatever well-founded relation you'd like to use may need to be defined by recursion itself. (Not sure about the last point.)

[Marcus Rossel]

Jannis Limperg said:

constructorCountA₂ does not compile unless marked noncomputable (and I guess if marked noncomputable, it doesn't compile in a different sense).

constructorCountA₂ compiles fine for me.

[Marcus Rossel]

Oh, that's what you mean by "doesn't compile in a different sense".

[Marcus Rossel]

So if I'm fine with noncomputability, then the recursor approach is fine, isn't it?

[Jannis Limperg]

I think so, yes, if you can stomach the resulting ugliness.

[Mac]

Marcus Rossel said:

Fundamentally, all of the types I had to define were structures. But since it isn't possible to directly declare structures in a mutual block, I'm t

If you just have mutual nested structure, It is important to note that you can get away with avoiding mutual blocks altogether by making your types parametrized by the mutual type. See this Zulip thread for an example of how this works.

[Mac]

For example, your mutual block from here could have been written like this:

structure BaseMutationOutput (R : Type) (ι : Type) where
  prtVals : List ι
  state   : Finset ι
  newCns  : List (ι × ι)
  newRcns : List (R)

structure BaseMutation (R : Type) (ι : Type) where
  deps : Finset ι
  body : List ι → Nat → BaseMutationOutput R ι
  outPrtValsDepOnly : ∀ i s {o}, (o ∉ deps) → (body i s).prtVals.nth o = none)

inductive Reaction (ι : Type)
  | mk
    (core : BaseMutation (Reaction ι) ι)
    (noNewCns  : ∀ i s, (core.body i s).newCns = [])

abbrev MutationOutput (ι : Type) := BaseMutationOutput (Reaction ι) ι
abbrev Mutation (ι : Type) := BaseMutation (Reaction ι) ι

[Marcus Rossel]

Mac said:

If you just have mutual nested structure, It is important to note that you can get away with avoiding mutual blocks altogether by making your types parametrized by the mutual type.

Nice, that worked pretty well for the most part! I just have one case again where I'm getting an error that I don't understand:

structure Network (ι ρ) where
  (nodes : Finmap ι ρ)

inductive Reactor (ι υ : Type _)
  | mk
    (nest : Network ι (Reactor ι υ))

Gives:

(kernel) arg #3 of '_nested.C.Network_1.mk' contains a non valid occurrence of the datatypes being declared

And removing the nodes from Network resolves the error.

---

Context for MWE:

def Set.finite (s : Set α) : Prop := sorry

structure Finmap (α β) where
  map : α → Option β
  finite : (Set.univ.image map).finite

[Marcus Rossel]

Ok I just noticed that the sorry might actually be the problem.

[Marcus Rossel]

@Mac What's the benefit of using the parameter-based approach? Because (e.g.) the recursor that I get for Reactor that way is still

Reactor.rec : ((ports : Role → Ports ?m.11182 ?m.11183) →
    (state : StateVars ?m.11182 ?m.11183) →
      (rcns muts : Finmap ?m.11182 (Mutation ?m.11182 ?m.11183 (Reactor ?m.11182 ?m.11183))) →
        (prios : PartialOrder ?m.11182) →
          (nest : Network ?m.11182 (Reactor ?m.11182 ?m.11183)) →
            ?m.11185 rcns → ?m.11185 muts → ?m.11186 nest → ?m.11184 (Reactor.mk ports state rcns muts prios nest)) →
  ((map : ?m.11182 → Option (Mutation ?m.11182 ?m.11183 (Reactor ?m.11182 ?m.11183))) →
      (finite : Set.finite (Set.image map Set.univ)) →
        ((a : ?m.11182) → ?m.11187 (map a)) → ?m.11185 { map := map, finite := finite }) →
    ((nodes : Finmap ?m.11182 (Reactor ?m.11182 ?m.11183)) →
        (edges : Finset (Connection ?m.11182)) → ?m.11188 nodes → ?m.11186 { nodes := nodes, edges := edges }) →
      ?m.11187 none →
        ((val : Mutation ?m.11182 ?m.11183 (Reactor ?m.11182 ?m.11183)) → ?m.11189 val → ?m.11187 (some val)) →
          ((map : ?m.11182 → Option (Reactor ?m.11182 ?m.11183)) →
              (finite : Set.finite (Set.image map Set.univ)) →
                ((a : ?m.11182) → ?m.11190 (map a)) → ?m.11188 { map := map, finite := finite }) →
            ((deps : Role → Finset ?m.11182) →
                (triggers : Finset ?m.11182) →
                  (body :
                      Ports ?m.11182 ?m.11183 →
                        StateVars ?m.11182 ?m.11183 → MutationOutput ?m.11182 ?m.11183 (Reactor ?m.11182 ?m.11183)) →
                    ((a : Ports ?m.11182 ?m.11183) → (a_1 : StateVars ?m.11182 ?m.11183) → ?m.11191 (body a a_1)) →
                      ?m.11189 { deps := deps, triggers := triggers, body := body }) →
              ?m.11190 Option.none →
                ((val : Reactor ?m.11182 ?m.11183) → ?m.11184 val → ?m.11190 (Option.some val)) →
                  ((prtVals : Ports ?m.11182 ?m.11183) →
                      (state : StateVars ?m.11182 ?m.11183) →
                        (newCns delCns : List (?m.11182 × ?m.11182)) →
                          (newRtrs : List (Reactor ?m.11182 ?m.11183)) →
                            (delRtrs : Finset ?m.11182) →
                              ?m.11192 newRtrs →
                                ?m.11191
                                  { prtVals := prtVals, state := state, newCns := newCns, delCns := delCns,
                                    newRtrs := newRtrs, delRtrs := delRtrs }) →
                    ?m.11192 [] →
                      ((head : Reactor ?m.11182 ?m.11183) →
                          (tail : List (Reactor ?m.11182 ?m.11183)) →
                            ?m.11184 head → ?m.11192 tail → ?m.11192 (head :: tail)) →
                        (t : Reactor ?m.11182 ?m.11183) → ?m.11184 t

[Mario Carneiro]

the benefit is that the structures are structures, and you get the usual niceties of field projections and structure instances

[Marcus Rossel]

"structure instances"?

[Mario Carneiro]

{foo := 1, bar := 2}