Probes as interaction and satisfaction specifications

This file defines a probe over a goal type as two predicates on goals, following Deal's interaction/satisfaction theory of Agree. A goal interacts with the probe when it bears features the probe copies, and satisfies it when it bears features that halt the search. A search over an ordered goal sequence stops at the first satisfying goal, and the probe Agrees with that goal when it also interacts; a satisfying goal that does not interact absorbs the probe, Deal's satisfaction without interaction. The outcome of a search is valued iff some goal satisfies the probe, and an unvalued outcome is failed Agree, tolerated under Preminger's obligatory-operations model. A goal is licensed when the search reaches it, as for Béjar and Rezac; which goals need licensing and which satisfy the probe come apart in general, as for Halpert's Zulu L⁰, which every goal satisfies while only augmentless nominals need it. The full operation, which copies from every interacting goal up to the satisfier, is Probe.run in Probe/Run.lean.

Probe specifications, such as relativized targets, horizon profiles and articulated probes, denote a Probe by a toProbe map rather than re-implementing search.

Main definitions

• Minimalist.Probe: an interaction predicate and a satisfaction predicate on goals.
• Minimalist.Probe.relativized, Minimalist.Probe.ofInt, Minimalist.Probe.insatiable, Minimalist.Probe.indiscriminate: the probes [INT:F, SAT:F], [INT:F, SAT:⊤], [INT:F, SAT:⊥] and [INT:⊤, SAT:⊤].
• Minimalist.Probe.search, Minimalist.Probe.agree: the first satisfying goal, and that goal when it interacts.
• Minimalist.Probe.outcome: valued iff the search finds a goal.
• Minimalist.Probe.Licensed, Minimalist.Probe.AllLicensed: a goal the search reaches, and every needy goal occurrence being reached.
• Minimalist.Probe.cascade: the first finding of an ordered sequence of probes.

Main results

• Minimalist.Probe.search_eq_some_iff_closest: locality as list search.
• Minimalist.Probe.not_rel_of_search_eq_some: the found goal is minimal for any precedence the sequence respects.
• Minimalist.Probe.AllLicensed.countP_le_one, Minimalist.Probe.relativized_allLicensed_iff: one search licenses at most one goal.
• Minimalist.Probe.indiscriminate_allLicensed_iff: under bare minimality only the closest goal may need licensing.

References

• [Dea25a], [Dea24]
• [BR03], [Pre14], [Hal12]
• [Cho00]

structure Minimalist.Probe (α : Type u_2) : Type u_2

A probe over goals of type α is an interaction predicate, the goals it copies from, and a satisfaction predicate, the goals that halt its search ([Dea25a]).

• int : α → Bool

  The goal bears features the probe copies.

• sat : α → Bool

  The goal bears features that halt the probe's search.

inductive Minimalist.Probe.Outcome : Type

The outcome of an obligatory probing operation, valued iff the search found a goal. An unvalued outcome is failed Agree, tolerated under [Pre14]'s obligatory-operations model and spelled out as the default exponent.

• valued : Outcome

  The search found a goal.

• unvalued : Outcome

  The search found no goal.

@[instance_reducible]

instance Minimalist.Probe.instDecidableEqOutcome : DecidableEq Outcome

Equations

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

@[instance_reducible]

instance Minimalist.Probe.instReprOutcome : Repr Outcome

Equations

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

def Minimalist.Probe.instReprOutcome.repr : Outcome → ℕ → Std.Format

Equations

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

def Minimalist.Probe.relativized {α : Type u_1} (f : α → Bool) : Probe α

The probe relativized to f, which interacts with and is satisfied by the same goals, the [INT:F, SAT:F] probe of [BR03] and [Pre14].

Equations

• Minimalist.Probe.relativized f = { int := f, sat := f }

def Minimalist.Probe.ofInt {α : Type u_1} (int : α → Bool) : Probe α

The probe satisfied by every goal and interacting with those that pass int, which Agrees with the closest goal iff that goal is active, the Active Goal Hypothesis of [Cho00].

