Default arguments for induction/recursion principles

Stream: mathlib4

[Edward van de Meent]

At the suggestion of @Christian Merten , i've been writing an induction-like tactic which allows you to specify default discharger tactics, which get called when using this new tactic.

The following code should give a general flavour of what this in the future might look like:

@[auto_induction (case1 := by simp) (case2 := by intros; simp_all) (case3 := by your_discharger)]
def Foo.induction {motive : Foo → Sort u} (case1 : motive ()) (case2 :∀ x, motive x →  motive (id x)) (case3 :∀ x y, motive x → motive y) (x:Foo) : motive x := sorry

example : ∀ x:Foo, x = x := by
  intro x
  autoinduction x

Christian has told me he thinks that this is something that mathlib could use, but i have no good view of typical uses of induction to be able to make that judgement, so i'd like to ask the opinion of other contributors and maintainers

[Edward van de Meent]

the plan is to allow all induction tactic syntax except for using

[Edward van de Meent]

in particular, this includes using with | case1 => some_other_tactics to override the default

[Edward van de Meent]

additionally, if the default closure tactic fails, the goal is created anyway or the user is asked to provide the relevant with branch anyway, depending on if with syntax is being used

[Yaël Dillies]

How is that different from

def Foo.induction {motive : Foo → Sort u}
    (case1 : motive () := by simp)
    (case2 : ∀ x, motive x → motive (id x) := by intros; simp_all)
    (case3 : ∀ x y, motive x → motive y := by your_discharger)
    (x : Foo) : motive x := sorry

[Edward van de Meent]

i imagine you don't want these defaults for creating data

[Christian Merten]

(For reference, typical applications I had in mind are induction principles like docs#MvPolynomial.induction_on or docs#TensorProduct.induction_on)

[Yaël Dillies]

Then maybe you should have Foo.rec and Foo.induction?

[Yaël Dillies]

Christian Merten said:

(For reference, typical applications I had in mind are induction principles like docs#MvPolynomial.induction_on or docs#TensorProduct.induction_on)

Yes so indeed those are Prop-valued already

[Edward van de Meent]

Yaël Dillies said:

How is that different from

def Foo.induction {motive : Foo → Sort u}
    (case1 : motive () := by simp)
    (case2 : ∀ x, motive x → motive (id x) := by intros; simp_all)
    (case3 : ∀ x y, motive x → motive y := by your_discharger)
    (x : Foo) : motive x := sorry

also, i don't know how that interacts with using the induction tactic

[Yaël Dillies]

Any chance you can turn your new tactic into an improvement to induction? :smile:

[Edward van de Meent]

that would be a PR to core, which is scary

[Edward van de Meent]

additionally, i imagine that such a PR would be more readily accepted if there were concensus that this indeed would be a useful feature to have, and a proof of concept that actually demonstrates it

[Yaël Dillies]

I think it is useful, yes. I simply do not want users having to learn yet another syntax when it could nicely be done with existing concepts

[Christian Merten]

Yaël Dillies said:

I think it is useful, yes. I simply do not want users having to learn yet another syntax when it could nicely be done with existing concepts

We could maybe override the syntax for induction in mathlib to accept an additional argument that replaces it by autoinduction so something like induction +auto .... I believe you want to be able to control when the automatic mode is used.

[Edward van de Meent]

i imagine that indeed might be useful when discharger tactics take a long time to fail

[Edward van de Meent]

although i don't know that we can override the induction tactic syntax

[Eric Wieser]

Is there a tactic which means "populate autoparams"?

[Edward van de Meent]

indeed, you'd need something like that when there are default arguments to your induction principle.
for example:

import Mathlib.Data.Vector.MapLemmas

set_option autoImplicit false
open List


@[induction_eliminator]
def principle {α : Type*} {β : Type*} {motive : {n : ℕ} → List.Vector α n → List.Vector β n → Sort*}
    {n : ℕ} (v : List.Vector α n) (w : List.Vector β n)
    (nil : motive Vector.nil Vector.nil := by simp_all)
    (snoc : {n : ℕ} → (xs : List.Vector α n) → (ys : List.Vector β n) → (x : α) → (y : β) → motive xs ys → motive (xs.snoc x) (ys.snoc y) := by simp_all) : motive v w :=
  Vector.revInductionOn₂ v w nil snoc


variable {α β γ ζ σ σ₁ σ₂ φ : Type*} {n : ℕ} {s : σ} {s₁ : σ₁} {s₂ : σ₂}
namespace List
namespace Vector

variable (xs : Vector α n) (ys : Vector β n)

lemma map₂_map_left' (f₁ : γ → β → ζ) (f₂ : α → γ) :
    map₂ f₁ (map f₂ xs) ys = map₂ (fun x y => f₁ (f₂ x) y) xs ys := by
  induction xs, ys using principle
  · -- ⊢ autoParam (map₂ f₁ (map f₂ nil) nil = map₂ (fun x y => f₁ (f₂ x) y) nil nil) _auto✝
    sorry
  · /- ⊢ autoParam (∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
          map₂ f₁ (map f₂ xs) ys = map₂ (fun x y => f₁ (f₂ x) y) xs ys →
            map₂ f₁ (map f₂ (xs.snoc x)) (ys.snoc y) = map₂ (fun x y => f₁ (f₂ x) y) (xs.snoc x) (ys.snoc y)) _auto✝
    -/
    sorry

[Edward van de Meent]

so evidently induction doesn't look at it.

[Kyle Miller]

What are some concrete use cases for induction principles where there's a universally good choice for default dischargers for particular minor hypotheses? I'm a bit dubious, given that induction principles can be used for any goal whatsoever that happens to contain the target.

[Kyle Miller]

Also, are you aware that there is a way to run a discharger on every goal with the induction syntax?

induction n with try (simp; done)
| succ n' ih => ...

In individual files, one could create a local macro for the discharger that works locally, and write induction n with myDischarger | ...

[Edward van de Meent]

Kyle Miller said:

What are some concrete use cases for induction principles where there's a universally good choice for default dischargers for particular minor hypotheses?

like i said,

Edward van de Meent said:

but i have no good view of typical uses of induction to be able to make that judgement, so i'd like to ask the opinion of other contributors and maintainers

[Edward van de Meent]

i don't know

[Edward van de Meent]

i did not come up with the idea, i basically only got nerd-sniped into writing it without knowing if there's actually a place in mathlib for this, or if it actually is only occasionally useful and the maintainence cost outweigh the small decrease in lines written

[Jireh Loreaux]

Kyle Miller said:

I'm a bit dubious, given that induction principles can be used for any goal whatsoever that happens to contain the target.

:this: I agree with this.

[Kyle Miller]

Edward van de Meent said:

i don't know

That's fine, and you don't have to be the one to answer the question (and I didn't mean for it to seem like I was grilling you in particular). These are just questions that need to be answered for it to move from experimentation/hacking to practice.