Czech nouns

This file defines the Czech noun as a lexical entry with its controller gender, its declension class and the nominative plural it takes lexically, and gives the model nouns of Short's declension tables and kluk 'boy', the nouns the grammars name as changing class with number, and the nouns of Stump's tables of Czech heteroclisis, whose classes follow from Short's grammar and the Academy grammar Mluvnice češtiny.

A noun's class is that of its singular, and its plural follows the same class unless the noun changes class with number: "Modern masculines like den 'day' and kořen 'root' generally follow stroj in the singular and hrady in the plural" (Short, p. 469), and Mluvnice češtiny gives the masculines with a stem in -en-, kořen and pramen among them, the soft declension in the singular and the hard one in the plural (p. 310). The stem is the citation form less the nominative singular ending of its class.

Where a class leaves the nominative plural of the masculine animates open, Mluvnice češtiny assigns it noun by noun: its three endings -i, -ové and -é are taken "buď jen jednu, nebo dvě" 'either only one or two' by a noun (pp. 292–293). An entry records the endings the grammar assigns it, and its forms are those of its class with these endings in the nominative and vocative plural.

Main definitions

• Czech.Noun: a noun with its controller gender, its class in each number and its lexical nominative plural
• Czech.Noun.clsAt, Czech.Noun.stem: the class of a number, and the stem
• Czech.Noun.endingsIn, Czech.Noun.endings, Czech.Noun.forms: a noun's endings in a class, its endings and its forms
• Czech.nouns: the entries

Main results

• Czech.stem_append_nomSg: every entry's citation form is its stem followed by the nominative singular ending of its class
• Czech.gender_eq_cls_gender: every entry has the gender of its class's table
• Czech.isVelar_stem_iff, Czech.isSome_ofChars_forms: the velar stems are those of kluk, sluha and filolog, and every form is written in Czech letters
• Czech.forms_examples: the forms the grammars give Stump's nouns in the cells where they depart from the model nouns' tables

Implementation notes

The stem is that of the nominative singular. Short's e ~ ∅ alternation between the nominative singular and the oblique cases, as den/dne (p. 463), gives den an oblique stem dn- that Noun.stem does not record, and the stem of jehně is written jehň- before the plural endings (p. 459). The hard forms that Mluvnice češtiny says enter the singular of the -en- stems (p. 310) are not recorded, the grammar naming no cell they occupy. A lexical nominative plural is recorded only where Mluvnice češtiny names the noun, Short placing none of the entries among the subclasses with a nominative plural in -é or -ové (p. 466).

References

• [Sho93a]
• [KKP+86]
• [Stu06]

structure Czech.Nounextends GenderedNoun Czech.Gender.Value : Type

A Czech noun with its controller gender, its declension class in each number, and the nominative plural it takes lexically.

• form : String
• gloss : String
• gender : Czech.Gender.Value
• naturalGender : Option Gender
• cls : Declension.Class

  The class of the singular.

• clsPlural : Declension.Class

  The class of the plural, that of the singular unless the noun changes class.

• nomPlural : Option (List (List String))

  The nominative and vocative plural endings the grammar assigns the noun lexically, where its class leaves a choice, or none where the noun takes its class's.

def Czech.instDecidableEqNoun.decEq (x✝ x✝¹ : Noun) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Czech.instDecidableEqNoun : DecidableEq Noun

Equations

• Czech.instDecidableEqNoun = Czech.instDecidableEqNoun.decEq

@[instance_reducible]

instance Czech.instReprNoun : Repr Noun

Equations

• Czech.instReprNoun = { reprPrec := Czech.instReprNoun.repr }

def Czech.instReprNoun.repr : Noun → ℕ → Std.Format

Equations

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

def Czech.Noun.clsAt (n : Noun) (m : Number) : Declension.Class

The class a noun follows in a number.

Equations

• n.clsAt m = if m = Number.plural then n.clsPlural else n.cls

def Czech.Noun.stem (n : Noun) : List String

The stem of a noun is its citation form less the nominative singular ending of its class.

Equations

• n.stem = List.take ((Czech.Declension.segments n.form).length - n.cls.nomSg.length) (Czech.Declension.segments n.form)

