Resolution rules

This file defines resolution rules, which give the agreement form of a coordination from its conjuncts, and their application in order.

A resolution rule is of one of two types: at least one conjunct is of a sort (type A), or every conjunct is (type B), and the rule then selects a form; the logically possible type referring to a majority of the conjuncts is unattested. A language's rules are ordered, the first that applies selects the form, and a coordination to which no rule applies has no resolved form, an ineffable coordination. The final rule is often unconditional, an "otherwise" clause, and then every coordination has a form. The sort may be read off the conjuncts' gender, a syntactic rule, or their meaning, a semantic rule; the descriptor type is a parameter.

Rules of both types see only which descriptors occur among the conjuncts, never how many conjuncts bear one, so they cannot count: number resolution, which gives two singulars the dual and three the plural, is not of this form.

Main definitions

• Agreement.ResolutionRule: a rule, of type A (any) or type B (all), with its sort and the form it selects.
• Agreement.ResolutionRule.Applies: whether a rule applies to a list of conjuncts.
• Agreement.ResolutionRule.resolve: the form the first applicable rule of an ordered list selects.

Main results

• Agreement.ResolutionRule.resolve_congr: resolution depends only on which descriptors occur among the conjuncts.
• Agreement.ResolutionRule.resolve_any_otherwise: a type-A rule and its default are the type-B rule for the complementary sort with the two forms swapped.
• Agreement.ResolutionRule.resolve_factorsThrough: rules reading their sorts through a map resolve through it.

References

• [Cor91] — chapter 9; the two types, §9.4, pp. 279–280, and §9.6, p. 290
• [Giv70] — the resolution of gender conflicts in Bantu
• [Cor06] — the standard monograph on agreement

inductive Agreement.ResolutionRule (α : Type u_1) (G : Type u_2) : Type (max u_1 u_2)

A resolution rule: at least one conjunct (any) or every conjunct (all) of a sort, and the form it selects.

• any {α : Type u_1} {G : Type u_2} (p : α → Prop) [DecidablePred p] (g : G) : ResolutionRule α G

  The type-A rule: some conjunct is of the sort p.

• all {α : Type u_1} {G : Type u_2} (p : α → Prop) [DecidablePred p] (g : G) : ResolutionRule α G

  The type-B rule: every conjunct is of the sort p.

def Agreement.ResolutionRule.pred {α : Type u_1} {G : Type u_3} : ResolutionRule α G → α → Prop

The sort a rule asks of its conjuncts.

Equations

• (Agreement.ResolutionRule.any p g).pred = p
• (Agreement.ResolutionRule.all p g).pred = p

def Agreement.ResolutionRule.out {α : Type u_1} {G : Type u_3} : ResolutionRule α G → G

The form a rule selects.

Equations

• (Agreement.ResolutionRule.any p g).out = g
• (Agreement.ResolutionRule.all p g).out = g

def Agreement.ResolutionRule.Applies {α : Type u_1} {G : Type u_3} : ResolutionRule α G → List α → Prop

Whether the rule applies to a coordination.

Equations

• (Agreement.ResolutionRule.any p g).Applies x✝ = ∃ (c : α), c ∈ x✝ ∧ p c
• (Agreement.ResolutionRule.all p g).Applies x✝ = ∀ (c : α), c ∈ x✝ → p c

@[instance_reducible]

instance Agreement.ResolutionRule.instDecidableApplies {α : Type u_1} {G : Type u_3} (r : ResolutionRule α G) (cs : List α) : Decidable (r.Applies cs)

Equations

• (Agreement.ResolutionRule.any p g).instDecidableApplies x✝ = Agreement.ResolutionRule.instDecidableApplies._aux_1 p inst g x✝
• (Agreement.ResolutionRule.all p g).instDecidableApplies x✝ = Agreement.ResolutionRule.instDecidableApplies._aux_3 p inst g x✝

def Agreement.ResolutionRule.otherwise {α : Type u_1} {G : Type u_3} (g : G) : ResolutionRule α G

The unconditional final rule.

Equations

• Agreement.ResolutionRule.otherwise g = Agreement.ResolutionRule.all (fun (x : α) => True) g

@[simp]

theorem Agreement.ResolutionRule.out_any {α : Type u_1} {G : Type u_3} {p : α → Prop} [DecidablePred p] {g : G} : (any p g).out = g

@[simp]

theorem Agreement.ResolutionRule.out_all {α : Type u_1} {G : Type u_3} {p : α → Prop} [DecidablePred p] {g : G} : (all p g).out = g

@[simp]

theorem Agreement.ResolutionRule.out_otherwise {α : Type u_1} {G : Type u_3} {g : G} : (otherwise g).out = g

@[simp]

theorem Agreement.ResolutionRule.applies_any {α : Type u_1} {G : Type u_3} {p : α → Prop} [DecidablePred p] {g : G} {cs : List α} : (any p g).Applies cs ↔ ∃ (c : α), c ∈ cs ∧ p c

@[simp]

theorem Agreement.ResolutionRule.applies_all {α : Type u_1} {G : Type u_3} {p : α → Prop} [DecidablePred p] {g : G} {cs : List α} : (all p g).Applies cs ↔ ∀ (c : α), c ∈ cs → p c

