Subject–auxiliary inversion helpers

Word-list predicates for detecting subject–auxiliary inversion in a linearised string, shared by HPSG (Theories/Syntax/HPSG/Inversion.lean) and Minimalism (Theories/Syntax/Minimalism/Inversion.lean) accounts.

The helpers operate on raw List Word, using UD UPOS tags and the wh feature. They make no commitment to either theory's representation of the inversion alternation; both theories' bridge theorems quantify over these predicates to license their own inversion derivations.

Two API layers:

• Bool helpers (precedes, isSubjectCat, isSubjectWord, auxPrecedesSubject, subjectPrecedesAux) — computational, used by existing theorem statements ... ws = true.
• Prop wrappers (IsSubjectWord, AuxPrecedesSubject, SubjectPrecedesAux) with Decidable instances — for new propositional use sites per the project's Bool→Prop migration policy.

Note isSubjectWord is so named (rather than isSubject) to avoid a naming collision with UD.DepRel.isSubject, which classifies dependency labels rather than words.

def Inversion.precedes (p q : Word → Bool) (ws : List Word) : Bool

Does the earliest p-word precede the earliest q-word in ws?

Returns false if no p-word or no q-word exists. Note this is weaker than the existential reading "∃ i, j, p (ws[i]) ∧ q (ws[j]) ∧ i < j" — only the first match of each predicate is considered. For inversion-style word-order questions this matches the linguist's intended reading (was the first auxiliary before the first subject?).

Equations

• Inversion.precedes p q ws = match List.findIdx? p ws, List.findIdx? q ws with | some i, some j => decide (i < j) | x, x_1 => false

def Inversion.isSubjectCat (c : UD.UPOS) : Bool

Is this a nominal category that can be a subject?

Equations

• Inversion.isSubjectCat c = (c == UD.UPOS.PROPN || c == UD.UPOS.NOUN || c == UD.UPOS.PRON)

def Inversion.isSubjectWord (w : Word) : Bool

Is this word a non-wh subject?

Named isSubjectWord rather than isSubject to avoid a name collision with UD.DepRel.isSubject (which classifies dependency labels).

Equations

• Inversion.isSubjectWord w = (Inversion.isSubjectCat w.cat && !w.features.wh)

def Inversion.auxPrecedesSubject (ws : List Word) : Bool

Does the auxiliary precede the subject?

Equations

• Inversion.auxPrecedesSubject ws = Inversion.precedes (fun (x : Word) => x.cat == UD.UPOS.AUX) Inversion.isSubjectWord ws

def Inversion.subjectPrecedesAux (ws : List Word) : Bool

Does the subject precede the auxiliary?

Equations

• Inversion.subjectPrecedesAux ws = Inversion.precedes Inversion.isSubjectWord (fun (x : Word) => x.cat == UD.UPOS.AUX) ws

def Inversion.IsSubjectWord (w : Word) : Prop

Prop-valued companion to isSubjectWord.

Equations

• Inversion.IsSubjectWord w = (Inversion.isSubjectWord w = true)

def Inversion.AuxPrecedesSubject (ws : List Word) : Prop

Prop-valued companion to auxPrecedesSubject.

Equations

• Inversion.AuxPrecedesSubject ws = (Inversion.auxPrecedesSubject ws = true)

def Inversion.SubjectPrecedesAux (ws : List Word) : Prop

Prop-valued companion to subjectPrecedesAux.

Equations

• Inversion.SubjectPrecedesAux ws = (Inversion.subjectPrecedesAux ws = true)

@[implicit_reducible]

instance Inversion.instDecidableIsSubjectWord (w : Word) : Decidable (IsSubjectWord w)

Equations

• Inversion.instDecidableIsSubjectWord w = Inversion.instDecidableIsSubjectWord._aux_1 w

@[implicit_reducible]

instance Inversion.instDecidableAuxPrecedesSubject (ws : List Word) : Decidable (AuxPrecedesSubject ws)

Equations

• Inversion.instDecidableAuxPrecedesSubject ws = Inversion.instDecidableAuxPrecedesSubject._aux_1 ws

@[implicit_reducible]

instance Inversion.instDecidableSubjectPrecedesAux (ws : List Word) : Decidable (SubjectPrecedesAux ws)

Equations

• Inversion.instDecidableSubjectPrecedesAux ws = Inversion.instDecidableSubjectPrecedesAux._aux_1 ws