Use recursor within inductive def

Stream: lean4

[Marcus Rossel]

Perhaps the answer to this question is very type-theoretical, but why can't I use an inductive type's recursor within its own definition?
E.g., if I try:

inductive X
  | base (b : Nat)
  | next (x : X) (h : x.rec (true) (λ b => false))

I get an error telling me:

invalid field notation, type is not of the form (C ...) where C is a constant
  x
has type
  X

Is it because that would make the recursor recursive (:drum:)? Because it would have to know about its own definition in order to be defined?

[Mario Carneiro]

the boring answer is that this is not allowed by the inductive definition schema

[Marcus Rossel]

Mario Carneiro said:

the boring answer is that this is not allowed by the inductive definition schema

Good enough for me ¯\_(ツ)_/¯

[Marcus Rossel]

Can this be circumvented by using an inductive family somehow?

[Mario Carneiro]

I don't think this is a higher inductive type - even HITs don't let you reference the recursor in the constructors because that almost certainly leads to the liar paradox somehow

[Mario Carneiro]

not to mention, what does the recursor's type even look like? it has to reference itself

[Mario Carneiro]

Maybe you could start with a description of what you want to do

[Mario Carneiro]

in the example, you are saying you want x to be a base, but in that cause the parameter could just be a Nat

[Marcus Rossel]

We have in fact had a discussion on this before :D.

[Marcus Rossel]

I want to define this cycle of mutually inductive types MutationOutput, Mutation, Reaction, Reactor, Network.
Using Lean 4 seems to fix the issue with nested inductives.

Now my only problem is that (e.g.) Reaction takes an instance of Mutation in its constructor, but also should impose constraints on this instance.

[Marcus Rossel]

In a more MWE-syle this would be (basically):

mutual

inductive A
  | zero
  | next (d : D)

inductive B
  | mk (a : A) (h : a.rec (false) (fun _ => true))

inductive C
  | mk (b : B)

inductive D
  | mk (c : C)
end

[Marcus Rossel]

I think I might be able to work around this though by ignoring all of these kinds of constraints at first and then defining a type (e.g.) ProperReactor which imposes all of these constraints on its contained instances (if that makes sense).

[Mario Carneiro]

what kind of constraints?

[Mario Carneiro]

The general case of this is called an inductive-recursive type, where the constraint is a recursive function defined on the other inductive

[Mario Carneiro]

but if it's a simple function you might be able to write it another way

[Mario Carneiro]

the examples where you say that it has to be just one variant can be rephrased so that you just take the arguments to that variant instead of the inductive argument itself

[Mario Carneiro]

i.e.

mutual

inductive A
  | zero
  | next (d : D)

inductive B
  | mk (d : D)

inductive C
  | mk (b : B)

inductive D
  | mk (c : C)
end

[Mario Carneiro]

if it can be multiple variants, you can still do it with a ProperA type expressing the conjunction of A and the constraints

[Marcus Rossel]

Ok the strategy for this simple example definitely makes sense. I'll try to come up with an MWE that's a bit closer to my real-world use case.

[Marcus Rossel]

Ok, probably not a working example, but I hope it's sufficient.

Mutation defines a function body that produces a MutationOutput.
The output of this function should be constrained (outPrtValsDepOnly) depending the mutation's own deps.
Note, for simplicity in this example, I've expressed outPrtValsDepOnly as if MutationOutput were a simple structure - i.e. I haven't used (body i s).rec ... and just wrote the (body i s).prtVals directly.

Now a Reaction should extend a Mutation by further constraining the output of its body (via noNewCns).

mutual

inductive MutationOutput
  | mk
    (prtVals : List ι)
    (state   : Finset ι)
    (newCns  : List (ι × ι))
    (newRcns : List (Reaction))

inductive Mutation
  | mk
    (deps : Finset ι)
    (body : List ι → Nat → MutationOutput)
    (outPrtValsDepOnly : ∀ i s {o}, (o ∉ deps) → (body i s).prtVals.nth o = none))

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

end

[Marcus Rossel]

So basically these types should all feel like structures. But their mutual inductive nature makes it not so.

[Mario Carneiro]

