Tanti Dargwa locative forms

This file defines the locative forms of Tanti Dargwa as Sumbatova describes them. A locative form is the oblique stem followed by three suffix slots: a localization, the domain in space with respect to the reference point, of which Tanti has eight; an orientation, whether the object is in that domain, moving towards it, from it or across it; and a direction of the motion with respect to the speaker, which the essive lacks, the elative requires and the lative admits. The translative combines only with the localizations sub, ante and post, and post with the translative alone. The orientations are the path heads of Pantcheva's decomposition and the localizations refine its regions, so the forms fill the region-by-path grid except for the route outside the exterior. An elative without the direction marker the spatial paradigm demands has a non-locative use, as the causee of a transitive causative and the standard of comparison.

Main definitions

• Dargwa.Localization, Dargwa.Orientation, Dargwa.Direction: the three categories with their suffixes, and Localization.region and Orientation.pathDir their comparative labels
• Dargwa.LocativeForm: a form, with LocativeForm.morphs its suffixes and LocativeForm.IsSpatial the combinatorics of the spatial paradigm
• Dargwa.comparisonStandard: the super-elative of the standard of comparison

Main results

• Dargwa.LocativeForm.not_isSpatial_elative_none: no directionless elative is spatial
• Dargwa.LocativeForm.isSpatial_post_iff: post takes the translative alone
• Dargwa.LocativeForm.exists_isSpatial_iff: the region-by-path grid is filled except for the route outside the exterior

Implementation notes

• The essive is the localization followed by the gender marker, so morphs takes the marker.
• The direction suffixes are cited in their long forms; the short forms drop -le, and -sale and -dale vary with -sele and -dele. Whether the translative takes a direction marker is not stated, so IsSpatial leaves it open.
• The general-localization form of some nouns, kis-na-b 'in the pocket', is irregular and left out, as are the locative adverbs and postpositions, which inflect for orientation.

References

• N. Sumbatova, Dargwa (2021)
• M. Pantcheva, Decomposing Path: The Nanosyntax of Directional Expressions (2011)

Localization

inductive Dargwa.Localization : Type

A localization is the domain in space a locative form specifies with respect to the reference point.

• super : Localization

  super -ja, on the surface of the object.

• sub : Localization

  sub -gu, under the object.

• ante : Localization

  ante -sa, in front of the object.

• in_ : Localization

  in -ʜe, -ʜaˁ for some nouns, inside a container.

• inter : Localization

  inter -cːe, in a solid substance.

• apud : Localization

  apud -hira, near the object.

• ad : Localization

  ad -šːu, in the place functionally associated with the object.

• post : Localization

  post -hi, behind the object.

@[instance_reducible]

instance Dargwa.instDecidableEqLocalization : DecidableEq Localization

Equations

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

@[instance_reducible]

instance Dargwa.instReprLocalization : Repr Localization

Equations

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

def Dargwa.instReprLocalization.repr : Localization → ℕ → Std.Format

Equations

• Dargwa.instReprLocalization.repr Dargwa.Localization.super prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Localization.super")).group prec✝
• Dargwa.instReprLocalization.repr Dargwa.Localization.sub prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Localization.sub")).group prec✝
• Dargwa.instReprLocalization.repr Dargwa.Localization.ante prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Localization.ante")).group prec✝
• Dargwa.instReprLocalization.repr Dargwa.Localization.in_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Localization.in_")).group prec✝
• Dargwa.instReprLocalization.repr Dargwa.Localization.inter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Localization.inter")).group prec✝
• Dargwa.instReprLocalization.repr Dargwa.Localization.apud prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Localization.apud")).group prec✝
• Dargwa.instReprLocalization.repr Dargwa.Localization.ad prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Localization.ad")).group prec✝
• Dargwa.instReprLocalization.repr Dargwa.Localization.post prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Localization.post")).group prec✝

@[instance_reducible]

instance Dargwa.instFintypeLocalization : Fintype Localization

Equations

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

def Dargwa.Localization.suffix : Localization → Morphology.Morph

The localization suffix.

Equations

• Dargwa.Localization.super.suffix = Morphology.Morph.suff "ja"
• Dargwa.Localization.sub.suffix = Morphology.Morph.suff "gu"
• Dargwa.Localization.ante.suffix = Morphology.Morph.suff "sa"
• Dargwa.Localization.in_.suffix = Morphology.Morph.suff "ʜe"
• Dargwa.Localization.inter.suffix = Morphology.Morph.suff "cːe"
• Dargwa.Localization.apud.suffix = Morphology.Morph.suff "hira"
• Dargwa.Localization.ad.suffix = Morphology.Morph.suff "šːu"
• Dargwa.Localization.post.suffix = Morphology.Morph.suff "hi"

def Dargwa.Localization.region : Localization → Spatial.Localization

