Tutorial for custom recursors/eliminators/inductors

Stream: new members

[Alex Mobius]

I've came across several of these things, e.g.

• ReflTransGen.head_induction_on is a custom reduction principle (which I understand somewhat)
• Batteries.Vector.elimAsArray is a custom eliminator, which I'm not sure how to apply. (again using induction using?)
• Docs also mention "cases eliminators" and "induction eliminators", seem to be a way to override the default eliminators for types, am I correct?
  If there's documentation on this, I'd be much pleased to be informed of it.

[Kyle Miller]

There are three kinds of things you can define:

• If you give a declaration @[cases_eliminator], then that changes the default eliminator to use for the cases tactic. This way you don't have to write cases val using customCasesEliminator. A cases eliminator should not introduce induction hypotheses. That means the motive argument shouldn't appear as a hypothesis to any of the premises. (The default cases eliminator is the MyType.casesOn function.)

• If you give a declaration @[induction_eliminator], then that changes the default eliminator to use for the induction tactic. An induction eliminator can have induction hypotheses. (The default induction eliminator is MyType.recOn.)

• If you give a declaration the @[elab_as_elim] attribute, then this changes how it elaborates, using a special procedure that makes use of the expected type to solve for a motive argument. The definition of an "eliminator" here is fairly broad, but basically, if you have a theorem myInduction {motive : MyType -> Prop} (hyp1 : hypothesis) (hyp2 : hypothesis) (x : MyType) : motive x, then if you use it with refine like refine myInduction ?_ ?_ val, it'll generalize val out of the goal automatically and create the correct motive, leaving you with two goals. A declaration given this attribute must have an expected type available, otherwise during elaboration you get an error message.

The third one does not affect induction or cases. If you want to use *_eliminators with refine, you can add elab_as_elim. Often you can use apply without needing to add elab_as_elim since it has some capacity for the higher-order unification that elab_as_elim is performing.

[Kyle Miller]

(cases_eliminator and induction_eliminator are why it is that when you do cases/induction on Nat that everything is in terms of 0 and n + 1 rather than Nat.zero and Nat.succ n.)

[Alex Mobius]

Thanks a lot.

• Judging by https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/App.html#Lean.Elab.Term.elabAsElim, the first two cases also require that the return type is a motive applied to other parameters - I'm guessing it makes for a simple unification?
• Can you also clarify what exactly is meant by "must have an expected type available" in the third case? That's the error I got hen trying to use Vector.elimAsArraywith apply. refine also doesn't seem to work:

theorem vec_set_local (v: Vector α n): ∀ i j, i = j \/ (v.set i t)[j] = v[j] := by
  intro i j
  refine Vector.elimAsArray ?x v -- failed to elaborate eliminator, motive is not type correct: fun x y => ...

• If I understand correctly, the names of the parameters become my subgoal tags, and if they have a shape of forall/arrow, then that becomes my case hypotheses. Does match also use cases eliminator (TPIL mentions match procedures using casesOn)? What happens with explicit arguments that aren't motive applications? It seems that one of them can match with p at induction p using.

[Kyle Miller]

Alex Mobius said:

• the first two cases also require that the return type is a motive applied to other parameters - I'm guessing it makes for a simple unification?

Yeah, all three cases require that the return type be an applied motive. The induction_eliminator and cases_eliminator need the arguments to be other parameters (these are "targets", the things that are arguments in the induction tactic, like induction x, y, z — this is how the targets are identified). You may need to way for a future release of Lean, but elab_as_elim doesn't require that the arguments be parameters, since it has no concept of targets.

[Kyle Miller]

Alex Mobius said:

• Can you also clarify what exactly is meant by "must have an expected type available" in the third case?

The elaboration procedure is at a high level a function Syntax -> (expectedType? : Option Expr) -> TermElabM Expr. There can be an expected type that comes from context, and it is a hint for what type would be great to get back — though elaboration doesn't need to respect the expected type. For example, the (... : Ty) notation sets the expected type to Ty, and then inserts a coercion if the type doesn't match.

