what’s the rule for generating the rec function of an ind...

Stream: new members

[Shanghe Chen]

Hi I am a layman in type theory but I am curious in how is the rec function generated given a inductive families defined with the form

inductive foo : ... → Sort u where
  | constructor₁ : ... → foo ...
  | constructor₂ : ... → foo ...
  ...
  | constructorₙ : ... → foo ...

mentioned in https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html

[Shanghe Chen]

For example why Eq.rec has a signature like @Eq.rec : {α : Sort u} → {a : α} → {motive : (x : α) → a = x → Sort v} → motive a rfl → {b : α} → (h : a = b) → motive b h)?

[Shanghe Chen]

ForNat.rec it seems intuitive since it restates the inductive principle. But Eq.rec seems not containing such intuition

[Kevin Cheung]

I have the same question. I hope someone could shed some light.

[Shanghe Chen]

I am still not getting the exact rule or impl but now I got a feeling that rec is like "proof by cases" intuitively. Each constructor in the def of inductive foo contributes "a case". Btw I found https://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf quite helpful

[Giacomo Stevanato]

I'm not a type theory expert but AFAIK the intuition is that the constructors are the only way to construct an element of that type*, and thus to show some fact about a value it sufficies to show that it holds for every way could have possibly been constructed with. For Eq the only way to construct it is with refl a, getting a Eq a a, for some a given as argument to refl, hence the requirement for motive a rfl (which can also be written as motive a (refl a)).

You can also find a nice explanation of this in the Homotopy Type Theory book, at page 51.

*technically this is not completly true as noncomputable functions can create instances of types without explicitly using one of the constructors, but they still need to be consistent with this.

---

That said, the recursor produced by Lean is the one I would expect for an equality type defined with path induction i.e. generic over the left side of the equality but indexed over the right side, but Lean's equality type is indexed over both, so I would expect a recursor with the following signature (notice how motive takes two a parameters, one for each index).

Eq.rec.{u, u_1} :
  {α : Sort u_1}
  → {motive : (a_0 a_1 : α) → a_0 = a_1 → Sort u}
  → ((a : α) → motive a a (Eq.refl a))
  → {a_0 a_1 : α} → (t : a_0 = a_1) → motive a_0 a_1 t

For completeness, an equality type defined with path induction would be the following:

inductive Eq {α : Sort u} (a : α) : α → Prop where
  | refl : Eq a a

I guess Lean is doing some transformation due to seeing that the first index is not really constrained?

[Florent Schaffhauser]

If T is an inductive type, the associated function T.rec can be used to construct dependent functions out of T. This means that, given a type family F : T -> Type, we can construct a dependent function f : (t : T) -> F t by applying T.rec (motive := fun t => F t). As a special case, if F is the constant family F t = X, we can apply T.rec (motive := fun _ => X) to construct functions from T to X.

Since T is inductively defined, we can construct a function out of T by pattern-matching, meaning by case analysis on the constructors of T. For instance, if c (p1 : P1) ... (pn : Pn) (t1 : T) ... (tm : T) : T is a term of type T (the function c here is a constructor with n parameters of type P1 ... Pn and m parameters ti : T), then in order to define f t for t = c p1 ... pn t1 ... tm it suffices to have a term h (p1 : P1) ... (pn : Pn) (t1 : T) ... (tm : T) (f t1 : F t1) ... (f tm : F tm) of type F t. By definition, that long term h ... will be f t in our definition of f by pattern-matching.

In this example, the auxiliary function h is a dependent function of type signature (p1 : P1) -> ... -> (pn : Pn) -> (t1 : T) -> ... -> (tm : T) -> (P t1) -> ... -> (P tm) -> P (c p1 ... pn f1 ... fm). We get one of these for each constructor of the inductive type T, and we curry them to get the full recursor (encapsulating each one between brackets appropriately).

For List R for instance, the recursor List.rec has type signature {R : Type} -> {F : List R -> Type} -> F nil -> ((a : R) -> (l : List R) -> F l -> F (a :: l)) -> (L : List R) -> F L. The first {R : Type} is only there because List takes a type as a parameter. But then we get h1 : F nil for the constructor List.nil : List R and h2 : ((a : R) -> (l : List R) -> F l -> F (a :: l)) for the constructor List.cons : R -> List R -> List R.

Indeed, with such a function List.rec, we can construct a dependent function f : {R : List} -> (L : List R) -> F L using just a term h1 : F nil and a function h2 : (a : R) -> (l : List R) -> F l -> F (a :: l) as inputs, by setting f [] = h1 if L = nil and f (a :: l) = h2 a l (f l) if L = (a :: l). This is exactly the induction principle for lists. The general formula for the function f associated to h1 and h2 is then f := fun L => List.rec (motive := fun L => F L) h1 h2 L.

