Definition of acc (accessible)

Stream: new members

[Martin C. Martin]

Theorem Proving in Lean section 8.4 says "According to its definition, acc r x is equivalent to ∀ y, r y x → acc r y. " However, this does not uniquely define acc. For example, on the integers where r is the standard <, an acc < x that is true for all x satisfies the above proposition, as does one that is false for all x. I'm assuming the false is what is intended here. Is there another way I should be thinking of acc?

[Yaël Dillies]

false is not valid for all x because acc r 0 (as ∀ y, y < 0, acc r y vacuously).

[Yaël Dillies]

Also, doesn't acc stand for Ascending Chain Condition?

[Martin C. Martin]

Yaël Dillies said:

false is not valid for all x because acc r 0 (as ∀ y, y < 0, acc r y vacuously).

That's true for the natural numbers ℕ, but here I'm talking about the integers ℤ.

[Yaël Dillies]

Ah yes sorry. The fact that it's an inductive definition means that it's the smallest relation respecting this property, so indeed it is false everywhere.

[Martin C. Martin]

Yaël Dillies said:

Ah yes sorry. The fact that it's an inductive definition means that it's the smallest relation respecting this property, so indeed it is false everywhere.

Thanks a lot, that makes sense and is very helpful. How does one define "smallest relation" in this context? For example, what if one relation is true on a subset S and false on a subset T, and another relation is opposite? Or can you prove that the "infinite and" of all relations satisfying the definition also satisfies the definition, and call that the smallest relation?

[Mario Carneiro]

Yaël Dillies said:

Also, doesn't acc stand for Ascending Chain Condition?

acc in lean stands for the accessibility relation

[Mario Carneiro]

Martin C. Martin said:

Yaël Dillies said:

Ah yes sorry. The fact that it's an inductive definition means that it's the smallest relation respecting this property, so indeed it is false everywhere.

Thanks a lot, that makes sense and is very helpful. How does one define "smallest relation" in this context? For example, what if one relation is true on a subset S and false on a subset T, and another relation is opposite? Or can you prove that the "infinite and" of all relations satisfying the definition also satisfies the definition, and call that the smallest relation?

It's the intersection of all relations satisfying the definition

[Mario Carneiro]

the structure of inductive types ensures that the set of fixed points of the operator is closed under intersection