refactor(Syntax/Minimalist): extension order read from cited structures

Linglib/Syntax/Cartography.lean

@@ -1,7 +1,7 @@
 module
 
 public import Linglib.Core.Order.OrdConnected
-public import Linglib.Syntax.Minimalist.ExtendedProjection
+public import Linglib.Syntax.Minimalist.Category
 public import Mathlib.Order.Interval.Set.LinearOrder
 public import Mathlib.Tactic.DeriveFintype
 
@@ -20,22 +20,23 @@ A clause that projects up to a head contains every head below it, so the heads o
 `h` are the lower set `Set.Iic h`, and the heads in a clause of size `b` but not in one of size `a`
 form the interval `Set.Ioc a b` (`Set.Iic_sdiff_Iic`). A later proposal that adds heads to
 Cinque's refines the order: its hierarchy receives an order embedding of `Cartography.Head`, and a
-head it places immediately above or below one of Cinque's covers it or is covered by it. The
-categorial features of `Minimalist.Cat` coarsen the order: `Cartography.Head.cat` sends each head
-to its category, and a higher head's category has at least as high an F-value in the verbal
-extended projection, so each F-value is taken by an interval of the hierarchy. Cinque's own kinds of head are not:
+head it places immediately above or below one of Cinque's covers it or is covered by it.
+`Cartography.Head.cat` sends each head to its category in `Minimalist.Cat`, and the list
+`Cartography.Head.hierarchy` of the heads bottom-up is one of the structures the extension order
+of `Minimalist.Cat` is read from. Cinque's own kinds of head are not intervals of the hierarchy:
 moods, modalities, tenses and aspects interleave.
 
 ## Main definitions
 
 * `Cartography.Head`: the heads of the universal hierarchy, with its linear order.
 * `Cartography.Head.family`: the kind of head, `Cartography.Family`.
 * `Cartography.Head.cat`: the category of a head in `Minimalist.Cat`.
+* `Cartography.Head.hierarchy`: the heads bottom-up, as a list.
 
 ## Main statements
 
-* `Cartography.Head.monotone_fValue_cat`: the F-values of the categories are monotone in the
-  hierarchy.
+* `Cartography.Head.mem_hierarchy`, `Cartography.Head.pairwise_hierarchy`: the list holds every
+  head once, in order.
 * `Cartography.Head.not_isContiguous_family`: the kinds of head are not intervals of it.
 
 ## Implementation notes
@@ -48,12 +49,14 @@ moods, modalities, tenses and aspects interleave.
 * Cinque marks the pairing of *characteristically* with generic or progressive aspect, and the
   head of *always*, as uncertain.
 * `Head.cat` sends Cinque's four aspect heads below Voice to inner aspect, the aspect of the v
-  shell, the other aspect heads to outer aspect, and the moods other than the evidential to
-  `Cat.Mood`.
+  shell, the other aspect heads to outer aspect, the speech-act mood to the speech-act head, as
+  Speas and Tenny project their speech-act phrase from Cinque's speech-act mood head, and the
+  other moods but the evidential to `Cat.Mood`.
 
 ## References
 
 * [cinque-1999]
+* [speas-tenny-2003]
 -/
 
 @[expose] public section
@@ -154,18 +157,19 @@ def cat : Head → Minimalist.Cat
   | tAnterior | tFuture | tPast => .T
   | modVolitional | modPossibility | modNecessity | modEpistemic => .Mod
   | moodEvidential => .Evid
-  | moodIrrealis | moodEvaluative | moodSpeechAct => .Mood
+  | moodSpeechAct => .SA
+  | moodIrrealis | moodEvaluative => .Mood
   | _ => .Asp
 
 theorem family_cat (h : Head) : h.cat.family = .verbal := by
   cases h <;> rfl
 
-theorem monotone_fValue_cat : Monotone fun h : Head ↦ h.cat.fValue := by
-  unfold Monotone
-  decide
+/-- The heads, bottom-up. -/
+def hierarchy : List Head := (List.range 30).map Head.ofNat
+
+theorem mem_hierarchy (h : Head) : h ∈ hierarchy := by cases h <;> decide
 
-theorem isContiguous_fValue_cat : IsContiguous fun h : Head ↦ h.cat.fValue :=
-  monotone_fValue_cat.isContiguous
+theorem pairwise_hierarchy : hierarchy.Pairwise (· < ·) := by decide
 
 /-- No order on the kinds of head is coarsened by the hierarchy
 (`isContiguous_iff_exists_monotone`): the anterior tense and the volitional modality sit among the

Linglib/Syntax/Minimalist/Category.lean

@@ -80,8 +80,7 @@ inductive Cat where
   | Num
   /-- The demonstrative, above number ([cinque-2005]). -/
   | Dem
