Scenarios

A scenario is the pair of co-arguments of a clause ordered by role rank, A over P in a monotransitive clause and R over T in a ditransitive one, each carried as its value on a referential prominence scale. Scenarios are ordered componentwise with the lower-ranked value reversed, so a scenario lies above another when its higher-ranked argument is at least as prominent and its lower-ranked one at most as prominent. The kind of a scenario compares its two values: downstream when the higher-ranked argument is the more prominent, upstream when it is the less prominent, and balanced when they tie. The direct and inverse contexts of cyclic Agree, the IO–DO combinations the person-case constraint restricts, and co-argument-sensitive indexing are all scenarios over the person scale, and Haspelmath's argument coding splits are scenarios over his prominence scales.

Main declarations

• Clause.Scenario: the two prominence values, high and low, with Scenario.map and Scenario.equivProd, ordered with ⊤ = ⟨⊤, ⊥⟩.
• Clause.Scenario.Kind: upstream, balanced, downstream, as a bounded linear order in that order.
• Clause.Scenario.kind: the kind of a scenario over a linearly ordered scale, monotone (kind_mono) and unchanged by a strictly monotone map of the scale (kind_map).
• Clause.Scenario.kind_lt_kind_iff: on a two-element scale one scenario's kind is below another's exactly when the scenario is below the other.

Implementation notes

The kind is the three-way comparison compare read into the three labels by Kind.ofOrdering, and the order on kinds, downstream above upstream, is Haspelmath's order of usualness (11). A scenario over a scale that is not linearly ordered, such as persons, is read on a rank map p as s.map p.

References

• [Has21c]
• [BR09]
• [Dea24]
• [WMZB+16]

structure Clause.Scenario (α : Type u_1) : Type u_1

A scenario records the prominence values of the two co-arguments of a clause, the higher-ranked one first. Haspelmath writes X > Y for ⟨X, Y⟩.

• high : α

  The prominence of the higher-ranked argument, A or R.

• low : α

  The prominence of the lower-ranked argument, P or T.

theorem Clause.Scenario.ext_iff {α : Type u_1} {x y : Scenario α} : x = y ↔ x.high = y.high ∧ x.low = y.low

theorem Clause.Scenario.ext {α : Type u_1} {x y : Scenario α} (high : x.high = y.high) (low : x.low = y.low) : x = y

def Clause.instDecidableEqScenario.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Scenario α✝) : Decidable (x✝ = x✝¹)

Equations

