induction on Type

Stream: general

[Joachim Breitner]

I can define a custom induction principle with a major premise of type ℕ (or any other “normal” type) just fine:

@[elab_as_eliminator]
lemma silly_nat_ind (P : ℕ -> Prop) (a : ℕ) (h1 : ∀ a, 1=1 → P a) (h2 : ∀ a, 2=2 → P a) : P a :=
sorry

example (n : ℕ) (h : n > 0) : n = 42 :=
begin
  induction n using silly_nat_ind,
  sorry
end

But if I try to do the same with a major premise of type Type, like this:

@[elab_as_eliminator]
lemma silly_type_ind (P : Type -> Prop) (a : Type) (h1 : ∀ a, 1=1 → P a) (h2 : ∀ a, 2=2 → P a) : P a :=
sorry

example (x : Type) (h : fintype x) : fintype.card x = 42 :=
begin
  induction x using silly_type_ind,
  sorry
end

the induction tactic complains with

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

Is Type not a constant?
Is there a deep reason why this can’t work, or is there just a check in the induction premise too strict?

This may not be too relevant in practice because usually the major premise is not just a Type, but also a predicate on Type such as fintype or is_nilpotent, and then the induction proceeds on that, and that works, so I am mostly curious.

[Sebastian Ullrich]

Yeah, that may very well be an implementation limitation. "Constants" are declarations in the environment referenced with the Expr.const constructor, while Type is a primitive Expr.sort application https://github.com/leanprover/lean4/blob/3dfd14dfffaaa7e5479e2c40c10ff94848681d93/src/Lean/Expr.lean#L205-L206 (referencing Lean 4 because I'm lazy).

[Kyle Miller]

I guess Type doesn't count as a constant. This works:

def Type' := Type

@[elab_as_eliminator]
lemma silly_type_ind (P : Type' -> Prop) (a : Type') (h1 : ∀ a, 1=1 → P a) (h2 : ∀ a, 2=2 → P a) : P a :=
sorry

example (x : Type') (h : fintype x) : fintype.card x = 42 :=
begin
  unfreezingI { induction x using silly_type_ind },
  sorry
end

[Kyle Miller]

(the unfreezingI is to deal with the fintype hypothesis.)

[Sebastian Ullrich]

I don't recall the two ever being unified into a common concept anywhere in the codebase, so it looks like this need doesn't really come up that often.

[Joachim Breitner]

Ah, TIL. I thought I only need to unfreezeI stuff that is in [ … ]

[Joachim Breitner]

And neat trick with def Type' = Type. So if this trick works, it means that the implementation limitation is not fundamental, and could (if this becomes relevant in practice) be relaxed?

[Joachim Breitner]

Related to that: I assume there is no way to have conditional induction lemmas like the following in a way (with extra assumptions)

lemma silly_nat_ind (P : ℕ -> Prop) (a : ℕ) (h : a > 0) (h1 : ∀ a, 1=1 → P a) (h2 : ∀ a, 2=2 → P a) : P a :=
sorry

that still allow me to write induction n (rather than induction h)? (I believe Isabelle’s induction tactic could handle this).

Right now I (think I) have to make the P dependent on a > 0 and then a > 0 becomes the major premise. But this means a is not generalized, and _other_ assumptions about a are not threaded through the induction properly if I don’t manually revert them.

[Sebastian Ullrich]

Remind me again how the assumptions are discharged in Isabelle, from the proof context? And/or a dedicated case?

[Damiano Testa]

@Joachim Breitner in the Lean Zulip chat, 42 is 37.

[Sebastian Ullrich]

There is induction e using r, see docs#tactic.interactive.induction. Not sure off the top of my mind what it will do with your induction principle.

[Sebastian Ullrich]

My first docs link, yay...

[Joachim Breitner]

Here is an example of an induction lemma with assumptions from Isabelle:

lemma dec_induct [consumes 1, case_names base step]:
  "i ≤ j ⟹ P i ⟹ (⋀n. i ≤ n ⟹ n < j ⟹ P n ⟹ P (Suc n)) ⟹ P j"

I think the consumes 1 is a hint to the tactic that there is an assumption to discharge.

It then takes these from the “current facts”, which corresponds to the hyps of Lean’s goal state, I think:

lemma transitive_stepwise_le:
  assumes "m ≤ n" "⋀x. R x x" "⋀x y z. R x y ⟹ R y z ⟹ R x z" and "⋀n. R n (Suc n)"
  shows "R m n"
using ‹m ≤ n›
  by (induction rule: dec_induct) (use assms in blast)+

[Sebastian Ullrich]

Since the "current facts" are ordered (right?), I'd say the corresponding solution would be to make induction accept an arbitrary term after using:

induction using dec_induct ‹m ≤ n›

Currently it does not (and also expects at least one term after induction).

[Joachim Breitner]

With hidden arguments resolved automatically, like with apply? That might work, but I am not sure :)

