Tense and tense forms

This file defines the grammatical tenses and the tense forms of a verb. A tense is past, present or future (Tense); the cell of times it denotes is the matter of Semantics/Tense/Defs.lean. A tense form of a verb, in the sense of the traditional grammars, is a member of the verb's tense paradigm, such as the simple past or the present perfect. It is described here by its make-up, the tense inflection of its finite verb and the nonfinite forms stacked under that verb. A synthetic form has a finite lexical verb and nothing else. A periphrastic form is built from another form by putting its verb, in a nonfinite form, under an auxiliary that takes over the tense inflection, so that the perfect of the simple present builds is the present perfect has built, and the perfect of that is the double perfect has had built of the South German dialects. Two languages whose forms have the same make-up share the form, and which tense and which aspect it expresses in each is a matter of analysis left to studies.

Main declarations

• Tense: the grammatical tenses.
• Tense.Form.Nonfinite: the nonfinite verb forms that build periphrastic tense forms.
• Tense.Form: a tense form, by the inflection of its finite verb and its nonfinite chain.
• Tense.Form.under, Tense.Form.perfect, Tense.Form.progressive: the periphrastic form built on a form.
• Tense.Form.simplePresent, Tense.Form.simplePast and the forms built on them, among them Tense.Form.presentPerfect, Tense.Form.doublePerfect and Tense.Form.future.
• Tense.Form.IsPerfect: the form is the perfect of some form.
• Tense.Periphrasis, Tense.Periphrasis.realize: a language's means of building tense forms over its verbs, and the words of a form of a verb.

inductive Tense : Type

A grammatical tense is past, present or future.

• past : Tense
• present : Tense
• future : Tense

@[instance_reducible]

instance instDecidableEqTense : DecidableEq Tense

Equations

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

@[instance_reducible]

instance instReprTense : Repr Tense

Equations

• instReprTense = { reprPrec := instReprTense.repr }

def instReprTense.repr : Tense → ℕ → Std.Format

Equations

• instReprTense.repr Tense.past prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tense.past")).group prec✝
• instReprTense.repr Tense.present prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tense.present")).group prec✝
• instReprTense.repr Tense.future prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tense.future")).group prec✝

@[instance_reducible]

instance instInhabitedTense : Inhabited Tense

Equations

• instInhabitedTense = { default := instInhabitedTense.default }

@[instance_reducible]

instance instFintypeTense : Fintype Tense

Equations

• instFintypeTense = { elems := { val := ↑Tense.enumList, nodup := Tense.enumList_nodup }, complete := instFintypeTense._proof_1 }

inductive Tense.Form.Nonfinite : Type

A nonfinite verb form in a periphrastic tense form.

• infinitive : Nonfinite

  The infinitive, as German bauen under werden.

• presentParticiple : Nonfinite

  The present participle, as English building under be.

• pastParticiple : Nonfinite

  The past participle, as English built under have and German gebaut under haben.

@[instance_reducible]

instance Tense.Form.instDecidableEqNonfinite : DecidableEq Nonfinite

Equations

• Tense.Form.instDecidableEqNonfinite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Tense.Form.instReprNonfinite : Repr Nonfinite

Equations

• Tense.Form.instReprNonfinite = { reprPrec := Tense.Form.instReprNonfinite.repr }

def Tense.Form.instReprNonfinite.repr : Nonfinite → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Tense.Form.instInhabitedNonfinite : Inhabited Nonfinite

Equations

• Tense.Form.instInhabitedNonfinite = { default := Tense.Form.instInhabitedNonfinite.default }

structure Tense.Form : Type

A tense form of a verb consists of the tense inflection of its finite verb and the nonfinite forms under the finite verb, outermost first, so that the lexical verb is the last of them, or the finite verb itself when there are none.

• finite : Tense

  The tense inflection of the finite verb.

• nonfinite : List Nonfinite

  The nonfinite forms under the finite verb, outermost first.

theorem Tense.Form.ext_iff {x y : Form} : x = y ↔ x.finite = y.finite ∧ x.nonfinite = y.nonfinite

theorem Tense.Form.ext {x y : Form} (finite : x.finite = y.finite) (nonfinite : x.nonfinite = y.nonfinite) : x = y

@[instance_reducible]

instance Tense.instDecidableEqForm : DecidableEq Form

Equations

• Tense.instDecidableEqForm = Tense.instDecidableEqForm.decEq

def Tense.instDecidableEqForm.decEq (x✝ x✝¹ : Form) : Decidable (x✝ = x✝¹)

Equations

