induction using with a parametrized eliminator

Stream: lean4

[Joachim Breitner]

Consider a function like merge (as known from merge sort:

universe uu
variable {α : Type uu} (r : α → α → Prop) [DecidableRel r]
local infixl:50 " ≼ " => r
open List

def merge : List α × List α → List α
  | ([], l') => l'
  | (l, []) => l
  | (a :: l, b :: l') => if a ≼ b then a :: merge (l, b :: l') else b :: merge (a :: l, l')
  termination_by merge l => length l.1 + length l.2

When proving things about this, I might be inclined to define a custom induction principle, like the following, which will directly focus on the four cases and give me suitable induction hypotheses:

theorem merge.induct {α : Type uu} (r : α → α → Prop) [DecidableRel r] (motive : List α × List α → Prop)
  (case1 : ∀ (l' : List α), motive ([], l'))
  (case2 : ∀ (l : List α), ¬ (l = []) → motive (l, []))
  (case3 : ∀ (a : α) (l : List α) (b : α) (l' : List α), r a b → motive (l, b :: l') → motive (a :: l, b :: l'))
  (case4 : ∀ (a : α) (l : List α) (b : α) (l' : List α), ¬r a b → motive (a :: l, l') → motive (a :: l, b :: l'))
  (x : List α × List α) : motive x := sorry

But if I try to use it like this

theorem perm_length (l) : length (merge r l) = length l.1 + length l.2 := by
  induction l using merge.induct

I get 6 goals, including two unwanted ones for r and DecidbableRel r.

This is understandable, induction has no good way to knowing what r is. But how can I specify it? I can’t specify it as part of the “target”, e.g.

  induction r, l using merge.induct

but I also can’t give instantiations after using:

   induction l using merge.induct (r := r)

What I can do is artificially make the motive take the r as an argument:

theorem merge.induct2 {α : Type uu} (r : α → α → Prop) [DecidableRel r] (motive : (α → α → Prop) → List α × List α → Prop)
  (case1 : ∀ (l' : List α), motive r ([], l'))
  (case2 : ∀ (l : List α), ¬ (l = []) →  motive r (l, []))
  (case3 : ∀ (a : α) (l : List α) (b : α) (l' : List α), r a b → motive r (l, b :: l') → motive r (a :: l, b :: l'))
  (case4 : ∀ (a : α) (l : List α) (b : α) (l' : List α), ¬r a b → motive r (a :: l, l') → motive r (a :: l, b :: l'))
  (x : List α × List α) : motive r x := sorry

and now I can indicate the r as part of the target.

theorem perm_length (l) : length (merge r l) = length l.1 + length l.2 := by
  induction r, l using merge.induct2
  case case1 => simp [merge]
  case case2 => simp [merge]
  case case3 a l b l' hr IH =>
    simp [merge, hr, IH]
    simp_arith
  case case4 a l b l' hr IH =>
    simp [merge, hr, IH]
    simp_arith

Is that just a bad hack, or is that the way to go here?

And if it is a bad hack, what should be the proper solution? Make induction accept explicit parameters of the induction principle in the target list, or maybe support arguments after using?

[Eric Wieser]

Explicit parameters sound like the nice solution to me, though I'm surprised your hack works!

[Joachim Breitner]

Actually, it doesn't, I just noticed that I see red squiggly lines under perm_length saying

application type mismatch
  merge r
argument has type
  (a b : α) → Decidable (r✝ a b)
but function has type
  [inst : DecidableRel r] → List α × List α → List α

so I guess the induction tactic does something weird with the hack.

[Joachim Breitner]

Ok, so ignoring the hack:

One argument for supporting

  induction r, l using merge.induct

is that to the user, given

merge : {α } → (r : α → α → Prop) → [inst : DecidableRel r] → List α × List α → List α

it’s not immediately clear why the function's parameter r and l need be treated differently.

[Eric Wieser]

This works:

theorem merge.induct2 {α : Type uu} (r : α → α → Prop) (dr : DecidableRel r) (motive : (r : α → α → Prop) → (DecidableRel r) → List α × List α → Prop)
  (case1 : ∀ (l' : List α), motive r ‹_› ([], l'))
  (case2 : ∀ (l : List α), ¬ (l = []) →  motive r ‹_› (l, []))
  (case3 : ∀ (a : α) (l : List α) (b : α) (l' : List α), r a b → motive r ‹_› (l, b :: l') → motive r ‹_› (a :: l, b :: l'))
  (case4 : ∀ (a : α) (l : List α) (b : α) (l' : List α), ¬r a b → motive r ‹_› (a :: l, l') → motive r ‹_› (a :: l, b :: l'))
  (x : List α × List α)  : motive r ‹_› x := sorry


theorem perm_length (r : α → α → Prop) [DecidableRel r] (l) : length (merge r l) = length l.1 + length l.2 := by
  induction r, ‹DecidableRel r›, l using merge.induct2
  case case1 => simp [merge]
  case case2 => simp [merge]
  case case3 a l b l' hr IH =>
    simp [merge, hr, IH]
    simp_arith
  case case4 a l b l' hr IH =>
    simp [merge, hr, IH]
    simp_arith

[Eric Wieser]

There seem to be some rough edges here around binder types

[Eric Wieser]

I think your version fails because you generalized over r but not : DecidableRel r

[Joachim Breitner]

Thanks! Doesn’t make make me more confident that this is direction is a good workaround, compared to explicit support of some form.

[Eric Wieser]

Edited one more time

[Joachim Breitner]

I tried a variant of your working solution, where the motive takes implicit arguments:

theorem merge.induct2 {α : Type uu} (r : α → α → Prop) (dr : DecidableRel r) (motive : (r : α → α → Prop) → [DecidableRel r] → List α × List α → Prop)
  (case1 : ∀ (l' : List α), motive r ([], l'))
  (case2 : ∀ (l : List α), ¬ (l = []) →  motive r (l, []))
  (case3 : ∀ (a : α) (l : List α) (b : α) (l' : List α), r a b → motive r (l, b :: l') → motive r (a :: l, b :: l'))
  (case4 : ∀ (a : α) (l : List α) (b : α) (l' : List α), ¬r a b → motive r (a :: l, l') → motive r (a :: l, b :: l'))
  (x : List α × List α)  : motive r x := sorry

but both

induction r, ‹_›, l using merge.induct2

and

induction r, l using merge.induct2

say

unexpected eliminator resulting type
  motive r x

But maybe induction can be taught about implicit parameters of the motive?

It still feels wrong to put fixed parameters into the motive. Wouldn’t this also make induction needlessly generalize over these parameters?

[Joachim Breitner]

Let’s see what Isabelle does:

theory Scratch imports Main begin

context
fixes r :: "'a ⇒ 'a ⇒ bool"
begin
fun merge :: "'a list ⇒ 'a list ⇒ 'a list" where
  "merge [] l' = l'"
| "merge l' [] = l'"
| "merge (a # l) (b # l') =
    (if r a  b then a # merge l (b # l') else b # merge (a # l)  l')"
end

thm merge.induct
(*
(⋀l'. ?P [] l') ⟹
(⋀v va. ?P (v # va) []) ⟹
(⋀a l b l'.
    (?r a b ⟹ ?P l (b # l')) ⟹
    (¬ ?r a b ⟹ ?P (a # l) l') ⟹ ?P (a # l) (b # l')) ⟹
?P ?a0.0 ?a1.0
*)

theorem  "length (merge r l1 l2) = length l1 + length l2"
by(induction l1 l2 rule: merge.induct[where r = r]) auto

If I pass the r parameter explicitly (but unchanged) through merge, it is added to the motive. If I make sure it is fixed (like in Isabelle) using the context construct, it becomes universally bound in the induction principle, and is not part of the target. I can however instantiate it with [where r = r].

So supporting

induction l using merge.induct (r := r)

seems useful in any case.

What I am unsure still is whether Lean, when autogenerating the inductive principle, should keep fixed parameters in the motive, or not. The former leads to nicer proofs (no need to generalize a fixed paramter), the latter is more predictable.

[Joachim Breitner]

How about existing induction theorems with extra parameters, like

Nat.decreasingInduction.{u_1} {m n : ℕ} {P : ℕ → Sort u_1} (h : (n : ℕ) → P (n + 1) → P n) (mn : m ≤ n) (hP : P n) : P m

can we use them with the induction tactic somehow? I couldn’t get it to work:

import Mathlib.Data.Nat.Basic

#check Nat.decreasingInduction

example (n : Nat) (h : n ≤ 10): n = n := by
  induction n using Nat.decreasingInduction

With my proposed syntax,

example (n : Nat) (h : n ≤ 10): n = n := by
  induction n using Nat.decreasingInduction (mn := h)

should ideally work. (Maybe only if the mn parameter is moved before h?)

[Sebastian Ullrich]

I wonder if at some point it makes more sense to just do something uniform like induction using <term> where all remaining arguments are assumed to be minor premises. But yes, that would also require some parameter shuffling.

[Joachim Breitner]

Yeah, I’m actually reading through the code how much the induction needs to know from the actual decl, or whether it just cares about the thing’s type and a term there would be fine.

If we say <term>, we still would want to interpret using foo.induct (without parameters) as using @foo.induct, right, and not instantiate implicit parameters during elaboration, right? I assume there is precedence for that (maybe the arguments of simp)?

[Sebastian Ullrich]

Yes, we sometimes do ident <|> term for that. I can't say whether it's necessary for induction.

[Sebastian Ullrich]

Or rather, just specializing terms that turn out to be idents

[Joachim Breitner]

It does look at an attribute recursorAttribute for “user defined recursor, numerical parameter specifies position of the major premise”…

[Sebastian Ullrich]

Ah but my syntax does not distinguish a major premise :)

[Joachim Breitner]

Phew, there is quite a big surface area here:

structure RecursorInfo where
  recursorName  : Name
  typeName      : Name
  univLevelPos  : List RecursorUnivLevelPos
  depElim       : Bool
  recursive     : Bool
  numArgs       : Nat -- Total number of arguments
  majorPos      : Nat
  paramsPos     : List (Option Nat) -- Position of the recursor parameters in the major premise, instance implicit arguments are `none`
  indicesPos    : List Nat -- Position of the recursor indices in the major premise
  produceMotive : List Bool -- If the i-th element is true then i-th minor premise produces the motive

But mkRecursorInfoAux seems to infer that from the type. So it might work.

But

throwError"invalid user defined recursor '{declName}', type of the major premise does not contain the recursor parameter

indicates that that concept of recursor does not support parameters not appearing in the major premise.

And this custom attribute to set the major premise is not used or tested in core and std, and has only two uses in mathlib :cold_sweat:

Ah, RecursorInfo was the wrong tree to bark up. It seems that getElimInfo is the function used with induction … using, and while it takes a declName, it only looks at its type. So using using <term> might actually work nicely.

[Joachim Breitner]

While this might work fine with parameters that don’t affect the resulting type, int he case of decreasingInduction, if we instantiate the mn parameter, like this

def Nat.decreasingInduction2.{u_1} {m n : ℕ} (mn : m ≤ n) {P : ℕ → Sort u_1} (hP : P n)  (h : (n : ℕ) → P (n + 1) → P n) : P m :=
  @Nat.decreasingInduction m n P h mn hP

example (n : Nat) (h : n ≤ 10): n = n := by
  induction n using Nat.decreasingInduction2 (mn := h)

then the target gets instantiated (is no longer the motive applied to other paramters of the eliminator), confusing the getElemInfo code

Crudely checked using this code

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Common

#check Nat.decreasingInduction

#eval Lean.Meta.getElimInfo ``Nat.decreasingInduction2

def Nat.decreasingInduction2.{u_1} {m n : ℕ} (mn : m ≤ n) {P : ℕ → Sort u_1} (hP : P n)  (h : (n : ℕ) → P (n + 1) → P n) : P m :=
  @Nat.decreasingInduction m n P h mn hP

example (n : Nat) (h : n ≤ 10): n = n := by
  induction n using Nat.decreasingInduction2 (mn := h)

open Lean Meta
def getElimInfoType (declType : Expr) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do
  forallTelescopeReducing declType fun xs type => do
    let motive  := type.getAppFn
    let targets := type.getAppArgs
    unless motive.isFVar && targets.all (·.isFVar) && targets.size > 0 do
      throwError "unexpected eliminator resulting type{indentExpr type}"
    let motiveType ← inferType motive
    forallTelescopeReducing motiveType fun motiveArgs motiveResultType => do
      unless motiveArgs.size == targets.size do
        throwError "unexpected number of arguments at motive type{indentExpr motiveType}"
      unless motiveResultType.isSort do
        throwError "motive result type must be a sort{indentExpr motiveType}"
    let some motivePos ← pure (xs.indexOf? motive) |
      throwError "unexpected eliminator type{indentExpr declType}"
    let targetsPos ← targets.mapM fun target => do
      match xs.indexOf? target with
      | none => throwError "unexpected eliminator type{indentExpr declType}"
      | some targetPos => pure targetPos.val
    let mut altsInfo := #[]
    let env ← getEnv
    for i in [:xs.size] do
      let x := xs[i]!
      if x != motive && !targets.contains x then
        let xDecl ← x.fvarId!.getDecl
        if xDecl.binderInfo.isExplicit then
          let numFields ← forallTelescopeReducing xDecl.type fun args _ => pure args.size
          let name := xDecl.userName
          let declName? := do
            let base ← baseDeclName?
            let altDeclName := base ++ name
            if env.contains altDeclName then some altDeclName else none
          altsInfo := altsInfo.push { name, declName?, numFields }
    pure { name := `foo, motivePos, targetsPos, altsInfo }

def getElimInfo (declName : Name) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do
  let declInfo ← getConstInfo declName
  getElimInfoType declInfo.type baseDeclName?

example (n : Nat) (h : n ≤ 10): n = n := by
  #eval do
    let s  ← `(@Nat.decreasingInduction2 (mn:=h))
    let e ← (Lean.Elab.Term.elabTerm s none).run' {}
    getElimInfoType (← inferType e)

So while it might help in the case of merge.induct above, it wouldn’t in the case of decreasingInduction.

[Sebastian Ullrich]

It's not clear to me whether it is even useful to talk about a major premise and motive for this induction principle. But again I don't know the induction code very well, or how it could be generalized.

[Joachim Breitner]

Indeed, if “major premise” (the m, right) is something we expect to be able to generalize, then providing m ≤ n may prevent that generalization. Maybe the major premise here is actually m≤n?
It may make sense to focus on the simpler case of parameters that don’t affect the targets, where the generalization to terms rather than identifiers might just work fine – if the term is elaborated carefully, i.e. like @merge.induct (r := …), not like @merge.induct (r := …).

[Joachim Breitner]

I keep going back and forth. Maybe it is nicer after all to treat the r in merge.induct in the first post as a “fixed target”, so

• require it to be passed as a target it induction r, l using merge.induct, but
• do not generalize it (as it is fixed throughout the induction)
  This would require less syntax changes, is a bit more natural to a user who doesn’t spot the difference in how r and l is used in the recursion of merge. And (assuming I can recognize them reliably in getElimInfo the implementation wouldn’t be not too bad).

Maybe the specification should be “a fixed parameter is one that is not implicit and bound before the motive”.

[Jannis Limperg]

I'm always a bit skeptical about changing the behaviour of a tactic based on implicitness. Imo, changing the implicitness of an argument should only lead to the expected breakage, i.e. having to provide or omit the argument at use sites.

[Joachim Breitner]

But I think my proposal adheres to that expectation, if I understand you correctly: If the r argument of merge.induct is implicit, you don’t have to mention it. If it is explicit, you have to mention it in the induction … using list of “targets”.

Or put differently: The targets in the induction … using syntax are (already) a subset of the induction principle’s parameters, while other parameters are set up as as goals (the minor premises), calculated from the goal state (the major premise) or inferred (implicit arguments). My proposal extend that set of “explicit arguments”.

[Joachim Breitner]

I’m recording/continuing this discussion on an RFC: https://github.com/leanprover/lean4/issues/3170

[Jannis Limperg]

I would rather have implicitness affect the elaboration of applications and nothing else. Otherwise the simple explanation "an implicit argument is inferred in applications" becomes "... and also a certain obscure form of induction may break".

Of course, I realise that my position is somewhat extreme, and maybe your design is, in fact, optimal in practice. I also agree that this proposed effect of implicitness is at least somewhat analogous to the standard effect.

[Joachim Breitner]

Well, induction is a form of application, and it already treats explicit and implicit parameters differently: Explicit ones (that aren’t the motive or a target) become alternative, implicit ones not (I believe). But I do see your point.

[Mario Carneiro]

I think we should not confuse targets with parameters. Targets are the major premises and the indices of the inductive, parameters are things that do not depend on the major premise or the indices and on which everything else can depend

[Mario Carneiro]

m <= n is not a parameter if m is the induction target

[Joachim Breitner]

Agreed. So, what is m <= n, and how should induction treat it?

I guess n is a proper parameter, and ideally instantateable (maybe using (n := …)), and then it's reasonable to treat nm like the induction cases.

[Kyle Miller]

Joachim Breitner said:

and not instantiate implicit parameters during elaboration, right?

The docs#Lean.Elab.Tactic.elabTermForApply elaboration function is how some tactics handle elaborating identifiers f as @f

[Joachim Breitner]

Thanks! That looks useful, I’ll play around with it.
I also found this idiom in the simp code of elaborating first, and then abstracting over mvars again:
https://github.com/leanprover/lean4/blob/b614ff1d12bc38f39077f9ce9f2d48b42c003ad0/src/Lean/Elab/Tactic/Simp.lean#L118-L129
(but it may be that simp [foo] where foo is really just an ident has been handled before separately)

[Kyle Miller]

Yeah, simp [foo] and simp [(foo)] behave differently -- I believe it does something like elabTermForApply while processing the list of simp lemmas, but I'm not very confident about that. The second abstracts over mvars (and mathlib is taking advantage of this to work around how instances are synthesized in the first case...)

[Joachim Breitner]

Hyrum's law is strong with us

[Kyle Miller]

Reading quickly, I think here's where identifiers are handled differently: https://github.com/leanprover/lean4/blob/b614ff1d12bc38f39077f9ce9f2d48b42c003ad0/src/Lean/Elab/Tactic/Simp.lean#L202

[Joachim Breitner]

Playing around with this, but I think it’s not quite what I want. I'd like to elaborate term in a mode where, given `ident : {motive : … } → { motive2 : … } … ,

• ident is elaborated as @ident and not @ident ?mvar
• ident (motive2 := m2) is elaborated as fun m1 => @ident m1 m2, with type {motive : … } → … and not @ident ?mvar m2
• ident a b is elaborated normally, even if ident is marked as “elab_as_elim”
  Not sure if that’s a reasonable thing to want :-)

Lean.Elab.Tactic.addSimpTheorem almost does that, but it forgets the names, for examples.

Actually, Lean.Elab.Tactic.addSimpTheorem seems to kinda work. Pretty big hammer, but at least something (https://github.com/leanprover/lean4/pull/3188). Doesn’t address the third point above.

Maybe I should not use normal term elaboration at all, and instead parse

foo (arg := e)…

explicitly, supporting only (arg := …) syntax, and then doing the right thing behind the scenes. Probably much easier to control what’s happening this way, and also produce good error messages (e.g. when the user wants to set the motive or the target, which wouldn’t work.)