Equations

• Minimalist.Probe.ofInt int = { int := int, sat := fun (x : α) => true }

def Minimalist.Probe.insatiable {α : Type u_1} (f : α → Bool) : Probe α

The insatiable probe interacting with f, which no goal halts, so that it copies from every f-goal in its domain, Multiple Agree ([Dea25a]).

Equations

• Minimalist.Probe.insatiable f = { int := f, sat := fun (x : α) => false }

def Minimalist.Probe.indiscriminate {α : Type u_1} : Probe α

The indiscriminate probe, which every goal satisfies and interacts with, so that bare minimality delivers the closest goal ([Hal12]'s L⁰).

Equations

• Minimalist.Probe.indiscriminate = Minimalist.Probe.relativized fun (x : α) => true

@[simp]

theorem Minimalist.Probe.relativized_int {α : Type u_1} (f : α → Bool) : (relativized f).int = f

@[simp]

theorem Minimalist.Probe.relativized_sat {α : Type u_1} (f : α → Bool) : (relativized f).sat = f

@[simp]

theorem Minimalist.Probe.ofInt_int {α : Type u_1} (f : α → Bool) : (ofInt f).int = f

@[simp]

theorem Minimalist.Probe.ofInt_sat {α : Type u_1} (f : α → Bool) (a : α) : (ofInt f).sat a = true

@[simp]

theorem Minimalist.Probe.insatiable_int {α : Type u_1} (f : α → Bool) : (insatiable f).int = f

@[simp]

theorem Minimalist.Probe.insatiable_sat {α : Type u_1} (f : α → Bool) (a : α) : (insatiable f).sat a = false

Search

def Minimalist.Probe.search {α : Type u_1} (p : Probe α) (goals : List α) : Option α

The goal a probe finds in an ordered goal sequence, the first goal that satisfies it.

Equations

• p.search goals = List.find? p.sat goals

def Minimalist.Probe.agree {α : Type u_1} (p : Probe α) (goals : List α) : Option α

The found goal, if it interacts with the probe. A satisfying goal that does not interact absorbs the probe.

Equations

• p.agree goals = Option.filter p.int (p.search goals)

@[simp]

theorem Minimalist.Probe.search_eq_none_iff {α : Type u_1} {p : Probe α} {goals : List α} : p.search goals = none ↔ ∀ (a : α), a ∈ goals → ¬p.sat a = true

A probe finds nothing iff no goal satisfies it.

theorem Minimalist.Probe.mem_of_search_eq_some {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.search goals = some a) : a ∈ goals

The found goal is a member of the sequence.

theorem Minimalist.Probe.sat_of_search_eq_some {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.search goals = some a) : p.sat a = true

The found goal satisfies the probe.

theorem Minimalist.Probe.search_pair_of_imp {α : Type u_1} {p : Probe α} {a b : α} (h : p.sat b = true → p.sat a = true) : p.search [a, b] = if p.sat a = true then some a else none

Over a two-goal sequence whose lower goal's satisfaction entails the higher's, the search lands on the higher goal if anywhere, the kernel of gluttony only in inverse configurations ([CK21]) and of highest-only licensing ([Hal12]).

theorem Minimalist.Probe.agree_eq_some_iff {α : Type u_1} {p : Probe α} {goals : List α} {a : α} : p.agree goals = some a ↔ p.search goals = some a ∧ p.int a = true

The probe Agrees with a iff the search finds a and a interacts.

@[simp]

theorem Minimalist.Probe.ofInt_search {α : Type u_1} {goals : List α} (int : α → Bool) : (ofInt int).search goals = goals.head?

A probe satisfied by every goal finds the closest one.

theorem Minimalist.Probe.ofInt_agree_eq_some_iff {α : Type u_1} {goals : List α} {int : α → Bool} {a : α} : (ofInt int).agree goals = some a ↔ goals.head? = some a ∧ int a = true

A probe satisfied by every goal Agrees with the closest one iff it interacts.

theorem Minimalist.Probe.agree_eq_none_of_not_int {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.search goals = some a) (ha : p.int a = false) : p.agree goals = none

A satisfying goal that does not interact absorbs the probe.

@[simp]

theorem Minimalist.Probe.search_nil {α : Type u_1} {p : Probe α} : p.search [] = none

theorem Minimalist.Probe.agree_le_search {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.agree goals = some a) : p.search goals = some a

What the probe Agrees with, it found.

theorem Minimalist.Probe.agree_eq_search_of_int {α : Type u_1} {p : Probe α} {goals : List α} (h : ∀ (a : α), p.sat a = true → p.int a = true) : p.agree goals = p.search goals

When every satisfying goal interacts, Agree coincides with search.

theorem Minimalist.Probe.relativized_agree {α : Type u_1} {goals : List α} (f : α → Bool) : (relativized f).agree goals = (relativized f).search goals

A relativized probe Agrees with the goal it finds.

theorem Minimalist.Probe.agree_eq_none_iff {α : Type u_1} {p : Probe α} {goals : List α} : p.agree goals = none ↔ ¬∃ (a : α), p.search goals = some a ∧ p.int a = true

theorem Minimalist.Probe.search_eq_some_iff_closest {α : Type u_1} {p : Probe α} {goals : List α} {a : α} : p.search goals = some a ↔ p.sat a = true ∧ ∃ (l₁ : List α), ∃ (l₂ : List α), goals = l₁ ++ a :: l₂ ∧ ∀ (b : α), b ∈ l₁ → (!p.sat b) = true

Locality as list search. The probe finds a iff a satisfies it and every earlier goal does not, so that nothing intervenes.

theorem Minimalist.Probe.not_rel_of_search_eq_some {α : Type u_1} {p : Probe α} {goals : List α} {r : α → α → Prop} {a : α} (hord : List.Pairwise (fun (x y : α) => ¬r y x) goals) (h : p.search goals = some a) (b : α) : b ∈ goals → p.sat b = true → b ≠ a → ¬r b a

Over a goal sequence in which no later goal precedes an earlier one, the found goal is minimal among the satisfying goals.

Outcomes

def Minimalist.Probe.outcome {α : Type u_1} (p : Probe α) (goals : List α) : Outcome

The outcome of an obligatory probing operation over a goal sequence, valued iff the search finds a goal.

Equations

• p.outcome goals = if (p.search goals).isSome = true then Minimalist.Probe.Outcome.valued else Minimalist.Probe.Outcome.unvalued

theorem Minimalist.Probe.outcome_eq_valued_iff_isSome {α : Type u_1} {p : Probe α} {goals : List α} : p.outcome goals = Outcome.valued ↔ (p.search goals).isSome = true

The probe is valued iff the search finds a goal.

theorem Minimalist.Probe.outcome_eq_unvalued_iff_eq_none {α : Type u_1} {p : Probe α} {goals : List α} : p.outcome goals = Outcome.unvalued ↔ p.search goals = none

The probe ends unvalued iff the search comes back empty.

@[simp]

theorem Minimalist.Probe.outcome_eq_valued_iff {α : Type u_1} {p : Probe α} {goals : List α} : p.outcome goals = Outcome.valued ↔ ∃ (a : α), a ∈ goals ∧ p.sat a = true

The probe is valued iff some goal satisfies it.

@[simp]

theorem Minimalist.Probe.outcome_eq_unvalued_iff {α : Type u_1} {p : Probe α} {goals : List α} : p.outcome goals = Outcome.unvalued ↔ ∀ (a : α), a ∈ goals → ¬p.sat a = true

The probe ends unvalued iff no goal satisfies it.

theorem Minimalist.Probe.outcome_valued_mono {α : Type u_1} {p : Probe α} {goals : List α} {q : Probe α} (h : ∀ (a : α), a ∈ goals → p.sat a = true → q.sat a = true) : p.outcome goals = Outcome.valued → q.outcome goals = Outcome.valued

Widening satisfaction can only keep a probe valued. If p is valued and q is satisfied by everything that satisfies p among goals, so is q.

Licensing

def Minimalist.Probe.Licensed {α : Type u_1} (p : Probe α) (goals : List α) (a : α) : Prop

A goal is licensed by a probe iff the probe's single search reaches it, since for [BR03] licensing is an Agree relation with the probe.

Equations

• p.Licensed goals a = (p.search goals = some a)

@[instance_reducible]

instance Minimalist.Probe.instDecidableLicensedOfDecidableEq {α : Type u_1} [DecidableEq α] (p : Probe α) (goals : List α) (a : α) : Decidable (p.Licensed goals a)

Equations

• p.instDecidableLicensedOfDecidableEq goals a = Minimalist.Probe.instDecidableLicensedOfDecidableEq._aux_1 p goals a

theorem Minimalist.Probe.Licensed.unique {α : Type u_1} {p : Probe α} {goals : List α} {a b : α} (ha : p.Licensed goals a) (hb : p.Licensed goals b) : a = b

One search licenses at most one goal.

theorem Minimalist.Probe.licensed_iff_closest {α : Type u_1} {p : Probe α} {goals : List α} {a : α} : p.Licensed goals a ↔ p.sat a = true ∧ ∃ (l₁ : List α), ∃ (l₂ : List α), goals = l₁ ++ a :: l₂ ∧ ∀ (b : α), b ∈ l₁ → (!p.sat b) = true

Licensing is being the closest satisfying goal, with no satisfying goal intervening.

theorem Minimalist.Probe.Licensed.mem {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.Licensed goals a) : a ∈ goals

A licensed goal is a member of the sequence.

theorem Minimalist.Probe.Licensed.sat {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.Licensed goals a) : p.sat a = true

A licensed goal satisfies the probe.

theorem Minimalist.Probe.indiscriminate_licensed_iff {α : Type u_1} {goals : List α} {a : α} : indiscriminate.Licensed goals a ↔ goals.head? = some a

Licensing by the indiscriminate probe is being the structurally closest goal, bare minimality ([Hal12]'s L⁰).

def Minimalist.Probe.AllLicensed {α : Type u_1} (p : Probe α) (needs : α → Bool) (goals : List α) : Prop

The goals that needs selects are all licensed by the probe's single search when each of them satisfies the probe and no goal before it does. The condition is on occurrences, like List.Nodup, so one search licenses one occurrence and two equal needy goals are not both licensed.

Equations

• p.AllLicensed needs goals = ((∀ (a : α), a ∈ goals → needs a = true → p.sat a = true) ∧ List.Pairwise (fun (a b : α) => needs b = true → p.sat a = false) goals)

@[instance_reducible]

instance Minimalist.Probe.instDecidableAllLicensed {α : Type u_1} (p : Probe α) (needs : α → Bool) (goals : List α) : Decidable (p.AllLicensed needs goals)

Equations

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

@[simp]

theorem Minimalist.Probe.allLicensed_nil {α : Type u_1} {p : Probe α} {needs : α → Bool} : p.AllLicensed needs []

theorem Minimalist.Probe.allLicensed_cons {α : Type u_1} {p : Probe α} {goals : List α} {needs : α → Bool} {a : α} : p.AllLicensed needs (a :: goals) ↔ (needs a = true → p.sat a = true) ∧ (∀ (b : α), b ∈ goals → needs b = true → p.sat a = false) ∧ p.AllLicensed needs goals

theorem Minimalist.Probe.AllLicensed.licensed {α : Type u_1} {p : Probe α} {goals : List α} {needs : α → Bool} (h : p.AllLicensed needs goals) {a : α} (ha : a ∈ goals) (hn : needs a = true) : p.Licensed goals a

When all needy goals are licensed, the search reaches each of them.

theorem Minimalist.Probe.allLicensed_of_forall_not {α : Type u_1} {p : Probe α} {goals : List α} {needs : α → Bool} (h : ∀ (a : α), a ∈ goals → needs a = false) : p.AllLicensed needs goals

Goals none of which needs licensing are all licensed.

theorem Minimalist.Probe.AllLicensed.countP_le_one {α : Type u_1} {p : Probe α} {goals : List α} {needs : α → Bool} (h : p.AllLicensed needs goals) : List.countP needs goals ≤ 1

One search licenses at most one needy goal.

theorem Minimalist.Probe.allLicensed_iff_forall_licensed {α : Type u_1} {p : Probe α} {goals : List α} {needs : α → Bool} (hnd : goals.Nodup) : p.AllLicensed needs goals ↔ ∀ (a : α), a ∈ goals → needs a = true → p.Licensed goals a

Over goals without repetitions, all needy goals are licensed iff each is reached by the search.

theorem Minimalist.Probe.relativized_allLicensed_iff {α : Type u_1} {goals : List α} {f : α → Bool} : (relativized f).AllLicensed f goals ↔ List.countP f goals ≤ 1

On the diagonal, where the probe is relativized to exactly the needy goals, all needy goals are licensed iff at most one goal is needy, one search licensing one goal, the fact behind [Pre14]'s person restriction.

theorem Minimalist.Probe.indiscriminate_allLicensed_iff {α : Type u_1} {goals : List α} {needs : α → Bool} : indiscriminate.AllLicensed needs goals ↔ ∀ (a : α), a ∈ goals.tail → needs a = false

Licensing by the indiscriminate probe allows no needy goal below the head of the sequence, the highest-element condition of [Hal12].

Cascades

def Minimalist.Probe.cascade {α : Type u_1} (ps : List (Probe α)) (goals : List α) : Option α

The goal an ordered sequence of probes delivers, the first probe's finding, else the next's, and so on. This is Probe.search at the goal level composed with List.findSome? at the probe level, and also the single-slot morphological competition in which the first probe with output wins the slot, as in [Pre14] where π⁰'s clitic beats #⁰'s exponent beats nothing.

Equations

• Minimalist.Probe.cascade ps goals = List.findSome? (fun (x : Minimalist.Probe α) => x.search goals) ps

@[simp]

theorem Minimalist.Probe.cascade_eq_none_iff {α : Type u_1} {goals : List α} {ps : List (Probe α)} : cascade ps goals = none ↔ ∀ (q : Probe α), q ∈ ps → ∀ (a : α), a ∈ goals → ¬q.sat a = true

A cascade delivers nothing iff no goal satisfies any probe.

theorem Minimalist.Probe.cascade_cons {α : Type u_1} {goals : List α} {ps : List (Probe α)} {q : Probe α} : cascade (q :: ps) goals = (q.search goals <|> cascade ps goals)

Unfold one probe of the cascade.

@[simp]

theorem Minimalist.Probe.cascade_nil {α : Type u_1} {goals : List α} : cascade [] goals = none

@[simp]

theorem Minimalist.Probe.cascade_singleton {α : Type u_1} {goals : List α} {q : Probe α} : cascade [q] goals = q.search goals

theorem Minimalist.Probe.cascade_append {α : Type u_1} {goals : List α} {ps qs : List (Probe α)} : cascade (ps ++ qs) goals = (cascade ps goals <|> cascade qs goals)

cascade is a monoid map (List (Probe α), ++) → (Option α, <|>), the single-slot competition running the left probes and then the right.

theorem Minimalist.Probe.exists_licensed_of_cascade_eq_some {α : Type u_1} {goals : List α} {ps : List (Probe α)} {a : α} (h : cascade ps goals = some a) : ∃ (q : Probe α), q ∈ ps ∧ q.Licensed goals a

The cascade's goal is licensed by one of its probes.

theorem Minimalist.Probe.mem_of_cascade_eq_some {α : Type u_1} {goals : List α} {ps : List (Probe α)} {a : α} (h : cascade ps goals = some a) : a ∈ goals

The cascade's goal is a member of the sequence.