Documentation

Linglib.Features.Case.Basic

Case — the canonical inventory #

[Bla94b] [dMMNZ21] [Sta85]

The root-namespace Case type is the canonical, analytical case inventory: the values languages' case systems distinguish. All theoretical machinery — Blake's hierarchy (here), Caha containment (Syntax/Case/Order.lean), syncretism and *ABA (Morphology/Case/Allomorphy.lean), grammaticalization clines (Diachronic/CaseGrammaticalization.lean) — operates over this type.

UD.Case (Data/UD/Basic.lean) is the realization vocabulary — what corpora annotate — reachable by toUD/fromUD. The two inventories currently coincide cell-for-cell, so both round-trips hold; the analytical inventory is where refinements that UD conflates would land (e.g. the Latin-type syncretic general ablative and the Finnish exterior-source ablative both realize as Abl), breaking only fromUD_toUD — exactly as Person.fromUD_toUD degrades to coarsen under UD's clusivity conflation.

This mirrors the Person/Number/Gender API (Features/{Person,Number,Gender}/Basic.lean): canonical analytical inventory at root namespace, UD demoted to realization.

Main declarations #

Case — the 28-cell analytical inventory
Case.toUD/Case.fromUD — UD realization round-trip
Case.hierarchyRank — Blake's implicational hierarchy ([Bla94b], Fin 7-codomain rank)
Case.IsValidInventory — inventory contiguity on the hierarchy, decidable, with the order-theoretic characterization isValidInventory_iff_ordConnected
Features.AlignmentFamily, Features.CaseAssignment, Features.FixedCaseEncoding — small per-entry companion enums

inductive Case :

Grammatical case — the canonical analytical inventory.

nom : Case
Nominative: citation/subject case.
acc : Case
Accusative: direct object.
gen : Case
Genitive: possessor, nominal dependent.
dat : Case
Dative: indirect object, recipient.
inst : Case
Instrumental: means, instrument.
loc : Case
Locative: static location (general).
voc : Case
Vocative: address form.
abl : Case
Ablative: source, motion from (general).
erg : Case
Ergative: transitive subject in ergative alignment.
abs : Case
Absolutive: intransitive subject / transitive object in ergative alignment.
part : Case
Partitive: partial affectedness, indeterminate quantity (Finnic).
ess : Case
Essive: temporary state, capacity ("as an X").
transl : Case
Translative: change of state ("into an X").
com : Case
Comitative: accompaniment ("with X").
ade : Case
Adessive: at/near (exterior static).
ine : Case
Inessive: in (interior static).
ill : Case
Illative: into (interior goal).
ela : Case
Elative: out of (interior source).
all : Case
Allative: onto/towards (exterior goal).
sub : Case
Sublative: onto (surface goal; Hungarian).
sup : Case
Superessive: on (surface static; Hungarian).
del : Case
Delative: off of (surface source; Hungarian).
ter : Case
Terminative: up to a limit ("as far as X").
tem : Case
Temporal: at a time.
caus : Case
Causative/causal: because of X.
ben : Case
Benefactive: for the benefit of X.
perl : Case
Perlative: path, motion through.
abess : Case
Abessive/privative: without X.

Instances For

@[implicit_reducible]

instance instDecidableEqCase :

DecidableEq Case

Equations

instDecidableEqCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprCase.repr :

Case → ℕ → Std.Format

Equations

instReprCase.repr Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.nom")).group prec✝
instReprCase.repr Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.acc")).group prec✝
instReprCase.repr Case.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.gen")).group prec✝
instReprCase.repr Case.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.dat")).group prec✝
instReprCase.repr Case.inst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.inst")).group prec✝
instReprCase.repr Case.loc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.loc")).group prec✝
instReprCase.repr Case.voc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.voc")).group prec✝
instReprCase.repr Case.abl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.abl")).group prec✝
instReprCase.repr Case.erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.erg")).group prec✝
instReprCase.repr Case.abs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.abs")).group prec✝
instReprCase.repr Case.part prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.part")).group prec✝
instReprCase.repr Case.ess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ess")).group prec✝
instReprCase.repr Case.transl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.transl")).group prec✝
instReprCase.repr Case.com prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.com")).group prec✝
instReprCase.repr Case.ade prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ade")).group prec✝
instReprCase.repr Case.ine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ine")).group prec✝
instReprCase.repr Case.ill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ill")).group prec✝
instReprCase.repr Case.ela prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ela")).group prec✝
instReprCase.repr Case.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.all")).group prec✝
instReprCase.repr Case.sub prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.sub")).group prec✝
instReprCase.repr Case.sup prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.sup")).group prec✝
instReprCase.repr Case.del prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.del")).group prec✝
instReprCase.repr Case.ter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ter")).group prec✝
instReprCase.repr Case.tem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.tem")).group prec✝
instReprCase.repr Case.caus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.caus")).group prec✝
instReprCase.repr Case.ben prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ben")).group prec✝
instReprCase.repr Case.perl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.perl")).group prec✝
instReprCase.repr Case.abess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.abess")).group prec✝

Instances For

@[implicit_reducible]

instance instReprCase :

Repr Case

Equations

instReprCase = { reprPrec := instReprCase.repr }

@[implicit_reducible]

instance instInhabitedCase :

Inhabited Case

Equations

