Right congruence

Stream: Is there code for X?

[Ching-Tsun Chou]

I'm introducing a notion of "right congruence" over Language in cslib#265. @Chris Henson suggested that I ask here to see if anyone have any thoughts about the definitions I made in RightCongruence.lean.

[Eric Wieser]

I think this might be similar to docs#CovariantClass ?

[Ching-Tsun Chou]

I do want the underlying relation to be an equivalence relation and I will form the quotient type of the equivalence relation. But I guess I can state the right_congr condition using CovariantClass?

[Chris Henson]

To follow up on this, yes this does line up. Also, I think we would rather this be a Prop class rather than extend Setoid, which is in Sort? Regardless, the following are equivalent:

import Mathlib

class RightCongruence (α : Type*) : Prop where
  right_congr {u v} (huv : u ≈ v) (w : List α) : u ++ w ≈ v ++ w

theorem RightCongruence_iff_CovariantClass :
    RightCongruence α ↔ CovariantClass (List α) (List α) (flip (·++·)) (· ≈ ·) := by
  unfold flip
  grind [Covariant, CovariantClass, RightCongruence]

[Ching-Tsun Chou]

Where is the equivalence ≈ defined?

[Chris Henson]

This is using the instance for lists, is that not what you intended?

[Ching-Tsun Chou]

I must be missing something. In the class definition above, is ≈ a free variable?

[Ching-Tsun Chou]

Two questions:
(1) How do I give a specific definition to ≈, as I need to do in cslib#278?
(2) I do need form the quotient type of ≈. How do I do that if it is not a Setoid?

[Chris Henson]

Ching-Tsun Chou said:

I must be missing something. In the class definition above, is ≈ a free variable?

I think I see the confusion. The Prop version I used above is picking up docs#List.isSetoid. I did not realize you really needed to specify a different setoid until seeing an example. I think (but am not sure) that the CovariantClass is still applicable here. I'll take a closer look again at the new PR maybe tomorrow.

[Chris Henson]

(in retrospect this is somewhat obvious, sorry for the noise!)