feat(Foundations/Data/Relation): strongly normalising elements of a type equipped with a relation#549
Conversation
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
I think this makes sense and is consistent with how we defined Terminating. I had in mind something pretty similar and hadn't found the time, so thanks!
Just a few mostly style reviews:
|
|
||
| /-- An element `x` is `SN` (for strongly-normalising) for a relation `r` if it is accesible under | ||
| the inverse of `r`. -/ | ||
| abbrev SN (r : α → α → Prop) (x : α) := Acc (fun a b => r b a) x |
There was a problem hiding this comment.
I think for consistency with Terminating I'd write
| abbrev SN (r : α → α → Prop) (x : α) := Acc (fun a b => r b a) x | |
| abbrev SN (r : α → α → Prop) := Acc (fun a b => r b a) |
Do you have an opinion about us writing fun a b => r b a versus using Function.swap? It seems a bit painful either way.
There was a problem hiding this comment.
i agree, no particular opinion i went with what you had for terminating (flip is also an option)
There was a problem hiding this comment.
Yeah, let's leave this for now. It is somewhat dissatisfying that we do all this work just to change the direction that the relation goes...
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
Looks good, thanks for doing this!
2 participants
This PR defines a predicate
SN r x(better naming suggestions welcome) expressing that there is no infinite chain ofr-related elements starting withx. This extends the definition ofTerminatingusingWellFoundedto individual elements, usingAcc.I'm very open to being told this is not a useful generalisation / abstraction, but the existing API for
Accdoes seem to make certain proofs easier. For instance,sn_app_leftinLambdaCalculus/LocallyNameless/Untyped/StrongNormfalls out as reduction onMis a subrelation of reduction onM.app N.