def Czech.Noun.endingsIn (n : Noun) (k : Declension.Class) (σ : Declension.Cell) : List (List String)

The endings of a noun in a class at a cell are those of the class on the noun's stem, save that the noun's lexical nominative plural replaces the class's in the nominative and the vocative plural.

Equations

• n.endingsIn k σ = if σ.number = Number.plural ∧ (σ.case = Czech.Case.nom ∨ σ.case = Czech.Case.voc) then n.nomPlural.getD (k.endingsOn n.stem σ) else k.endingsOn n.stem σ

def Czech.Noun.endings (n : Noun) (σ : Declension.Cell) : List (List String)

The endings of a noun at a cell are its endings in the class it follows in the cell's number.

Equations

• n.endings σ = n.endingsIn (n.clsAt σ.number) σ

def Czech.Noun.forms (n : Noun) (σ : Declension.Cell) : List (List String)

The forms of a noun at a cell are its stem inflected with each of its endings there.

Equations

• n.forms σ = List.map ((n.clsAt σ.number).inflect n.stem σ) (n.endings σ)

The model nouns of Short's tables

def Czech.chlap : Noun

chlap 'fellow', the hard masculine animate model (Table 9.2, p. 465).

Equations

• Czech.chlap = { form := "chlap", gloss := "fellow", gender := Czech.Gender.Value.mascAnimate, naturalGender := some Gender.masculine, cls := Czech.Declension.Class.chlap }

def Czech.hrad : Noun

hrad 'castle', the hard masculine inanimate model (Table 9.2, p. 465).

Equations

• Czech.hrad = { form := "hrad", gloss := "castle", gender := Czech.Gender.Value.mascInanimate, cls := Czech.Declension.Class.hrad }

def Czech.muz : Noun

muž 'man', the soft masculine animate model (Table 9.3, p. 466). Short's table gives the nominative plural muži alone, and Mluvnice češtiny says that "jméno muž může mít podobu obojí, -ové i -i" 'the noun muž can have both forms, -ové and -i' (p. 298).

Equations

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

def Czech.stroj : Noun

stroj 'machine', the soft masculine inanimate model (Table 9.3, p. 466).

Equations

• Czech.stroj = { form := "stroj", gloss := "machine", gender := Czech.Gender.Value.mascInanimate, cls := Czech.Declension.Class.stroj }

def Czech.mesto : Noun

město 'town', the neuter o-stem model (Table 9.4, p. 467).

Equations

• Czech.mesto = { form := "město", gloss := "town", gender := Czech.Gender.Value.neuter, cls := Czech.Declension.Class.mesto }

def Czech.srdce : Noun

srdce 'heart', the neuter jo-stem model (Table 9.4, p. 467).

Equations

• Czech.srdce = { form := "srdce", gloss := "heart", gender := Czech.Gender.Value.neuter, cls := Czech.Declension.Class.srdce }

def Czech.uceni : Noun

učení 'study', the neuter ьjo-stem model (Table 9.4, p. 467).

Equations

• Czech.uceni = { form := "učení", gloss := "study", gender := Czech.Gender.Value.neuter, cls := Czech.Declension.Class.uceni }

def Czech.zena : Noun

žena 'woman', the hard feminine a-stem model (Table 9.5, p. 468).

Equations

• Czech.zena = { form := "žena", gloss := "woman", gender := Czech.Gender.Value.feminine, naturalGender := some Gender.feminine, cls := Czech.Declension.Class.zena }

def Czech.hrdina : Noun

hrdina 'hero', the hard masculine a-stem model (Table 9.5, p. 468).

Equations

• Czech.hrdina = { form := "hrdina", gloss := "hero", gender := Czech.Gender.Value.mascAnimate, cls := Czech.Declension.Class.hrdina }

def Czech.duse : Noun

duše 'soul', the soft feminine ja-stem model (Table 9.5, p. 468).

Equations

• Czech.duse = { form := "duše", gloss := "soul", gender := Czech.Gender.Value.feminine, cls := Czech.Declension.Class.duse }

def Czech.pani : Noun

paní 'lady', "a unique item" (p. 468), the one ьja-stem (Table 9.5, p. 468).

Equations

