Russian agreement targets

This file defines the Russian agreement targets whose forms Wade's grammar tabulates, the long and the short adjective and the nonpast and the past finite verb, by their endings in each cell, and derives what each inflects for.

A cell gives a person, a number, a gender with its animacy subgender and a case, Russian having no definiteness. The long adjective is attributive and predicative and inflects for gender, number and case, its subgender showing in the accusative. The short adjective is predicative and inflects for gender and number. The nonpast verb of either conjugation inflects for person and number, and the past tense for gender and number but not person, so that the two tenses of the verb differ in what they agree in, as Corbett observes.

Implementation notes

Whether an inflected value is copied from a controller is a question about a position and is left to the studies: a predicative long form is inflected for case, but its case is fixed by the copula, nominative or instrumental (Wade §156), rather than shared with the subject.

The feminine instrumental singular of the long adjective has a variant -oju, which survives mainly in poetry (Wade §145) and which the table leaves out.

References

• [Wad20]
• [Cor98]

Cells

@[reducible, inline]

abbrev Russian.Agreement.Value : Agreement.Dimension → Type

The values Russian distinguishes in each dimension are the persons of the standard tripartition, the singular and the plural, the genders with their subgenders, and the six cases, and it distinguishes no definiteness.

Equations

• Russian.Agreement.Value Agreement.Dimension.person = { p : Person // ¬p.MarksClusivity }
• Russian.Agreement.Value Agreement.Dimension.number = ↥Russian.Gender.numberSystem.values
• Russian.Agreement.Value Agreement.Dimension.gender = (Russian.Gender.Value × Russian.Gender.Animacy)
• Russian.Agreement.Value Agreement.Dimension.case = Russian.Case
• Russian.Agreement.Value Agreement.Dimension.definiteness = Unit

@[reducible, inline]

abbrev Russian.Agreement.Cell : Type

A cell of a Russian paradigm, a value in each dimension.

Equations

• Russian.Agreement.Cell = ((d : Agreement.Dimension) → Russian.Agreement.Value d)

The long adjective

inductive Russian.Agreement.LongEnding : Type

The endings of the hard-stem long adjective.

• yj : LongEnding

  -yj (-ый).

• aja : LongEnding

  -aja (-ая).

• oe : LongEnding

  -oe (-ое).

• ye : LongEnding

  -ye (-ые).

• ogo : LongEnding

  -ogo (-ого).

• uju : LongEnding

  -uju (-ую).

• oj : LongEnding

  -oj (-ой).

• omu : LongEnding

  -omu (-ому).

• ym : LongEnding

  -ym (-ым).

• om : LongEnding

  -om (-ом).

• yx : LongEnding

  -yx (-ых).

• ymi : LongEnding

  -ymi (-ыми).

@[instance_reducible]

instance Russian.Agreement.instDecidableEqLongEnding : DecidableEq LongEnding

Equations

• Russian.Agreement.instDecidableEqLongEnding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Russian.Agreement.instReprLongEnding : Repr LongEnding

Equations

• Russian.Agreement.instReprLongEnding = { reprPrec := Russian.Agreement.instReprLongEnding.repr }

def Russian.Agreement.instReprLongEnding.repr : LongEnding → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Russian.Agreement.instFintypeLongEnding : Fintype LongEnding

Equations

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

def Russian.Agreement.LongEnding.form : LongEnding → String

e.form is the ending e in transliteration.

Equations

• Russian.Agreement.LongEnding.yj.form = "yj"
• Russian.Agreement.LongEnding.aja.form = "aja"
• Russian.Agreement.LongEnding.oe.form = "oe"
• Russian.Agreement.LongEnding.ye.form = "ye"
• Russian.Agreement.LongEnding.ogo.form = "ogo"
• Russian.Agreement.LongEnding.uju.form = "uju"
• Russian.Agreement.LongEnding.oj.form = "oj"
• Russian.Agreement.LongEnding.omu.form = "omu"
• Russian.Agreement.LongEnding.ym.form = "ym"
• Russian.Agreement.LongEnding.om.form = "om"
• Russian.Agreement.LongEnding.yx.form = "yx"
• Russian.Agreement.LongEnding.ymi.form = "ymi"

def Russian.Agreement.longEnding (g : Gender.Value) (a : Gender.Animacy) (n : ↥Gender.numberSystem.values) (c : Case) : LongEnding

The ending of the hard-stem long adjective nóvyj 'new' by the gender and subgender of its controller, its number and its case, the table of [Wad20] §145.

def Russian.Agreement.longAdjective : Agreement.Target Value LongEnding

The long adjective, used attributively and predicatively ([Wad20] §155, §156), inflects for gender, number and case.

Equations

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

theorem Russian.Agreement.longEnding_animate_acc_eq_gen_iff (g : Gender.Value) (n : ↥Gender.numberSystem.values) : longEnding g Gender.Animacy.animate n Case.acc = longEnding g Gender.Animacy.animate n Case.gen ↔ g = Gender.Value.masc ∨ ↑n = Number.plural

The animate accusative of the long adjective is its genitive exactly in the masculine singular and the plural ([Wad20] §47).

theorem Russian.Agreement.longEnding_inanimate_acc_eq_nom_iff (g : Gender.Value) (n : ↥Gender.numberSystem.values) : longEnding g Gender.Animacy.inanimate n Case.acc = longEnding g Gender.Animacy.inanimate n Case.nom ↔ g ≠ Gender.Value.fem ∨ ↑n = Number.plural

theorem Russian.Agreement.injective_longEnding_nom (a : Gender.Animacy) : Function.Injective fun (x : Gender.Value) => longEnding x a (Gender.numberSystem.value Number.singular injective_longEnding_nom._proof_1) Case.nom

The short adjective

inductive Russian.Agreement.ShortEnding : Type

The endings of the short adjective.

• zero : ShortEnding

  No ending.

• a : ShortEnding

  -a (-а).

• o : ShortEnding

  -o (-о).

• y : ShortEnding

  -y (-ы).

@[instance_reducible]

instance Russian.Agreement.instDecidableEqShortEnding : DecidableEq ShortEnding

Equations

• Russian.Agreement.instDecidableEqShortEnding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Russian.Agreement.instReprShortEnding : Repr ShortEnding

Equations

• Russian.Agreement.instReprShortEnding = { reprPrec := Russian.Agreement.instReprShortEnding.repr }

def Russian.Agreement.instReprShortEnding.repr : ShortEnding → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Russian.Agreement.instFintypeShortEnding : Fintype ShortEnding

Equations

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

def Russian.Agreement.shortEnding (g : Gender.Value) : ↥Gender.numberSystem.values → ShortEnding

The ending of the short adjective suróv 'severe' by gender and number ([Wad20] §159).

Equations

• One or more equations did not get rendered due to their size.
• Russian.Agreement.shortEnding Russian.Gender.Value.fem = Russian.Gender.numberSystem.elim Russian.Agreement.ShortEnding.a Russian.Agreement.ShortEnding.y Russian.Agreement.longEnding._proof_5
• Russian.Agreement.shortEnding Russian.Gender.Value.neut = Russian.Gender.numberSystem.elim Russian.Agreement.ShortEnding.o Russian.Agreement.ShortEnding.y Russian.Agreement.longEnding._proof_5

def Russian.Agreement.shortAdjective : Agreement.Target Value ShortEnding

The short adjective, used predicatively ([Wad20] §144), inflects for gender and number.

Equations

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

The finite verb

inductive Russian.Agreement.Conjugation : Type

The two conjugations, of the endings in -e- and in -i- ([Wad20] §213).

• first : Conjugation
• second : Conjugation

@[instance_reducible]

instance Russian.Agreement.instDecidableEqConjugation : DecidableEq Conjugation

Equations

• Russian.Agreement.instDecidableEqConjugation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Russian.Agreement.instReprConjugation.repr : Conjugation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Russian.Agreement.instReprConjugation : Repr Conjugation

Equations

• Russian.Agreement.instReprConjugation = { reprPrec := Russian.Agreement.instReprConjugation.repr }

@[instance_reducible]

instance Russian.Agreement.instFintypeConjugation : Fintype Conjugation

Equations

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

inductive Russian.Agreement.NonpastEnding : Type

The endings of the nonpast.

• u : NonpastEnding

  -u (-ю, or -у after a consonant).

• eš' : NonpastEnding

  -eš' (-ешь).

• et : NonpastEnding

  -et (-ет).

• em : NonpastEnding

  -em (-ем).

• ete : NonpastEnding

  -ete (-ете).

• ut : NonpastEnding

  -ut (-ют, or -ут after a consonant).

• iš' : NonpastEnding

  -iš' (-ишь).

• it : NonpastEnding

  -it (-ит).

• im : NonpastEnding

  -im (-им).

• ite : NonpastEnding

  -ite (-ите).

• at : NonpastEnding

  -at (-ят, or -ат after a palatal sibilant).

@[instance_reducible]

instance Russian.Agreement.instDecidableEqNonpastEnding : DecidableEq NonpastEnding

Equations

• Russian.Agreement.instDecidableEqNonpastEnding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Russian.Agreement.instReprNonpastEnding.repr : NonpastEnding → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Russian.Agreement.instReprNonpastEnding : Repr NonpastEnding

Equations

• Russian.Agreement.instReprNonpastEnding = { reprPrec := Russian.Agreement.instReprNonpastEnding.repr }

@[instance_reducible]

instance Russian.Agreement.instFintypeNonpastEnding : Fintype NonpastEnding

Equations

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

def Russian.Agreement.nonpastEnding (k : Conjugation) (p : Person) : ↥Gender.numberSystem.values → NonpastEnding

The nonpast ending by conjugation, person and number ([Wad20] §213). Clusivity is not distinguished, so both first persons take the first person's ending.

def Russian.Agreement.nonpastVerb (k : Conjugation) : Agreement.Target Value NonpastEnding

The nonpast finite verb of each conjugation is predicative and inflects for person and number.

Equations

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

inductive Russian.Agreement.PastEnding : Type

The endings of the past tense, added to its -l-.

• zero : PastEnding

  No ending.

• a : PastEnding

  -a (-а).

• o : PastEnding

  -o (-о).

• i : PastEnding

  -i (-и).

@[instance_reducible]

instance Russian.Agreement.instDecidableEqPastEnding : DecidableEq PastEnding

Equations

• Russian.Agreement.instDecidableEqPastEnding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Russian.Agreement.instReprPastEnding : Repr PastEnding

Equations

• Russian.Agreement.instReprPastEnding = { reprPrec := Russian.Agreement.instReprPastEnding.repr }

def Russian.Agreement.instReprPastEnding.repr : PastEnding → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Russian.Agreement.instFintypePastEnding : Fintype PastEnding

Equations

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

def Russian.Agreement.pastEnding (g : Gender.Value) : ↥Gender.numberSystem.values → PastEnding

The past ending by gender and number ([Wad20] §230).

Equations

• Russian.Agreement.pastEnding Russian.Gender.Value.masc = Russian.Gender.numberSystem.elim Russian.Agreement.PastEnding.zero Russian.Agreement.PastEnding.i Russian.Agreement.longEnding._proof_5
• Russian.Agreement.pastEnding Russian.Gender.Value.fem = Russian.Gender.numberSystem.elim Russian.Agreement.PastEnding.a Russian.Agreement.PastEnding.i Russian.Agreement.longEnding._proof_5
• Russian.Agreement.pastEnding Russian.Gender.Value.neut = Russian.Gender.numberSystem.elim Russian.Agreement.PastEnding.o Russian.Agreement.PastEnding.i Russian.Agreement.longEnding._proof_5

def Russian.Agreement.pastVerb : Agreement.Target Value PastEnding

The past finite verb is predicative and inflects for gender and number, ja pisal or ja pisala 'I was writing' by the speaker's gender ([Wad20] §230).

Equations

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

theorem Russian.Agreement.injective_pastEnding : Function.Injective fun (x : Gender.Value) => pastEnding x (Gender.numberSystem.value Number.singular injective_longEnding_nom._proof_1)