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 Causation.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

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

@[reducible, inline]

abbrev Causation.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

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

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

The empty valuation: nothing is determined.

Equations

• Causation.Valuation.empty x✝ = none

@[implicit_reducible]

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

Equations

• Causation.Valuation.instInhabited = { default := Causation.Valuation.empty }

def Causation.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 Causation.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 Causation.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 = Causation.Valuation.instDecidableHasValueOfDecidableValuation._aux_1 s v x

def Causation.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 Causation.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 Causation.Valuation.le {V : Type u_1} {α : V → Type u_2} (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

theorem Causation.Valuation.le_refl {V : Type u_1} {α : V → Type u_2} (s : Valuation α) : s.le s

theorem Causation.Valuation.le_trans {V : Type u_1} {α : V → Type u_2} {s₁ s₂ s₃ : Valuation α} (h₁ : s₁.le s₂) (h₂ : s₂.le s₃) : s₁.le s₃

theorem Causation.Valuation.le_antisymm {V : Type u_1} {α : V → Type u_2} {s₁ s₂ : Valuation α} (h₁ : s₁.le s₂) (h₂ : s₂.le s₁) : s₁ = s₂

@[implicit_reducible]

instance Causation.Valuation.instPartialOrder {V : Type u_1} {α : V → Type u_2} : PartialOrder (Valuation α)

The information order is a partial order (mathlib Finset-style instance; s₁.le s₂ and s₁ ≤ s₂ are definitionally equal).

Equations

• Causation.Valuation.instPartialOrder = { le := fun (s₁ s₂ : Causation.Valuation α) => s₁.le s₂, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[simp]

theorem Causation.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 Causation.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

theorem Causation.Valuation.le_extend {V : Type u_1} {α : V → Type u_2} [DecidableEq V] {s : Valuation α} {v : V} (x : α v) (h : s.get v = none) : s.le (s.extend v x)

Extending at an undetermined vertex only adds information.

@[simp]

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

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