Zulip Chat Archive

Stream: lean4

Topic: Destructor of Inductive Types


Yicheng Qian (Aug 20 2022 at 11:34):

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 (Aug 20 2022 at 15:20):

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

Mario Carneiro (Aug 20 2022 at 15:22):

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 (Aug 20 2022 at 15:24):

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 (Aug 20 2022 at 15:25):

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

Mario Carneiro (Aug 20 2022 at 15:27):

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)

Last updated: Dec 20 2023 at 11:08 UTC