@[simp]

theorem Agreement.ResolutionRule.applies_otherwise {α : Type u_1} {G : Type u_3} {g : G} {cs : List α} : (otherwise g).Applies cs

theorem Agreement.ResolutionRule.applies_congr {α : Type u_1} {G : Type u_3} {cs ds : List α} (r : ResolutionRule α G) (h : ∀ (c : α), c ∈ cs ↔ c ∈ ds) : r.Applies cs ↔ r.Applies ds

Whether a rule applies depends only on which descriptors occur among the conjuncts.

def Agreement.ResolutionRule.resolve {α : Type u_1} {G : Type u_3} (rs : List (ResolutionRule α G)) (cs : List α) : Option G

Apply ordered rules: the first that applies selects the form; none applying, the coordination has no resolved form.

Equations

• Agreement.ResolutionRule.resolve rs cs = Option.map Agreement.ResolutionRule.out (List.find? (fun (x : Agreement.ResolutionRule α G) => decide (x.Applies cs)) rs)

@[simp]

theorem Agreement.ResolutionRule.resolve_nil {α : Type u_1} {G : Type u_3} {cs : List α} : resolve [] cs = none

theorem Agreement.ResolutionRule.resolve_cons {α : Type u_1} {G : Type u_3} {cs : List α} {r : ResolutionRule α G} {rs : List (ResolutionRule α G)} : resolve (r :: rs) cs = if r.Applies cs then some r.out else resolve rs cs

@[simp]

theorem Agreement.ResolutionRule.resolve_cons_of_applies {α : Type u_1} {G : Type u_3} {cs : List α} {r : ResolutionRule α G} {rs : List (ResolutionRule α G)} (h : r.Applies cs) : resolve (r :: rs) cs = some r.out

@[simp]

theorem Agreement.ResolutionRule.resolve_cons_of_not_applies {α : Type u_1} {G : Type u_3} {cs : List α} {r : ResolutionRule α G} {rs : List (ResolutionRule α G)} (h : ¬r.Applies cs) : resolve (r :: rs) cs = resolve rs cs

theorem Agreement.ResolutionRule.resolve_append {α : Type u_1} {G : Type u_3} {cs : List α} {rs rs' : List (ResolutionRule α G)} : resolve (rs ++ rs') cs = (resolve rs cs).or (resolve rs' cs)

@[simp]

theorem Agreement.ResolutionRule.resolve_eq_none_iff {α : Type u_1} {G : Type u_3} {cs : List α} {rs : List (ResolutionRule α G)} : resolve rs cs = none ↔ ∀ (r : ResolutionRule α G), r ∈ rs → ¬r.Applies cs

@[simp]

theorem Agreement.ResolutionRule.resolve_isSome_iff {α : Type u_1} {G : Type u_3} {cs : List α} {rs : List (ResolutionRule α G)} : (resolve rs cs).isSome = true ↔ ∃ (r : ResolutionRule α G), r ∈ rs ∧ r.Applies cs

theorem Agreement.ResolutionRule.mem_map_out_of_resolve_eq_some {α : Type u_1} {G : Type u_3} {g : G} {cs : List α} {rs : List (ResolutionRule α G)} (h : resolve rs cs = some g) : g ∈ List.map out rs

A resolved form is the form of one of the rules.

theorem Agreement.ResolutionRule.resolve_append_otherwise_isSome {α : Type u_1} {G : Type u_3} {g : G} {cs : List α} {rs : List (ResolutionRule α G)} : (resolve (rs ++ [otherwise g]) cs).isSome = true

Rules ending in an unconditional rule resolve every coordination.

theorem Agreement.ResolutionRule.resolve_congr_of_applies_iff {α : Type u_1} {G : Type u_3} {cs ds : List α} {rs : List (ResolutionRule α G)} (h : ∀ (r : ResolutionRule α G), r ∈ rs → (r.Applies cs ↔ r.Applies ds)) : resolve rs cs = resolve rs ds

Rules applying alike to two coordinations resolve them alike.

theorem Agreement.ResolutionRule.resolve_congr {α : Type u_1} {G : Type u_3} {cs ds : List α} (rs : List (ResolutionRule α G)) (h : ∀ (c : α), c ∈ cs ↔ c ∈ ds) : resolve rs cs = resolve rs ds

Resolution depends only on which descriptors occur among the conjuncts, so rules cannot count them.

theorem Agreement.ResolutionRule.resolve_any_otherwise {α : Type u_1} {G : Type u_3} {p q : α → Prop} [DecidablePred p] [DecidablePred q] {cs : List α} {a b : G} (h : ∀ (c : α), q c ↔ ¬p c) : resolve [any p a, otherwise b] cs = resolve [all q b, otherwise a] cs

A type-A rule with its default is the type-B rule for the complementary sort with the default swapped.

theorem Agreement.ResolutionRule.resolve_factorsThrough {α : Type u_1} {β : Type u_2} {G : Type u_3} {rs : List (ResolutionRule α G)} {f : α → β} (h : ∀ (r : ResolutionRule α G), r ∈ rs → Function.FactorsThrough r.pred f) : Function.FactorsThrough (resolve rs) (List.map f)

Rules whose sorts read the conjuncts through f give a resolution reading them through f.