2
$\begingroup$

Update: this has been fixed and the fix is available in the latest nightly release of Lean 4.

In Lean 4, structural recursion on functions on types is no issue.

inductive F where
  | nil (n: Nat)
  | fn (f: Nat → F)

def inc: F → F
  | F.nil n => F.nil (n+1)
  | F.fn f => F.fn fun n => inc (f n)

However, the same cannot be said of functions to propositions. In the above, when inductive F is replaced by inductive F: Prop, the function inc starts throwing this error:

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

Question: Why is this the case? Is this a type theory thing, or a Lean thing?


I thought of one potential answer, but I have no idea whether it's right. Here's my guess:

Propositions are impredicative, that means they can quantify over themselves, and that means that unlike for types, function application on propositions is not necessarily a structurally decreasing operation. Members of inductive propositions aren't necessarily structurally smaller. (In other words, the Prop version of F is not a W-type, but an M-type, is that right?)

What I find puzzling about this is that even if it's true, then "structurally-looking" recusion on propositions stil seems well-defined to me, and also perhaps I'm totally wrong.

$\endgroup$
10
  • $\begingroup$ Is invImage what you are looking for? You can just do def subtypeWellfounded {T: Type} (s: Set T) [wfr : WellFoundedRelation T] : WellFoundedRelation { t: T // t ∈ s } := invImage Subtype.val wfr $\endgroup$
    – Jason Rute
    Sep 30, 2022 at 0:26
  • $\begingroup$ Then for your relOut definition, we have (relOut T s wfr.rel) = (@subtypeWellfounded T s wfr).rel definitionally. $\endgroup$
    – Jason Rute
    Sep 30, 2022 at 0:45
  • 1
    $\begingroup$ I found this on the Lean Zulip from a few months ago "We have structural recursion on arbitrary arguments for types and soon for predicates. This doesn't cover mutually recursive definitions for now. And we don't have well-founded recursion yet." I wonder if it is just not implemented yet. $\endgroup$
    – Jason Rute
    Sep 30, 2022 at 12:10
  • 1
    $\begingroup$ Just in case, I added it as an issue on the Lean 4 github: github.com/leanprover/lean4/issues/1674 $\endgroup$
    – Jason Rute
    Oct 2, 2022 at 16:56
  • 1
    $\begingroup$ Leo just fixed it. See the issue I linked to above. $\endgroup$
    – Jason Rute
    Oct 7, 2022 at 20:38

1 Answer 1

4
$\begingroup$

TL;DR: There is no logical reason I see that Lean can't do this. It just seems like it is not implemented (and possibly it will be implemented in the future as this comment on Zulip suggests). Nonetheless, you can directly construct this using induction (or the underlying rec operator). Moreover, since Lean is proof-irrelevant, there is no logical reason to give a proof via recursion, and in my opinion induction is always a better choice.


Mario's Carneiro's answer on Zulip from a month ago may give some light, so let me repeat it here (although I am not positive I understand it correctly):

Lean's equation compiler doesn't support direct structural recursion, which is paradoxical since it is the simplest kind of recursion.

Instead it currently supports the following two types of recursion:

  • bounded recursion is like structural recursion except it also allows doing multiple layers of inductive constructors at once
  • well founded recursion is where you recurse on a well founded type with a natural number measure function

Bounded recursion doesn't work for inductives in Prop, just inductive in Type u. Well founded recursion will attempt to do recursion on a natural number measure (or "height"). It might work on your toy example, but it is not powerful enough to proof that say Acc is well-founded.


A better option when using recursion to prove a Prop is just to use induction instead. In your toy example you could do:

inductive F : Prop where
  | nil (n: Nat)
  | fn (f: Nat → F)

theorem inc: F → F := by
  intro t 
  induction t with 
  | nil n => exact F.nil (n+1)
  | fn f f_ih => exact F.fn f_ih

Not only is this proof valid, but it is also a faithful representation of your recursive construction. The induction hypothesis f_ih : forall x : Nat, F is the inductive equivalent of the recursive step inc (f ...) in your structural recursion. The induction hypothesis is assuming that inc holds true for all the outputs of f: Nat -> F. (Notice both f_ih and lambda n, inc (f n) have type Nat -> F.)

Nonetheless, Lean is proof-irrelevant and the proof doesn't matter logically. This is even more reason to avoid recursive proofs of Props, when induction is a better choice.


Digging deeper, we can even give a convincing argument that this is the correct way to translate your recursive proofs to induction. If we print the inductive proof above we get:

theorem inc : F → F :=
fun t => F.rec (fun n => F.nil (n + 1)) (fun f ih => F.fn ih) t

Now, we can see that this exact definition when applied to the Type-valued F gives exactly the same result as your recursive formula:

inductive F where
  | nil (n: Nat)
  | fn (f: Nat → F)

def inc1: F → F
  | F.nil n => F.nil (n+1)
  | F.fn f => F.fn fun n => inc1 (f n)

def inc2 : F → F :=
fun t => F.rec (fun n => F.nil (n + 1)) (fun f ih => F.fn ih) t

-- check if they behave the same
variable (foo : Nat -> Nat -> Nat)
#reduce inc1 (F.fn (fun n => F.fn (fun m => F.nil (foo n m))))
-- F.fn fun n => F.fn fun n_1 => F.nil (Nat.succ (foo n n_1))
#reduce inc2 (F.fn (fun n => F.fn (fun m => F.nil (foo n m))))
-- F.fn fun n => F.fn fun n_1 => F.nil (Nat.succ (foo n n_1))

-- prove they are the same
theorem same_inc (t : F) : inc1 t = inc2 t := by
  induction t with
  | nil n => rfl
  | fn f ih => calc
    inc1 (F.fn f) = F.fn fun n => inc1 (f n) := rfl
    _             = F.fn fun n => inc2 (f n) := by simp [ih]
    _             = inc2 (F.fn f)            := rfl

Finally, it should be noted that structural recursion seems to already be working for simpler inductive definitions in Prop:

inductive F : Prop where
  | nil (n: Int)
  | fn (f: F)

def inc: F → F
  | F.nil n => F.nil (n+1)
  | F.fn f => F.fn (inc f)

Indeed, it seems that parameters of the form (... -> F) in the inductive definition are what gives Lean 4 trouble.

$\endgroup$
2
  • $\begingroup$ Personally, I think the most important piece of info is in your comment: "We have structural recursion on arbitrary arguments for types and soon for predicates.". So in Lean 4, bounded recursion doesn't yet work for inductives in Prop, but there is no fundamental reason it shouldn't, it just needs to get implemented in Lean, and eventually it will. $\endgroup$ Oct 1, 2022 at 13:26
  • $\begingroup$ @JozefMikušinec I updated the answer accordingly, but personally, I think the most important piece of info is when I said: "just to use induction instead". Indeed, since Lean is proof-irrelevant, I see no reason to ever need to use recursion to prove a proposition. I've updated my answer with a specific recipe for translating your recursive definition (and others like it) into induction. $\endgroup$
    – Jason Rute
    Oct 1, 2022 at 21:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.