German conjugation

This file defines the stem of a German verb, the forms its conjugation is built from, and the rules that build them. A verb is weak or strong. A weak verb forms its past with -te and its past participle with -t on its root, so that all its forms follow from the infinitive; a strong verb changes the vowel of its root, and its forms have to be learnt. A root in -d or -t, or in -m or -n after a consonant other than l or r, puts a linking -e- before these endings, as in arbeitet and zeichnete. The past participle has the prefix ge- when the verb is stressed on its first syllable, and so lacks it in the verbs in -ieren and in the verbs with an inseparable prefix such as be-, ver- or ent-: gratuliert, bezahlt.

A separable verb conjugates like the simple verb it is formed from. Its particle stands at the end of a main clause, ruft … an, and is joined to the non-finite forms, with the ge- of the simple verb and the zu of the infinitive after it: angerufen, anzurufen. The present tense has the endings -e, -st, -t, -en, -t and -en in weak and strong verbs alike. The rules and the examples are Durrell's.

Main definitions

• German.Conjugation.Stem: the infinitive, third person singular present and past, and past participle of a verb.
• German.Conjugation.weak, German.Conjugation.strong: the stem of a weak verb from its infinitive, and of a strong verb from its principal parts.
• German.Conjugation.Stem.inseparable, German.Conjugation.Stem.separable: the stem of a verb with an inseparable prefix or a separable particle.
• German.Conjugation.weakPresent: the present tense of a weak verb.

Implementation notes

The rules read the spelling. A root in -ier is taken to be the suffix of the verbs in -ieren, and an h after a vowel, as in lohnen, marks vowel length and is not a consonant. Irregular weak verbs, the vowel changes of strong verbs in the present and the verbs stressed off their first syllable for other reasons are not covered: their forms are given as those of a strong verb.

References

• [Dur11]

def German.Conjugation.IsVowel (c : Char) : Prop

The vowel letters.

Equations

• German.Conjugation.IsVowel c = (c ∈ ['a', 'e', 'i', 'o', 'u', 'ä', 'ö', 'ü', 'y'])

@[instance_reducible]

instance German.Conjugation.instDecidablePredCharIsVowel : DecidablePred IsVowel

Equations

• German.Conjugation.instDecidablePredCharIsVowel c = { decide := decide (List.elem c ['a', 'e', 'i', 'o', 'u', 'ä', 'ö', 'ü', 'y'] = true), reflects_decide := ⋯ }

def German.Conjugation.root (inf : String) : String

root inf is the root of the infinitive inf: less -n after -el and -er, less -en otherwise.

Equations

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

def German.Conjugation.linking (r : String) : String

linking r is the -e- a root in -d or -t, or in -m or -n after a consonant other than l or r, puts before the endings -st, -t and -te, and is empty otherwise.

Equations

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

def German.Conjugation.IsIer (r : String) : Prop

IsIer r holds of a root in -ier, the suffix of the verbs in -ieren.

Equations

• German.Conjugation.IsIer r = (['i', 'e', 'r'] <:+ r.toList)

@[instance_reducible]

instance German.Conjugation.instDecidableIsIer (r : String) : Decidable (IsIer r)

Equations

• German.Conjugation.instDecidableIsIer r = { decide := decide (['i', 'e', 'r'].isSuffixOf r.toList = true), reflects_decide := ⋯ }

structure German.Conjugation.Stem : Type

The stem of a verb is its infinitive, its third person singular present and past, and its past participle without a leading ge-, with whether the participle takes one.

• infinitive : String

  The infinitive.

• present : String

  The third person singular present.

• past : String

  The first and third person singular past.

• participle : String

  The past participle without a leading ge-.

• prefixGe : Bool

  The past participle takes a leading ge-, as that of a simple verb stressed on its first syllable does.

@[instance_reducible]

instance German.Conjugation.instDecidableEqStem : DecidableEq Stem

Equations

• German.Conjugation.instDecidableEqStem = German.Conjugation.instDecidableEqStem.decEq

def German.Conjugation.instDecidableEqStem.decEq (x✝ x✝¹ : Stem) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance German.Conjugation.instReprStem : Repr Stem

Equations

• German.Conjugation.instReprStem = { reprPrec := German.Conjugation.instReprStem.repr }

def German.Conjugation.instReprStem.repr : Stem → ℕ → Std.Format

Equations

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

def German.Conjugation.Stem.pastParticiple (s : Stem) : String

s.pastParticiple is the past participle.

Equations

• s.pastParticiple = if s.prefixGe = true then "ge" ++ s.participle else s.participle

def German.Conjugation.Stem.zuInfinitive (s : Stem) : String

s.zuInfinitive is the infinitive with zu.

Equations

• s.zuInfinitive = "zu " ++ s.infinitive

def German.Conjugation.weak (inf : String) : Stem

weak inf is the stem of the weak verb with the infinitive inf: the root with the endings -t, -te and -t, after the linking -e- where the root takes one, and stressed on its first syllable unless it is a verb in -ieren.

Equations

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

def German.Conjugation.strong (inf present past pp : String) : Stem

strong inf present past pp is the stem of the strong verb with those principal parts, the past participle pp given with its ge-.

Equations

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

def German.Conjugation.Stem.inseparable (s : Stem) (pfx : String) : Stem

s.inseparable pfx is the stem of the verb formed from s with the inseparable prefix pfx, which is joined to every form and, taking the stress off the first syllable, leaves the past participle without ge-.

Equations

• s.inseparable pfx = { infinitive := pfx ++ s.infinitive, present := pfx ++ s.present, past := pfx ++ s.past, participle := pfx ++ s.participle, prefixGe := false }

def German.Conjugation.Stem.separable (s : Stem) (prt : String) : Stem

s.separable prt is the stem of the verb formed from s with the separable particle prt. The particle follows the finite forms, as at the end of a main clause, and precedes the non-finite ones, where the ge- of s stays after it.

Equations

• s.separable prt = { infinitive := prt ++ s.infinitive, present := s.present ++ " " ++ prt, past := s.past ++ " " ++ prt, participle := prt ++ s.pastParticiple, prefixGe := false }

def German.Conjugation.Stem.separableZuInfinitive (s : Stem) (prt : String) : String

s.separableZuInfinitive prt is the infinitive with zu of the verb formed from s with the separable particle prt, zu standing between the two.

Equations

• s.separableZuInfinitive prt = prt ++ "zu" ++ s.infinitive

def German.Conjugation.weakPresent (inf : String) : Person × Number → Option String

weakPresent inf gives the present tense of the weak verb with the infinitive inf: the root with -e, -st, -t, -t in the singular and the second person plural, after the linking -e- before -st and -t, and the infinitive in the first and third person plural.

Equations

• German.Conjugation.weakPresent inf (Person.first, Number.singular) = some (German.Conjugation.root inf ++ "e")
• German.Conjugation.weakPresent inf (Person.second, Number.singular) = some (German.Conjugation.root inf ++ German.Conjugation.linking (German.Conjugation.root inf) ++ "st")
• German.Conjugation.weakPresent inf (Person.third, Number.singular) = some (German.Conjugation.root inf ++ German.Conjugation.linking (German.Conjugation.root inf) ++ "t")
• German.Conjugation.weakPresent inf (Person.second, Number.plural) = some (German.Conjugation.root inf ++ German.Conjugation.linking (German.Conjugation.root inf) ++ "t")
• German.Conjugation.weakPresent inf (Person.first, Number.plural) = some inf
• German.Conjugation.weakPresent inf (Person.third, Number.plural) = some inf
• German.Conjugation.weakPresent inf x✝ = none

Examples