Hausa Verb Grades (Parsons System) — mathlib-style

[New00]

Hausa verbs are organised by the Parsons grade system (Parsons 1960b, codified in [New00] ch. 74): a closed inventory of derivational stem-templates (gr0–gr7) defined by a fixed pairing of tone melody, final-vowel template, and derivational function. Each grade also has up to four syntactic forms (A/B/C/D) selected by the post-verbal environment.

Architectural shape (mathlib analogy)

This file is the interpretation of two existing Theory interfaces in Hausa, not a parallel hierarchy:

• Semantics/Lexical/VerbEntry.Verb carries argument structure, voice, and Vendler class. A Hausa verb is a Verb plus a Parsons grade.
• Phonology/Autosegmental/RegisterTier.TRN carries the autosegmental tone primitives. A grade's tone melody is a list of TRNs, not a fresh enum.

The grade itself is a record of predictions (StemTemplate): tone, final-vowel template, derivational function, and the argument-structure defaults the grade entails. Concrete verbs derive their Verb fields from their grade by default; per-verb overrides are explicit.

The named theorems below are universal claims about the grade system or about Hausa verb lists, not rfl checks on per-verb stipulations. Per-cell verifications appear as examples.

inductive Hausa.SynForm : Type

The four syntactic forms selected by the post-verbal environment. A/B/C are pre-pause / pre-pronoun / pre-noun direct object; D is pre-indirect-object (host of the -aC H pre-dative suffix).

• A : SynForm
• B : SynForm
• C : SynForm
• D : SynForm

@[implicit_reducible]

instance Hausa.instDecidableEqSynForm : DecidableEq SynForm

Equations

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

def Hausa.instReprSynForm.repr : SynForm → ℕ → Std.Format

Equations

• Hausa.instReprSynForm.repr Hausa.SynForm.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.SynForm.A")).group prec✝
• Hausa.instReprSynForm.repr Hausa.SynForm.B prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.SynForm.B")).group prec✝
• Hausa.instReprSynForm.repr Hausa.SynForm.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.SynForm.C")).group prec✝
• Hausa.instReprSynForm.repr Hausa.SynForm.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.SynForm.D")).group prec✝

@[implicit_reducible]

instance Hausa.instReprSynForm : Repr SynForm

Equations

• Hausa.instReprSynForm = { reprPrec := Hausa.instReprSynForm.repr }

@[implicit_reducible]

instance Hausa.instInhabitedSynForm : Inhabited SynForm

Equations

• Hausa.instInhabitedSynForm = { default := Hausa.instInhabitedSynForm.default }

def Hausa.SynForm.all : List SynForm

The four forms in canonical order.

Equations

• Hausa.SynForm.all = [Hausa.SynForm.A, Hausa.SynForm.B, Hausa.SynForm.C, Hausa.SynForm.D]

theorem Hausa.SynForm.all_length : all.length = 4

inductive Hausa.FinalVowel : Type

Final vowel of a verb stem in a given form. We use Newman's citation glyphs; the gr5 -ar/-ad allomorphy and the lexical monoverb vowels are collapsed to one constructor each.

• aa : FinalVowel
• a : FinalVowel
• ee : FinalVowel
• i : FinalVowel
• oo : FinalVowel
• u : FinalVowel
• ar : FinalVowel
• lex : FinalVowel

@[implicit_reducible]

instance Hausa.instDecidableEqFinalVowel : DecidableEq FinalVowel

Equations

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

@[implicit_reducible]

instance Hausa.instReprFinalVowel : Repr FinalVowel

Equations

• Hausa.instReprFinalVowel = { reprPrec := Hausa.instReprFinalVowel.repr }

def Hausa.instReprFinalVowel.repr : FinalVowel → ℕ → Std.Format

Equations

