Little addition to HasSubstitution

Stream: CSLib

[Fabrizio Montesi]

@Chris Henson What do you think of adding to HasSubstitution the requirement that substitution never touches things it cannot find? I'm finding myself repeating this over and over in the preparation of a general framework for logics in CSLib.

For example:

/-- Typeclass for substitution relations and access to their notation. -/
class HasSubstitution (α : Type u) (β : Type v) (γ : Type w) where
  /-- Substitution function. Replaces `x` in `t` with `t'`. -/
  subst (t : α) (x : β) (t' : γ) : α
  /-- Substitution does not add elements. -/
  subst_mem_eq [Membership β α] {t : α} {x : β} {t' : γ} (h : x ∉ t) : subst t x t' = t

[Chris Henson]

This is fine if it is put in a class extending this one. My reasoning:

• In general we don't want to tie propositions to very general notation typeclasses
• It is preferable for any propositions like this to use the substitution notation, which can't happen if it's in the same class.
• For things like System F, where there are multiple instances for substitution, this is true but a little awkward

[Fabrizio Montesi]

You mean, a class that extends HasSubstitution with subst_mem_eq?

[Fabrizio Montesi]

Ah, of course (I initially misinterpreted what you meant by proposition).

I agree. Also, there are other properties we'll probably add as classes. Any idea for what we could call the extended class?

[Chris Henson]

If you anticipate multiple such classes the pattern could be Lawful + <part that changes> + Subst. So maybe LawfulMemSubst here? (Trying to keep it reasonably short here with some abbreviation...)

[Fabrizio Montesi]

Sounds good for when there's no established name (like idempotent, etc.).

[Fabrizio Montesi]

here's a proposal in line with 'HAdd' from Lean core:

/--
Typeclass for heterogeneous substitutions (all input types can differ) and access to their notation.
-/
class HSubst (α : Type u) (β : Type v) (γ : Type w) where
  /-- Substitution function. Replaces `x` in `t` with `t'`. -/
  subst (t : α) (x : β) (t' : γ) : α

/-- Notation for substitution. -/
notation t:max "[" x ":=" t' "]" => HSubst.subst t x t'

/-- Typeclass for heterogeneous substitutions that require membership for modification. -/
class MemHSubst (α : Type u) (β : Type v) (γ : Type w) extends HSubst α β γ where
  /-- Substituting a non-present element is the identity. -/
  subst_mem_eq [Membership β α] {t : α} {x : β} {t' : γ} (h : x ∉ t) : subst t x t' = t

[Eric Wieser]

subst_mem_eq [Membership β α] seems like it makes this useless

[Eric Wieser]

Because that says "for every possible definition of membership, substitution is a no-op":

theorem bad {α β γ} [MemHSubst α β γ] {t : α} {x : β} {t' : γ} : HSubst.subst t x t' = t :=
  @MemHSubst.subst_mem_eq _ _ _ _ ⟨fun _ _ => False⟩ _ _ _ False.elim

[Eric Wieser]

You want to say "for the canonical one", which means the [Membership β α] needs to be a parameter of the typeclass, not a quantifier in a field

[Fabrizio Montesi]

only MemHSubsts, and only if x ∉ t

[Fabrizio Montesi]

huh

[Fabrizio Montesi]

I see what you mean

[Fabrizio Montesi]

this, right?

/-- Typeclass for heterogeneous substitutions that require membership for modification. -/
class MemHSubst (α : Type u) (β : Type v) (γ : Type w) [Membership β α] extends HSubst α β γ where
  /-- Substituting a non-present element is the identity. -/
  subst_mem_eq {t : α} {x : β} {t' : γ} (h : x ∉ t) : subst t x t' = t

[Eric Wieser]

yes, that's safe

[Fabrizio Montesi]

good catch, thx :)

[Fabrizio Montesi]

.... grind has proven it just works for linear logic sequents without me doing anything. I love these moments :grinning_face_with_smiling_eyes:

instance [DecidableEq (Proposition Atom)] :
    MemHSubst (Sequent Atom) (Proposition Atom) (Proposition Atom) where
  subst Γ a b := if a ∈ Γ then Γ.erase a |> insert b else Γ
  subst_mem_eq := by grind

[Eric Wieser]

I mean the proof is probably just := if_neg so this isn't particularly impressive

[Fabrizio Montesi]

I tried if_neg and it didn't work

[Fabrizio Montesi]

mmmh but you're right, so it's probably due to something silly with the parameters...

[Fabrizio Montesi]

this works:

subst_mem_eq := by
    intro _ _ _ _
    apply if_neg
    assumption

[Eric Wieser]

I would guess that subst_mem_eq h := if_neg h does too

[Fabrizio Montesi]

It does, thanks for the golfing!