• Tense.instDecidableEqForm.decEq { finite := a, nonfinite := a_1 } { finite := b, nonfinite := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Tense.instReprForm.repr : Form → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Tense.instReprForm : Repr Form

Equations

• Tense.instReprForm = { reprPrec := Tense.instReprForm.repr }

def Tense.Form.under (n : Nonfinite) (f : Form) : Form

The periphrastic form built on f puts the verb of f in the nonfinite form n under an auxiliary with the tense inflection of f.

Equations

• Tense.Form.under n f = { finite := f.finite, nonfinite := n :: f.nonfinite }

def Tense.Form.perfect : Form → Form

The perfect of a form puts its verb in the past participle under an auxiliary.

Equations

• Tense.Form.perfect = Tense.Form.under Tense.Form.Nonfinite.pastParticiple

def Tense.Form.progressive : Form → Form

The progressive of a form puts its verb in the present participle under an auxiliary.

Equations

• Tense.Form.progressive = Tense.Form.under Tense.Form.Nonfinite.presentParticiple

@[simp]

theorem Tense.Form.under_finite (n : Nonfinite) (f : Form) : (under n f).finite = f.finite

@[simp]

theorem Tense.Form.under_nonfinite (n : Nonfinite) (f : Form) : (under n f).nonfinite = n :: f.nonfinite

theorem Tense.Form.under_injective (n : Nonfinite) : Function.Injective (under n)

@[simp]

theorem Tense.Form.perfect_inj {f g : Form} : f.perfect = g.perfect ↔ f = g

def Tense.Form.simplePresent : Form

The simple present is the synthetic present, as builds.

Equations

• Tense.Form.simplePresent = { finite := Tense.present }

def Tense.Form.simplePast : Form

The simple past is the synthetic past, as built.

Equations

• Tense.Form.simplePast = { finite := Tense.past }

def Tense.Form.presentProgressive : Form

The present progressive is the progressive of the simple present, as is building.

Equations

• Tense.Form.presentProgressive = Tense.Form.simplePresent.progressive

def Tense.Form.pastProgressive : Form

The past progressive is the progressive of the simple past, as was building.

Equations

• Tense.Form.pastProgressive = Tense.Form.simplePast.progressive

def Tense.Form.presentPerfect : Form

The present perfect is the perfect of the simple present, as has built.

Equations

• Tense.Form.presentPerfect = Tense.Form.simplePresent.perfect

def Tense.Form.pastPerfect : Form

The past perfect is the perfect of the simple past, as had built.

Equations

• Tense.Form.pastPerfect = Tense.Form.simplePast.perfect

def Tense.Form.doublePerfect : Form

The double perfect is the perfect of the present perfect.

Equations

• Tense.Form.doublePerfect = Tense.Form.presentPerfect.perfect

def Tense.Form.future : Form

The future is the simple present of an auxiliary over the infinitive, as will build.

Equations

• Tense.Form.future = Tense.Form.under Tense.Form.Nonfinite.infinitive Tense.Form.simplePresent

def Tense.Form.futurePerfect : Form

The future perfect is the future of the perfect, as will have built.

Equations

• Tense.Form.futurePerfect = Tense.Form.under Tense.Form.Nonfinite.infinitive Tense.Form.presentPerfect

def Tense.Form.IsPerfect (f : Form) : Prop

A form is a perfect when it is the perfect of some form.

Equations

• f.IsPerfect = ∃ (g : Tense.Form), f = g.perfect

theorem Tense.Form.isPerfect_iff {f : Form} : f.IsPerfect ↔ f.nonfinite.head? = some Nonfinite.pastParticiple

@[instance_reducible]

instance Tense.Form.instDecidablePredIsPerfect : DecidablePred IsPerfect

Equations

• x✝.instDecidablePredIsPerfect = decidable_of_iff (x✝.nonfinite.head? = some Tense.Form.Nonfinite.pastParticiple) ⋯

structure Tense.Periphrasis (V : Type u_1) : Type u_1

A periphrasis is the means by which a language builds tense forms over its verbs V. It gives the finite form of a verb in each tense, its nonfinite forms, and the auxiliary under which a verb stands when it is in a given nonfinite form. Each is partial, since a language may lack an inflection, as German lacks a future inflection, or a construction, as German lacks a progressive.

• finite : V → Tense → Option String

  The finite form of a verb in a tense.

• nonfinite : V → Form.Nonfinite → Option String

  A nonfinite form of a verb.

• auxiliary : V → Form.Nonfinite → Option V

  The auxiliary that governs a verb in a nonfinite form.

def Tense.Periphrasis.chain {V : Type u_1} (L : Periphrasis V) (v : V) : List Form.Nonfinite → Option (List String × V)

L.chain v ns gives the nonfinite verbs of a tense form of v with nonfinite chain ns, innermost first, and the verb left to be inflected. Each nonfinite form is taken by the verb below it, and the auxiliary that governs it is the next verb up.

Equations

• L.chain v [] = some ([], v)
• L.chain v (n :: ns) = match L.chain v ns with | none => none | some (ws, u) => match L.nonfinite u n, L.auxiliary u n with | some w, some a => some (ws ++ [w], a) | x, x_1 => none

def Tense.Periphrasis.realize {V : Type u_1} (L : Periphrasis V) (v : V) (f : Form) : Option (String × List String)

L.realize v f gives the finite verb of the tense form f of v and its nonfinite verbs, innermost first.

Equations

• L.realize v f = match L.chain v f.nonfinite with | none => none | some (ws, u) => Option.map (fun (x : String) => (x, ws)) (L.finite u f.finite)

theorem Tense.Periphrasis.length_of_chain {V : Type u_1} (L : Periphrasis V) (v : V) (ns : List Form.Nonfinite) {ws : List String} {u : V} : L.chain v ns = some (ws, u) → ws.length = ns.length

theorem Tense.Periphrasis.length_of_mem_realize {V : Type u_1} (L : Periphrasis V) {v : V} {f : Form} {x : String × List String} (h : x ∈ L.realize v f) : x.2.length = f.nonfinite.length

A realized tense form has one nonfinite verb for each nonfinite form in its make-up.