• Hausa.instReprFinalVowel.repr Hausa.FinalVowel.aa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.FinalVowel.aa")).group prec✝
• Hausa.instReprFinalVowel.repr Hausa.FinalVowel.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.FinalVowel.a")).group prec✝
• Hausa.instReprFinalVowel.repr Hausa.FinalVowel.ee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.FinalVowel.ee")).group prec✝
• Hausa.instReprFinalVowel.repr Hausa.FinalVowel.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.FinalVowel.i")).group prec✝
• Hausa.instReprFinalVowel.repr Hausa.FinalVowel.oo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.FinalVowel.oo")).group prec✝
• Hausa.instReprFinalVowel.repr Hausa.FinalVowel.u prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.FinalVowel.u")).group prec✝
• Hausa.instReprFinalVowel.repr Hausa.FinalVowel.ar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.FinalVowel.ar")).group prec✝
• Hausa.instReprFinalVowel.repr Hausa.FinalVowel.lex prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.FinalVowel.lex")).group prec✝

@[implicit_reducible]

instance Hausa.instInhabitedFinalVowel : Inhabited FinalVowel

Equations

• Hausa.instInhabitedFinalVowel = { default := Hausa.instInhabitedFinalVowel.default }

@[reducible, inline]

abbrev Hausa.FVTemplate : Type

A final-vowel template is a function from syntactic forms to final vowels. The empirical content of a grade's vowel pattern is its image and how it varies across SynForm.all.

Equations

• Hausa.FVTemplate = (Hausa.SynForm → Hausa.FinalVowel)

def Hausa.FVTemplate.threeWayChanging (t : FVTemplate) : Prop

A template is three-way changing iff its A, B, C images are pairwise distinct. The Parsons system has exactly one three-way changing template — gr2 (A: ā, B: ē, C: i). gr4 has a two-way split A/D = ē vs C = i; only gr2 is three-way.

Equations

• t.threeWayChanging = (t Hausa.SynForm.A ≠ t Hausa.SynForm.B ∧ t Hausa.SynForm.B ≠ t Hausa.SynForm.C ∧ t Hausa.SynForm.A ≠ t Hausa.SynForm.C)

@[implicit_reducible]

instance Hausa.instDecidableThreeWayChanging (t : FVTemplate) : Decidable t.threeWayChanging

Equations

• Hausa.instDecidableThreeWayChanging t = Hausa.instDecidableThreeWayChanging._aux_1 t

inductive Hausa.GradeFunction : Type