[Joachim Breitner]

Damiano Testa said:

Joachim Breitner in the Lean Zulip chat, 42 is 37.

And :thumbs_up: is :octopus:, right? But why 37?

[Yaël Dillies]

Because Kevin

[Patrick Johnson]

And foo/bar is fish/banana (since recently).

[Johan Commelin]

Joachim Breitner said:

And :thumbs_up: is :octopus:, right? But why 37?

I think :octopus: plays the role of :tada:, the octopus is performing a victory dance :wink: But of course this is all a subjective matter of taste.

Kevin is the authority on why 37 is his favourite number. But src/algebraic_geometry/EllipticCurve.lean might contain a hint. And https://en.wikipedia.org/wiki/37_(number)#In_mathematics might contain a few more.

[Julian Berman]

There's also https://en.wikipedia.org/wiki/List_of_numbers_better_than_37

[Eric Wieser]

I'm late here, but regarding the h : a > 0 question, the solution is often to replace P a with P a h - you did this before in a previous thread / PR

[Kevin Buzzard]

Apparently if you ask people to choose a random number between 1 and 50, the chances they choose 37 are way way over 1/50. It's the most popular random number.

[Eric Wieser]

I think you might be experiencing selection bias :wink:

[Joachim Breitner]

I'm late here, but regarding the h : a > 0 question, the solution is often to replace P a with P a h - you did this before in a previous thread / PR

Right, and thanks for that, that’s what I am using now. But I'd say that’s a work around because

• it only works if that assumption is also to be passed to all the cases, which may not always be true
• I find it unnatural to say induction h when my conceptual model is that it’s an induction over , say n
• It doesn’t nicely and conveniently revert the actual object of interest, and doesn't automatically thread other assumptions about it through (as it does with induction n)
• Is annoying if the h is a class that otherwise could just stay be unnamed.

Of course ¾ of these are mostly subjective points, and so not a big deal

[Kyle Miller]

(This Dilbert comic that I totally didn't edit in any way agrees with Kevin:

dilbert-10-25-01.png

37 as a random number was actually new to me when I joined this Zulip. I'd heard about 17, but that was for 1-100, so maybe that's the difference.)

[Kyle Miller]

@Joachim Breitner Does the generalizing feature of induction help with reverting things for you? induction h generalizing n?

[Eric Wieser]

Note that when the goal really is of the form P a h (ie, depends on h), it's usually very annoying to use an induction principle of the form P a, and induction makes a mess.

[Joachim Breitner]

Kyle Miller said:

Joachim Breitner Does the generalizing feature of induction help with reverting things for you? induction h generalizing n?

No, that doesn't work; generalizing effectively just reverts n, and then his out of scope

[Eric Wieser]

Is n the a in h : 0 < a?

[Joachim Breitner]

Yes

[Eric Wieser]

It should generalize automatically - you might need to put a later in the argument list