structure Semantics.Dynamic.Core.Possibility (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A possibility: world paired with variable assignment.

• world : W
• assignment : ℕ → E

def Semantics.Dynamic.Core.Possibility.agreeOn {W : Type u_1} {E : Type u_2} (p q : Possibility W E) (vars : Set ℕ) : Prop

Two possibilities agree on all variables in a set

Equations

• p.agreeOn q vars = ∀ (x : ℕ), x ∈ vars → p.assignment x = q.assignment x

def Semantics.Dynamic.Core.Possibility.sameWorld {W : Type u_1} {E : Type u_2} (p q : Possibility W E) : Prop

Same world, possibly different assignment

Equations

• p.sameWorld q = (p.world = q.world)

def Semantics.Dynamic.Core.Possibility.extend {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x : ℕ) (e : E) : Possibility W E

Extend an assignment at a single variable

Equations

• p.extend x e = { world := p.world, assignment := fun (n : ℕ) => if n = x then e else p.assignment n }

@[simp]

theorem Semantics.Dynamic.Core.Possibility.extend_at {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x : ℕ) (e : E) : (p.extend x e).assignment x = e

@[simp]

theorem Semantics.Dynamic.Core.Possibility.extend_other {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x y : ℕ) (e : E) (h : y ≠ x) : (p.extend x e).assignment y = p.assignment y

@[simp]

theorem Semantics.Dynamic.Core.Possibility.extend_world {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x : ℕ) (e : E) : (p.extend x e).world = p.world

@[reducible, inline]

abbrev Semantics.Dynamic.Core.InfoState (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

Information state: set of possibilities.

Equations

• Semantics.Dynamic.Core.InfoState W E = Set (Semantics.Dynamic.Core.Possibility W E)

def Semantics.Dynamic.Core.InfoState.univ {W : Type u_1} {E : Type u_2} : InfoState W E

The trivial state: all possibilities

Equations

• Semantics.Dynamic.Core.InfoState.univ = Set.univ

def Semantics.Dynamic.Core.InfoState.empty {W : Type u_1} {E : Type u_2} : InfoState W E

The absurd state: no possibilities

Equations

• Semantics.Dynamic.Core.InfoState.empty = ∅

def Semantics.Dynamic.Core.InfoState.consistent {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Prop

State is consistent (non-empty)

Equations

• s.consistent = Set.Nonempty s

def Semantics.Dynamic.Core.InfoState.trivial {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Prop

State is trivial (all possibilities)

Equations

• s.trivial = (s = Set.univ)

def Semantics.Dynamic.Core.InfoState.definedAt {W : Type u_1} {E : Type u_2} (s : InfoState W E) (x : ℕ) : Prop

Variable x is defined in state s iff all possibilities agree on x's value.

Equations

• s.definedAt x = ∀ (p q : Semantics.Dynamic.Core.Possibility W E), p ∈ s → q ∈ s → p.assignment x = q.assignment x

def Semantics.Dynamic.Core.InfoState.definedVars {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Set ℕ

The set of defined variables in a state

Equations

• s.definedVars = {x : ℕ | s.definedAt x}

def Semantics.Dynamic.Core.InfoState.novelAt {W : Type u_1} {E : Type u_2} (s : InfoState W E) (x : ℕ) : Prop

Variable x is novel in state s iff x is not defined.

Equations

• s.novelAt x = ¬s.definedAt x

theorem Semantics.Dynamic.Core.InfoState.novelAt_iff_disagree {W : Type u_1} {E : Type u_2} (s : InfoState W E) (x : ℕ) (hs : s.consistent) : s.novelAt x ↔ ∃ (p : Possibility W E), ∃ (q : Possibility W E), p ∈ s ∧ q ∈ s ∧ p.assignment x ≠ q.assignment x

In a consistent state, novel means assignments actually disagree

def Semantics.Dynamic.Core.InfoState.worlds {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Set W

Project to the set of worlds in the state

Equations

• s.worlds = {w : W | ∃ (p : Semantics.Dynamic.Core.Possibility W E), p ∈ s ∧ p.world = w}

def Semantics.Dynamic.Core.InfoState.filterWorlds {W : Type u_1} {E : Type u_2} (s : InfoState W E) (pred : W → Bool) : InfoState W E

Filter state by a world predicate

Equations

• s.filterWorlds pred = {p : Semantics.Dynamic.Core.Possibility W E | p ∈ s ∧ pred p.world = true}

def Semantics.Dynamic.Core.InfoState.filterAssign {W : Type u_1} {E : Type u_2} (s : InfoState W E) (pred : (ℕ → E) → Bool) : InfoState W E

Filter state by an assignment predicate

Equations

• s.filterAssign pred = {p : Semantics.Dynamic.Core.Possibility W E | p ∈ s ∧ pred p.assignment = true}

structure Semantics.Dynamic.Core.Context (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Context extends InfoState with metadata.

• state : InfoState W E
• definedVars : Set ℕ
• domain : Set E

def Semantics.Dynamic.Core.Context.initial {W : Type u_1} {E : Type u_2} : Context W E

Empty context with all possibilities

Equations

• Semantics.Dynamic.Core.Context.initial = { state := Semantics.Dynamic.Core.InfoState.univ }

def Semantics.Dynamic.Core.Context.consistent {W : Type u_1} {E : Type u_2} (c : Context W E) : Prop

Context is consistent iff its state is

Equations

• c.consistent = c.state.consistent

def Semantics.Dynamic.Core.Context.introduce {W : Type u_1} {E : Type u_2} (c : Context W E) (x : ℕ) : Context W E

Mark a variable as defined

Equations

• c.introduce x = { state := c.state, definedVars := c.definedVars ∪ {x}, domain := c.domain }

def Semantics.Dynamic.Core.Context.narrow {W : Type u_1} {E : Type u_2} (c : Context W E) (s : InfoState W E) : Context W E

Narrow the state

Equations

• c.narrow s = { state := c.state ∩ s, definedVars := c.definedVars, domain := c.domain }

def Semantics.Dynamic.Core.InfoState.subsistsIn {W : Type u_1} {E : Type u_2} (s s' : InfoState W E) : Prop

State subsistence: s subsists in s' iff every possibility in s has a descendant in s'.

Equations

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

def Semantics.Dynamic.Core.«term_⪯_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.Core.InfoState.subsistsIn_refl {W : Type u_1} {E : Type u_2} (s : InfoState W E) : s ⪯ s

Subsistence is reflexive

theorem Semantics.Dynamic.Core.InfoState.subset_subsistsIn {W : Type u_1} {E : Type u_2} {s s' : InfoState W E} (h : s ⊆ s') : s ⪯ s'

Subset implies subsistence

def Semantics.Dynamic.Core.InfoState.supports {W : Type u_1} {E : Type u_2} (s : InfoState W E) (φ : W → Bool) : Prop

State s supports proposition φ iff φ holds at all worlds in s.

Equations

• (s ⊫ φ) = ∀ (p : Semantics.Dynamic.Core.Possibility W E), p ∈ s → φ p.world = true

def Semantics.Dynamic.Core.InfoState.«term_⊫_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.Core.InfoState.supports_mono {W : Type u_1} {E : Type u_2} {s s' : InfoState W E} (h : s ⊆ s') (φ : W → Bool) (hsupp : s' ⊫ φ) : s ⊫ φ

Support is preserved by subset