Korean case markers

Korean marks case with postpositional particles, which Sohn treats as bound words rather than clitics, several with allomorphs chosen by the final segment of the noun: the nominative -i after a consonant and -ga after a vowel, the accusative -eul and -reul, the genitive -ui, the dative -ege, colloquially -hante and to a social superior -kke, the locative -e of a state and goal and -eseo of an action and source, the ablative -buteo, the instrumental and directional -(eu)ro, and the comitative, formal -gwa and -wa and informal -hago and -(i)rang ([Soh99], p. 339). Casual speech drops the nominative, accusative, genitive and dative particles. Forms are in the Revised Romanization; Sohn writes ka, (l)ul, uy, eykey, hanthey, kkey, ey, eyse, pwuthe, (u)lo and (k)wa.

Main definitions

• Korean.Case, Korean.Case.exponents: the case particles, with their allomorphs.
• Korean.Case.label, Korean.Case.functions: the comparative value each is named for, and the values it expresses.

References

• [Soh94]
• [Soh99]

inductive Korean.Case : Type

The case particles.

• ga : Case

  The nominative -i after a consonant and -ga after a vowel.

• reul : Case

  The accusative -eul after a consonant and -reul after a vowel.

• ui : Case

  The genitive -ui.

• ege : Case

  The dative -ege, colloquially -hante.

• kke : Case

  The honorific dative -kke.

• e : Case

  -e, the locative of a state and the goal of motion.

• eseo : Case

  -eseo, the locative of an action and the source of motion.

• buteo : Case

  The ablative -buteo 'from', also after -eseo and -(eu)ro.

• ro : Case

  -(eu)ro, the instrumental and the directional 'toward'.

• wa : Case

  The comitative -gwa after a consonant and -wa after a vowel, -hago, and the casual -(i)rang.

@[instance_reducible]

instance Korean.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Korean.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Korean.instReprCase : Repr Case

Equations

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

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

Equations

• Korean.instReprCase.repr Korean.Case.ga prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Case.ga")).group prec✝
• Korean.instReprCase.repr Korean.Case.reul prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Case.reul")).group prec✝
• Korean.instReprCase.repr Korean.Case.ui prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Case.ui")).group prec✝
• Korean.instReprCase.repr Korean.Case.ege prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Case.ege")).group prec✝
• Korean.instReprCase.repr Korean.Case.kke prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Case.kke")).group prec✝
• Korean.instReprCase.repr Korean.Case.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Case.e")).group prec✝
• Korean.instReprCase.repr Korean.Case.eseo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Case.eseo")).group prec✝
• Korean.instReprCase.repr Korean.Case.buteo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Case.buteo")).group prec✝
• Korean.instReprCase.repr Korean.Case.ro prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Case.ro")).group prec✝
• Korean.instReprCase.repr Korean.Case.wa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Korean.Case.wa")).group prec✝

def Korean.Case.exponents : Case → List Morphology.Morph

The forms of a particle, its allomorphs and variants, with a segment in parentheses where one allomorph lacks it.

Equations

• Korean.Case.ga.exponents = [Morphology.Morph.encl "i", Morphology.Morph.encl "ga"]
• Korean.Case.reul.exponents = [Morphology.Morph.encl "eul", Morphology.Morph.encl "reul"]
• Korean.Case.ui.exponents = [Morphology.Morph.encl "ui"]
• Korean.Case.ege.exponents = [Morphology.Morph.encl "ege", Morphology.Morph.encl "hante"]
• Korean.Case.kke.exponents = [Morphology.Morph.encl "kke"]
• Korean.Case.e.exponents = [Morphology.Morph.encl "e"]
• Korean.Case.eseo.exponents = [Morphology.Morph.encl "eseo"]
• Korean.Case.buteo.exponents = [Morphology.Morph.encl "buteo"]
• Korean.Case.ro.exponents = [Morphology.Morph.encl "(eu)ro"]
• Korean.Case.wa.exponents = [Morphology.Morph.encl "(g)wa", Morphology.Morph.encl "hago", Morphology.Morph.encl "(i)rang"]

def Korean.Case.label : Case → _root_.Case

The comparative value a particle is named for.

Equations

• Korean.Case.ga.label = Case.nom
• Korean.Case.reul.label = Case.acc
• Korean.Case.ui.label = Case.gen
• Korean.Case.ege.label = Case.dat
• Korean.Case.kke.label = Case.dat
• Korean.Case.e.label = Case.loc
• Korean.Case.eseo.label = Case.loc
• Korean.Case.buteo.label = Case.abl
• Korean.Case.ro.label = Case.inst
• Korean.Case.wa.label = Case.com

def Korean.Case.functions : Case → Finset _root_.Case

The comparative values a particle expresses: -e also the goal, -eseo also the source, and -(eu)ro also the direction of motion.

Equations

• Korean.Case.e.functions = {Case.loc, Case.all}
• Korean.Case.eseo.functions = {Case.loc, Case.abl}
• Korean.Case.ro.functions = {Case.inst, Case.all}
• x✝.functions = {x✝.label}

theorem Korean.Case.label_mem_functions (c : Case) : c.label ∈ c.functions