• Czech.pani = { form := "paní", gloss := "lady", gender := Czech.Gender.Value.feminine, naturalGender := some Gender.feminine, cls := Czech.Declension.Class.pani }

def Czech.kost : Noun

kost 'bone', the i-stem model (Table 9.6, p. 469).

Equations

• Czech.kost = { form := "kost", gloss := "bone", gender := Czech.Gender.Value.feminine, cls := Czech.Declension.Class.kost }

def Czech.jehne : Noun

jehně 'lamb', the neuter t-stem model (Table 9.7, p. 470).

Equations

• Czech.jehne = { form := "jehně", gloss := "lamb", gender := Czech.Gender.Value.neuter, cls := Czech.Declension.Class.jehne }

def Czech.kluk : Noun

kluk 'boy', a hard masculine animate with a velar stem, whose vocative singular kluku Short gives as a survival of the u-stem vocative, "chiefly as a means to avoid palatalization of velar stems" (p. 465).

Equations

• Czech.kluk = { form := "kluk", gloss := "boy", gender := Czech.Gender.Value.mascAnimate, naturalGender := some Gender.masculine, cls := Czech.Declension.Class.chlap }

Nouns that change class with number

def Czech.den : Noun

den 'day', which follows stroj in the singular and hrady in the plural (Short, p. 469), and whose oblique stem is dn- (Short, p. 463).

Equations

• Czech.den = { form := "den", gloss := "day", gender := Czech.Gender.Value.mascInanimate, cls := Czech.Declension.Class.stroj, clsPlural := Czech.Declension.Class.hrad }

def Czech.koren : Noun

kořen 'root', which follows stroj in the singular and hrady in the plural (Short, p. 469), and which Mluvnice češtiny lists among the masculines with a stem in -en- that decline soft in the singular and hard in the plural (p. 310).

Equations

• Czech.koren = { form := "kořen", gloss := "root", gender := Czech.Gender.Value.mascInanimate, cls := Czech.Declension.Class.stroj, clsPlural := Czech.Declension.Class.hrad }

def Czech.pramen : Noun

pramen 'spring', which follows stroj in the singular and hrady in the plural. Mluvnice češtiny lists it with the masculines whose stem ends in -en-, the former n-stems, "řemen, ječmen, kámen, kmen, hřeben, kořen, křemen, plamen, pramen ap.", and says that "Tato jména mají dnes v sg tvary shodné se skloňováním měkkým, v pl se skloňováním tvrdým (tvary „tvrdé“ pronikají i do sg)" 'these nouns today have the forms of the soft declension in the singular and of the hard declension in the plural (the hard forms also entering the singular)' (p. 310). Short does not mention it.

Equations

• Czech.pramen = { form := "pramen", gloss := "spring", gender := Czech.Gender.Value.mascInanimate, cls := Czech.Declension.Class.stroj, clsPlural := Czech.Declension.Class.hrad }

Stump's nouns

def Czech.pokoj : Noun

pokoj 'room', a masculine inanimate declined as stroj. Mluvnice češtiny makes the soft declension obligatory for a stem ending in a morphonologically soft consonant (p. 290, of the animates) and the final consonant of the stroj type soft (p. 309), and the nouns it lists for the type include kraj, boj and orloj, in j like pokoj (p. 309). It names no soft consonants, nor pokoj itself.

Equations

• Czech.pokoj = { form := "pokoj", gloss := "room", gender := Czech.Gender.Value.mascInanimate, cls := Czech.Declension.Class.stroj }

def Czech.most : Noun

most 'bridge', a masculine inanimate declined as hrad.

Equations

• Czech.most = { form := "most", gloss := "bridge", gender := Czech.Gender.Value.mascInanimate, cls := Czech.Declension.Class.hrad }

def Czech.predseda : Noun

předseda 'chairman', a masculine a-stem declined as hrdina, of "the masculine a-declension" (Short, p. 467), and the model noun of Mluvnice češtiny's third type of the masculine animates (p. 290).

Equations

• Czech.predseda = { form := "předseda", gloss := "chairman", gender := Czech.Gender.Value.mascAnimate, cls := Czech.Declension.Class.hrdina }

def Czech.sluha : Noun

