Inductive Bug with Array + Prop

Stream: lean4

[Mac]

I have an Array2 type derived from an Array that restricts its length to >= 2 and am attempting to use it in in an inductive. However, I am getting a weird error I don't understand. Can anyone explain what is going on here?

structure Array2 (α : Type u) extends Array α where
  size_ge_2 : toArray.size  ≥ 2

inductive Data
| tuple : Array2 Data → Data

/-
application type mismatch
  Array.size toArray
argument has type
  _nested.Array_2
but function has type
  Array Data → Nat
-/

[Mario Carneiro]

I don't think nested inductives support dependent types like that. I don't know how the desugaring to the core calculus would work, I think you would get an inductive-recursive type

[Mac]

@Mario Carneiro does that mean it is impossible to have a inductive data type that includes collections of itself that satisfy certain prosperities? That seems very limiting.

[Mario Carneiro]

There are often ways to write around it with other constructions, in particular not using nested inductives

[Mario Carneiro]

I think if you make it an unsafe inductive lean will get off your back as well

[Mario Carneiro]

Also, it's not that you can't have properties in a nested inductive, it's that the properties can't make reference to Array functions when Array is one of the things involved in the nested inductive

[Mario Carneiro]

In this case, one way to get the structure you want is to separate the inductive from the property and put them back together with a subtype

[Mario Carneiro]

inductive RawData
| tuple : Array RawData → RawData

partial def RawData.ok : RawData → Prop
| ⟨arr⟩ => arr.size ≥ 2 ∧ ∀ i, (arr.get i).ok

