Hausa Verb Grades (Parsons System) — mathlib-style

@cite{newman-2000}

Hausa verbs are organised by the Parsons grade system (Parsons 1960b, codified in @cite{newman-2000} 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:

• Theories/Semantics/Lexical/VerbEntry.VerbCore carries argument structure, voice, and Vendler class. A Hausa verb is a VerbCore plus a Parsons grade.
• Theories/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 VerbCore 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 Fragments.Hausa.VerbGrades.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 Fragments.Hausa.VerbGrades.instDecidableEqSynForm : DecidableEq SynForm

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.VerbGrades.instReprSynForm : Repr SynForm

Equations

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.VerbGrades.instInhabitedSynForm : Inhabited SynForm

Equations

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

def Fragments.Hausa.VerbGrades.instInhabitedSynForm.default : SynForm

Equations

• Fragments.Hausa.VerbGrades.instInhabitedSynForm.default = Fragments.Hausa.VerbGrades.SynForm.A

def Fragments.Hausa.VerbGrades.SynForm.all : List SynForm

The four forms in canonical order.

Equations

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

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

inductive Fragments.Hausa.VerbGrades.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 Fragments.Hausa.VerbGrades.instDecidableEqFinalVowel : DecidableEq FinalVowel

Equations

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.VerbGrades.instReprFinalVowel : Repr FinalVowel

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.VerbGrades.instInhabitedFinalVowel : Inhabited FinalVowel

Equations

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

def Fragments.Hausa.VerbGrades.instInhabitedFinalVowel.default : FinalVowel

Equations

• Fragments.Hausa.VerbGrades.instInhabitedFinalVowel.default = Fragments.Hausa.VerbGrades.FinalVowel.aa

@[reducible, inline]

abbrev Fragments.Hausa.VerbGrades.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

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

def Fragments.Hausa.VerbGrades.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

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

@[implicit_reducible]

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

Equations

• Fragments.Hausa.VerbGrades.instDecidableThreeWayChanging t = Fragments.Hausa.VerbGrades.instDecidableThreeWayChanging._aux_1 t

inductive Fragments.Hausa.VerbGrades.GradeFunction : Type

Coarse derivational function of a grade (@cite{newman-2000} §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 Fragments.Hausa.VerbGrades.instDecidableEqGradeFunction : DecidableEq GradeFunction

Equations

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.VerbGrades.instReprGradeFunction : Repr GradeFunction

Equations

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

def Fragments.Hausa.VerbGrades.GradeFunction.defaultCT : GradeFunction → Semantics.Lexical.ComplementType

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

Equations

• Fragments.Hausa.VerbGrades.GradeFunction.intransitive.defaultCT = Semantics.Lexical.ComplementType.none
• Fragments.Hausa.VerbGrades.GradeFunction.sustentative.defaultCT = Semantics.Lexical.ComplementType.none
• x✝.defaultCT = Semantics.Lexical.ComplementType.np

def Fragments.Hausa.VerbGrades.GradeFunction.defaultVoice : GradeFunction → Semantics.Lexical.VoiceType

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

Equations

• Fragments.Hausa.VerbGrades.GradeFunction.sustentative.defaultVoice = Semantics.Lexical.VoiceType.nonThematic
• x✝.defaultVoice = Semantics.Lexical.VoiceType.agentive

structure Fragments.Hausa.VerbGrades.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 Phonology.Autosegmental.RegisterTier.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 Fragments.Hausa.VerbGrades.StemTemplate.defaultCT (t : StemTemplate) : Semantics.Lexical.ComplementType

Predicted complement type from the template's function.

Equations

• t.defaultCT = t.function.defaultCT

def Fragments.Hausa.VerbGrades.StemTemplate.defaultVoice (t : StemTemplate) : Semantics.Lexical.VoiceType

Predicted voice type from the template's function.

Equations

• t.defaultVoice = t.function.defaultVoice

def Fragments.Hausa.VerbGrades.gr0 : StemTemplate

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

Equations

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

def Fragments.Hausa.VerbGrades.gr1 : StemTemplate

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

Equations

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

def Fragments.Hausa.VerbGrades.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 Fragments.Hausa.VerbGrades.gr3 : StemTemplate

gr3: L–H intransitive (-a).

Equations

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

def Fragments.Hausa.VerbGrades.gr4 : StemTemplate

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

Equations

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

def Fragments.Hausa.VerbGrades.gr5 : StemTemplate

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

Equations

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

def Fragments.Hausa.VerbGrades.gr6 : StemTemplate

gr6: H–H ventive (-ō).

Equations

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

def Fragments.Hausa.VerbGrades.gr7 : StemTemplate

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

Equations

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

def Fragments.Hausa.VerbGrades.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

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

structure Fragments.Hausa.VerbGrades.HausaVerbextends Semantics.Lexical.VerbCore : Type

A Hausa verb extends VerbCore 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.

• form : String
• complementType : ComplementType
• subjectEntailments : Option ArgumentStructure.EntailmentProfile.EntailmentProfile
• objectEntailments : Option ArgumentStructure.EntailmentProfile.EntailmentProfile
• controlType : ControlType
• altComplementType : Option ComplementType
• altControlType : ControlType
• unaccusative : Bool
• voiceType : Option VoiceType
• passivizable : Bool
• implicitObj : Option ImplicitInterp
• implicitGoal : Option ImplicitInterp
• speechActVerb : Bool
• vendlerClass : Option Features.VendlerClass
• degreeAchievementScale : Option Features.DegreeAchievement.DegreeAchievementScale
• verbIncClass : Option Aspect.Incremental.VerbIncClass
• presupType : Option PresupTriggerType
• postsupType : Option PostsupType
• projectionBehavior : Option ProjectionBehavior
• selectsDimension : Option Features.Dimension.Dimension
• cosType : Option Features.ChangeOfState.CoSType
• implicative : Option Features.Implicative
• causative : Option Features.Causative
• causalSource : Option Causation.Psych.CausalSource
• opaqueContext : Bool
• attitude : Option Features.Attitude
• takesQuestionBase : Bool
• complementSig : Option Core.NaturalLogic.EntailmentSig
• senseTag : SenseTag
• levinClass : Option LevinClass
• rootProfile : Option Roots.RootProfile
• grade : StemTemplate

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

• lexTones : List Phonology.Autosegmental.RegisterTier.TRN

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

def Fragments.Hausa.VerbGrades.HausaVerb.tones (v : HausaVerb) : List Phonology.Autosegmental.RegisterTier.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 Fragments.Hausa.VerbGrades.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 Fragments.Hausa.VerbGrades.HausaVerb.canonical (v : HausaVerb) : Prop

A verb is canonical iff its VerbCore 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 Fragments.Hausa.VerbGrades.instDecidableCanonical (v : HausaVerb) : Decidable v.canonical

Equations

• Fragments.Hausa.VerbGrades.instDecidableCanonical v = Fragments.Hausa.VerbGrades.instDecidableCanonical._aux_1 v

def Fragments.Hausa.VerbGrades.mkVerb (form : String) (g : StemTemplate) (lexTones : List Phonology.Autosegmental.RegisterTier.TRN := []) : HausaVerb

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

Equations

• Fragments.Hausa.VerbGrades.mkVerb form g lexTones = { form := form, complementType := g.defaultCT, voiceType := some g.defaultVoice, grade := g, lexTones := lexTones }

def Fragments.Hausa.VerbGrades.ci : HausaVerb

Equations

• Fragments.Hausa.VerbGrades.ci = Fragments.Hausa.VerbGrades.mkVerb "ci" Fragments.Hausa.VerbGrades.gr0 [Phonology.Autosegmental.RegisterTier.TRN.H]

def Fragments.Hausa.VerbGrades.shaa : HausaVerb

Equations

• Fragments.Hausa.VerbGrades.shaa = Fragments.Hausa.VerbGrades.mkVerb "shā" Fragments.Hausa.VerbGrades.gr0 [Phonology.Autosegmental.RegisterTier.TRN.H]

def Fragments.Hausa.VerbGrades.soo : HausaVerb

Equations

• Fragments.Hausa.VerbGrades.soo = Fragments.Hausa.VerbGrades.mkVerb "sō" Fragments.Hausa.VerbGrades.gr0 [Phonology.Autosegmental.RegisterTier.TRN.H]

def Fragments.Hausa.VerbGrades.saya : HausaVerb

Equations

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

def Fragments.Hausa.VerbGrades.sayi : HausaVerb

Equations

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

def Fragments.Hausa.VerbGrades.fita : HausaVerb

Equations

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

def Fragments.Hausa.VerbGrades.kashe : HausaVerb

Equations

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

def Fragments.Hausa.VerbGrades.sayar : HausaVerb

gr5 efferential of sayā 'buy' — sayař 'sell'. Same root as saya (gr1 basic) — minimal pair illustrating the efferential derivation (@cite{newman-2000} §74.9).

Equations

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

def Fragments.Hausa.VerbGrades.koomoo : HausaVerb

gr6 ventive kōmō 'return here' (@cite{newman-2000} §74.11). Note: zō 'come' is irregular (v*) and not gr6, despite semantic overlap with the ventive function.

Equations

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

def Fragments.Hausa.VerbGrades.taaru : HausaVerb

gr7 sustentative tāru 'meet' / 'be assembled' (@cite{newman-2000} §74.13). gr7 derives a passive-like reading: the action is successfully sustained, with no external argument introduced.

Equations

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

def Fragments.Hausa.VerbGrades.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

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

def Fragments.Hausa.VerbGrades.gangara : HausaVerb

Override demonstration. Some gr1 verbs have an actor-intransitive sub-use (@cite{newman-2000} §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 Fragments.Hausa.VerbGrades.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 Fragments.Hausa.VerbGrades.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 Fragments.Hausa.VerbGrades.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 Fragments.Hausa.VerbGrades.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 Fragments.Hausa.VerbGrades.gr3_intransitive (v : HausaVerb) (hg : v.grade = gr3) (hc : v.canonical) : v.complementType = Semantics.Lexical.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 Fragments.Hausa.VerbGrades.gr7_nonThematic (v : HausaVerb) (hg : v.grade = gr7) (hc : v.canonical) : v.voiceType = some Semantics.Lexical.VoiceType.nonThematic

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

theorem Fragments.Hausa.VerbGrades.mkVerb_is_canonical (form : String) (g : StemTemplate) (lexTones : List Phonology.Autosegmental.RegisterTier.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 Fragments.Hausa.VerbGrades.hh_grades_agentive : gr5.defaultVoice = Semantics.Lexical.VoiceType.agentive ∧ gr6.defaultVoice = Semantics.Lexical.VoiceType.agentive

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