Valuation: Pi-Typed Partial Variable Assignment (V2)

Replaces the old Situation (which fixed Variable → Option Bool). A Valuation α is a Π-type partial valuation where each vertex v has its own value type α v. The Pi pattern follows mathlib's Algebra/Group/Pi/Basic.lean idiom for index-dependent value families.

α := fun _ => Bool recovers the legacy binary substrate.

A DecidableValuation aggregator typeclass bundles ∀ v, DecidableEq (α v) for use throughout the API.

@[reducible, inline]

abbrev Core.Causal.Valuation {V : Type u_1} (α : V → Type u_2) : Type (max u_1 u_2)

Partial valuation: each vertex v either has a value of type α v (encoded some x) or is undetermined (none). Generalizes the old Situation (which fixed α := fun _ => Bool).

Defined as an abbrev for Π-type rather than a structure, so elaboration unifies Valuation α with Π v, Option (α v) directly.

Equations

• Core.Causal.Valuation α = ((v : V) → Option (α v))

@[reducible, inline]

abbrev Core.Causal.DecidableValuation {V : Type u_1} (α : V → Type u_2) : Type (max u_1 u_2)

Per-vertex decidable equality. An abbrev (not a class) so it unfolds transparently to the bare ∀ v, DecidableEq (α v) constraint typeclass search expects. Avoids the bundled-class antipattern.

Equations

• Core.Causal.DecidableValuation α = ((v : V) → DecidableEq (α v))

def Core.Causal.Valuation.empty {V : Type u_1} {α : V → Type u_2} : Valuation α

The empty valuation: nothing is determined.

Equations

• Core.Causal.Valuation.empty x✝ = none

@[implicit_reducible]

instance Core.Causal.Valuation.instInhabited {V : Type u_1} {α : V → Type u_2} : Inhabited (Valuation α)

Equations

• Core.Causal.Valuation.instInhabited = { default := Core.Causal.Valuation.empty }

def Core.Causal.Valuation.get {V : Type u_1} {α : V → Type u_2} (s : Valuation α) (v : V) : Option (α v)

Get the value of a variable (if determined).

Equations

• s.get v = s v

def Core.Causal.Valuation.hasValue {V : Type u_1} {α : V → Type u_2} (s : Valuation α) (v : V) (x : α v) : Prop

The variable has the given value in the valuation.

Equations

• s.hasValue v x = (s.get v = some x)

@[implicit_reducible]

instance Core.Causal.Valuation.instDecidableHasValueOfDecidableValuation {V : Type u_1} {α : V → Type u_2} [DecidableValuation α] (s : Valuation α) (v : V) (x : α v) : Decidable (s.hasValue v x)

Equations

• s.instDecidableHasValueOfDecidableValuation v x = Core.Causal.Valuation.instDecidableHasValueOfDecidableValuation._aux_1 s v x

def Core.Causal.Valuation.extend {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (s : Valuation α) (v : V) (x : α v) : Valuation α

Extend a valuation with a new assignment. Overwrites if already set.

Equations

• s.extend v x w = if h : w = v then some (⋯ ▸ x) else s w

def Core.Causal.Valuation.remove {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (s : Valuation α) (v : V) : Valuation α

Remove a variable from the valuation (set to undetermined).

Equations

• s.remove v w = if w = v then none else s w

def Core.Causal.Valuation.le {V : Type u_1} {α : V → Type u_2} [DecidableValuation α] (s₁ s₂ : Valuation α) : Prop

Information ordering: every value defined in s₁ matches in s₂.

Equations

• s₁.le s₂ = ∀ (v : V) (x : α v), s₁.hasValue v x → s₂.hasValue v x

def Core.Causal.Valuation.undeterminedCount {V : Type u_1} {α : V → Type u_2} (s : Valuation α) (l : List V) : ℕ

Count of undetermined vertices over a finite list. Termination measure for the forward-development fixpoint (mirrors the old Monotonicity.lean measure but generalized over α).

Equations

• s.undeterminedCount l = List.countP (fun (v : V) => (s.get v).isNone) l

@[simp]

theorem Core.Causal.Valuation.extend_get_same {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (s : Valuation α) (v : V) (x : α v) : (s.extend v x).get v = some x

theorem Core.Causal.Valuation.extend_get_ne {V : Type u_1} {α : V → Type u_2} [DecidableEq V] {s : Valuation α} {v w : V} {x : α v} (h : w ≠ v) : (s.extend v x).get w = s.get w

@[simp]

theorem Core.Causal.Valuation.empty_get {V : Type u_1} {α : V → Type u_2} (v : V) : empty.get v = none

theorem Core.Causal.Valuation.hasValue_empty_iff {V : Type u_1} {α : V → Type u_2} (v : V) (x : α v) : ¬empty.hasValue v x