How to convince Lean a type is inductive?

Stream: lean4

[jthulhu]

I need a nested-quotient-inductive type, but Lean does not currently support them. In the long term, I'd like to build a library to implement them (until they are supported in the kernel, which AFAIK is something currently discussed), but for now I'd like to build one "by hand", to understand how to make that work exactly. For that, I have built a type, I have proven a dependent induction principle for it, and I have proven that it computes (up to propositional equality). Importantly, it does not compute definitionally (this may be relevant), or, at least, not all cases do compute definitionally (some do). It works with tactics like induction and cases, but only by explicitly specifying the recursor to use. Pattern matching does not work, and neither does the convenient syntax of rcases. I'd like to know how much I can "convince" the elaborator that this type is inductive, that is, by poking enough in Lean's internals, to register it as an inductive data type so that it works "natively" as an inductive type. I know that the current code is probably not able to derive some of the lemmas, functions, types and instances for it (like the SizeOf instance), so would it be enough for me to just implement them all by hand? If so, I'd like to have an exhaustive list of stuff I have to implement by hand (like below, recOn, casesOn, noConfusion, ...) because I'm not sure where to find the documentation for this. If not, what do I need to do? Is there some data structure used by the elaborator where metadata about inductive types is registered?

Also, broadly speaking, I'm not sure where to find documentation for this kind of stuff. I have already written a library that offered "custom" inductive types, but it was kind of a pain to implement, I had to read part of the elaboration pipeline, and to figure out stuff from the code. If there is a better way to learn the exposed API, or how things are implemented, I'd be glad to hear about it.

Thanks in advance

[Aaron Liu]

You can mark the dependent induction principle as @[induction_eliminator, cases_eliminator] and it will be the default eliminator for induction and cases. afaik there's no simple way to just "register" it as an inductive type and therefore you can't get it to work with rcases or match.

[Jakub Nowak]

About implementing by hand, I did a hack where I have separate inductive I match on, and actual structure is defined as def. But this was because the native definition would not terminate, so not sure if it applies to your case.
#new members > Stuck on ManyT in "Functional Programming in Lean" @ 💬

If you post #mwe maybe someone could try to help.

[jthulhu]

After having discussed with @Arthur Adjedj about how inductive types are looked up, it seems that there is no decent low-cost solution, the reason being that the elaborator apparently asks the kernel whether a given constant is an inductive type or not, so the only "simple" solution would be to hook into that and lie to the elaborator about the nature of the type, but it's a shaky solution.

[jthulhu]

Jakub Nowak said:

If you post #mwe maybe someone could try to help.

Sure, a minimal request would be: make the following code work.

-- you can assume anything reasonable about this type
axiom Finset (α : Type) : Type

axiom Ω : Type
axiom Ω.true : Ω
axiom Ω.false : Ω
axiom Ω.inl : Ω → Ω
axiom Ω.inr : Ω → Ω
axiom Ω.pair : Ω → Ω → Ω
axiom Ω.set : Finset Ω → Ω

axiom Ω.rec :
  {motive : Ω → Sort _} →
  (true : motive .true) →
  (false : motive.false) →
  (inl : ∀ x, motive x → motive x.inl) →
  (inr : ∀ x, motive x → motive x.inr) →
  (pair : ∀ x y, motive x → motive y → motive (x.pair y)) →
  (set : ∀ X : Finset Ω, (∀ x ∈ X, motive x) → motive (.set X)) →
  ∀ o, motive o

axiom rec_true true false inl inr pair set : Ω.true.rec true false inl inr pair set = true
...

def id : Ω → Ω
  | true => .true
  | false => .false
  | inl x => .inl (id x)
  | inr x => .inr (id x)
  | pair x y => .pair (id x) (id y)
  | set X => .set (X.map id)   -- or whatever that is compatible with the recursor

[Jakub Nowak]

