feat: syntactic contexts and congruence relations

[fmontesi]

This PR introduces notions of (single hole) syntactic contexts (HasContext) and congruence relations (Congruence), along with the standard notation c[t] for 'fill the hole in the context c with term t'.

The development of CCS is adapted accordingly and should hold for many other calculi. The idea actually comes from an ongoing development on the generalisation of sequent calculi and logics, but these require more concepts. Also, in the future, it might be interesting to study approaches similar to HasContext in semantics that use different kinds of contexts.

The PR also scopes the grind annotations in CCS.

[chenson2018]

Does α need to be a Sort here? This builds if you make it a Type, so I wondered if you did this just because you were extending IsEquiv.

If this can be in Type, the following is equivalent:

class Congruence (α : Type*) [HasContext α] (r : α → α → Prop) extends
  IsEquiv α r,
  is_congruence : CovariantClass (HasContext.Context α) α (·[·]) r

up to ordering of arguments, e.g.

instance bisimilarityCongruence :
    Congruence (Process Name Constant) (Bisimilarity (lts (defs := defs))) where
  is_congruence := ⟨by grind [Covariant, bisimilarity_is_congruence]⟩

works in CCS.BehaviouralTheory.

If we end up using this sort of thing in multiple places (i.e. here and @ctchou's #278), I'd prefer that we use the same naming like covariant : CovariantClass ... so that you get the constructor covariant.elim : Covariant ....

[ctchou]

In #278, I used the name right_cov, because one can also define a congruence that is both a left congruence and a right congruence (in which case there will be two covariant fields). Perhaps context_cov is a good name here.

[fmontesi]

I was doing it to be consistent with HasEquiv in Lean core, because I don't need it to be a type, strictly speaking. But I think using Type is fine for our purposes, so integrating with mathlib should take priority here. I'll change it to what you suggest, I think it's a good idea!

…

On Sat, 24 Jan 2026, 08:38 Chris Henson, ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In Cslib/Foundations/Syntax/Congruence.lean <#284 (comment)>: > +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi +-/ + +module + +public import Cslib.Foundations.Syntax.Context + ***@***.*** public section + +namespace Cslib + +/-- An equivalence relation preserved by all contexts. -/ +class Congruence (α : Sort*) [HasContext α] (r : α → α → Prop) extends IsEquiv α r where Does α need to be a Sort here? This builds if you make it a Type, so I wondered if you did this just because you were extending IsEquiv. If this can be in Type, the following is equivalent: class Congruence (α : Type*) [HasContext α] (r : α → α → Prop) extends IsEquiv α r, is_congruence : CovariantClass (HasContext.Context α) α (·[·]) r up to ordering of arguments, e.g. instance bisimilarityCongruence : Congruence (Process Name Constant) (Bisimilarity (lts (defs := defs))) where is_congruence := ⟨by grind [Covariant, bisimilarity_is_congruence]⟩ works in CCS.BehaviouralTheory. If we end up using this sort of thing in multiple places (i.e. here and @ctchou <https://github.com/ctchou>'s #278 <#278>), I'd prefer that we use the same naming like covariant : CovariantClass ... so that you get the constructor covariant.elim : Covariant .... — Reply to this email directly, view it on GitHub <#284 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAP3DSPGPNW6ZCTVO6NMNED4IMOOJAVCNFSM6AAAAACSU4BY52VHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZTOMBQHE4DANZYGM> . You are receiving this because you authored the thread.Message ID: ***@***.***>