more flexible nested inductives

Stream: lean4

[Arthur Adjedj]

Mario Carneiro said:

While you can't use RBMap in a nested inductive, you can use RBNode, the inductive it is defined from

I still hold the belief that Lean would benefit from having either a somehow smarter way to detect strict positivity, or a way for the end-user to annotate things as strictly positive. HashMap and RBMap would benefit a lot from that imo

[Mario Carneiro]

Sigma types are fundamentally not strictly positive though

[Mario Carneiro]

They are a pair of an element of T and an element of an element of T -> Prop

[Mario Carneiro]

And an annotation is hard because this is a kernel-level check

[Arthur Adjedj]

While it's obviously not strictly positive over the first argument, would Sigma A not be strictly positive for any A ?

[Mario Carneiro]

What is Sigma A? Sigma takes two arguments

[Arthur Adjedj]

the type Sigma A, given any type A

[Mario Carneiro]

inductive Sigma.{u, v} : {α : Type u} → (α → Type v) → Type (max u v)

[Mario Carneiro]

sorry, the first one is implicit. But I still don't know what you mean

[Mario Carneiro]

because the explicit argument of Sigma is not a type

[Arthur Adjedj]

oops, you're right, nevermind then

[Arthur Adjedj]

Mario Carneiro said:

And an annotation is hard because this is a kernel-level check

Other proof-assistants (namely, Coq) do allow for the modification of certain kernel-checks through the use of pragmas/flags though

[Mario Carneiro]

in some cases, with heavy reworking, it is possible to rephrase sigma types as inductive types by pushing properties into the leaves. This creates very dependent types though so I am wary of this approach

[Mario Carneiro]

Arthur Adjedj said:

Mario Carneiro said:

And an annotation is hard because this is a kernel-level check

Other proof-assistants (namely, Coq) do allow for the modification of certain kernel-checks through the use of pragmas/flags though

yep, this is never going to happen, we want a better soundness story than that

[Arthur Adjedj]

Alright, makes sense.

[Mario Carneiro]

also Coq would not allow this type, for the same reason

[Arthur Adjedj]

It would, if you tagged the inductive definition of BkTree with a tag to cancel the positivity-checking on it.

[Arthur Adjedj]

Some much more innocuous inductive types could also stand to be accepted by the positivity-checker. Agda is smarter for that matter. For example, the following gets accepted by Agda, but not by lean:

structure Foo (x : Type →  Type) where

inductive Bar : Type → Type :=
| bar : Bar (Foo Bar)

[Mario Carneiro]

I'm not sure I would describe that type as innocuous

[Mario Carneiro]

specifically, what are the bounds on when such types are accepted, and where is the paper proof of soundness of such an extension? I wouldn't even want to consider an extension without that

[Arthur Adjedj]

I would have to dive into Agda's codebase again, but I believe the criteria is that Foomust be strictly positivive. As for a soundness proof of that extension, I do not have a paper-proof justification in hand, and would need to look into that. Such extension is however useful for formalising things like logical relations of other type theories, and is an issue I encountered when trying to port a formalisation from Agda to Lean.

[Arthur Adjedj]

I do however have an example in hand of a justifyably sound inductive type that doesn't get accepted by lean, let me find it again.

[Mario Carneiro]

My opinion of the agda soundness story is very low, so "agda can do it, why can't lean?" isn't very persuasive to me

[Arthur Adjedj]

here
I don't know if lean 4 still compiles nested inductives to mutual ones, but it seems to have trouble compiling down nested inductive predicates. I should be able to make a MWE quickly enough. This sort of stuff is accepted by Coq with no issue.

[Mario Carneiro]

I think the example you gave above is also justifiably sound (take Foo x := Unit and Bar x := if x = Unit then Unit else Empty), but that's just one example, not a whole scheme

[Mario Carneiro]

Lean 4 does not compile nested inductives to mutual

[Mario Carneiro]

but it does a check that should be equivalent to the existence of such a reduction

[Mario Carneiro]

and it needs to compute essentially the reduction in order to determine the structure of the recursor

[Mario Carneiro]

Does agda even have recursors for these types?

[Arthur Adjedj]

Mario Carneiro said:

I think the example you gave above is also justifiably sound (take Foo x := Unit and Bar x := if x = Unit then Unit else Empty), but that's just one example, not a whole scheme

It is ! In general, there is a way to re-encode such types by "inlining" the structure Foo in some way, at least as long as Foo is not recursive. I've had to do that on a more complex example myself, and there hasn't been any fundamental issue to doing the translation.