-  /-- Borer's dividing head, the classifier position, between little n and `Num`
-  ([borer-2005]). -/
+  /-- Borer's dividing head, the classifier position, below `Num` ([borer-2005]). -/
   | Q
   /-- Voice, which introduces the external argument ([kratzer-1996], [schaefer-2008]). -/
   | Voice

Linglib/Syntax/Minimalist/Clause/Size.lean

@@ -13,25 +13,24 @@ public import Linglib.Syntax.Minimalist.Clause.Spine
 A clausal complement is measured by its highest projected head. Wurmbrand classifies infinitival
 complements by the structure they project, a bare vP for restructuring, a TP for propositional
 attitudes and a modal projection for future infinitives, beside the full CP of a finite clause,
-and a complement is at most as large as another when its highest head is no higher in the
-functional sequence. Two sizes with distinct heads at one level, tense and negation for instance,
-are then equivalent but not equal, so the order is a preorder. The size of a clause spine is its
-highest head. On extended projections the extension order of spines, inclusion of labels, refines
-the size order, and the standard sizes are those of the standard spines.
+and a complement is at most as large as another when its highest head is extended by the other's.
+Two sizes with distinct heads at one level, tense and negation for instance, are then equivalent
+but not equal, so the order is a preorder, and two sizes no source relates, a nominalized clause
+and a CP, are incomparable. The size of a clause spine is its highest head. On extended
+projections the extension order of spines, inclusion of labels, refines the size order, and the
+standard sizes are those of the standard spines.
 
 ## Main definitions
 
 * `Minimalist.ComplementSize`: a clausal complement measured by its highest head.
-* `Minimalist.ComplementSize.fLevel`: the functional level of the highest head.
 * `Minimalist.ClauseSpine.size`: the size of a spine, its highest head.
 * `Minimalist.ComplementSize.vP`, `Minimalist.ComplementSize.tP`,
   `Minimalist.ComplementSize.modP`, `Minimalist.ComplementSize.finP`,
   `Minimalist.ComplementSize.cP`: the standard sizes.
 
 ## Main results
 
-* `Minimalist.ComplementSize.le_def`, `Minimalist.ComplementSize.lt_def`: the order is that of
-  functional levels.
+* `Minimalist.ComplementSize.le_def`: the order is the extension order of the highest heads.
 * `Minimalist.ClauseSpine.size_le_size`: on extended projections, the extension order refines the
   size order, so that the standard sizes ascend as their spines do
   (`Minimalist.ComplementSize.vP_le_tP`, `Minimalist.ComplementSize.tP_le_cP`).
@@ -56,20 +55,21 @@ namespace ComplementSize
 
 variable {a b : ComplementSize}
 
-/-- The functional level of a complement is that of its highest head. -/
-def fLevel (cs : ComplementSize) : ℕ := cs.highestHead.fValue
+/-- Complement sizes are ordered by the extension order of their highest heads, so that a
+complement is at most another when the other's highest head extends its own. -/
+instance : Preorder ComplementSize where
+  le a b := a.highestHead.ExtendsTo b.highestHead
+  le_refl _ := refl_of Cat.ExtendsTo _
+  le_trans _ _ _ := trans_of Cat.ExtendsTo
 
-/-- Complement sizes are ordered by functional level, so that a complement is at most another when
-it projects no higher in the functional sequence. -/
-instance : Preorder ComplementSize := Preorder.lift fLevel
+instance : DecidableLE ComplementSize := fun a b ↦
+  inferInstanceAs (Decidable (a.highestHead.ExtendsTo b.highestHead))
 
-instance : DecidableLE ComplementSize := fun a b ↦ inferInstanceAs (Decidable (a.fLevel ≤ b.fLevel))
+instance : DecidableLT ComplementSize := fun a b ↦
+  inferInstanceAs (Decidable (a.highestHead.ExtendsTo b.highestHead ∧
+    ¬ b.highestHead.ExtendsTo a.highestHead))
 
-instance : DecidableLT ComplementSize := fun a b ↦ inferInstanceAs (Decidable (a.fLevel < b.fLevel))
-
-theorem le_def : a ≤ b ↔ a.fLevel ≤ b.fLevel := Iff.rfl
-
-theorem lt_def : a < b ↔ a.fLevel < b.fLevel := Iff.rfl
+theorem le_def : a ≤ b ↔ a.highestHead.ExtendsTo b.highestHead := Iff.rfl
 
 end ComplementSize
 
@@ -83,29 +83,29 @@ variable {s t : ClauseSpine} {c : Cat}
 the least size. -/
 def size (s : ClauseSpine) : ComplementSize := ⟨s.heads.getLastD .V⟩
 
