Destructor of Inductive Types

Stream: lean4

[Yicheng Qian]

I was a Coq user and have just begun working on a project in Lean. I'm trying to understand Lean based on my experience with Coq, and encountered multiple problems related to destructors of inductive types.
In Coq, there is a match ... in ... return ... with | ... | ... | ... clause which does dependent pattern matching, and recursors of inductive types are defined using the match ... in ... return ... with | ... | ... | ... clause and the fix keyword.
On the contrary, (it seems to me that) the match expressions in Lean are defined using recursors of the inductive types, and the recursor <indtype>.rec is "atomic". However, the behaviour of Lean's match ... with | ... | ... | ... clause and structural recursion makes me very confused.

The first thing that confuses me is that Lean sometimes does not recognize decreasing arguments of recursive functions. Consider Acc (the accessibility predicate, used to define well-foundedness)

inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop where
  | intro (x : α) (h : (y : α) → r y x → Acc r y) : Acc r x

In Coq, the predicate is defined as follows

Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
    Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x.

and the destructor of this predicate is defined as

Definition Acc_rect' (A : Type) (R : A -> A -> Prop) (P : A -> Type)
   (f : forall x : A, (forall y : A, R y x -> Acc R y) -> (forall y : A, R y x -> P y) -> P x)
    : forall x : A, Acc R x -> P x :=
fix F (x : A) (a : Acc R x) {struct a} : P x :=
  match a with
  | Acc_intro _ Q => f x Q (fun (y : A) (r : R y x) => F y (Q y r))
  end.

However, when I tried to define the same thing in Lean

def Acc_rec' {α : Sort u} {r : α → α → Prop}
               (motive : (a : α) → Acc r a → Sort v)
               (H : (x : α) → (∀ (y : α), r y x → Acc r y) →
                       ((y : α) → r y x → (Ry : Acc r y) → motive y Ry) →
                       (Rx : Acc r x) → motive x Rx)
               (a : α) : (t : Acc r a) → motive a t
  | Acc.intro a' Q => H a' Q (fun y Hr Ry => Acc_rec' motive H y (Q y Hr)) (Acc.intro a' Q)

It produces the error message

  fail to show termination for
    Acc_rec'
  with errors
  structural recursion cannot be used

  failed to prove termination, use `termination_by` to specify a well-founded relation

which (if I'm right) indicates that it didn't recognize the decreasing argument (t : Acc r a).
I know that the predicate Acc.rec is automatically generated by Lean and there is no need to define it by hand. But the problem is that Lean did not recognize the decreasing argument, which makes me confused.

[Mario Carneiro]

Yes, lean's equation compiler does not support direct structural recursion

[Mario Carneiro]

which is counterintuitive since this is the simplest kind of recursion. It supports "bounded recursion", which is like structural recursion except it also allows doing multiple layers of inductive constructors at once, and well founded recursion which is where you recurse on a well founded type with a measure function

[Mario Carneiro]

However, neither of those methods apply here: bounded recursion only works for "regular inductives" which are not in Prop, and well founded recursion in default configuration will attempt to use recursion on a natural number "height" function which is not powerful enough to show Acc is well founded

[Mario Carneiro]

The simplest way to do direct structural recursion in lean is to use the induction tactic instead of the equation compiler

[Mario Carneiro]

noncomputable def Acc_rec' {α : Sort u} {r : α → α → Prop}
               (motive : (a : α) → Acc r a → Sort v)
               (H : (x : α) → (∀ (y : α), r y x → Acc r y) →
                       ((y : α) → r y x → (Ry : Acc r y) → motive y Ry) →
                       (Rx : Acc r x) → motive x Rx)
               (a : α) : (t : Acc r a) → motive a t := by
  intro t
  induction t with
  | intro a' Q ih => exact H a' Q (fun y Hr Ry => ih y Hr) (Acc.intro a' Q)