• Clause.instDecidableEqScenario.decEq { high := a, low := a_1 } { high := b, low := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Clause.instDecidableEqScenario {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Scenario α✝)

Equations

• Clause.instDecidableEqScenario = Clause.instDecidableEqScenario.decEq

@[instance_reducible]

instance Clause.instFintypeScenario {α✝ : Type u_1} [Fintype α✝] : Fintype (Scenario α✝)

Equations

• Clause.instFintypeScenario = Fintype.ofEquiv ((_ : α✝) × α✝) (Clause.Scenario.proxyTypeEquiv α✝)

def Clause.Scenario.map {α : Type u_1} {β : Type u_2} (f : α → β) (s : Scenario α) : Scenario β

Apply a map to both prominence values.

Equations

• Clause.Scenario.map f s = { high := f s.high, low := f s.low }

@[simp]

theorem Clause.Scenario.map_high {α : Type u_1} {β : Type u_2} (f : α → β) (s : Scenario α) : (map f s).high = f s.high

@[simp]

theorem Clause.Scenario.map_low {α : Type u_1} {β : Type u_2} (f : α → β) (s : Scenario α) : (map f s).low = f s.low

def Clause.Scenario.equivProd {α : Type u_1} : Scenario α ≃ α × α

A scenario is the pair of its higher- and lower-ranked values.

Equations

• Clause.Scenario.equivProd = { toFun := fun (s : Clause.Scenario α) => (s.high, s.low), invFun := fun (p : α × α) => { high := p.1, low := p.2 }, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Clause.Scenario.equivProd_symm_apply_low {α : Type u_1} (p : α × α) : (equivProd.symm p).low = p.2

@[simp]

theorem Clause.Scenario.equivProd_apply {α : Type u_1} (s : Scenario α) : equivProd s = (s.high, s.low)

@[simp]

theorem Clause.Scenario.equivProd_symm_apply_high {α : Type u_1} (p : α × α) : (equivProd.symm p).high = p.1

The order on scenarios

@[instance_reducible]

instance Clause.Scenario.instLE {α : Type u_1} [LE α] : LE (Scenario α)

Equations

• Clause.Scenario.instLE = { le := fun (s t : Clause.Scenario α) => s.high ≤ t.high ∧ t.low ≤ s.low }

theorem Clause.Scenario.le_def {α : Type u_1} [LE α] {s t : Scenario α} : s ≤ t ↔ s.high ≤ t.high ∧ t.low ≤ s.low

@[instance_reducible]

instance Clause.Scenario.instDecidableLE {α : Type u_1} [LE α] [DecidableLE α] : DecidableLE (Scenario α)

Equations

• x✝¹.instDecidableLE x✝ = decidable_of_iff' (x✝¹.high ≤ x✝.high ∧ x✝.low ≤ x✝¹.low) ⋯

@[instance_reducible]

instance Clause.Scenario.instBoundedOrder {α : Type u_1} [LE α] [BoundedOrder α] : BoundedOrder (Scenario α)

The top scenario is ⟨⊤, ⊥⟩ and the bottom one ⟨⊥, ⊤⟩.

Equations

• Clause.Scenario.instBoundedOrder = { top := { high := ⊤, low := ⊥ }, le_top := ⋯, bot := { high := ⊥, low := ⊤ }, bot_le := ⋯ }

@[simp]

theorem Clause.Scenario.top_high {α : Type u_1} [LE α] [BoundedOrder α] : ⊤.high = ⊤

@[simp]

theorem Clause.Scenario.top_low {α : Type u_1} [LE α] [BoundedOrder α] : ⊤.low = ⊥

@[simp]

theorem Clause.Scenario.bot_high {α : Type u_1} [LE α] [BoundedOrder α] : ⊥.high = ⊥

@[simp]

theorem Clause.Scenario.bot_low {α : Type u_1} [LE α] [BoundedOrder α] : ⊥.low = ⊤

@[instance_reducible]

instance Clause.Scenario.instPreorder {α : Type u_1} [Preorder α] : Preorder (Scenario α)

Equations

• Clause.Scenario.instPreorder = { toLE := Clause.Scenario.instLE, lt := fun (a b : Clause.Scenario α) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[instance_reducible]

instance Clause.Scenario.instDecidableLTOfDecidableLE {α : Type u_1} [Preorder α] [DecidableLE α] : DecidableLT (Scenario α)

Equations

• Clause.Scenario.instDecidableLTOfDecidableLE = decidableLTOfDecidableLE

theorem Clause.Scenario.high_mono {α : Type u_1} [Preorder α] : Monotone high

theorem Clause.Scenario.low_anti {α : Type u_1} [Preorder α] : Antitone low

@[instance_reducible]

instance Clause.Scenario.instPartialOrder {α : Type u_1} [PartialOrder α] : PartialOrder (Scenario α)

Equations

• Clause.Scenario.instPartialOrder = { toPreorder := Clause.Scenario.instPreorder, le_antisymm := ⋯ }

Kinds

inductive Clause.Scenario.Kind : Type

The kinds of scenario, in order of usualness, Haspelmath's three kinds of scenarios. A kind classifies what a scenario means, not how it is coded, so it is not called a direction, the category that direct and inverse markers realize.

• upstream : Kind
• balanced : Kind
• downstream : Kind

@[instance_reducible]

instance Clause.Scenario.instDecidableEqKind : DecidableEq Kind

Equations

• Clause.Scenario.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Clause.Scenario.instFintypeKind : Fintype Kind

Equations

• Clause.Scenario.instFintypeKind = { elems := { val := ↑Clause.Scenario.Kind.enumList, nodup := Clause.Scenario.Kind.enumList_nodup }, complete := Clause.Scenario.instFintypeKind._proof_1 }

@[instance_reducible]

instance Clause.Scenario.instReprKind : Repr Kind

Equations

• Clause.Scenario.instReprKind = { reprPrec := Clause.Scenario.instReprKind.repr }

def Clause.Scenario.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Scenario.Kind.instLinearOrder : LinearOrder Kind

Equations

• Clause.Scenario.Kind.instLinearOrder = LinearOrder.lift' (fun (x : Clause.Scenario.Kind) => x.ctorIdx) Clause.Scenario.Kind.instLinearOrder._proof_1

instance Clause.Scenario.Kind.instNontrivial : Nontrivial Kind

@[instance_reducible]

instance Clause.Scenario.Kind.instBoundedOrder : BoundedOrder Kind

⊥ = upstream, ⊤ = downstream.

Equations

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

theorem Clause.Scenario.Kind.le_balanced_iff {k : Kind} : k ≤ balanced ↔ k ≠ downstream

theorem Clause.Scenario.Kind.balanced_le_iff {k : Kind} : balanced ≤ k ↔ k ≠ upstream

def Clause.Scenario.Kind.ofOrdering : Ordering → Kind

The kind a comparison of the higher-ranked argument's prominence with the lower-ranked one's yields.

Equations

• Clause.Scenario.Kind.ofOrdering Ordering.lt = Clause.Scenario.Kind.upstream
• Clause.Scenario.Kind.ofOrdering Ordering.eq = Clause.Scenario.Kind.balanced
• Clause.Scenario.Kind.ofOrdering Ordering.gt = Clause.Scenario.Kind.downstream

@[simp]

theorem Clause.Scenario.Kind.ofOrdering_eq_upstream {o : Ordering} : ofOrdering o = upstream ↔ o = Ordering.lt

@[simp]

theorem Clause.Scenario.Kind.ofOrdering_eq_balanced {o : Ordering} : ofOrdering o = balanced ↔ o = Ordering.eq

@[simp]

theorem Clause.Scenario.Kind.ofOrdering_eq_downstream {o : Ordering} : ofOrdering o = downstream ↔ o = Ordering.gt

def Clause.Scenario.kind {α : Type u_1} [LinearOrder α] (s : Scenario α) : Kind

A scenario is downstream when its higher-ranked argument ranks higher on the scale, upstream when it ranks lower, and balanced when the two tie.

Equations

• s.kind = Clause.Scenario.Kind.ofOrdering (compare s.high s.low)

theorem Clause.Scenario.kind_eq_downstream_iff {α : Type u_1} [LinearOrder α] {s : Scenario α} : s.kind = Kind.downstream ↔ s.low < s.high

theorem Clause.Scenario.kind_eq_upstream_iff {α : Type u_1} [LinearOrder α] {s : Scenario α} : s.kind = Kind.upstream ↔ s.high < s.low

theorem Clause.Scenario.kind_eq_balanced_iff {α : Type u_1} [LinearOrder α] {s : Scenario α} : s.kind = Kind.balanced ↔ s.high = s.low

theorem Clause.Scenario.kind_le_balanced_iff {α : Type u_1} [LinearOrder α] {s : Scenario α} : s.kind ≤ Kind.balanced ↔ s.high ≤ s.low

theorem Clause.Scenario.balanced_le_kind_iff {α : Type u_1} [LinearOrder α] {s : Scenario α} : Kind.balanced ≤ s.kind ↔ s.low ≤ s.high

theorem Clause.Scenario.kind_mono {α : Type u_1} [LinearOrder α] : Monotone kind

Raising the higher-ranked argument or lowering the lower-ranked one never lowers the kind.

theorem Clause.Scenario.kind_map {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : StrictMono f) (s : Scenario α) : (map f s).kind = s.kind

A strictly monotone map of the scale preserves the kind.

theorem Clause.Scenario.map_le_map_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] {s t : Scenario α} [LinearOrder β] {f : α → β} (hf : StrictMono f) : map f s ≤ map f t ↔ s ≤ t

theorem Clause.Scenario.map_lt_map_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] {s t : Scenario α} [LinearOrder β] {f : α → β} (hf : StrictMono f) : map f s < map f t ↔ s < t

Two-element scales

theorem Clause.Scenario.kind_lt_kind_iff {α : Type u_1} [LinearOrder α] {s t : Scenario α} [BoundedOrder α] [IsSimpleOrder α] : s.kind < t.kind ↔ s < t

On a two-element scale a scenario's kind is below another's exactly when the scenario is below the other, since such a scale is Bool.

theorem Clause.Scenario.kind_eq_downstream_iff_eq_top {α : Type u_1} [LinearOrder α] {s : Scenario α} [BoundedOrder α] [IsSimpleOrder α] : s.kind = Kind.downstream ↔ s = ⊤

On a two-element scale the downstream scenario is ⊤ = ⟨⊤, ⊥⟩ alone.