feat: add time step counting for relations

[BoltonBailey]

This PR adds Reduction.relates{In,Within}Steps, functions that communicate whether a relation forms a directed path of length (at most) n between two elements.

Specifically, it includes:

• Definitions of these functions
• Theorems about reflexivity and transitivity
• Theorems that track the growth of ancillary functions with respect to the relation

These are a prerequisite to defining time bounds, perhaps for multiple models of computation, but in particular for Turing machines, see PR #269.

[chenson2018]

This looks great to have, thanks for working on this! I am wondering though if we should at least initially put this in Cslib.Foundations.Data.Relation instead (or make an appropriate subdirectory) and work with just unbundled relations. My reasoning is:

• there is some overlap there, for instance the definition Relation.Reducible and Relation.Normal could be reused
• I am a bit unsure about fully committing to using ReductionSystem as an API because of the duplication of proofs about relations that would be required

What do you think?

[BoltonBailey]

What do you think?

Sounds fine to me! I have moved this content to the Relation file and made some name changes that might make more sense in this context.

[chenson2018]

Thanks for moving this over to this module. I left some additional style/naming comments.

[chenson2018]

LGTM, thank you!

[BoltonBailey]

With the additional lemmas this is getting longer, and there is more ReflTransGen content from Mathlib.Logic.Relation that could be replicated. Would you like me to move this to a new file?

[chenson2018]

With the additional lemmas this is getting longer, and there is more ReflTransGen content from Mathlib.Logic.Relation that could be replicated. Would you like me to move this to a new file?

Sure, feel free. Another file in this same directory seems appropriate for now?

[chenson2018]

I think you need to run lake exe mk_all --module