instInhabitedCase = { default := instInhabitedCase.default }

@[implicit_reducible]

instance instFintypeCase :

Fintype Case

Equations

instFintypeCase = { elems := { val := ↑Case.enumList, nodup := Case.enumList_nodup }, complete := instFintypeCase._proof_1 }

UD realization vocabulary #

def Case.toUD :

Case → UD.Case

Realize as UD annotation. Currently cell-for-cell; analytical refinements that UD conflates collapse here.

Equations

Instances For

def Case.fromUD :

UD.Case → Case

Analytical value of a UD annotation.

Equations

Instances For

@[simp]

theorem Case.toUD_fromUD (u : UD.Case) :

(fromUD u).toUD = u

UD round-trips on its own image.

@[simp]

theorem Case.fromUD_toUD (c : Case) :

fromUD c.toUD = c

The analytical inventory round-trips through UD — for now. This is the theorem that degrades (to a coarsen identity, as in Person.fromUD_toUD) when an analytical refinement splits a UD cell.

Blake's case hierarchy [Bla94b] #

Implicational hierarchy over case inventories with contiguity checking. The fine-grained spatial cases all sit at the peripheral spatial tier (rank 1) since Blake's hierarchy collapses them into a single locative/ spatial group.

def Case.hierarchyRank :

Case → Fin 7

Position on Blake's case hierarchy ([Bla94b]).

Higher rank = more likely to exist in a language's case inventory. Blake's hierarchy orders NOM/ACC/ERG/ABS > GEN > DAT > LOC > ABL/INST and lumps everything below into a single undifferentiated "others" tier; the further split of that tier into rank 1 (COM/ALL/PERL/BEN + fine-grained spatial cases — Finnish/Hungarian ADE/INE/ILL/ELA/SUB/SUP/DEL) vs rank 0 (peripheral non-spatial: VOC/PART/CAUS/ESS/TRANSL/ABESS/TER/TEM) is this formalization's extrapolation, not Blake's.

Codomain is Fin 7 — the boundedness is encoded in the type, not as a separate *_bounded theorem.

Equations

Instances For

def Case.IsValidInventory (inv : Finset Case) :

An inventory is contiguous on Blake's hierarchy: every rank between two realized ranks is itself realized. Formalizes Blake's implicational tendency ([Bla94b]), in a form decide can mechanically check; isValidInventory_iff_ordConnected is the order-theoretic content.

Equations

Case.IsValidInventory inv = ∀ (r : Fin 7), (∃ c ∈ inv, c.hierarchyRank < r) → (∃ c ∈ inv, r < c.hierarchyRank) → ∃ c ∈ inv, c.hierarchyRank = r

Instances For

@[implicit_reducible]

instance Case.instDecidableIsValidInventory (inv : Finset Case) :

Decidable (IsValidInventory inv)

Equations

Case.instDecidableIsValidInventory inv = id inferInstance

theorem Case.isValidInventory_iff_ordConnected (inv : Finset Case) :

IsValidInventory inv ↔ (↑(Finset.image hierarchyRank inv)).OrdConnected

The transfer equation: inventory validity is order-connectedness of the rank image — Blake's implicational tendency is Icc-closure in Fin 7.

Contiguity verdicts on representative inventories (positive: Latin- through Finnish-sized systems; negative: hierarchy skips). Kept as examples — no codebase consumer references them by name.

Companion per-entry enums #

inductive Features.AlignmentFamily :

The two major morphosyntactic alignment families.

accusative : AlignmentFamily
ergative : AlignmentFamily

Instances For

@[implicit_reducible]

instance Features.instDecidableEqAlignmentFamily :

DecidableEq AlignmentFamily

Equations

Features.instDecidableEqAlignmentFamily x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instReprAlignmentFamily :

Repr AlignmentFamily

Equations

Features.instReprAlignmentFamily = { reprPrec := Features.instReprAlignmentFamily.repr }

def Features.instReprAlignmentFamily.repr :

AlignmentFamily → ℕ → Std.Format

Equations

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

Instances For

inductive Features.CaseAssignment :

How case is assigned to an NP in a given construction ([Sta85], §2.2.1).

derived : CaseAssignment
fixed : CaseAssignment

Instances For

@[implicit_reducible]

instance Features.instDecidableEqCaseAssignment :

DecidableEq CaseAssignment

Equations

Features.instDecidableEqCaseAssignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instReprCaseAssignment :

Repr CaseAssignment

Equations

Features.instReprCaseAssignment = { reprPrec := Features.instReprCaseAssignment.repr }

def Features.instReprCaseAssignment.repr :

CaseAssignment → ℕ → Std.Format

Equations

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

Instances For

inductive Features.FixedCaseEncoding :

For fixed-case NPs, what syntactic role the NP occupies.

directObject : FixedCaseEncoding
adverbial : FixedCaseEncoding

Instances For

@[implicit_reducible]

instance Features.instDecidableEqFixedCaseEncoding :

DecidableEq FixedCaseEncoding

Equations

Features.instDecidableEqFixedCaseEncoding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprFixedCaseEncoding.repr :

FixedCaseEncoding → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Features.instReprFixedCaseEncoding :

Repr FixedCaseEncoding

Equations

Features.instReprFixedCaseEncoding = { reprPrec := Features.instReprFixedCaseEncoding.repr }