[Chris Bailey]

The details for this w.r.t. Lean's type theory are described in Mario Carneiro's thesis (section 2.6.0) (https://github.com/digama0/lean-type-theory/releases/tag/v1.0), and Lean's inductive types come from a paper by Peter Dybjer called "Inductive Families" (Formal aspects of computing, 6(4):440–465, 1994). You can also read the source for the kernel, but the inclusion of mutual and nested inductives adds quite a bit of noise.

[Shanghe Chen]

Thanks for all these great insights and information!

[Giacomo Stevanato]

Flo (Florent Schaffhauser) said:

If T is an inductive type, the associated function T.rec can be used to construct dependent functions out of T. This means that, given a type family F : T -> Type, we can construct a dependent function f : (t : T) -> F t by applying T.rec (motive := fun t => F t). As a special case, if F is the constant family F t = X, we can apply T.rec (motive := fun _ => X) to construct functions from T to X.

Since T is inductively defined, we can construct a function out of T by pattern-matching, meaning by case analysis on the constructors of T. For instance, if c (p1 : P1) ... (pn : Pn) (t1 : T) ... (tm : T) : T is a term of type T (the function c here is a constructor with n parameters of type P1 ... Pn and m parameters ti : T), then in order to define f t for t = c p1 ... pn t1 ... tm it suffices to have a term h (p1 : P1) ... (pn : Pn) (t1 : T) ... (tm : T) (f t1 : F t1) ... (f tm : F tm) of type F t. By definition, that long term h ... will be f t in our definition of f by pattern-matching.

In this example, the auxiliary function h is a dependent function of type signature (p1 : P1) -> ... -> (pn : Pn) -> (t1 : T) -> ... -> (tm : T) -> (P t1) -> ... -> (P tm) -> P (c p1 ... pn f1 ... fm). We get one of these for each constructor of the inductive type T, and we curry them to get the full recursor (encapsulating each one between brackets appropriately).

For List R for instance, the recursor List.rec has type signature {R : Type} -> {F : List R -> Type} -> F nil -> ((a : R) -> (l : List R) -> F l -> F (a :: l)) -> (L : List R) -> F L. The first {R : Type} is only there because List takes a type as a parameter. But then we get h1 : F nil for the constructor List.nil : List R and h2 : ((a : R) -> (l : List R) -> F l -> F (a :: l)) for the constructor List.cons : R -> List R -> List R.

Indeed, with such a function List.rec, we can construct a dependent function f : {R : List} -> (L : List R) -> F L using just a term h1 : F nil and a function h2 : (a : R) -> (l : List R) -> F l -> F (a :: l) as inputs, by setting f [] = h1 if L = nil and f (a :: l) = h2 a l (f l) if L = (a :: l). This is exactly the induction principle for lists. The general formula for the function f associated to h1 and h2 is then f := fun L => List.rec (motive := fun L => F L) h1 h2 L.

What about indexed type families though? This doesn't seem to cover them (e.g. all your motive/Fs take only one parameter, but clearly Eq.rec's takes two).

[Florent Schaffhauser]

Right, so for Eq : {A : Type} -> (a a' : A) -> Type , the constructor Eq.refl : (a : A) -> Eq a a is itself a dependent function. A type family over Eq is a function F : (a a' : A) -> Eq a a' -> Type and, in order to define a dependent function f : (a a' : A) -> (t : Eq a a') -> F t, it suffices to cover the case when a = a' and t = Eq.refl a.

This means that it suffices to have a dependent function h : (a : A) -> F a a (Eq.refl a)(and to define f a a (Eq.refl a) as h a). So Eq.rec should have type signature {A : Type} -> {F : (a a' : A) -> Eq a a' -> Type} -> ((a : A) -> F a a (Eq.refl a)) -> (a a' : A) -> (t : Eq a a') -> F a a' t. In this case, the induction principle is more complicated to state than to use. Also, there might be variants in the implementation (check out for instance the type signature of Eq.rec in Lean).

The point is that the induction principle for Eq a a' tells us that the only case to check for t : Eq a a' is when a = a' and t = Eq.refl a, which is how one proves that for all {A : Type} and all (a a' : A), (a = a') -> a' = a , for instance. In tactic mode, one can use induction or cases indifferently for Eq (because Eq.refl does not take terms of the form t : Eq a a' as inputs).