Modern Greek case

Standard Modern Greek has four cases: nominative, accusative, genitive and vocative. The dative of Ancient Greek (Greek.Ancient.Case) is gone, and the indirect object of a ditransitive is a genitive, beside a prepositional phrase in se with the accusative ([MS10]). Blake gives the system, vocative aside, as a three-case nominative–accusative–genitive system ([Bla94b]).

Main declarations

• Greek.StandardModern.Case: the four cases.
• Greek.StandardModern.Case.label, Greek.StandardModern.Case.functions: the comparative value each case is named for, and the values it expresses.

References

• [Bla94b]
• [MS10]

inductive Greek.StandardModern.Case : Type

The four cases.

• nom : Case

  The nominative.

• acc : Case

  The accusative.

• gen : Case

  The genitive.

• voc : Case

  The vocative.

@[instance_reducible]

instance Greek.StandardModern.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Greek.StandardModern.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Greek.StandardModern.instReprCase : Repr Case

Equations

• Greek.StandardModern.instReprCase = { reprPrec := Greek.StandardModern.instReprCase.repr }

def Greek.StandardModern.instReprCase.repr : Case → ℕ → Std.Format

Equations

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

def Greek.StandardModern.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• Greek.StandardModern.Case.nom.label = Case.nom
• Greek.StandardModern.Case.acc.label = Case.acc
• Greek.StandardModern.Case.gen.label = Case.gen
• Greek.StandardModern.Case.voc.label = Case.voc

def Greek.StandardModern.Case.functions : Case → Finset _root_.Case

The comparative values a case expresses: the genitive also expresses the indirect object.

Equations

• Greek.StandardModern.Case.gen.functions = {Case.gen, Case.dat}
• x✝.functions = {x✝.label}

theorem Greek.StandardModern.Case.label_mem_functions (c : Case) : c.label ∈ c.functions

theorem Greek.StandardModern.Case.biUnion_functions_eq_insert_dat : Finset.univ.biUnion functions = insert Case.dat (Finset.image label Finset.univ)

The dative function outlives the dative case.