The region of the comparative decomposition a localization falls in. super is the surface, in and inter are the interior and the rest are the exterior.

Equations

• Dargwa.Localization.super.region = Spatial.Localization.surface
• Dargwa.Localization.in_.region = Spatial.Localization.interior
• Dargwa.Localization.inter.region = Spatial.Localization.interior
• Dargwa.Localization.sub.region = Spatial.Localization.exterior
• Dargwa.Localization.ante.region = Spatial.Localization.exterior
• Dargwa.Localization.apud.region = Spatial.Localization.exterior
• Dargwa.Localization.ad.region = Spatial.Localization.exterior
• Dargwa.Localization.post.region = Spatial.Localization.exterior

def Dargwa.Localization.TakesTranslative (l : Localization) : Prop

The localizations the translative combines with.

Equations

• l.TakesTranslative = (l = Dargwa.Localization.sub ∨ l = Dargwa.Localization.ante ∨ l = Dargwa.Localization.post)

@[instance_reducible]

instance Dargwa.instDecidablePredLocalizationTakesTranslative : DecidablePred Localization.TakesTranslative

Equations

• Dargwa.instDecidablePredLocalizationTakesTranslative l = id inferInstance

Orientation

inductive Dargwa.Orientation : Type

An orientation is the motion, or its absence, with respect to the reference point.

• lative : Orientation

  The lative, unmarked, motion towards the reference point.

• elative : Orientation

  The elative -r, motion from the reference point.

• essive : Orientation

  The essive, the gender marker after the localization, location in the reference point.

• translative : Orientation

  The translative -tːi, motion across the reference point.

@[instance_reducible]

instance Dargwa.instDecidableEqOrientation : DecidableEq Orientation

Equations

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

@[instance_reducible]

instance Dargwa.instReprOrientation : Repr Orientation

Equations

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

def Dargwa.instReprOrientation.repr : Orientation → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Dargwa.instReprOrientation.repr Dargwa.Orientation.lative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Orientation.lative")).group prec✝
• Dargwa.instReprOrientation.repr Dargwa.Orientation.elative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Orientation.elative")).group prec✝
• Dargwa.instReprOrientation.repr Dargwa.Orientation.essive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Orientation.essive")).group prec✝

@[instance_reducible]

instance Dargwa.instFintypeOrientation : Fintype Orientation

Equations

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

def Dargwa.Orientation.morphs : Orientation → Gender.Marker → List Morphology.Morph

The orientation suffixes, with the gender marker g the essive takes.

Equations

• Dargwa.Orientation.lative.morphs x✝ = []
• Dargwa.Orientation.elative.morphs x✝ = [Morphology.Morph.suff "r"]
• Dargwa.Orientation.essive.morphs x✝ = [Morphology.Morph.suff x✝.form]
• Dargwa.Orientation.translative.morphs x✝ = [Morphology.Morph.suff "tːi"]

def Dargwa.Orientation.pathDir : Orientation → Spatial.Path.Direction

The path head of the comparative decomposition an orientation expresses.

Equations

• Dargwa.Orientation.essive.pathDir = Spatial.Path.Direction.place
• Dargwa.Orientation.lative.pathDir = Spatial.Path.Direction.goal
• Dargwa.Orientation.elative.pathDir = Spatial.Path.Direction.source
• Dargwa.Orientation.translative.pathDir = Spatial.Path.Direction.route

Direction

inductive Dargwa.Direction : Type

A direction orients the motion with respect to the speaker or another point of reference.

• up : Direction

  -ha(le), upward.

• down : Direction

  -ka(le), downward.

• hither : Direction

  -se(le) or -sale, towards the speaker.

• thither : Direction

  -de(le) or -dale, away from the speaker.

@[instance_reducible]

instance Dargwa.instDecidableEqDirection : DecidableEq Direction

Equations

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

def Dargwa.instReprDirection.repr : Direction → ℕ → Std.Format

Equations

• Dargwa.instReprDirection.repr Dargwa.Direction.up prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Direction.up")).group prec✝
• Dargwa.instReprDirection.repr Dargwa.Direction.down prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Direction.down")).group prec✝
• Dargwa.instReprDirection.repr Dargwa.Direction.hither prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Direction.hither")).group prec✝
• Dargwa.instReprDirection.repr Dargwa.Direction.thither prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.Direction.thither")).group prec✝

@[instance_reducible]

instance Dargwa.instReprDirection : Repr Direction

Equations

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

@[instance_reducible]

instance Dargwa.instFintypeDirection : Fintype Direction

Equations

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

def Dargwa.Direction.suffix : Direction → Morphology.Morph

The direction suffix, in its long form.

Equations

• Dargwa.Direction.up.suffix = Morphology.Morph.suff "hale"
• Dargwa.Direction.down.suffix = Morphology.Morph.suff "kale"
• Dargwa.Direction.hither.suffix = Morphology.Morph.suff "sele"
• Dargwa.Direction.thither.suffix = Morphology.Morph.suff "dele"

