The Elsewhere Condition

This file defines Elsewhere winners — ≤-minimal applicable rules of exponence under the specificity preorder ([Kip73]) — and the prediction relation they induce.

Main definitions

• IsElsewhereWinner: a ≤-minimal applicable rule of a vocabulary at a context.
• Coherent: equivalent rules carry the same exponent.
• Realizes: some Elsewhere winner carries the given exponent.

Elsewhere winners

theorem Minimal.antisymmRel {α : Type u_4} [Preorder α] {P : α → Prop} {x y : α} (hx : Minimal P x) (hy : Minimal P y) (h : y ≤ x ∨ x ≤ y) : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) x y

Two comparable minimal elements of the same predicate are equivalent. [UPSTREAM] candidate for Mathlib/Order/Minimal.lean.

@[reducible, inline]

abbrev Morphology.Exponence.IsElsewhereWinner {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [Preorder R] (v : List R) (c : Ctx) (r : R) : Prop

A ≤-minimal applicable rule of v at c.

Equations

• Morphology.Exponence.IsElsewhereWinner v c r = Minimal (fun (s : R) => s ∈ v ∧ Morphology.Exponence.Applies s c) r

def Morphology.Exponence.Coherent {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [Preorder R] (v : List R) : Prop

A vocabulary is coherent if equivalent rules carry the same exponent.

Equations

• Morphology.Exponence.Coherent v = ∀ r ∈ v, ∀ s ∈ v, AntisymmRel (fun (x1 x2 : R) => x1 ≤ x2) r s → Morphology.Exponence.exponent r = Morphology.Exponence.exponent s

theorem Morphology.Exponence.IsElsewhereWinner.exponent_eq {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [Preorder R] {v : List R} {c : Ctx} {r s : R} (hv : Coherent v) (hr : IsElsewhereWinner v c r) (hs : IsElsewhereWinner v c s) (h : s ≤ r ∨ r ≤ s) : exponent r = exponent s

Comparable winners of a coherent vocabulary carry the same exponent.

theorem Morphology.Exponence.exists_isElsewhereWinner {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [Preorder R] {v : List R} {c : Ctx} (h : ∃ r ∈ v, Applies r c) : ∃ (r : R), IsElsewhereWinner v c r

A vocabulary with an applicable rule has an Elsewhere winner.

The prediction relation

def Morphology.Exponence.Realizes {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [Preorder R] (v : List R) (c : Ctx) (φ : E) : Prop

φ is realized at c when some Elsewhere winner carries it.

Equations

• Morphology.Exponence.Realizes v c φ = ∃ (r : R), Morphology.Exponence.IsElsewhereWinner v c r ∧ Morphology.Exponence.exponent r = φ

theorem Morphology.Exponence.Realizes.eq {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [Preorder R] {v : List R} {c : Ctx} {φ ψ : E} (hv : Coherent v) (hcmp : ∀ ⦃r s : R⦄, IsElsewhereWinner v c r → IsElsewhereWinner v c s → s ≤ r ∨ r ≤ s) (hφ : Realizes v c φ) (hψ : Realizes v c ψ) : φ = ψ

Over a coherent vocabulary with comparable winners, the prediction is unique.