Georgian case

Georgian has seven cases, the nominative, vocative, dative, ergative, genitive, instrumental and adverbial, in essentially one declension for all nouns ([Hew95] §3.1, p. 33). The modern plural adds the same endings to the plural suffix -eb-. The older plural, still found in archaising styles, has its own nominative and vocative and one portmanteau for the other cases, rare if attested at all in the instrumental and the adverbial (pp. 33–34).

Main definitions

• Georgian.Case, Georgian.Case.label: the seven cases, and the comparative value each is named for.
• Georgian.kaci: the declension of k'ac-i 'man', singular, plural and older plural (p. 34).

Main results

• Georgian.singular_kaci_injective, Georgian.plural_kaci_injective: the modern declension keeps the seven cases apart in both numbers.
• Georgian.oldPlural_kaci_oblique: the older plural has one form for the dative, ergative and genitive.

Implementation notes

The forms are Hewitt's, with the long variants of the four endings that have them in parentheses. The older plural of the instrumental and the adverbial, which Hewitt gives in parentheses as rarely attested, is left out.

References

• [Hew95]

inductive Georgian.Case : Type

The seven cases, in Hewitt's order.

• nom : Case

  The nominative.

• voc : Case

  The vocative.

• dat : Case

  The dative.

• erg : Case

  The ergative.

• gen : Case

  The genitive.

• inst : Case

  The instrumental.

• adv : Case

  The adverbial, as in briq'v-ada 'as an idiot' (p. 34).

@[instance_reducible]

instance Georgian.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Georgian.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Georgian.instReprCase : Repr Case

Equations

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

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

Equations

• Georgian.instReprCase.repr Georgian.Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.Case.nom")).group prec✝
• Georgian.instReprCase.repr Georgian.Case.voc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.Case.voc")).group prec✝
• Georgian.instReprCase.repr Georgian.Case.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.Case.dat")).group prec✝
• Georgian.instReprCase.repr Georgian.Case.erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.Case.erg")).group prec✝
• Georgian.instReprCase.repr Georgian.Case.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.Case.gen")).group prec✝
• Georgian.instReprCase.repr Georgian.Case.inst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.Case.inst")).group prec✝
• Georgian.instReprCase.repr Georgian.Case.adv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Georgian.Case.adv")).group prec✝

def Georgian.Case.label : Case → _root_.Case

The comparative value a case is named for, the essive for the adverbial.

Equations

• Georgian.Case.nom.label = Case.nom
• Georgian.Case.voc.label = Case.voc
• Georgian.Case.dat.label = Case.dat
• Georgian.Case.erg.label = Case.erg
• Georgian.Case.gen.label = Case.gen
• Georgian.Case.inst.label = Case.inst
• Georgian.Case.adv.label = Case.ess

def Georgian.Case.forms {α : Type u_1} (nom voc dat erg gen inst adv : α) : Case → α

forms nom voc dat erg gen inst adv assigns each case its form.

Equations

• Georgian.Case.forms nom voc dat erg gen inst adv Georgian.Case.nom = nom
• Georgian.Case.forms nom voc dat erg gen inst adv Georgian.Case.voc = voc
• Georgian.Case.forms nom voc dat erg gen inst adv Georgian.Case.dat = dat
• Georgian.Case.forms nom voc dat erg gen inst adv Georgian.Case.erg = erg
• Georgian.Case.forms nom voc dat erg gen inst adv Georgian.Case.gen = gen
• Georgian.Case.forms nom voc dat erg gen inst adv Georgian.Case.inst = inst
• Georgian.Case.forms nom voc dat erg gen inst adv Georgian.Case.adv = adv

def Georgian.kaci.singular : Case → String

The singular of k'ac-i 'man'.

Equations

• Georgian.kaci.singular = Georgian.Case.forms "k'ac-i" "k'ac-o" "k'ac-s(a)" "k'ac-ma" "k'ac-is(a)" "k'ac-it(a)" "k'ac-ad(a)"

def Georgian.kaci.plural : Case → String

The plural of k'ac-i 'man'.

Equations

• Georgian.kaci.plural = Georgian.Case.forms "k'ac-eb-i" "k'ac-eb-o" "k'ac-eb-s(a)" "k'ac-eb-ma" "k'ac-eb-is(a)" "k'ac-eb-it(a)" "k'ac-eb-ad(a)"

def Georgian.kaci.oldPlural : Case → Option String

The older plural of k'ac-i 'man', where it is attested.

Equations

• Georgian.kaci.oldPlural = Georgian.Case.forms (some "k'ac-n-i") (some "k'ac-n-o") (some "k'ac-t(a)") (some "k'ac-t(a)") (some "k'ac-t(a)") none none

theorem Georgian.singular_kaci_injective : Function.Injective kaci.singular

The modern singular keeps the seven cases apart.

theorem Georgian.plural_kaci_injective : Function.Injective kaci.plural

The modern plural keeps the seven cases apart.

theorem Georgian.oldPlural_kaci_oblique : kaci.oldPlural Case.dat = kaci.oldPlural Case.erg ∧ kaci.oldPlural Case.erg = kaci.oldPlural Case.gen

The older plural has one form for the dative, ergative and genitive.