-private theorem fValue_le_getLastD {l : List Cat} (hp : l.Pairwise Cat.ExtendsTo) (hc : c ∈ l) :
-    c.fValue ≤ (l.getLastD .V).fValue := by
+private theorem extendsTo_getLastD {l : List Cat} (hp : l.Pairwise Cat.ExtendsTo) (hc : c ∈ l) :
+    c.ExtendsTo (l.getLastD .V) := by
   have hne : l ≠ [] := List.ne_nil_of_mem hc
   rw [List.getLastD_eq_getLast?, List.getLast?_eq_some_getLast hne, Option.getD_some]
   rw [← List.dropLast_append_getLast hne, List.mem_append, List.mem_singleton] at hc
   rcases hc with hc | rfl
   · rw [← List.dropLast_append_getLast hne, List.pairwise_append] at hp
-    exact (hp.2.2 c hc _ (List.mem_singleton_self _)).2
-  · exact le_rfl
-
-theorem IsExtendedProjection.fValue_le_fLevel (hs : s.IsExtendedProjection) (hc : c ∈ s) :
-    c.fValue ≤ s.size.fLevel :=
-  fValue_le_getLastD hs.pairwise hc
-
-/-- On extended projections, the extension order refines the size order: a spine whose heads
-another projects is no larger. -/
-theorem size_le_size (h : s ≤ t) (ht : t.IsExtendedProjection) : s.size ≤ t.size := by
-  rcases List.eq_nil_or_concat s.heads with hs | ⟨l, c, hs⟩
-  · show (s.heads.getLastD .V).fValue ≤ t.size.fLevel
-    simp [hs, Cat.fValue]
-  · show (s.heads.getLastD .V).fValue ≤ t.size.fLevel
-    rw [hs, List.concat_eq_append, List.getLastD_concat]
-    exact ht.fValue_le_fLevel (le_iff_forall_mem.1 h c (by simp [hs]))
+    exact hp.2.2 c hc _ (List.mem_singleton_self _)
+  · exact refl_of Cat.ExtendsTo _
+
+/-- In an extended projection every head is extended by the highest one. -/
+theorem IsExtendedProjection.extendsTo_size (hs : s.IsExtendedProjection) (hc : c ∈ s) :
+    c.ExtendsTo s.size.highestHead :=
+  extendsTo_getLastD hs.pairwise hc
+
+/-- On extended projections, the extension order refines the size order: a nonempty spine whose
+heads another projects is no larger. -/
+theorem size_le_size (h : s ≤ t) (ht : t.IsExtendedProjection) (hs : s.heads ≠ []) :
+    s.size ≤ t.size := by
+  obtain ⟨l, c, hlc⟩ := (List.eq_nil_or_concat s.heads).resolve_left hs
+  show (s.heads.getLastD .V).ExtendsTo t.size.highestHead
+  rw [hlc, List.concat_eq_append, List.getLastD_concat]
+  exact ht.extendsTo_size (le_iff_forall_mem.1 h c (by simp [hlc]))
 
 end ClauseSpine
 
@@ -129,9 +129,12 @@ def finP : ComplementSize := ⟨.Fin⟩
 def cP : ComplementSize := ClauseSpine.cP.size
 
 /-- The standard sizes ascend as their spines do. -/
-theorem vP_le_tP : vP ≤ tP := ClauseSpine.size_le_size ClauseSpine.vP_le_tP (by decide)
+theorem vP_le_tP : vP ≤ tP :=
+  ClauseSpine.size_le_size ClauseSpine.vP_le_tP (by decide +kernel) (List.cons_ne_nil _ _)
 
-theorem tP_le_cP : tP ≤ cP := ClauseSpine.size_le_size ClauseSpine.tP_le_cP (by decide)
+theorem tP_le_cP : tP ≤ cP :=
+  ClauseSpine.size_le_size ClauseSpine.tP_le_cP ClauseSpine.cP_isExtendedProjection
+    (List.cons_ne_nil _ _)
 
 end ComplementSize
 

Linglib/Syntax/Minimalist/Clause/Spine.lean

@@ -86,7 +86,7 @@ instance (P : Cat → Prop) [DecidablePred P] (s : ClauseSpine) : Decidable (∃
 /-! ### Extended projections -/
 
 /-- A spine is an extended projection when each head extends the one below it, so that its heads
-are of one family and their F-values do not decrease. -/
+are of one family. -/
 def IsExtendedProjection (s : ClauseSpine) : Prop := s.heads.IsChain Cat.ExtendsTo
 
 instance (s : ClauseSpine) : Decidable s.IsExtendedProjection :=
@@ -171,7 +171,7 @@ theorem vP_le_tP : vP ≤ tP := by decide
 
 theorem tP_le_cP : tP ≤ cP := by decide
 
-theorem cP_isExtendedProjection : cP.IsExtendedProjection := by decide
+theorem cP_isExtendedProjection : cP.IsExtendedProjection := by decide +kernel
 
 end ClauseSpine