The apply tactic elaborates its argument without an expected type, and the refine tactic elaborates using the goal as the expected type.

[Kyle Miller]

Alex Mobius said:

failed to elaborate eliminator, motive is not type correct: fun x y => ...

If this happens, it means that generalizing failed. It's similar to the "motive not type correct" error in rw. It looks like if you revert i and j first it should work, since these depend on n. Notice that n is one of the motive arguments — that means it's very likely to get a type incorrect motive if you let anything depend on n in the goal expression.

[Kyle Miller]

Yeah, this works:

theorem vec_set_local (v: Vector α n): ∀ i j, i = j \/ (v.set i t)[j] = v[j] := by
  refine Vector.elimAsArray ?x v
  intro a i j
  sorry

[Kyle Miller]

Alex Mobius said:

• If I understand correctly, the names of the parameters become my subgoal tags, and if they have a shape of forall/arrow, then that becomes my case hypotheses. Does match also use cases eliminator (TPIL mentions match procedures using casesOn)?

Yes, names of hypotheses become subgoal tags. These are the tags you can use in induction ... with | tag1 ... => ... | ... notation too.

Regarding match, no, you can't override anything about match. The best you can do is create new patterns with @[pattern]. All @[pattern] does is let match unfold it.

What happens with explicit arguments that aren't motive applications? It seems that one of them can match with p at induction p using.

These are "major premises". They're the parameters that are supposed to appear as arguments to the motive in the whole eliminator's return type. (See the induction x, y, z message a few before this one.)

[Alex Mobius]

Yeah, all three cases require that the return type be an applied motive. The induction_eliminator and cases_eliminator need the arguments to be other parameters (these are "targets", the things that are arguments in the induction tactic, like induction x, y, z — this is how the targets are identified). You may need to way for a future release of Lean, but elab_as_elim doesn't require that the arguments be parameters, since it has no concept of targets.
so, to clarify, induction x using uses induction_eliminator rules too.
If this happens, it means that generalizing failed.
Curiously, induction does just fine:

theorem vec_set_local (v: Vector α n): ∀ i j, i = j \/ (v.set i t)[j] = v[j] := by
  intro i j
  induction v using Vector.elimAsArray
  case mk a => sorry

i j get rewritten to type Fin .(toArray).size, but n doesn't. It seems that it's able to treat N as an output parameter there and infer its value from rfl. (Which is interesting, because n should indeed be a "major parameter" here?)
I'm guessing it's because induction can generalize/specialize hypotheses, and refine only targets and motive?
generalize n=m at * fails with a cryptic error failed to generalize vec_set_local, which is an internal definition; guessig that has to do with lacking an explicit forall n.

[Kyle Miller]

Yes, induction auto-generalizes variables that appear in the goal.

[Alex Mobius]

I see; is that an effect reproducible by other means?

[Kyle Miller]

Alex Mobius said:

generalize n=m at * fails with a cryptic error failed to generalize vec_set_local, which is an internal definition

That one seems like it might be a bug in generalize — there are some auxiliary local definitions that tactics are not supposed to see, but it's easy to get this wrong.

[Kyle Miller]

Alex Mobius said:

I see; is that an effect reproducible by other means?

Sometimes I wish there were a revert tactic that just reverted the variables appearing in the goal, but there isn't one as far as I know.

[Alex Mobius]

I think generalize here is referring to the fact that if I were use a name vec_set_local in this context, it would refer to vec_set_local specialized to specific n and v, since they're to the left of colon. But yeah, it either shouldn't try, or should succeed.

[Kyle Miller]

Yes, vec_set_local is an auxiliary local definition that's in the local context but hidden. It's used for elaborating recursive declarations, and tactics are supposed to pay no attention to it.