Locative forms

structure Dargwa.LocativeForm : Type

A locative form is a localization, an orientation and, where the form has one, a direction.

• localization : Localization
• orientation : Orientation
• direction : Option Direction

def Dargwa.instDecidableEqLocativeForm.decEq (x✝ x✝¹ : LocativeForm) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Dargwa.instDecidableEqLocativeForm : DecidableEq LocativeForm

Equations

• Dargwa.instDecidableEqLocativeForm = Dargwa.instDecidableEqLocativeForm.decEq

@[instance_reducible]

instance Dargwa.instReprLocativeForm : Repr LocativeForm

Equations

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

def Dargwa.instReprLocativeForm.repr : LocativeForm → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Dargwa.instFintypeLocativeForm : Fintype LocativeForm

Equations

• Dargwa.instFintypeLocativeForm = Fintype.ofEquiv ((_ : Dargwa.Localization) × (_ : Dargwa.Orientation) × Option Dargwa.Direction) Dargwa.LocativeForm.proxyTypeEquiv

def Dargwa.LocativeForm.morphs (f : LocativeForm) (g : Gender.Marker) : List Morphology.Morph

The suffixes of a locative form after the oblique stem, with the gender marker g in the essive.

Equations

• f.morphs g = f.localization.suffix :: (f.orientation.morphs g ++ (Option.map Dargwa.Direction.suffix f.direction).toList)

def Dargwa.LocativeForm.IsSpatial (f : LocativeForm) : Prop

A form is spatial when its slots combine as the paradigm allows. The essive takes no direction marker, the elative requires one and the lative admits one; the translative combines only with the localizations that take it, and post only with the translative.

Equations

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

@[instance_reducible]

instance Dargwa.LocativeForm.instDecidablePredIsSpatial : DecidablePred IsSpatial

Equations

• f.instDecidablePredIsSpatial = id inferInstance

theorem Dargwa.LocativeForm.super_elative_hither : { localization := Localization.super, orientation := Orientation.elative, direction := some Direction.hither }.IsSpatial ∧ { localization := Localization.super, orientation := Orientation.elative, direction := some Direction.hither }.morphs Gender.Marker.b = [Morphology.Morph.suff "ja", Morphology.Morph.suff "r", Morphology.Morph.suff "sele"]

kːumi-li-ja-r-sele 'from the bridge hither' is the super-elative with the direction hither, a spatial form whose suffixes the slots derive.

theorem Dargwa.LocativeForm.not_isSpatial_elative_none (l : Localization) : ¬{ localization := l, orientation := Orientation.elative, direction := none }.IsSpatial

No elative without a direction marker is spatial.

theorem Dargwa.LocativeForm.isSpatial_essive {l : Localization} (h : l ≠ Localization.post) : { localization := l, orientation := Orientation.essive, direction := none }.IsSpatial

The essive of every localization but post is spatial.

theorem Dargwa.LocativeForm.isSpatial_lative {l : Localization} (d : Option Direction) (h : l ≠ Localization.post) : { localization := l, orientation := Orientation.lative, direction := d }.IsSpatial

The lative of every localization but post is spatial, with or without a direction.

theorem Dargwa.LocativeForm.isSpatial_elative_some {l : Localization} (d : Direction) (h : l ≠ Localization.post) : { localization := l, orientation := Orientation.elative, direction := some d }.IsSpatial

The elative with a direction of every localization but post is spatial.

theorem Dargwa.LocativeForm.isSpatial_translative_iff {l : Localization} {d : Option Direction} : { localization := l, orientation := Orientation.translative, direction := d }.IsSpatial ↔ l.TakesTranslative

The translative is spatial exactly with the localizations that take it.

theorem Dargwa.LocativeForm.isSpatial_post_iff {o : Orientation} {d : Option Direction} : { localization := Localization.post, orientation := o, direction := d }.IsSpatial ↔ o = Orientation.translative

post takes the translative alone.

theorem Dargwa.LocativeForm.exists_isSpatial_iff (r : Spatial.Localization) (d : Spatial.Path.Direction) : (∃ (f : LocativeForm), f.IsSpatial ∧ f.localization.region = r ∧ f.orientation.pathDir = d) ↔ d ≠ Spatial.Path.Direction.route ∨ r = Spatial.Localization.exterior

The forms fill the grid of regions and path heads except for the route, which the translative expresses, outside the exterior.

def Dargwa.comparisonStandard : LocativeForm

The super-elative without a direction marker of the standard of comparison.

Equations

• Dargwa.comparisonStandard = { localization := Dargwa.Localization.super, orientation := Dargwa.Orientation.elative, direction := none }

theorem Dargwa.not_isSpatial_comparisonStandard : ¬comparisonStandard.IsSpatial

The standard of comparison is not a spatial form.