feat(Foundations/Relation/Confluence): generalize results from confluence to commutation - #880
feat(Foundations/Relation/Confluence): generalize results from confluence to commutation#880thomaskwaring wants to merge 10 commits into
Conversation
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
Some minor organization comments:
| @[simp] theorem hJoin_eq_join : HJoin r r = Join r := rfl | ||
|
|
||
| @[grind =] theorem hJoin_eq_comp_swap : HJoin r₁ r₂ = Comp r₁ (swap r₂) := rfl |
There was a problem hiding this comment.
What was the thought behind the split simp and grind =? I'm always a bit suspicious when I don't see them in matching pairs.
There was a problem hiding this comment.
i don't think we want the latter as simp — in general i haven't systematically added grind annotations bc my proofs haven't used them (also many of the definitions are abbrev so they're not needed). should i at least add grind = to the simp lemmas where appropriate? i can also look for other possible grind lemmas.
There was a problem hiding this comment.
If we don't want it as simp, I would probably remove grind as well. You don't need to review systematically, but this one stuck out.
|
|
||
| theorem MJoin.single (h : ReflTransGen r a b) : MJoin r a b := by | ||
| use b | ||
| @[deprecated Join.single (since := "2026-09-07")] |
There was a problem hiding this comment.
Can you check that this doesn't give a warning under the nightly toolchain? For the last PR there where some +typeChanged that needed to be added. (Which is fine, but I think it's nicer to handle them now)
There was a problem hiding this comment.
yes will do though you will need to tell me how (sorry!)
There was a problem hiding this comment.
No worries, see leanprover/downstream-lean4#54 where this was fixed
|
|
||
| /-- The join of the reflexive transitive closure. This is not named in Mathlib, but see | ||
| `#loogle Relation.Join (Relation.ReflTransGen ?r)` -/ | ||
| abbrev MJoin (r : α → α → Prop) := Join (ReflTransGen r) |
There was a problem hiding this comment.
I wonder a bit how necessary these M variants are. It's harmless since they are abbrev and it does make combinatory logic a bit nicer looking, but otherwise it could be considered redundant.
There was a problem hiding this comment.
i would support deprecating them — it does make some of the statements less wordy so if you think it's harmless i'm okay with keeping them.
There was a problem hiding this comment.
If you also don't feel strongly, I think I would deprecate them just so there are fewer spellings
|
Why is |
|
Could we add this theorem to the PR? theorem diamond_commute_reflTransGen
(h : DiamondCommute r₂ r₁) :
DiamondCommute r₂ (Relation.ReflTransGen r₁) := by
intro q p r hB hA
induction hA generalizing p with
| refl => exact ⟨p, .refl, hB⟩
| tail _ a_step ih =>
obtain ⟨s, hs₁, hs₂⟩ := ih hB
obtain ⟨w, hw₁, hw₂⟩ := h hs₂ a_step
exact ⟨w, hs₁.tail hw₁, hw₂⟩ |
3 participants
This PR generalises many results from confluent to commuting relations, and obtains the classical case as a specialisation. We add
HJoinandMHJoin— heterogenous versions ofJoinandMJoin— and associated API for them and related relational constructions.NB: the theorem
confluent_equivalentsis now public, and theTFAEhas been extended with certain other properties which generalise better to the heterogenous case.