Tanti Dargwa case

This file defines the grammatical cases of Tanti Dargwa as Sumbatova describes them. A noun has a direct stem, its absolutive singular, and an oblique stem, the direct stem with -li, which is its ergative singular and the base of most other forms. The dative and the comitative add their suffix to the oblique stem, as do the locative forms of Locatives.lean, while the absolutive and the adverbial are built on the direct stem. Tanti has the absolutive, ergative, genitive, dative and comitative of most Dargwa varieties and an adverbial case of nominal and secondary predicates besides, which goes under the comparative label of the essive. The alignment is ergative without a split, A ergative and S and P absolutive.

Main definitions

• Dargwa.Case, Dargwa.Case.label: the six cases, and the comparative value each is named for
• Dargwa.obliqueStem: the oblique stem suffix -li
• Dargwa.Case.exponent: the suffixes of a case after the direct stem
• Dargwa.marking: the ergative marking of the core arguments

Main results

• Dargwa.Case.builtOnOblique_iff: the ergative, dative and comitative are the cases built on the oblique stem
• Dargwa.label_comp_marking: the marking is the ergative alignment

Implementation notes

• The genitive is -la, or -lla for some nouns, and for some nouns is built on the oblique stem; the exponent records the -la of dubur-la 'mountain's'. The plural builds its oblique forms on an oblique plural stem, the absolutive plural with -a, which is not treated.

References

• N. Sumbatova, Dargwa (2021)

def Dargwa.obliqueStem : Morphology.Morph

The oblique stem suffix -li. The oblique singular stem is the direct stem with it, and is the ergative singular.

Equations

• Dargwa.obliqueStem = Morphology.Morph.suff "li"

inductive Dargwa.Case : Type

The six grammatical cases.

• abs : Case

  The absolutive, the direct stem.

• erg : Case

  The ergative, the oblique stem.

• gen : Case

  The genitive.

• dat : Case

  The dative.

• com : Case

  The comitative.

• adv : Case

  The adverbial, of nominal and secondary predicates.

@[instance_reducible]

instance Dargwa.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Dargwa.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Dargwa.instReprCase : Repr Case

Equations

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

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

Equations

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

def Dargwa.Case.label : Case → _root_.Case

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

Equations

• Dargwa.Case.abs.label = Case.abs
• Dargwa.Case.erg.label = Case.erg
• Dargwa.Case.gen.label = Case.gen
• Dargwa.Case.dat.label = Case.dat
• Dargwa.Case.com.label = Case.com
• Dargwa.Case.adv.label = Case.ess

def Dargwa.Case.exponent : Case → List Morphology.Morph

The suffixes of a case after the direct singular stem. The absolutive is unmarked, the ergative is the oblique stem, the genitive takes -la, the dative -ž and the comitative -cːele on the oblique stem, and the adverbial -le.

Equations

• Dargwa.Case.abs.exponent = []
• Dargwa.Case.erg.exponent = [Dargwa.obliqueStem]
• Dargwa.Case.gen.exponent = [Morphology.Morph.suff "la"]
• Dargwa.Case.dat.exponent = [Dargwa.obliqueStem, Morphology.Morph.suff "ž"]
• Dargwa.Case.com.exponent = [Dargwa.obliqueStem, Morphology.Morph.suff "cːele"]
• Dargwa.Case.adv.exponent = [Morphology.Morph.suff "le"]

def Dargwa.Case.BuiltOnOblique (c : Case) : Prop

A case is built on the oblique stem when its exponent begins with the stem suffix.

Equations

• c.BuiltOnOblique = (c.exponent.head? = some Dargwa.obliqueStem)

@[instance_reducible]

instance Dargwa.Case.instDecidablePredBuiltOnOblique : DecidablePred BuiltOnOblique

Equations

• x✝.instDecidablePredBuiltOnOblique = Dargwa.Case.instDecidablePredBuiltOnOblique._aux_1 x✝

theorem Dargwa.Case.builtOnOblique_iff (c : Case) : c.BuiltOnOblique ↔ c = erg ∨ c = dat ∨ c = com

The ergative, dative and comitative are the cases built on the oblique stem.

def Dargwa.marking : ArgumentRole → Case

The marking of the core arguments is ergative, A ergative and S and P absolutive, with no split by tense or aspect.

Equations

• Dargwa.marking ArgumentRole.A = Dargwa.Case.erg
• Dargwa.marking ArgumentRole.S = Dargwa.Case.abs
• Dargwa.marking ArgumentRole.P = Dargwa.Case.abs
• Dargwa.marking ArgumentRole.R = Dargwa.Case.abs
• Dargwa.marking ArgumentRole.T = Dargwa.Case.abs

theorem Dargwa.label_comp_marking : Case.label ∘ marking = Alignment.ergative

The marking is the ergative alignment.