Typeclass for congruence over a context.

class Cslib.Congruence {α : Sort u_1} (r : α → α → Prop) : Type

The relation r is a congruence on α. This class gives access to the ≡[r] notation. To instantiate a canonical congruence for α, see HasCongruence.

Congruence relations should also instantiate LawfulCongruence to prove that the relation respects the expected congruence laws.

def Cslib.Congruence.r {α : Sort u_1} (r : α → α → Prop) [Congruence r] : α → α → Prop

a ≡[r] b means that the a and b are related by the congruence r.

Equations

• Cslib.Congruence.r r = r

def Cslib.«term_≡[_]_» : Lean.TrailingParserDescr

a ≡[r] b means that the a and b are related by the congruence r.

Equations

• One or more equations did not get rendered due to their size.

class Cslib.DefaultCongruence (α : Type u_1) (r : outParam (α → α → Prop)) : Type

The type α has a canonical congruence relation. This gives access to the ≡ notation.

def Cslib.DefaultCongruence.r {α : Type u_1} {r : α → α → Prop} [DefaultCongruence α r] (a b : α) : Prop

a ≡ b means that a and b are related by the canonical congruence relation for their type.

Equations

• Cslib.DefaultCongruence.r a b = r a b

def Cslib.«term_≡_» : Lean.TrailingParserDescr

a ≡ b means that a and b are related by the canonical congruence relation for their type.

Equations

• Cslib.«term_≡_» = Lean.ParserDescr.trailingNode `Cslib.«term_≡_» 29 30 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ ") (Lean.ParserDescr.cat `term 30))

@[instance_reducible]

instance Cslib.instCongruenceOfDefaultCongruence (α : Type u_1) (r : α → α → Prop) [DefaultCongruence α r] : Congruence r

Equations

• Cslib.instCongruenceOfDefaultCongruence α r = { }

class Cslib.LawfulCongruence {α : Type u_1} (r : α → α → Prop) [Congruence r] [HasContext α] extends IsEquiv α r, CovariantClass (Cslib.HasContext.Context α) α (fun (x1 : Cslib.HasContext.Context α) (x2 : α) => x1<[x2]) fun (x1 x2 : α) => Cslib.Congruence.r r x1 x2 : Prop

An equivalence relation on α preserved by all contexts.

• refl (a : α) : r a a
• trans (a b c : α) : r a b → r b c → r a c
• symm (a b : α) : r a b → r b a
• elim : Covariant (Cslib.HasContext.Context α) α (fun (x1 : Cslib.HasContext.Context α) (x2 : α) => x1<[x2]) fun (x1 x2 : α) => Cslib.Congruence.r r x1 x2