sluha 'servant', a masculine a-stem declined as hrdina, whose locative plural both grammars give as sluzích (Short, p. 467; Mluvnice češtiny, pp. 292, 300).

Equations

• Czech.sluha = { form := "sluha", gloss := "servant", gender := Czech.Gender.Value.mascAnimate, cls := Czech.Declension.Class.hrdina }

def Czech.filosof : Noun

filosof 'philosopher', a masculine animate declined as chlap, the hard subtype taking every noun whose stem ends in b, f, m, p or v (Mluvnice češtiny, p. 294). Its nominative plural is in neither grammar: Short does not place it among the subclasses in -é or -ové (p. 466), and Mluvnice češtiny mentions the noun once, spelled filozof, among the Latin borrowings that lost -us (p. 340).

Equations

• Czech.filosof = { form := "filosof", gloss := "philosopher", gender := Czech.Gender.Value.mascAnimate, cls := Czech.Declension.Class.chlap }

def Czech.filolog : Noun

filolog 'philologist', a masculine animate declined as chlap, with a velar stem, which takes the vocative singular -u (Short, p. 465; Mluvnice češtiny, p. 292) and the locative plural filolozích (Mluvnice češtiny, p. 295). Its nominative plural is -ové, which Mluvnice češtiny calls "výrazně jedinou podobou" 'clearly the only form' of the borrowed masculines in -log, naming filolog (p. 296), although it gives filolog – filolozi as its example of the alternation of g before the nominative plural -i (p. 294).

Equations

• Czech.filolog = { form := "filolog", gloss := "philologist", gender := Czech.Gender.Value.mascAnimate, cls := Czech.Declension.Class.chlap, nomPlural := some [["o", "v", "é"]] }

def Czech.nouns : List Noun

The entries are the model nouns of Short's tables, kluk, den, kořen and pramen, and Stump's other nouns.

Equations

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

theorem Czech.stem_append_nomSg (n : Noun) : n ∈ nouns → n.stem ++ n.cls.nomSg = Declension.segments n.form

Every entry's citation form is its stem followed by the nominative singular ending of its class, so each is declined in a class whose nominative singular it has.

theorem Czech.isVelar_stem_iff (n : Noun) : n ∈ nouns → (Declension.IsVelar n.stem ↔ n = kluk ∨ n = sluha ∨ n = filolog)

The velar stems among the entries are those of kluk, sluha and filolog, ending in k, h and g.

theorem Czech.isSome_ofChars_forms (n : Noun) : n ∈ nouns → ∀ (σ : Declension.Cell), ∀ w ∈ n.forms σ, (Phonology.ofChars (List.flatMap String.toList w)).isSome = true

Every form of every entry is written in Czech letters, and so has phonemes.

theorem Czech.gender_eq_cls_gender (n : Noun) : n ∈ nouns → n.gender = n.cls.gender

Every entry has the gender of its class's table.

theorem Czech.forms_examples : muz.forms (Declension.Cell.of Case.nom Number.plural forms_examples._proof_1) = [Declension.segments "muži", Declension.segments "mužové"] ∧ filolog.forms (Declension.Cell.of Case.nom Number.plural forms_examples._proof_1) = [Declension.segments "filologové"] ∧ filolog.forms (Declension.Cell.of Case.voc Number.singular forms_examples._proof_2) = [Declension.segments "filologu"] ∧ filolog.forms (Declension.Cell.of Case.loc Number.plural forms_examples._proof_1) = [Declension.segments "filolozích"] ∧ sluha.forms (Declension.Cell.of Case.loc Number.plural forms_examples._proof_1) = [Declension.segments "sluzích"] ∧ pramen.forms (Declension.Cell.of Case.gen Number.singular forms_examples._proof_2) = [Declension.segments "pramene"] ∧ pramen.forms (Declension.Cell.of Case.nom Number.plural forms_examples._proof_1) = [Declension.segments "prameny"]

The entries give Stump's nouns the forms that Mluvnice češtiny states where these depart from the model nouns' tables: muži and mužové (p. 298), filologové (p. 296), filolozích (p. 295) and sluzích (pp. 292, 300); filologu by the velar vocative rule (p. 292); and the soft genitive singular pramene beside the hard nominative plural prameny (p. 310).