def HPSG.matrixRequiresInvPlus (ct : Features.ClauseForm) (inv : Inv) : Prop

Matrix questions require [INV +]

Equations

• HPSG.matrixRequiresInvPlus ct inv = (ct = Features.ClauseForm.matrixQuestion → inv = HPSG.Inv.plus)

def HPSG.embeddedRequiresInvMinus (ct : Features.ClauseForm) (inv : Inv) : Prop

Embedded questions require [INV -]

Equations

• HPSG.embeddedRequiresInvMinus ct inv = (ct = Features.ClauseForm.embeddedQuestion → inv = HPSG.Inv.minus)

theorem HPSG.matrix_has_aux_before_subject (inv : Inv) (ws : List Word) (hct : matrixRequiresInvPlus Features.ClauseForm.matrixQuestion inv) (hord : invPlusImpliesAuxFirst inv ws) : Inversion.auxPrecedesSubject ws = true

Matrix questions have aux before subject

theorem HPSG.embedded_has_subject_before_aux (inv : Inv) (ws : List Word) (hct : embeddedRequiresInvMinus Features.ClauseForm.embeddedQuestion inv) (hord : invMinusImpliesSubjectFirst inv ws) : Inversion.subjectPrecedesAux ws = true

Embedded questions have subject before aux

structure HPSG.Clause : Type

A clause: words + INV feature + clause type

• words : List Word
• inv : Inv
• clauseType : Features.ClauseForm

def HPSG.wordOrderMatchesInv (c : Clause) : Prop

Word order must match INV feature

Equations

• HPSG.wordOrderMatchesInv c = (HPSG.invPlusImpliesAuxFirst c.inv c.words ∧ HPSG.invMinusImpliesSubjectFirst c.inv c.words)

def HPSG.wellFormed (c : Clause) : Prop

Well-formed clause

Equations

• HPSG.wellFormed c = (HPSG.wordOrderMatchesInv c ∧ HPSG.matrixRequiresInvPlus c.clauseType c.inv ∧ HPSG.embeddedRequiresInvMinus c.clauseType c.inv)

def HPSG.licenses (ws : List Word) (ct : Features.ClauseForm) : Prop

A word sequence is licensed for a clause type if some INV value works

Equations

• HPSG.licenses ws ct = ∃ (inv : HPSG.Inv), HPSG.wellFormed { words := ws, inv := inv, clauseType := ct }

theorem HPSG.licenses_matrix_aux_first (ws : List Word) (h : Inversion.auxPrecedesSubject ws = true) : licenses ws Features.ClauseForm.matrixQuestion

Matrix questions with aux-first order are licensed

theorem HPSG.not_licenses_matrix_subject_first (ws : List Word) (h : Inversion.auxPrecedesSubject ws = false) : ¬licenses ws Features.ClauseForm.matrixQuestion

Matrix questions with subject-first are NOT licensed

theorem HPSG.licenses_embedded_subject_first (ws : List Word) (h : Inversion.subjectPrecedesAux ws = true) : licenses ws Features.ClauseForm.embeddedQuestion

Embedded questions with subject-first are licensed

theorem HPSG.not_licenses_embedded_aux_first (ws : List Word) (h : Inversion.subjectPrecedesAux ws = false) : ¬licenses ws Features.ClauseForm.embeddedQuestion

Embedded questions with aux-first are NOT licensed