Custom induction for def

Stream: general

[Patrick Johnson]

In Isabelle/HOL, for each definition there is an automatically generated induction principle. For example, if we define predicate even recursively such that even 0 is true, even 1 is false and even (n+2) is even n for any natural number n, then we get nat.two_step_induction for free. Is there an equivalent in Lean?

Here is a simple example:

def P : ℕ → Prop
| 123 := true
| 45 := true
| _ := false

example {n : ℕ} (h : P n) : n = 123 ∨ n = 45 :=
begin
  sorry
end

It would be nice if cases h could split into two goals, one with n replaced with 123 and the other with n replaced with 45. Is there such a tactic?

[Reid Barton]

If you defined P as an inductive proposition then this would be the induction principle

[Yaël Dillies]

Probably you rather want

inductive P : ℕ → Prop
| intro123 : P 123
| intro45 : P 45

Then cases h will do what you want.

[Patrick Johnson]

Sure, my example is bad. I am talking about re-using the recursion principle generated by the equation compiler, rather than proving it manually (like the even/odd example).

[Patrick Johnson]

So that we can use that principle when proving facts about the function.

[Reid Barton]

I don't understand the even/odd example because docs#nat.two_step_induction does not mention even or odd

[Reid Barton]

But I guess the answer is that the equation compiler doesn't generate a recursion principle (for what?). It does generate equational lemmas.

[Reid Barton]

In Lean you can define an inductive family of propositions, in which case you get an induction principle that tells you all the ways that the proposition can be true. Or you can define a family of proposiitons by recursion on something else (like a nat), which tells you how to "compute" the proposition for a specific natural number (by doing recursion on that number). They are different tools and in general it might not be straightforward to convert from one presentation to the other in an interesting way.

[Reid Barton]

For example if you define even by recursion in Lean then it is basically the same as writing def even (n : nat) : Prop := nat.rec_on n true not. There are no constants or axioms being added, and you could replace a usage of even by this definition. I think it works quite differently in Isabelle/HOL.

[Patrick Johnson]

I am talking about this: suppose we define two functions f and g

open nat

def f : ℕ → ℕ
| 0 := 0
| 1 := 0
| 2 := 0
| (succ (succ (succ n))) := f n

def g {α : Type} : list α → list α → list α
| [] ys := ys
| (x::xs) ys := have ys.length + xs.length < (x::xs).length + ys.length := sorry,
  x :: g ys xs
using_well_founded { dec_tac := `[sorry] }

The equation compiler uses nat.rec and list.rec to build the functions. It would be nice if we could obtain the direct induction principle for the definition, rather than making a separate definition for it. For example, functions f and g would automatically generate

def f_rec {motive : ℕ → Sort*}
(f₀ : motive 0)
(f₁ : motive 1)
(f₂ : motive 2)
(fn : Π (n : ℕ), motive n → motive (succ (succ (succ n)))) :
Π (n : ℕ), motive n
| 0 := f₀
| 1 := f₁
| 2 := f₂
| (succ (succ (succ n))) := fn n (f_rec n)

def g_rec {α : Type} {motive : list α → list α → Sort*}
(g_nil : Π (ys : list α), motive [] ys)
(g_cons : Π (x : α) (xs ys : list α), motive ys xs → motive (x::xs) ys) :
Π (xs ys : list α), motive xs ys
| [] ys := g_nil ys
| (x::xs) ys := have ys.length + xs.length < (x::xs).length + ys.length := sorry,
  g_cons x xs ys (g_rec ys xs)
using_well_founded { dec_tac := `[sorry] }

[Reid Barton]

OK, so basically the most general function with the same recursive structure as the original one. For example you can recover f from f_rec by f = f_rec 0 0 0 (\lam n x, x).

[Patrick Johnson]

If you defined P as an inductive proposition then this would be the induction principle.

We can't always do that. For example, this works:

def P : ℕ → Prop
| 0 := true
| (nat.succ n) := ¬P n

but this does not:

inductive P : ℕ → Prop
| zero : P 0
| succ {n : ℕ} : ¬P n → P n.succ

[Reid Barton]

Right, that's why the original question was so confusing :upside_down:

[Reid Barton]

What you want to do makes sense, for example (for some reason) you defined f as above, and now you want to prove f n = 0 for all n. I think the usual wisdom is something like:

0. Avoid fancy recursive structures in the first place (not that common in math anyways, maybe more common in program verification)
1. If you want to prove something about f (defined using the equation compiler) then you should use the equation compiler for the proof also. (Rather than your f_rec which would only be palatable if applied in tactic mode.)
2. Try to minimize the amount to which you need to do 1, e.g. by completely characterizing the behavior of f by a single lemma, so you don't need to reason by recursion about f again and again.

[Reid Barton]

(For example even is not actually defined by recursion in mathlib, it wouldn't occur to most mathematicians to define it that way, and I would go so far to say it would be a bad way to define it.)

[Kyle Miller]

@Reid Barton I remember someone asking about something like this last year, and the impression I got was that this is equivalent to having the equation compiler also define an inductive type that gives the underlying relation for the the function along with defining some lemma proving that the the relation is functional and is equivalent to the defined function. Then you can do induction on the function's recursion by doing induction on that relation.

I saw in the Lean 4 changelog that it's able to do induction on a recursion now, but I haven't looked into how you do that yet.

[Kyle Miller]

I think we could define such a type using a user attribute in Lean 3, where there'd be a constructor per equation lemma.