For which constructors `inj` is generated?

Stream: new members

[Lauri Oksanen]

I would like to formulate a rule telling for which constructors an injectivity theorem is generated. My guesses are "Lean generates an injectivity theorem for each constructor taking fields" or perhaps "Lean generates an injectivity theorem for each constructor taking fields, unless those fields are determined by the constructor’s codomain.". These would explain why Eq.refl does not have inj while most other constructors do have it. If this is explained in the language reference, I would appreciate a pointer.

(My terminology is, based on help from @Kyle Miller: "The parameters of an inductive type consist of the largest prefix of arguments shared by the type constructor and all the constructors. The remaining arguments of the type constructor are called indices, and the remaining arguments of a constructor are called fields.")

[Joachim Breitner]

Eq is a proposition, all proofs of a proposition are equal, so no useful injectivity theorem can exist here.

[Lauri Oksanen]

This is not solely about Prop vs. Type. The following doesn't have inj:

set_option inductive.autoPromoteIndices false in
inductive Wrap : Nat → Type where
  | mk : (n : Nat) → Wrap n

#print Wrap.mk.inj

The #print command fails with Unknown constant .... This example says, in fact, that "Lean generates an injectivity theorem for each constructor taking fields" is not correct.

[Joachim Breitner]

Have you already checked the Lean code for a more detailed answer?

[Lauri Oksanen]

No, I haven't studied the code at all. I guess that I need to do that at some point if I want to understand Lean thoroughly. But there are quite a few other things to learn before that, I think.

[Joachim Breitner]

Ok, let me then do that for you real quick, I'm also curious

[Joachim Breitner]

Some checks are done here:
https://github.com/leanprover/lean4/blob/2e7fe7e79d151ee91039f086b8036252cdf9b725/src/Lean/Meta/Injective.lean#L187-L191
namely

• not if genInjectivity option is unset
• not if Eq.propIntro is not declared (only relevant during Init processing)
• not for inductive predicates
• not for unsafe inductives.

Another reason for it to not generate any is if it runs into this line of code:

https://github.com/leanprover/lean4/blob/2e7fe7e79d151ee91039f086b8036252cdf9b725/src/Lean/Meta/Injective.lean#L61

This happens if mkAnd? eqs returns none. I assume this simply means “no equations present”, which in the case of Wrap is not surprising – mk n1 = mk n2 can only hold if n1 = n2 (because they are indices), so no equation can be “injected out” here, and the theorem would be vacuous

[Kyle Miller]

Yeah, and if I'm reading that code correctly, it doesn't actually take the distinction between parameters and indices into account (except that, as an optimization, it skips parameters since they're already known to be equal across constructors).

It makes the assumption that any constructor argument appearing in its return type (or in the type of any subexpression of its return type) is determined by the return type and skips creating an equality hypothesis for that argument. This detects all "parameter-like" fields. If there are no equality hypotheses, it skips creating the inj theorem.

That assumption is however an approximation, and it's possible to trick it!

inductive Wrapped' : Nat → Type where
  | mk (n : Nat) : Wrapped' (Function.const _ 0 n)

#check Wrapped'.mk.inj -- unknown constant

theorem Wrapped'.mk.inj (m n : Nat) (h : Wrapped'.mk m = Wrapped'.mk n) : m = n := by
  cases h
  rfl

[Joachim Breitner]

Good catch! There is also the case where the index is a function (like /2). Then there are useful injectivity theorems for certain specific insides, but you cannot actually write them down easily. At that point, just use noConfusion directly

[Lauri Oksanen]

Thanks a lot! Without trying to read the code, my interpretation of this is that "Lean generates an injectivity theorem for each constructor taking fields, unless those fields appear in constructor’s codomain" is reasonably accurate.