Coarse derivational function of a grade ([New00] §74.3–74.10). A grade may have several uses; the primary function fixes the default argument structure. Secondary uses (e.g. gr1's actor-intransitive sub-use) appear as per-verb overrides.

• basic : GradeFunction
• applicative : GradeFunction
• intransitive : GradeFunction
• totality : GradeFunction
• efferential : GradeFunction
• ventive : GradeFunction
• sustentative : GradeFunction

@[implicit_reducible]

instance Hausa.instDecidableEqGradeFunction : DecidableEq GradeFunction

Equations

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

@[implicit_reducible]

instance Hausa.instReprGradeFunction : Repr GradeFunction

Equations

• Hausa.instReprGradeFunction = { reprPrec := Hausa.instReprGradeFunction.repr }

def Hausa.instReprGradeFunction.repr : GradeFunction → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hausa.instReprGradeFunction.repr Hausa.GradeFunction.basic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.GradeFunction.basic")).group prec✝

def Hausa.GradeFunction.defaultCT : GradeFunction → ComplementType

Default Verb.complementType predicted by the grade's primary function.

Equations

• Hausa.GradeFunction.intransitive.defaultCT = ComplementType.none
• Hausa.GradeFunction.sustentative.defaultCT = ComplementType.none
• x✝.defaultCT = ComplementType.np

def Hausa.GradeFunction.defaultVoice : GradeFunction → VoiceType

Default Verb.voiceType predicted by the grade's primary function. The sustentative (passive-like) gr7 selects nonThematic Voice; everything else introduces an external argument.

Equations

• Hausa.GradeFunction.sustentative.defaultVoice = VoiceType.nonThematic
• x✝.defaultVoice = VoiceType.agentive

structure Hausa.StemTemplate : Type

A stem template bundles the four invariants that pick out a grade: tone melody on a disyllabic stem, final-vowel template across A/B/C/D, derivational function, and a label. The argument-structure defaults are derived from function, not stored.

• label : String

  Display label (e.g. "gr2").

• tones : List Tone.TRN

  Tone melody on the disyllabic stem; empty for monoverbs (gr0) whose tone is lexical.

• fv : FVTemplate

  Final-vowel template across A/B/C/D.

• function : GradeFunction

  Primary derivational function.

def Hausa.StemTemplate.defaultCT (t : StemTemplate) : ComplementType

Predicted complement type from the template's function.

Equations

• t.defaultCT = t.function.defaultCT

def Hausa.StemTemplate.defaultVoice (t : StemTemplate) : VoiceType

Predicted voice type from the template's function.

Equations

• t.defaultVoice = t.function.defaultVoice

def Hausa.gr0 : StemTemplate

gr0: lexically-toned monoverbs (ci, shā, sō, jā).

Equations

• Hausa.gr0 = { label := "gr0", tones := [], fv := fun (x : Hausa.SynForm) => Hausa.FinalVowel.lex, function := Hausa.GradeFunction.basic }

def Hausa.gr1 : StemTemplate

gr1: H–L stems with -ā throughout (basic + applicative + actor-intr.).

Equations

• Hausa.gr1 = { label := "gr1", tones := [Tone.TRN.H, Tone.TRN.L], fv := fun (x : Hausa.SynForm) => Hausa.FinalVowel.aa, function := Hausa.GradeFunction.basic }

def Hausa.gr2 : StemTemplate

gr2: L–H "changing" verbs — A: -ā, B: -ē, C: -i, D: -ā. The unique grade with a non-constant final-vowel template.

Equations

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

def Hausa.gr3 : StemTemplate

gr3: L–H intransitive (-a).

Equations

• Hausa.gr3 = { label := "gr3", tones := [Tone.TRN.L, Tone.TRN.H], fv := fun (x : Hausa.SynForm) => Hausa.FinalVowel.a, function := Hausa.GradeFunction.intransitive }

def Hausa.gr4 : StemTemplate

gr4: H–L totality (-ē; "short C" -i).

Equations

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

def Hausa.gr5 : StemTemplate

gr5: H–H efferential / causative (-ar or -ad).

Equations

• Hausa.gr5 = { label := "gr5", tones := [Tone.TRN.H, Tone.TRN.H], fv := fun (x : Hausa.SynForm) => Hausa.FinalVowel.ar, function := Hausa.GradeFunction.efferential }

def Hausa.gr6 : StemTemplate

gr6: H–H ventive (-ō).

Equations

• Hausa.gr6 = { label := "gr6", tones := [Tone.TRN.H, Tone.TRN.H], fv := fun (x : Hausa.SynForm) => Hausa.FinalVowel.oo, function := Hausa.GradeFunction.ventive }

def Hausa.gr7 : StemTemplate

gr7: L–H sustentative / "passive" (-u).

Equations

• Hausa.gr7 = { label := "gr7", tones := [Tone.TRN.L, Tone.TRN.H], fv := fun (x : Hausa.SynForm) => Hausa.FinalVowel.u, function := Hausa.GradeFunction.sustentative }

def Hausa.parsons : List StemTemplate

The Parsons registry: all eight grades in canonical order. The universal theorems below quantify over this list, not over a pattern-match-based enum.

Equations

• Hausa.parsons = [Hausa.gr0, Hausa.gr1, Hausa.gr2, Hausa.gr3, Hausa.gr4, Hausa.gr5, Hausa.gr6, Hausa.gr7]

structure Hausa.HausaVerbextends Verb : Type

A Hausa verb extends Verb with its Parsons grade and its A-form citation tones (which may be lexical for gr0). All other morphological data is derived from the grade.

• frames : List Frame
• subjectEntailments : Option ArgumentStructure.EntailmentProfile
• objectEntailments : Option ArgumentStructure.EntailmentProfile
• unaccusative : Bool
• voiceType : Option VoiceType
• passivizable : Bool
• implicitObj : Option ImplicitInterp
• implicitGoal : Option ImplicitInterp
• vendlerClass : Option Features.VendlerClass
• degreeAchievementScale : Option Features.DegreeAchievement.DegreeAchievementScale
• verbIncClass : Option Semantics.Aspect.Incremental.VerbIncClass
• cosType : Option Features.ChangeOfState.CoSType
• presupType : Option PresupTriggerType
• projectionBehavior : Option ProjectionBehavior
• implicative : Option Features.Implicative
• causative : Option Features.Causative
• causalSource : Option Causation.Psych.CausalSource
• opaqueContext : Bool
• attitude : Option Features.Attitude
• readings : List Reading
• takesQuestionBase : Bool
• complementSig : Option NaturalLogic.EntailmentSig
• levinClass : Option Semantics.Lexical.LevinClass
• root : Root
• form : String
• speechActVerb : Bool
• senseTag : SenseTag
• grade : StemTemplate

  The Parsons grade fixing tone, final vowel, and argument-structure defaults.

• lexTones : List Tone.TRN

  For gr0 monoverbs only: lexically-specified tone(s). Empty list otherwise (the grade fixes the tones).

def Hausa.HausaVerb.tones (v : HausaVerb) : List Tone.TRN

The verb's tone melody: from the grade unless the grade is lexically-toned (gr0), in which case from lexTones.

Equations

• v.tones = match v.grade.tones with | [] => v.lexTones | ts => ts

def Hausa.HausaVerb.fv (v : HausaVerb) (f : SynForm) : FinalVowel

The verb's final vowel in a given syntactic form.

Equations

• v.fv f = v.grade.fv f

def Hausa.HausaVerb.canonical (v : HausaVerb) : Prop

A verb is canonical iff its Verb argument-structure fields agree with the defaults predicted by its grade. Per-verb overrides break canonicity (and become explicit empirical claims).

Equations

• v.canonical = (v.complementType = v.grade.defaultCT ∧ v.voiceType = some v.grade.defaultVoice)

@[implicit_reducible]

instance Hausa.instDecidableCanonical (v : HausaVerb) : Decidable v.canonical

Equations

• Hausa.instDecidableCanonical v = Hausa.instDecidableCanonical._aux_1 v

def Hausa.mkVerb (form : String) (g : StemTemplate) (lexTones : List Tone.TRN := []) : HausaVerb

Smart constructor: builds a canonical HausaVerb from form and grade by filling Verb from the grade's defaults. Concrete verb definitions use this; per-verb overrides spell out which field departs from the default.

Equations

• Hausa.mkVerb form g lexTones = { frames := [g.defaultCT.toFrame], voiceType := some g.defaultVoice, form := form, grade := g, lexTones := lexTones }

def Hausa.ci : HausaVerb

Equations

• Hausa.ci = Hausa.mkVerb "ci" Hausa.gr0 [Tone.TRN.H]

def Hausa.shaa : HausaVerb

Equations

• Hausa.shaa = Hausa.mkVerb "shā" Hausa.gr0 [Tone.TRN.H]

def Hausa.soo : HausaVerb

Equations

• Hausa.soo = Hausa.mkVerb "sō" Hausa.gr0 [Tone.TRN.H]

def Hausa.saya : HausaVerb

Equations

• Hausa.saya = Hausa.mkVerb "sayā" Hausa.gr1

def Hausa.sayi : HausaVerb

Equations

• Hausa.sayi = Hausa.mkVerb "sayi" Hausa.gr2

def Hausa.fita : HausaVerb

Equations

• Hausa.fita = Hausa.mkVerb "fita" Hausa.gr3

def Hausa.kashe : HausaVerb

Equations

• Hausa.kashe = Hausa.mkVerb "kashē" Hausa.gr4

def Hausa.sayar : HausaVerb

gr5 efferential of sayā 'buy' — sayař 'sell'. Same root as saya (gr1 basic) — minimal pair illustrating the efferential derivation ([New00] §74.9).

Equations

• Hausa.sayar = Hausa.mkVerb "sayař" Hausa.gr5

def Hausa.koomoo : HausaVerb

gr6 ventive kōmō 'return here' ([New00] §74.11). Note: zō 'come' is irregular (v*) and not gr6, despite semantic overlap with the ventive function.

Equations

• Hausa.koomoo = Hausa.mkVerb "kōmō" Hausa.gr6

def Hausa.taaru : HausaVerb

gr7 sustentative tāru 'meet' / 'be assembled' ([New00] §74.13). gr7 derives a passive-like reading: the action is successfully sustained, with no external argument introduced.

Equations

• Hausa.taaru = Hausa.mkVerb "tāru" Hausa.gr7

def Hausa.lexicon : List HausaVerb

Canonical Hausa verbs. Each entry is generated by mkVerb, so every entry is canonical by construction (see mkVerb_is_canonical below).

Equations

• Hausa.lexicon = [Hausa.ci, Hausa.shaa, Hausa.soo, Hausa.saya, Hausa.sayi, Hausa.fita, Hausa.kashe, Hausa.sayar, Hausa.koomoo, Hausa.taaru]

def Hausa.gangara : HausaVerb

Override demonstration. Some gr1 verbs have an actor-intransitive sub-use ([New00] §74.4): morphologically gr1 (H–L, -ā) but syntactically intransitive. We model this by overriding complementType while keeping the gr1 grade. The override breaks canonicity — making the empirical claim "gr1 has an intransitive sub-use" visible in the type system rather than buried in prose.

Equations

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

theorem Hausa.gr2_three_way_changing : gr2.fv.threeWayChanging

Changing-verb theorem (positive). gr2 has pairwise-distinct A/B/C final vowels: this is the empirical diagnostic of the "changing" verb class.

theorem Hausa.only_gr2_three_way_changing (g : StemTemplate) : g ∈ parsons → g.fv.threeWayChanging → g.label = "gr2"

Changing-verb theorem (uniqueness). No other Parsons grade has pairwise-distinct A/B/C final vowels. Together with gr2_three_way_changing, this characterises gr2 by the property of being three-way changing.

theorem Hausa.tone_fibre_count : (List.map (fun (x : StemTemplate) => x.tones) parsons).dedup.length = 4

Tone-fibre cardinality. The Parsons registry uses exactly three distinct disyllabic tone melodies (HL, LH, HH); gr0 contributes the empty melody. So the registry partitions into 4 tone-fibres.

theorem Hausa.hh_minimal_pair : gr5.tones = gr6.tones ∧ gr5.fv SynForm.A ≠ gr6.fv SynForm.A ∧ gr5.function ≠ gr6.function

Minimal pair gr5 / gr6. The two H–H grades differ in A-form final vowel and in derivational function — making them a tonally- matched minimal pair.

theorem Hausa.gr3_intransitive (v : HausaVerb) (hg : v.grade = gr3) (hc : v.canonical) : v.complementType = ComplementType.none

gr3 is intransitive by template. Any verb whose grade is gr3 and which is canonical has empty complement type. This is the universal claim that grade choice constrains argument structure; the per-verb verification (fita.complementType = .none) is demoted to an example below.

theorem Hausa.gr7_nonThematic (v : HausaVerb) (hg : v.grade = gr7) (hc : v.canonical) : v.voiceType = some VoiceType.nonThematic

gr7 suppresses the external argument. Any canonical gr7 verb has nonThematic Voice.

theorem Hausa.mkVerb_is_canonical (form : String) (g : StemTemplate) (lexTones : List Tone.TRN := []) : (mkVerb form g lexTones).canonical

mkVerb always yields a canonical verb. Hence every entry in lexicon is canonical by construction — no per-verb checking needed.

theorem Hausa.hh_grades_agentive : gr5.defaultVoice = VoiceType.agentive ∧ gr6.defaultVoice = VoiceType.agentive

Grades 5 and 6 introduce an external argument. The two H–H grades are both agentive at the Verb level.