Finnish case

Finnish has some fifteen cases, each with an ending in the singular. There are the grammatical nominative, genitive, accusative and partitive, six local cases, and the essive, translative, comitative, abessive and instructive. The accusative ending -t is confined to the personal pronouns, as in häne-t 'him, her'. The local cases cross the direction of motion with a region. The inessive -ssA 'in', the elative -stA 'out of' and the illative -Vn 'into' make up the interior series, and the adessive -llA 'on', the ablative -ltA 'off' and the allative -lle 'onto' the exterior series. Finnish has no surface series, which Hungarian has, and no dative, whose recipient function the allative covers, a gap Blake's hierarchy registers (Studies/Blake1994.lean).

The comparative label of the instructive, a case of manner and means as in jala-n 'on foot', is the instrumental.

Main definitions

• Finnish.Case, Finnish.Case.label: the cases, and the comparative value each is named for.

Main results

• Finnish.Case.toCase_mem_image_label_iff: the local cases are the interior and exterior series of the shared Localization × Direction decomposition.

The endings, spelled in segments, are in Finnish.Declension.

References

• [Kar18]
• [Bla94b]

inductive Finnish.Case : Type

The fifteen cases.

• nom : Case

  The nominative.

• gen : Case

  The genitive.

• acc : Case

  The accusative.

• part : Case

  The partitive.

• ine : Case

  The inessive.

• ela : Case

  The elative.

• ill : Case

  The illative.

• ade : Case

  The adessive.

• abl : Case

  The ablative.

• all : Case

  The allative.

• ess : Case

  The essive.

• transl : Case

  The translative.

• com : Case

  The comitative.

• abess : Case

  The abessive.

• instr : Case

  The instructive, of manner and means.

@[instance_reducible]

instance Finnish.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Finnish.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Finnish.instReprCase : Repr Case

Equations

• Finnish.instReprCase = { reprPrec := Finnish.instReprCase.repr }

def Finnish.instReprCase.repr : Case → ℕ → Std.Format

Equations

• Finnish.instReprCase.repr Finnish.Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.nom")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.gen")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.acc")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.part prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.part")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.ine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.ine")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.ela prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.ela")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.ill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.ill")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.ade prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.ade")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.abl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.abl")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.all")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.ess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.ess")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.transl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.transl")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.com prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.com")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.abess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.abess")).group prec✝
• Finnish.instReprCase.repr Finnish.Case.instr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Case.instr")).group prec✝

def Finnish.Case.label : Case → _root_.Case

The comparative value a case is named for, the instrumental for the instructive.

Equations

• Finnish.Case.nom.label = Case.nom
• Finnish.Case.gen.label = Case.gen
• Finnish.Case.acc.label = Case.acc
• Finnish.Case.part.label = Case.part
• Finnish.Case.ine.label = Case.ine
• Finnish.Case.ela.label = Case.ela
• Finnish.Case.ill.label = Case.ill
• Finnish.Case.ade.label = Case.ade
• Finnish.Case.abl.label = Case.abl
• Finnish.Case.all.label = Case.all
• Finnish.Case.ess.label = Case.ess
• Finnish.Case.transl.label = Case.transl
• Finnish.Case.com.label = Case.com
• Finnish.Case.abess.label = Case.abess
• Finnish.Case.instr.label = Case.inst

theorem Finnish.Case.toCase_mem_image_label_iff {r : Spatial.Localization} {d : Spatial.Path.Direction} {c : _root_.Case} (h : Case.toCase r d = some c) : c ∈ Finset.image label Finset.univ ↔ r ≠ Spatial.Localization.surface

The local cases are the interior and exterior series: a cell of the shared spatial decomposition is the label of a Finnish case exactly when its region is not the surface.