One solution would be to have implement version of Finset that works with recursive inductive. You could e.g. use sorted list (i.e. List, and a proof that it is sorted). You can prove that it is equivalent to Finset for easier proofs. See #Is there code for X? > extensional finite map inside inductive definition about similar problem. Another solution is to extract the quotient outside, i.e. you would define inductive Ω with List, and then define Setoid on Ω that divides this List by permutations (that's how Finset is implemented). But this approach is tedious and I wouldn't recommend it. For example of this, see the mentioned topic.

[Jakub Nowak]

@Mirek Olšák Sorry for pinging you. You recently gave a great explanation here: #new members > Idiomatically working with mutual inductive types @ 💬, so you might also be able to explain things here.
Given your set-counting argument I'm wondering why Quot/Quotient doesn't work with recursive inductive types. Quot is always not-greater than its underlying type, and the underlying type of Finset is List, so in theory, it should be possible? Is this also the case that no one worked on extending Lean to work with Quot, or is there some inherent problem with e.g. the fact that Quot is axiomatized?

[Mirek Olšák]

Similarly as with that other case, the issue is not that using Quot would be mathematically invalid but that using Quot is complicated. It is not that you are allowed to repeat your type anywhere with a few exceptions, rather that there is a limited set of positions where your type can recursively occur.

If we ignore mutual inductives and nested inductives (like List Foo), the rule is: you can only put your inductive Foo as the output type of an argument of a constructor. To be honest, I don't know exactly the details for mutual & nested inductives. However, Quot is super-tricky because you have to provide a relation Foo -> Foo -> Prop, so suddenly the type will occur at least as an argument type of a function before it was declared.

If you want to quotient inside an inductive type, you should first build an unquotiented type, and then build another type that does the quotient. As an example, look how ZFSet is the quotient of PSet.

[jthulhu]

Jakub Nowak said:

One solution would be to have implement version of Finset that works with recursive inductive. You could e.g. use sorted list (i.e. List, and a proof that it is sorted). You can prove that it is equivalent to Finset for easier proofs

That would require inductive-inductive or recursive-inductives, and AFAIK Lean does not support them. Ie

inductive Ω where
  ...
  | set (s : List Ω) : s.Sorted Le → s.Nodup → Ω

inductive Le : Ω → Ω → Prop where
   ...
-- or
def Le : Ω → Ω → Prop :=
  ...

both fail.

Jakub Nowak said:

See #Is there code for X? > extensional finite map inside inductive definition about similar problem. Another solution is to extract the quotient outside, i.e. you would define inductive Ω with List, and then define Setoid on Ω that divides this List by permutations (that's how Finset is implemented). But this approach is tedious and I wouldn't recommend it. For example of this, see the mentioned topic.

This is precisely what I have done, and indeed, this is extremely tedious. This is why I get an inductive-like type (ie. constructors + a recursor) but which is not an inductive type.

[Jakub Nowak]

You can do that:

import Mathlib

inductive PreΩ : Type where
| set (s : List Ω) : Ω

instance : LT Ω := sorry

def Ω.WF : Ω → Prop
| set s => s.Pairwise (· < ·)

And then either use PreΩ and PreΩ.WF unbundled, or bundled as def Ω := { x : PreΩ // x.WF }. In this case I think the latter will be better.

[Jakub Nowak]

From the computational perspective quotient approach doesn't require you to sort the list. But I think that working with sorted lists is easier than working with quotient of list by permutations. At least it was for me in a different setting.

[Aaron Liu]

this only works when your type is orderable :(

[Jakub Nowak]

(deleted)

[Jakub Nowak]

You could also not have s.Pairwise (· < ·) at all, if you don't care about equality being extensional.

[Aaron Liu]

then I can't prove extensionality :(

[jthulhu]

Jakub Nowak said:

You can do that:

import Mathlib

inductive PreΩ : Type where
| set (s : List Ω) : Ω

instance : LT Ω := sorry

def Ω.WF : Ω → Prop
| set s => s.Pairwise (· < ·)

And then either use PreΩ and PreΩ.WF unbundled, or bundled as def Ω := { x : PreΩ // x.WF }. In this case I think the latter will be better.

Oh! This is a solution I didn't think of. Indeed, I think it is better than using quotients, and in my case, PreΩ is not a large inductive so it can be ordered.