feat: define right congruence and prove its basic properties#265
feat: define right congruence and prove its basic properties#265ctchou wants to merge 6 commits intoleanprover:mainfrom
Conversation
|
Rebase on upstream/main. |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
This all looks reasonable to me, but would you mind posting in the "Is There Code for X?" channel to see if anyone has thoughts about RightCongruence/RightCongruence.QuotType/RightCongruence.eqvCls?
| by a setoid to to enable ready access to the quotient construction. -/ | ||
| class RightCongruence (α : Type*) extends eq : Setoid (List α) where | ||
| /-- If `u` an `v` are congruent, then `u ++ w` and `v ++ w` are also congruent for any `w`. -/ | ||
| right_congr : ∀ u v, eq u v → ∀ w, eq (u ++ w) (v ++ w) |
There was a problem hiding this comment.
Better spelling:
| right_congr : ∀ u v, eq u v → ∀ w, eq (u ++ w) (v ++ w) | |
| right_congr {u v} (huv : u ≈ v) (w : List α) : u ++ w ≈ v ++ w |
There was a problem hiding this comment.
Fixed. I'm surprised that this works. Isn't the ≈ notation defined only in the instance following this definition?
There was a problem hiding this comment.
Ah, the change you suggested does not work after all: it breaks DA/Congr.lean. In particular, it breaks the proof inside the definition of RightCongruence.toDA. It looks like Lean gets confused about what ≈ refers to. I'll keep my old code.
There was a problem hiding this comment.
It works, you just have to update the proof.
There was a problem hiding this comment.
Git it. You made u and v implicit.
There was a problem hiding this comment.
@chenson2018 In view of the discussion on Zulip:
https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Right.20congruence/with/569421397
does the change you suggested still make sense? Wouldn't the ≈ refer to the specific equivalence relation:
https://leanprover-community.github.io/mathlib4_docs/Init/Data/List/Perm.html#List.isSetoid
rather than a general equivalence relation which is what I want here?
There was a problem hiding this comment.
No, here it is still fine, just a mistake I made in the Zulip thread. You can use pp.all and check that the notation is properly using the provided instance in right_congr, and this still does correspond to CovariantClass.
I am working on a commit that does this, and your proofs stay almost exactly the same in #278. I will push it to that PR so we can discuss with the full context of what it looks like to actually use it.
There was a problem hiding this comment.
Is there any advantage in using the ≈ notation here at all? It just creates possible confusion with the existing List.Perm and doesn't really improve readability. In fact, so far as I can tell, the only occasion to use the ≈ notation is to state the right_congr condition.
There was a problem hiding this comment.
If a notation exists, my opinion is it is almost always preferable to use for reasons including making theorems easier to search for and avoiding problems around definitional equality.
The confusion here is really inherent to there already being an existing Setoid instance for lists, but I don't think it will cause actually ambiguity (in the sense of a typeclass diamond) because the instances are parameterized by an automaton.
There was a problem hiding this comment.
OK, I'll wait for your commit.
|
Per your suggestion, I have posted a query on Zulip: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Right.20congruence/with/568624176 |
|
I'm not sure the |
I followed up on the Zulip thread. |
|
This PR has been absorbed into #278. |
…of finite index (#278) This PR defines the notion of a "right congruence", which is an equivalence relation between finite words that is preserved by concatenation on the right, and proves its basic properties: - There is a natural deterministic automaton corresponding to each right congruence whose states are the equivalence classes of the congruence and whose transitions correspond to concatenation on the right of the input symbols. - If a right congruence is of finite index, then each of its equivalence classes is a regular language. Furthermore, this PR also defines a special type of right congruences introduced by J.R. Buchi and proves that it is of finite index if the underlying Buchi automaton is finite-state. The purpose of Buchi congruence is to prove the closure of ω-regular languages under complementation. But more work will be needed before we reach that goal. The old PR #265 has been absorbed into this PR. --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
…of finite index (leanprover#278) This PR defines the notion of a "right congruence", which is an equivalence relation between finite words that is preserved by concatenation on the right, and proves its basic properties: - There is a natural deterministic automaton corresponding to each right congruence whose states are the equivalence classes of the congruence and whose transitions correspond to concatenation on the right of the input symbols. - If a right congruence is of finite index, then each of its equivalence classes is a regular language. Furthermore, this PR also defines a special type of right congruences introduced by J.R. Buchi and proves that it is of finite index if the underlying Buchi automaton is finite-state. The purpose of Buchi congruence is to prove the closure of ω-regular languages under complementation. But more work will be needed before we reach that goal. The old PR leanprover#265 has been absorbed into this PR. --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
2 participants
This PR has been absorbed into #278.