[Arthur Adjedj]

Mario Carneiro said:

Does agda even have recursors for these types?

Agda doesn't generate recursors for anything

[Arthur Adjedj]

Arthur Adjedj said:

here
I don't know if lean 4 still compiles nested inductives to mutual ones, but it seems to have trouble compiling down nested inductive predicates. I should be able to make a MWE quickly enough. This sort of stuff is accepted by Coq with no issue.

Here is an MWE:

inductive Forall {α : Type u} (p : α → Prop) : α → Prop

inductive Foo {α : Type u} : α → Prop :=
  | foo : (a : α) → Forall Foo a → Foo a
/-only trivial inductive applications supported in premises:
  Forall Foo a-/

[Mario Carneiro]

and what would the recursor be?

[Mario Carneiro]

in that example, lean won't even allow it with unsafe inductive, probably because it has no idea how to generate the recursor

[Arthur Adjedj]

Coq manages to generate one:

Inductive Forall {α : Type} (p : α -> Prop) : α -> Prop :=.
Inductive Foo {α : Type} : α -> Prop :=
  | foo (a : α) : Forall Foo a -> Foo a.

Check Foo_ind. (*Foo_ind
     : forall (α : Type) (P : α -> Prop), (forall a : α, Forall Foo a -> P a) -> forall α0 : α, Foo α0 -> P α0*)

[Mario Carneiro]

what does that look like with | mk : p a -> Forall p a?

[Mario Carneiro]

and also | mk : (p a -> False) -> Forall p a (I hope this is rejected)

[Mario Carneiro]

That induction principle looks odd because it doesn't have two motives, even though there are two inductives involved

[Arthur Adjedj]