def Data : Type := { d : RawData // d.ok }

[Mario Carneiro]

(you wouldn't use a partial def in reality, you can prove this is decreasing)

[Mario Carneiro]

and if you are okay with an isomorphic type instead of Array, you can also write it like this:

inductive Data
| tuple {n} : n ≥ 2 → (Fin n → Data) → Data

[Mario Carneiro]

this one is not even a nested inductive, so it plays well with induction and such

[Marcus Rossel]

@Mario Carneiro Do you think the Raw+Subtype approach is generalizable to a syntactic sugar? That is, could it be possible to extend Lean in such a way that it compiles such an inductive type into a raw type and a corresponding subtype (and them exposes an appropriate API on the subtype, so the user doesnt notice what's going on under the hood)?
I've been using this approach too, and it feels like something generalizable.

[Mario Carneiro]

Yes in principle, but it's a quagmire of heuristics and I don't think it would yield a reliable mechanism. This is not too far from what lean 3 did to handle nested inductives, and it was kind of a mess

[Marcus Rossel]

Do you happen to know if other theorem provers do this well?

[Mario Carneiro]

The problem is that inductive types are connected to everything in lean, so you have to be aware of these sugar mechanisms in all other tactics, which is a huge complexity cost

[Marcus Rossel]

you have to be aware of these sugar mechanisms in all other tactics

...because the tactics can see behind the sugar (by virtue or using things like Syntax and Expr)?

[Mario Carneiro]

No other theorem prover handles inductive types quite like lean. Coq and Agda axiomatize everything, so there is nothing to prove but the resulting metatheory is shaky. Isabelle and HOL generate inductives with proofs under the hood, but simple types limit the kinds of constructions you can express enough that these issues largely don't arise.

[Mario Carneiro]

and of course regular programming languages shoot first and ask questions later

[Mario Carneiro]

Marcus Rossel said:

have to be aware of these sugar mechanisms in all other tactics

...because the tactics can see behind the sugar (by virtue or using things like Syntax and Expr)?

Because users expect the sugar to act just like an inductive type, even though technically it's not one, so every tactic is responsible for "upholding the fiction"

[Henrik Böving]

Is there some documentation or paper on how exactly inductive types are handled in Lean?

[Mario Carneiro]

Probably the closest thing is my thesis https://github.com/digama0/lean-type-theory/releases/tag/v1.0

[Marcus Rossel]

I feel like we need some shortcut like #ttol for your thesis at some point :D

[Mario Carneiro]

sure, why not? #leantt

[Mario Carneiro]

The paper is a bit out of date now though, since lean 4 made some kernel changes that are relevant to the theory

[Mario Carneiro]

The biggest new thing being kernel nested inductives

[Mario Carneiro]

and understanding how they work is key to this particular issue

[Mario Carneiro]

also eta for structures

[Marcus Rossel]

Wait, so the kernel can understand a certain class of nested inductives natively?!

[Mario Carneiro]

Yes, all nested inductives that lean 4 accepts are accepted "natively" now

[Mario Carneiro]

no more complicated sugar

[Mario Carneiro]

instead we have a complicated metatheory

[Mario Carneiro]

However, my understanding is that it is still essentially the same justification as the lean 3 simulation, just now being performed by the kernel, so I'm fairly confident that the theory still holds up

[Mario Carneiro]

But one of the dangers of adding this stuff to the kernel is that it makes it attractive to make feature suggestions to extend the kernel acceptance criterion by epsilon through issues just like this one, which is basically how Coq / Agda ended up the way they are now

[Marcus Rossel]

Just to make sure I understand: the only nice way of doing raw+subtype inductives would be to not do them at all and instead shove them into the kernel and hence the metatheory and that's undesirable?

[Mario Carneiro]

Right. I would be very uncomfortable with such a change without updating the consistency proof first

[Marcus Rossel]

Sound like we need you to do another MSc then :eyes::nerd:

[Mario Carneiro]

As I mentioned, I think that allowing constructions like this in general is equivalent in power to inductive-recursive types, which are known to be strictly axiomatically stronger than the current "ZFC + omega inaccessibles"

[Mario Carneiro]

It's probably more like "ZFC + omega Mahlo cardinals" instead

[Mario Carneiro]

http://www.cse.chalmers.se/~peterd/papers/Finite_IR.pdf validates my guess that type theory universes in an inductive-recursive world correspond to Mahlo cardinals

[Reid Barton]

I suspect some type theorists consider this a feature rather than a bug. I'm pretty sure there are some simple restrictions to avoid adding the extra logical power. For example, one which I'm pretty sure works is to only allow the recursive function to take values in a type which is smaller than the universe containing the inductive type being defined.

[Andrés Goens]

So a potential solution could be making this raw data + (nested) properties construction into a library that does not create the illusion of being a 'normal' inductive type thus making the user reason more explicitly about it, but still helping with all the boilerplate?
Mario Carneiro said:

Marcus Rossel said:

have to be aware of these sugar mechanisms in all other tactics

...because the tactics can see behind the sugar (by virtue or using things like Syntax and Expr)?

Because users expect the sugar to act just like an inductive type, even though technically it's not one, so every tactic is responsible for "upholding the fiction"

[Mac]

Reid Barton said:

I suspect some type theorists consider this a feature rather than a bug.

Fair enoguh! :laughing: However, even if this is true (which, deferring to @Mario Carneiro's expertise on the topic, it seems to be), there is still, in my view, a bug here. Namely, that the error message doesn't tell you this. It just produces an error about so mismatch in its internal representation (which, in many other cases, has meant there was a bug). The error message here should inform the user about what conceptually type theoretic mistake they made (like it does with universe issues and other inductive restrictions).

[Mario Carneiro]

I can explain a little bit of what the error is actually saying. Somewhere internally, we have to swap out the type Array Data for a local variable Array_Data : Type (about which we know nothing, because it is part of a mutual block of inductive definitions). This causes a type error when you try to use a function like Array.size on it, because the input is not an array anymore. If you used a function that did not care about the type like id I think it would still typecheck.

[Mario Carneiro]

It is hard for lean to determine in advance whether such an error is likely to occur without actually writing down the term and checking it for well formedness; but once you have done that the quality of error messages already goes down quite a bit because lots of things can go wrong when you type check a term

[Mario Carneiro]

It would not be difficult to paper over this error with another vaguer error, but I don't know how targeted that error can be.

[Mario Carneiro]

This error is roughly analogous to the infamous motive is not type correct error in rw. Is that what we want here?

[Mac]

Mario Carneiro said:

This error is roughly analogous to the infamous motive is not type correct error in rw. Is that what we want here?

While I certainly would like a more detailed error. I do think even that would be better. The current is simply not clear on whether the error is with the user or with Lean. In fact, the exposure of internal tricks makes it appear more like the later.