The Agree operation as a fold over the goal sequence

This file defines the Agree operation of [Dea25a]'s interaction/satisfaction theory as a fold over an ordered goal sequence. The probe inspects the goals in order; from every goal that interacts with it, it copies, and flags the goal as a goal of the probe; the first goal that satisfies it is flagged as its satisfier and ends the search. The state the fold threads is whatever the probe accumulates, so the operation is generic over what copying means, and a probe specification over a feature type instantiates it with feature sets, copying the goal's features that lie in the interaction specification.

The single-goal search of Probe/Basic.lean is the special case in which every interacting goal satisfies the probe (run_goals_eq_agree), Multiple Agree is the insatiable case (insatiable_run_goals), and a probe that finds no interacting goal leaves the state unchanged, Agree failing without penalty ([Pre14]). The satisfier of the fold is always the goal Probe.search finds (run_halt). Goal flagging, which [Dea25a] keeps distinct from valuation, is the list of interacting goals together with the satisfier.

Main definitions

• Minimalist.Probe.run: the Agree operation, a fold over the goal sequence returning a Minimalist.Probe.Result, the state, the flagged goals and the satisfier.
• Minimalist.Probe.inspected: the goals up to and including the first satisfier.
• Minimalist.Probe.Spec: an interaction and a satisfaction feature set, denoting a probe over goals exposing feature sets by Minimalist.Probe.Spec.toProbe and run by Minimalist.Probe.Spec.run.

Main results

• Minimalist.Probe.run_halt, Minimalist.Probe.run_goals, Minimalist.Probe.run_state
• Minimalist.Probe.run_goals_eq_agree, Minimalist.Probe.insatiable_run_goals
• Minimalist.Probe.Spec.run_state_eq_biUnion

References

• [Dea25a], [Dea24]
• [Hir01]
• [Pre14]

structure Minimalist.Probe.Result (α : Type u_4) (σ : Type u_5) : Type (max u_4 u_5)

The result of running a probe over a goal sequence, the state after copying from every interacting goal, the goals flagged as interacting, in search order, and the goal flagged as the satisfier, if any.

• state : σ

  The state after copying from every interacting goal.

• goals : List α

  The goals the probe interacted with, in search order.

• halt : Option α

  The goal that satisfied the probe, if the search was satisfied.

def Minimalist.Probe.run {α : Type u_1} {σ : Type u_2} (p : Probe α) (copy : α → σ → σ) : σ → List α → Result α σ

The Agree operation over an ordered goal sequence. Each goal in turn is copied from and flagged if it interacts, and ends the search if it satisfies.

Equations

• One or more equations did not get rendered due to their size.
• p.run copy x✝ [] = { state := x✝, goals := [], halt := none }

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

The goals a probe inspects, those before the first satisfying goal together with it.

Equations

• p.inspected goals = List.takeWhile (fun (x : α) => !p.sat x) goals ++ (p.search goals).toList

@[simp]

theorem Minimalist.Probe.run_nil {α : Type u_1} {σ : Type u_2} {p : Probe α} {copy : α → σ → σ} {s : σ} : p.run copy s [] = { state := s, goals := [], halt := none }

@[simp]

theorem Minimalist.Probe.run_halt {α : Type u_1} {σ : Type u_2} {p : Probe α} {copy : α → σ → σ} {s : σ} {goals : List α} : (p.run copy s goals).halt = p.search goals

The satisfier of the fold is the goal the search finds.

@[simp]

theorem Minimalist.Probe.run_goals {α : Type u_1} {σ : Type u_2} {p : Probe α} {copy : α → σ → σ} {s : σ} {goals : List α} : (p.run copy s goals).goals = List.filter p.int (p.inspected goals)

The flagged goals are the inspected goals that interact.

theorem Minimalist.Probe.run_state {α : Type u_1} {σ : Type u_2} {p : Probe α} {copy : α → σ → σ} {s : σ} {goals : List α} : (p.run copy s goals).state = List.foldl (fun (s : σ) (a : α) => copy a s) s (p.run copy s goals).goals

The state is the fold of copy over the flagged goals.