(jscoq gives horrible copy-pasted stuff, so I'm sending screenshots)
The former gives this:
image.png
The second doesn't get accepted.

[Mario Carneiro]

wait a minute, that's the same as the first one

[Arthur Adjedj]

even with p a, it doesn't add a new motive

[Mario Carneiro]

I think this recursor is not (intended to be) complete, it's only good enough to do induction over the Foo part without any mutual inductions that have to bounce back and forth between Foo and Forall Foo

[Arthur Adjedj]

Coq's auto-generated recursors are broken on nested/mutual inductives, I'd have to do some Scheme Induction stuff to retrieve the correct ones, and I don't remember how

[Arthur Adjedj]

I'll look into it

[Mario Carneiro]

in which case it may well be the case that no one has ever worked out the full scheme for nested inductives in coq and/or agda

[Arthur Adjedj]

Inductive Forall {α : Type} (p : α -> Prop) : α -> Prop :=
| mk (a : α): p a -> Forall p a.
Inductive Foo {α : Type} : α -> Prop :=
  | foo (a : α) : Forall Foo a -> Foo a.

Scheme Foo_ind_2 := Induction for Foo Sort Prop.
Check Foo_ind_2.

image.png

[Arthur Adjedj]

It doesn't add a motive here, but does do some "inlining" trick by asking for the motive to be indexed by α

[Mario Carneiro]

that looks like it is treating alpha as an index rather than a parameter

[Mario Carneiro]

that's usually undesirable, it makes the scheme weaker

[Mario Carneiro]

oh wait nvm, alpha0 is an element of type alpha

[Mario Carneiro]

okay yeah, this is just casesOn

[Mario Carneiro]

I don't think there is any inlining happening here, you would get the same result if the argument to foo was of some other type B

[Arthur Adjedj]

you're right

[Arthur Adjedj]

In any case, the same inductive definitions are allowed in Type in lean

[Arthur Adjedj]

However, it wouldn't make sense for lean to have trouble knowing whether Foo is a subsingleton here, since it's pretty obviously indexed

[Arthur Adjedj]

And also makes a seemingly correct recursors when defining this over Type :

inductive Forall (p : α → Type) : α → Type

inductive Foo : α → Type :=
  | foo : (a : α) → Forall Foo a → Foo a

#check @Foo.rec
/-{α : Sort u_2} →
  {a : α} →
    {motive_1 : Foo a → Sort u_1} →
      {motive_2 : Forall Foo a → Sort u_1} →
        ((a_1 : Forall Foo a) → motive_2 a_1 → motive_1 (Foo.foo a a_1)) → (t : Foo a) → motive_1 t-/

[Arthur Adjedj]

(Also, this conversation has strayed far away from termination-checking, maybe it's would be good to move it in some way ?)

[Notification Bot]

57 messages were moved here from #new members > Termination checking for dummies by Mario Carneiro.

[Mario Carneiro]

I have to admit I have not yet carefully studied the rules for nested/mutual inductives in lean 4 like I did for lean 3 (which only had plain inductives and simulated the other stuff). It is not immediately obvious to me why the type being in Prop should matter here, but the error message suggests that it is an incompleteness in the implementation

[Arthur Adjedj]

Should I open an issue then ?

[Mario Carneiro]

it would be best to have an implementation in hand first

[Arthur Adjedj]

I could find myself spending some time into trying to fix this

[Mario Carneiro]

I see now that the specific error message thrown here: only trivial inductive applications supported in premises is caused not by the kernel but the elaborator, when trying to create the Foo.Below type, which makes sense, these generally can't be created for Prop inductives

[Mario Carneiro]

there is an entirely different strategy used for prop inductives

[Mario Carneiro]

and perhaps it is not as complete

[Arthur Adjedj]

Mario Carneiro said:

it would be best to have an implementation in hand first

Speaking of implementation, I've made a fix to the transitivity issue of defeq regarding eta-for unit some time ago (#2258), but was hesitant on making a PR for that, would it be worth doing one ?

[Mario Carneiro]

unfortunately there doesn't seem to be an option to disable auxiliary constructions, although you could call the kernel directly

[Mario Carneiro]

another hack is to define the type from an empty prelude file (it won't generate the Below if Prod hasn't been defined yet), although lots of other things might break

[Arthur Adjedj]

Mario Carneiro said:

unfortunately there doesn't seem to be an option to disable auxiliary constructions, although you could call the kernel directly

I've tried in the past to do that, but didn't manage to write something working. I might try my hand at it again

[Arthur Adjedj]

Mario Carneiro said:

another hack is to define the type from an empty prelude file (it won't generate the Below if Prod hasn't been defined yet), although lots of other things might break

prelude doesn't help, I still get the same error here:

prelude

inductive Forall  (p : α → Prop) : α → Prop

inductive Foo : α → Prop :=
  | foo : (a : α) → Forall Foo a → Foo a

[Mario Carneiro]

oh interesting, apparently there are two implementations of mkBelow, one in C++ and one in lean

[Arthur Adjedj]

yeah, it sems like all the helper functions like noConfusion, CasesOn etc.. have corresponding C++ versions

[Mario Carneiro]

the C++ mk_below ignores inductive predicates, the lean one throws an error

[Arthur Adjedj]

I'm confused then, why would I still get that error on prelude ?

[Mario Carneiro]

elabInductiveViews calls mkBelow twice, once via mkInductiveDecl -> mkAuxConstructions (which checks for Prod) and once directly (unconditional)

[Mario Carneiro]

actually the first one is calling Lean.mkBelow, the C++ one

[Mario Carneiro]

which only does non-indpreds

[Mario Carneiro]

the second one is IndPredBelow.mkBelow, which fails on this inductive

[Arthur Adjedj]

Looking more into this, i've just realised that despite the red scary error message, Foo is still accepted, and all helpers other than below (and noConfusion, but Prop types shouldn't have one so all good). Also, this is a new regression from lean 4, the same piece of code works with no issue in Lean 3
Mario Carneiro said:

there is an entirely different strategy used for prop inductives

I couldn't find any piece of code which suggested that Prop-inductives are treated any differently when generating below lemmas, do you know where the difference in approach happens ?

[Mario Carneiro]

@Arthur Adjedj the C++ function mk_below starts with

    if (is_inductive_predicate(env, n))
        return env;

meaning that it does nothing on inductive predicates, and conversely IndPredBelow.mkBelow is wrapped in

def mkBelow (declName : Name) : MetaM Unit := do
  if (← isInductivePredicate declName) then
    <stuff>
  else trace[Meta.IndPredBelow] "Not inductive predicate"

meaning that it only does something on inductive predicates

[Arthur Adjedj]

As it turns out, any nested inductive predicate triggers the error, it just so happens that no one uses them:

inductive Foo : Prop → Prop

inductive Bar : Prop
  | bar : Foo Bar → Bar
/-only trivial inductive applications supported in premises:
  Foo Bar-/

Replacing the condition if x.isRec thenin mkBelow with if x.isRec && !x.isNested thenfixes the issue :) Should I make an issue + PR ? @Mario Carneiro

[Mario Carneiro]

yeah, generating nothing sounds better than erroring

[Arthur Adjedj]

I don't think there is a general scheme to generate below lemmas for inductive predicate since those may heavily depend on the shape of the nested application, simply not generating them might be better for now.