reflexive transitive closure

Stream: new members

[Huỳnh Trần Khanh]

what does that mean? I saw that word in the operational semantics lean file in the logical verification repo

and why is there a separate *=> operator in addition to the => operator?

[Huỳnh Trần Khanh]

https://github.com/blanchette/logical_verification_2020/blob/master/lean/love08_operational_semantics_demo.lean

[Mario Carneiro]

The star on a relation symbol usually means the reflexive transitive closure of the relation without the star. So if -> is a relation then ->* is the reflexive transitive closure of R

[Mario Carneiro]

The reflexive transitive closure is, as the name implies, the closure of a relation under reflexivity and transitivity. Concretely, that means that x R* y if there exists a finite sequence x = z0 R z1 R ... R zn = y

[Mario Carneiro]

in particular the sequence is allowed to be empty, so that x R* x

[Mario Carneiro]

i.e. it is reflexive

[Mario Carneiro]

and it is transitive because if you have two such chains of R-relations you can append them to get a longer chain, so x R* y R* z implies x R* z

[Mario Carneiro]

mathlib has a definition of the reflexive transitive closure at docs#relation.refl_trans_gen