theorem Minimalist.Probe.mem_of_mem_inspected {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (ha : a ∈ p.inspected goals) : a ∈ goals

An inspected goal is a member of the sequence.

theorem Minimalist.Probe.run_state_eq_of_forall_not_int {α : Type u_1} {σ : Type u_2} {p : Probe α} {copy : α → σ → σ} {s : σ} {goals : List α} (h : ∀ a ∈ goals, ¬p.int a = true) : (p.run copy s goals).state = s

A probe that interacts with no goal leaves the state unchanged.

theorem Minimalist.Probe.run_goals_eq_agree {α : Type u_1} {σ : Type u_2} {p : Probe α} {copy : α → σ → σ} {s : σ} {goals : List α} (h : ∀ (a : α), p.int a = true → p.sat a = true) : (p.run copy s goals).goals = (p.agree goals).toList

When every interacting goal satisfies the probe, the flagged goals are the single goal the probe Agrees with.

theorem Minimalist.Probe.relativized_run_goals {α : Type u_1} {σ : Type u_2} {copy : α → σ → σ} {s : σ} {goals : List α} (f : α → Bool) : ((relativized f).run copy s goals).goals = ((relativized f).search goals).toList

A relativized probe flags the goal it finds.

theorem Minimalist.Probe.insatiable_run_goals {α : Type u_1} {σ : Type u_2} {copy : α → σ → σ} {s : σ} {goals : List α} (f : α → Bool) : ((insatiable f).run copy s goals).goals = List.filter f goals

An insatiable probe flags every interacting goal, Multiple Agree ([Hir01]).

Feature specifications

structure Minimalist.Probe.Spec (F : Type u_4) : Type u_4

A probe specification over a feature type, the features the probe interacts with and the features that satisfy it, [INT:int, SAT:sat] in [Dea25a]'s notation.

• int : Finset F

  The features the probe copies.

• sat : Finset F

  The features that halt the probe's search.

def Minimalist.Probe.Spec.toProbe {α : Type u_1} {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) : Probe α

The probe a specification denotes over goals exposing feature sets, interacting with a goal iff it bears a feature of the interaction specification and satisfied iff it bears one of the satisfaction specification.

Equations

• sp.toProbe feats = { int := fun (a : α) => decide (feats a ∩ sp.int).Nonempty, sat := fun (a : α) => decide (feats a ∩ sp.sat).Nonempty }

def Minimalist.Probe.Spec.copyFrom {α : Type u_1} {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) (a : α) (s : Finset F) : Finset F

Copying from a goal adds its features that lie in the interaction specification.

Equations

• sp.copyFrom feats a s = s ∪ feats a ∩ sp.int

def Minimalist.Probe.Spec.run {α : Type u_1} {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) (goals : List α) : Result α (Finset F)

The Agree operation of a specification over a goal sequence, starting from no features.

Equations

• sp.run feats goals = (sp.toProbe feats).run (sp.copyFrom feats) ∅ goals

@[simp]

theorem Minimalist.Probe.Spec.toProbe_int {α : Type u_1} {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) (a : α) : (sp.toProbe feats).int a = decide (feats a ∩ sp.int).Nonempty

@[simp]

theorem Minimalist.Probe.Spec.toProbe_sat {α : Type u_1} {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) (a : α) : (sp.toProbe feats).sat a = decide (feats a ∩ sp.sat).Nonempty

theorem Minimalist.Probe.Spec.subset_copyFrom {α : Type u_1} {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) (a : α) (s : Finset F) : s ⊆ sp.copyFrom feats a s

The state a specification copies only grows.

theorem Minimalist.Probe.Spec.run_state_eq_biUnion {α : Type u_1} {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) [DecidableEq α] (goals : List α) : (sp.run feats goals).state = (sp.run feats goals).goals.toFinset.biUnion fun (x : α) => feats x ∩ sp.int

The copied features are the interaction-specified features of the flagged goals.

theorem Minimalist.Probe.Spec.run_state_subset {α : Type u_1} {F : Type u_3} [DecidableEq F] (sp : Spec F) (feats : α → Finset F) [DecidableEq α] (goals : List α) : (sp.run feats goals).state ⊆ sp.int

The copied features lie in the interaction specification.