Am I getting wellfounded recursion right?

Stream: new members

[Chris M]

I've been a bit puzzled by the wellfounded recursion definition in Lean, because the logical structure seems to be quite different from the usual mathematical definition. I just want to check if I understand things conceptually correctly.

The accessibility condition is stated in wf.lean as:

inductive acc {α : Sort u} (r : α → α → Prop) : α → Prop
| intro (x : α) (h : ∀ y, r y x → acc y) : acc x

If we were to (falsely) interpret this as an axiom for acc x, then well_founded would be different from the original definition of well-foundedness, and in fact it wouldn't work: It would be consistent with acc being defined so as to be true for every real number, and where r is the standard ordering on the reals.

However, what this is instead, is not an axiom for a predicate acc, but rather a rule for which lambda terms are accepted as proofs of acc x (i.e. which terms have type acc x).

(The following part I'm most uncertain about) Hence by extension this is a definition of a predicate, because we simply state that the predicate is false for any a:\a for which we cannot construct a proof that it's true. (edit: Actually, I just realized that all of this is intuitionistic logic and the propositions for which we don't have a proof aren't necessarily "false". This does make me confused about what such an inductively defined Prop "means", or how to think about it clearly).

In any case, we are getting the same "effect" as we do with a well-founded relation in classical mathematics, but the underlying definition seems to be somewhat different: In classical mathematics, we rely on an axiom on r that tells us that there is a minimal element. In Lean, we don't state this by an axiom, but rely on the meta-property of the typing system that it's impossible to construct a proof of this inductively defined Prop without there being a minimal element to "jumpstart" this proof. Moreover, in classical mathematics we can conclude that there won't be infinitely decreasing sequences by axiomatizing the minimal element for each set. In Lean, we get the same result directly from the fact that lambda terms must be finite and rec can only do a finite recursion on these proofs.

Am I correct about how this works in Lean? And am I correct that well-founded recursion in Lean is quite a bit different in this sense to classical well-founded recursion?

All of this leaves me kind of confused: Why is it so different? It must be related to intuitionistic logic (as I hinted at)? Is there a reason that Lean (or intuitionistic logic in general?) does this, rather than along more classical lines? Is this just to satisfy people who happen to have a preference for intuitionistic logic, or is there some deeper reason why a theorem prover has to do it this way?

[Daniel Fabian]

I am not sure if you missed it, but acc actually has two parameters, it's not acc x, but rather acc r x.

And the way how you have to read the inductive defined proposition is something like: Given an x : \alpha, and given a proof, that forall y, r y x -> acc r y you can conclude acc r x.

How would you like to define it in a way that it is true for all real numbers? If you consider the empty relation, then yes, you can conclude acc r x, but if you try to use it, you will not have an induction hypothesis.

Because now your IH is useless. Doing the opposite, proving that the universal relation is well-founded fails. So please provide the definition you would like to use.

def empty_rel : ℕ → ℕ → Prop := λ _ _, false

lemma wf_empty : well_founded empty_rel := ⟨λ n, ⟨n, λ y h, false.elim h⟩⟩

example : ∀ n: ℕ, n = n :=
begin
    intro n,
    apply well_founded.induction wf_empty, intros m h,
    specialize h m,
    --useless
end


def univ_rel : ℕ → ℕ → Prop := λ _ _, true

lemma wf_univ : well_founded univ_rel :=
begin
    constructor, intro n, constructor,
    intros m h, constructor,
    intros m h, constructor,
    intros m h, constructor,
    intros m h, constructor,
    intros m h, constructor,
    --doesn't work
end

[Chris M]

Yeah I know that its acc r x, I was just sloppy, sorry.

Regarding this: "How would you like to define it in a way that it is true for all real numbers?" I said that that would be the case if we would interpret it (falsely) as an axiom on acc rather than an inductive definition.