φ-probes

This file specializes Probe to φ-features, as probes over Agreement.Bundles relativized by the feature they seek, among them Preminger's person probe π⁰, which seeks [participant], and number probe #⁰, which seeks [plural], and the φ-goals they search, nominals with or without valued Case.

Main definitions

• Agreement.Bundle.IsParticipant: a cell bears the [participant] segment.
• Minimalist.Probe.Target, Agreement.Bundle.visibleTo: the features a relativized probe seeks, and the cells that bear them.
• Minimalist.Probe.Target.toProbe: a target's denotation as a Probe over φ-cells.
• Minimalist.PhiGoal: a nominal as a φ-goal, its case if already valued and its φ-cell.

References

• [Pre14]
• [HR02]
• [Cho00]

def Agreement.Bundle.IsParticipant (c : Bundle) : Prop

A cell bears the [participant] segment, by the person geometry of [HR02].

Equations

• c.IsParticipant = (Minimalist.PersonSegment.participant ∈ Minimalist.PersonSegment.spec c.person)

@[instance_reducible]

instance Minimalist.instDecidablePredBundleIsParticipant : DecidablePred Agreement.Bundle.IsParticipant

Equations

• Minimalist.instDecidablePredBundleIsParticipant x✝ = Minimalist.instDecidablePredBundleIsParticipant._aux_1 x✝

inductive Minimalist.Probe.Target : Type

The feature a relativized φ-probe seeks.

• participant : Target

  π⁰, the person probe, seeks [participant].

• plural : Target

  #⁰, the number probe, seeks [plural].

@[instance_reducible]

instance Minimalist.Probe.instDecidableEqTarget : DecidableEq Target

Equations

• Minimalist.Probe.instDecidableEqTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.Probe.instReprTarget.repr : Target → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.Probe.instReprTarget : Repr Target

Equations

• Minimalist.Probe.instReprTarget = { reprPrec := Minimalist.Probe.instReprTarget.repr }

def Agreement.Bundle.visibleTo (c : Bundle) : Minimalist.Probe.Target → Bool

A φ-cell is visible to a relativized probe when it bears the feature the probe seeks; the probe skips the cells that lack it.

Equations

• c.visibleTo Minimalist.Probe.Target.participant = decide c.IsParticipant
• c.visibleTo Minimalist.Probe.Target.plural = decide c.IsPlural

def Minimalist.Probe.Target.toProbe (t : Target) : Probe Agreement.Bundle

A Probe.Target denotes the probe over φ-cells relativized to the feature it seeks, π⁰ being Probe.Target.participant.toProbe.

Equations

• t.toProbe = Minimalist.Probe.relativized fun (x : Agreement.Bundle) => x.visibleTo t

structure Minimalist.PhiGoal : Type

A goal of a φ-probe records the case a head of its own has valued, if any, and its φ-cell. A relativized probe reads the cell for visibility, and Agree reads the case for activity, a goal being active iff its case is unvalued, the Active Goal Hypothesis of [Cho00].

• valuedCase : Option Case
• cell : Agreement.Bundle

@[instance_reducible]

instance Minimalist.instDecidableEqPhiGoal : DecidableEq PhiGoal

Equations

• Minimalist.instDecidableEqPhiGoal = Minimalist.instDecidableEqPhiGoal.decEq

def Minimalist.instDecidableEqPhiGoal.decEq (x✝ x✝¹ : PhiGoal) : Decidable (x✝ = x✝¹)

Equations

• Minimalist.instDecidableEqPhiGoal.decEq { valuedCase := a, cell := a_1 } { valuedCase := b, cell := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Minimalist.instReprPhiGoal.repr : PhiGoal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.instReprPhiGoal : Repr PhiGoal

Equations

• Minimalist.instReprPhiGoal = { reprPrec := Minimalist.instReprPhiGoal.repr }

def Minimalist.PhiGoal.isActive (g : PhiGoal) : Bool

A goal is active, visible to Agree, iff its case is unvalued.

Equations

• g.isActive = g.valuedCase.isNone

def Minimalist.PhiGoal.valued (c : Case) (cell : Agreement.Bundle) : PhiGoal

PhiGoal.valued c cell is a nominal whose case c a head of its own has already valued, so that it is inactive for Agree.

Equations

• Minimalist.PhiGoal.valued c cell = { valuedCase := some c, cell := cell }

def Minimalist.PhiGoal.unvalued (cell : Agreement.Bundle) : PhiGoal

PhiGoal.unvalued cell is a nominal with unvalued case, so that it is active for Agree.

Equations

• Minimalist.PhiGoal.unvalued cell = { valuedCase := none, cell := cell }

@[simp]

theorem Minimalist.PhiGoal.cell_valued (c : Case) (cell : Agreement.Bundle) : (valued c cell).cell = cell

@[simp]

theorem Minimalist.PhiGoal.valuedCase_valued (c : Case) (cell : Agreement.Bundle) : (valued c cell).valuedCase = some c

@[simp]

theorem Minimalist.PhiGoal.cell_unvalued (cell : Agreement.Bundle) : (unvalued cell).cell = cell

@[simp]

theorem Minimalist.PhiGoal.valuedCase_unvalued (cell : Agreement.Bundle) : (unvalued cell).valuedCase = none

@[simp]

theorem Minimalist.PhiGoal.isActive_valued (c : Case) (cell : Agreement.Bundle) : (valued c cell).isActive = false

@[simp]

theorem Minimalist.PhiGoal.isActive_unvalued (cell : Agreement.Bundle) : (unvalued cell).isActive = true

@[simp]

theorem Minimalist.PhiGoal.valued_ne_unvalued (c : Case) (cell cell' : Agreement.Bundle) : valued c cell ≠ unvalued cell'

@[simp]

theorem Minimalist.PhiGoal.unvalued_ne_valued (c : Case) (cell cell' : Agreement.Bundle) : unvalued cell' ≠ valued c cell