Instances in ∀

Stream: new members

[Joachim Breitner]

I am trying to phrase an induction prinicple like

lemma nilpotent_center_quotient_ind
  (P : Type* -> Prop)
  (hbase : ∀ G [group G] [subsingleton G], P G)
  (hstep : ∀ G [group G] [is_nilpotent G], P (G ⧸ center G) -> P G))
  [is_nilpotent G] :
  P G := sorry

but lean complains that, for example, the is_nilpotent P term’s implicit group G parameter cannot be solved. But it’s right there! Do I have to spell it out with @is_nilpotent G hG, or is there a prettier way of phrasing that?

[Henrik Böving]

I can't see a is_nilpotent P in your code, I'm guessing you mean G?. The reason it cannot solve this I think, is that the 3 G you are referring throughout the induction principle here are all considered different G by lean and thus the [is_nilpotent G] parameter outside of the hbase and hstep does not have access to thegroup G instance. If its complaining about an instance missing in hstep I would be confused though.

[Eric Wieser]

by exactI after the comma

[Eric Wieser]

∀ G [group G], by exactI ∀ [is_nilpotent G], ...

[Eric Rodriguez]

Testing my faq - would this have explained what was going on? Should I have made it more explicit for foralls and such?

[Joachim Breitner]

Hmm, I think I have seen that FAQ before and it makes sense to me, but since it talks only about tactics, I did not expect it to help in this application. And I didn’t think of using tactics inside the proof statement (as Eric suggests).

[Joachim Breitner]

Henrik: Oh, yes, sorry, there is an implicit group G in scope, but the one that causes problems is the one in hstep.

[Joachim Breitner]

Ok, this works and can be proven:

lemma nilpotent_center_quotient_ind
  {P : Type* -> Prop}
  (G : Type*)
  (hbase : ∀ G [group G] [subsingleton G], P G)
  (hstep : ∀ G [group G], by exactI ∀ [is_nilpotent G], P (G ⧸ center G) -> P G)
  [group G]
  [is_nilpotent G] :
  P G :=

but induction G using nilpotent_center_quotient_ind doesn’t quite like it, says

invalid user defined recursor, type of the major premise 'G' must be for the form (I ...), where I is a constant

I tried to reorder the various premisses, but it didn't help. Any idea?

[Eric Wieser]

The induction tactic is pretty picky and often doesn't work for custom recursors. At a guess, moving G to just before group might help, but I'm not optimistic

[Eric Wieser]

Tangentially related - is G / center G also nilpotent in that example?

[Joachim Breitner]

Yes, but that follows readily from is_nilpotent G via an instance, so I figured I don’t have to add it as extra information to hstep

[Eric Wieser]

Because then you can make P : Π G [group G], by exactI is_nilpotent G→Prop

[Eric Wieser]

Which will make the recursor work slightly better

[Joachim Breitner]

Ah, I see. I’ll try.

[Joachim Breitner]

Now I get induction tactic failed, major premise type is ill-formed.
BTW, which one is called the “major premise”?
According to https://exlean.org/what-the-rec-types-dependent-on-terms-lean-eliminators-and-threshold-concepts/ it would be G.

[Joachim Breitner]

The type of the major premise 'G' which must be for the form (I ...) is, in my case Type u. Maybe that's the problem; Type isn’t a normal constant here?

[Joachim Breitner]

I’ll just apply the lemma manually, with refine, for now. Good enough for me.