Case — carrier capabilities

[Bla94b] [Cor06]

The typeclass mixin for carriers that bear grammatical case — the case analogue of HasPerson (Features/Person/Capabilities.lean). caseOf extracts the carrier's analytical case value; carriers that store UD realization (UD.MorphFeatures) lift through Case.fromUD.

Compatible is the case-concord relation: symmetric, agree-or-wildcard slot compatibility (NP-internal agreement in case, e.g. Slavic/Latin adjective–noun). It is not case government/assignment — the asymmetric, head-to-dependent relation by which case enters an NP in the first place — which lives in Syntax/Case/Dependent.lean (Marantz dependent case) and Syntax/Case/Licensing.lean (Kalin licensing). Unlike person/number/gender, case is a non-canonical agreement feature ([Cor06]): the controller of case concord is itself the target of some other case relation; Blake's treatment of case assignment and concord ([Bla94b]) is the typological anchor.

The carrier is single-valued (Option Case), so syncretism (one form realizing several cases), case-stacking/Suffixaufnahme, and coordinate case resolution are out of scope — a faithful treatment of those would carry a Finset Case and check nonempty intersection. The present consumer (Studies/WechslerZlatic2000.lean, concord) treats concord case as single-valued, for which this carrier is adequate.

class HasCase (α : Type u_1) : Type u_1

A carrier of grammatical case. none = the carrier does not mark case.

• caseOf : α → Option Case

  The analytical case value, if marked.

@[implicit_reducible]

instance instHasCaseMorphFeatures : HasCase UD.MorphFeatures

Equations

• instHasCaseMorphFeatures = { caseOf := fun (mf : UD.MorphFeatures) => Option.map Case.fromUD mf.case_ }

@[implicit_reducible]

instance instHasCaseCase : HasCase Case

Equations

• instHasCaseCase = { caseOf := some }

@[implicit_reducible]

instance instHasCaseOptionCase : HasCase (Option Case)

Option Case is the free case-bearer: some c bears c, none is caseless.

Equations

• instHasCaseOptionCase = { caseOf := id }

@[reducible, inline]

abbrev HasCase.Compatible {α : Type u_1} {β : Type u_2} [HasCase α] [HasCase β] (a : α) (b : β) : Prop

Two carriers are case-compatible: the slot values are compatible in the flat information order (Compat) — if both mark case, the values agree; unmarked carriers are wildcards. The concord-checking relation.

Equations

• HasCase.Compatible a b = Compat (caseOf a) (caseOf b)

theorem UD.MorphFeatures.compatible_hasCase {f1 f2 : MorphFeatures} (h : f1.compatible f2 = true) : HasCase.Compatible f1 f2

φ-compatibility entails case compatibility: the HasCase mixin never diverges from the unification-based agreement engine (UD.MorphFeatures.compatible) — the case analogue of UD.MorphFeatures.compatible_hasPerson.