you forgot to define or import ∉:

constant notin : α → List α → Prop
infix:50 "∉" => notin

[Marcus Rossel]

Oh it could just as well be ∈ here - I've totally butchered the original definition anyway ^^

[Mario Carneiro]

Here's a reduction to eliminate the extra hypotheses:

mutual

inductive MutationOutput {ι : Type} : Finset ι → Type
  | mk {deps}
    (prtVals : List ι)
    (state   : Finset ι)
    (newCns  : List (ι × ι))
    (newRcns : List Reaction)
    (outPrtValsDepOnly : ∀ i s {o}, (o ∉ deps) → prtVals.nth o = none)
    (noNewCns  : newCns = [])
    : MutationOutput deps

inductive Mutation {ι : Type} : Type
  | mk
    (deps : Finset ι)
    (body : List ι → Nat → MutationOutput deps)

inductive Reaction {ι : Type} : Type
  | mk (core : Mutation)

end

[Mario Carneiro]

but I think you might want to consider another approach here, which applies the well formedness conditions outside the types

[Marcus Rossel]

Yeah, that's what I was guessing.

[Marcus Rossel]

Thanks for your help!

[Marcus Rossel]

I'm still having problems with these damned mutual inductives :see_no_evil:
In the following example:

instance List.isSetoid (α) : Setoid (List α) := sorry

def Multiset.{u} (α : Type u) : Type u := Quotient (List.isSetoid α)

mutual

inductive Mutation (ι : Type _)

inductive Reactor (ι : Type _)
  | mk (r : Multiset (Mutation ι))

end

I get the error:

(kernel) arg #2 of '_nested.Finmap_1.mk' contains a non valid occurrence of the datatypes being declared

If I define Multiset using a sorry instead of Quotient, the problem disappears.
Does this mean that Lean can't handle the nested inductive in Reactor.mk because Multiset is a quotient type?

[Eric Rodriguez]

did you make the List.isSetoid instance or is that still a sorry? That may cause issues

[Marcus Rossel]

That's still a sorry.

[Marcus Rossel]

A fully sorry-free version has the issue too though:

inductive List.perm : List α → List α → Prop
  | nil   : perm [] []
  | cons  : ∀ (x : α) {l₁ l₂ : List α}, perm l₁ l₂ → perm (x::l₁) (x::l₂)
  | swap  : ∀ (x y : α) (l : List α), perm (y::x::l) (x::y::l)
  | trans : ∀ {l₁ l₂ l₃ : List α}, perm l₁ l₂ → perm l₂ l₃ → perm l₁ l₃

infix:50 " ~ " => List.perm

protected theorem List.perm.refl : ∀ (l : List α), l ~ l
  | []      => perm.nil
  | (x::xs) => (perm.refl xs).cons x

protected theorem List.perm.symm {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₂ ~ l₁ := by
  induction p with
  | nil => exact nil
  | cons x _ p => exact cons x p
  | swap x y l => exact swap y x l
  | trans _ _ p₁ p₂ => exact trans p₂ p₁

theorem List.perm.eqv : Equivalence (@perm α) where
  refl := perm.refl
  symm := perm.symm
  trans := perm.trans

instance List.isSetoid (α) : Setoid (List α) := Setoid.mk _ perm.eqv

[Eric Rodriguez]

so I tried doing this defn in lean3, and it even though it has the same code for dealing with positivity issues, it actually complains about universes instead -- maybe that's the real issue that's getting obfuscated?

[Marcus Rossel]

What do you mean by "positivity issues"?

[Eric Rodriguez]

the error comes from this line, which tries to check that all terms in an inductive type's constructor are "positive"

[Eric Rodriguez]

#tpil covers this somewhere very briefly and links to a specific paper about it (e: here)

[Sebastian Ullrich]

Lean implements nested inductive types by translating them to mutually inductive types, but Quotient is not an inductive type, so this translation is not possible

[Sebastian Ullrich]

Basically, all types involved in the recursion must either be unfoldable or appropriate inductive types, but Quot is a constant

[Marcus Rossel]

Oh no, I'll have to do some trickery then.
Thanks y'all for the help!