State Transition Systems

This file contains simple definitions and lemmas for reasoning about state transition systems defined by a function σ → Option σ, where σ is the type of states.

def StateTransition.eval {σ : Type u_1} (f : σ → Option σ) : σ → Part σ

Run a state transition function σ → Option σ "to completion". The return value is the last state returned before a none result. If the state transition function always returns some, then the computation diverges, returning Part.none.

Equations

• StateTransition.eval f = PFun.fix fun (s : σ) => Part.some ((f s).elim (Sum.inl s) Sum.inr)

def StateTransition.Reaches {σ : Type u_1} (f : σ → Option σ) : σ → σ → Prop

The reflexive transitive closure of a state transition function. Reaches f a b means there is a finite sequence of steps f a = some a₁, f a₁ = some a₂, ... such that aₙ = b. This relation permits zero steps of the state transition function.

Equations

• StateTransition.Reaches f = Relation.ReflTransGen fun (a b : σ) => b ∈ f a

def StateTransition.Reaches₁ {σ : Type u_1} (f : σ → Option σ) : σ → σ → Prop

The transitive closure of a state transition function. Reaches₁ f a b means there is a nonempty finite sequence of steps f a = some a₁, f a₁ = some a₂, ... such that aₙ = b. This relation does not permit zero steps of the state transition function.

Equations

• StateTransition.Reaches₁ f = Relation.TransGen fun (a b : σ) => b ∈ f a

theorem StateTransition.reaches₁_eq {σ : Type u_1} {f : σ → Option σ} {a b c : σ} (h : f a = f b) : Reaches₁ f a c ↔ Reaches₁ f b c

theorem StateTransition.reaches_total {σ : Type u_1} {f : σ → Option σ} {a b c : σ} (hab : Reaches f a b) (hac : Reaches f a c) : Reaches f b c ∨ Reaches f c b

theorem StateTransition.reaches₁_fwd {σ : Type u_1} {f : σ → Option σ} {a b c : σ} (h₁ : Reaches₁ f a c) (h₂ : b ∈ f a) : Reaches f b c

def StateTransition.Reaches₀ {σ : Type u_1} (f : σ → Option σ) (a b : σ) : Prop

A variation on Reaches. Reaches₀ f a b holds if whenever Reaches₁ f b c then Reaches₁ f a c. This is a weaker property than Reaches and is useful for replacing states with equivalent states without taking a step.

Equations

• StateTransition.Reaches₀ f a b = ∀ (c : σ), StateTransition.Reaches₁ f b c → StateTransition.Reaches₁ f a c

theorem StateTransition.Reaches₀.trans {σ : Type u_1} {f : σ → Option σ} {a b c : σ} (h₁ : Reaches₀ f a b) (h₂ : Reaches₀ f b c) : Reaches₀ f a c

theorem StateTransition.Reaches₀.refl {σ : Type u_1} {f : σ → Option σ} (a : σ) : Reaches₀ f a a

theorem StateTransition.Reaches₀.single {σ : Type u_1} {f : σ → Option σ} {a b : σ} (h : b ∈ f a) : Reaches₀ f a b

theorem StateTransition.Reaches₀.head {σ : Type u_1} {f : σ → Option σ} {a b c : σ} (h : b ∈ f a) (h₂ : Reaches₀ f b c) : Reaches₀ f a c

theorem StateTransition.Reaches₀.tail {σ : Type u_1} {f : σ → Option σ} {a b c : σ} (h₁ : Reaches₀ f a b) (h : c ∈ f b) : Reaches₀ f a c

theorem StateTransition.reaches₀_eq {σ : Type u_1} {f : σ → Option σ} {a b : σ} (e : f a = f b) : Reaches₀ f a b

theorem StateTransition.Reaches₁.to₀ {σ : Type u_1} {f : σ → Option σ} {a b : σ} (h : Reaches₁ f a b) : Reaches₀ f a b

theorem StateTransition.Reaches.to₀ {σ : Type u_1} {f : σ → Option σ} {a b : σ} (h : Reaches f a b) : Reaches₀ f a b

theorem StateTransition.Reaches₀.tail' {σ : Type u_1} {f : σ → Option σ} {a b c : σ} (h : Reaches₀ f a b) (h₂ : c ∈ f b) : Reaches₁ f a c

def StateTransition.evalInduction {σ : Type u_2} {f : σ → Option σ} {b : σ} {C : σ → Sort u_1} {a : σ} (h : b ∈ eval f a) (H : (a : σ) → b ∈ eval f a → ((a' : σ) → f a = some a' → C a') → C a) : C a

(co-)Induction principle for eval. If a property C holds of any point a evaluating to b which is either terminal (meaning a = b) or where the next point also satisfies C, then it holds of any point where eval f a evaluates to b. This formalizes the notion that if eval f a evaluates to b then it reaches terminal state b in finitely many steps.

Equations

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

theorem StateTransition.mem_eval {σ : Type u_1} {f : σ → Option σ} {a b : σ} : b ∈ eval f a ↔ Reaches f a b ∧ f b = none

theorem StateTransition.eval_maximal₁ {σ : Type u_1} {f : σ → Option σ} {a b : σ} (h : b ∈ eval f a) (c : σ) : ¬Reaches₁ f b c

theorem StateTransition.eval_maximal {σ : Type u_1} {f : σ → Option σ} {a b : σ} (h : b ∈ eval f a) {c : σ} : Reaches f b c ↔ c = b

theorem StateTransition.reaches_eval {σ : Type u_1} {f : σ → Option σ} {a b : σ} (ab : Reaches f a b) : eval f a = eval f b

def StateTransition.Respects {σ₁ : Type u_1} {σ₂ : Type u_2} (f₁ : σ₁ → Option σ₁) (f₂ : σ₂ → Option σ₂) (tr : σ₁ → σ₂ → Prop) : Prop

Given a relation tr : σ₁ → σ₂ → Prop between state spaces, and state transition functions f₁ : σ₁ → Option σ₁ and f₂ : σ₂ → Option σ₂, Respects f₁ f₂ tr means that if tr a₁ a₂ holds initially and f₁ takes a step to a₂ then f₂ will take one or more steps before reaching a state b₂ satisfying tr a₂ b₂, and if f₁ a₁ terminates then f₂ a₂ also terminates. Such a relation tr is also known as a refinement.

Equations

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

theorem StateTransition.tr_reaches₁ {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ : σ₁} {a₂ : σ₂} (aa : tr a₁ a₂) {b₁ : σ₁} (ab : Reaches₁ f₁ a₁ b₁) : ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

theorem StateTransition.tr_reaches {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ : σ₁} {a₂ : σ₂} (aa : tr a₁ a₂) {b₁ : σ₁} (ab : Reaches f₁ a₁ b₁) : ∃ (b₂ : σ₂), tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

theorem StateTransition.tr_reaches_rev {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ : σ₁} {a₂ : σ₂} (aa : tr a₁ a₂) {b₂ : σ₂} (ab : Reaches f₂ a₂ b₂) : ∃ (c₁ : σ₁) (c₂ : σ₂), Reaches f₂ b₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

theorem StateTransition.tr_eval {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ b₁ : σ₁} {a₂ : σ₂} (aa : tr a₁ a₂) (ab : b₁ ∈ eval f₁ a₁) : ∃ (b₂ : σ₂), tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂

theorem StateTransition.tr_eval_rev {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ : σ₁} {b₂ a₂ : σ₂} (aa : tr a₁ a₂) (ab : b₂ ∈ eval f₂ a₂) : ∃ (b₁ : σ₁), tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁

theorem StateTransition.tr_eval_dom {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ : σ₁} {a₂ : σ₂} (aa : tr a₁ a₂) : (eval f₂ a₂).Dom ↔ (eval f₁ a₁).Dom

def StateTransition.FRespects {σ₁ : Type u_1} {σ₂ : Type u_2} (f₂ : σ₂ → Option σ₂) (tr : σ₁ → σ₂) (a₂ : σ₂) : Option σ₁ → Prop

A simpler version of Respects when the state transition relation tr is a function.

Equations

• StateTransition.FRespects f₂ tr a₂ (some b₁) = StateTransition.Reaches₁ f₂ a₂ (tr b₁)
• StateTransition.FRespects f₂ tr a₂ none = (f₂ a₂ = none)

theorem StateTransition.frespects_eq {σ₁ : Type u_1} {σ₂ : Type u_2} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂} {a₂ b₂ : σ₂} (h : f₂ a₂ = f₂ b₂) {b₁ : Option σ₁} : FRespects f₂ tr a₂ b₁ ↔ FRespects f₂ tr b₂ b₁

theorem StateTransition.fun_respects {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂} : (Respects f₁ f₂ fun (a : σ₁) (b : σ₂) => tr a = b) ↔ ∀ ⦃a₁ : σ₁⦄, FRespects f₂ tr (tr a₁) (f₁ a₁)

theorem StateTransition.tr_eval' {σ₁ σ₂ : Type u_1} (f₁ : σ₁ → Option σ₁) (f₂ : σ₂ → Option σ₂) (tr : σ₁ → σ₂) (H : Respects f₁ f₂ fun (a : σ₁) (b : σ₂) => tr a = b) (a₁ : σ₁) : eval f₂ (tr a₁) = tr <$> eval f₁ a₁

structure StateTransition.EvalsTo {σ : Type u_1} (f : σ → Option σ) (a : σ) (b : Option σ) : Type

A "proof" of the fact that f eventually reaches b when repeatedly evaluated on a, remembering the number of steps it takes.

• steps : ℕ

  number of steps taken

• evals_in_steps : (flip bind f)^[self.steps] (some a) = b

structure StateTransition.EvalsToInTime {σ : Type u_1} (f : σ → Option σ) (a : σ) (b : Option σ) (m : ℕ) extends StateTransition.EvalsTo f a b : Type

A "proof" of the fact that f eventually reaches b in at most m steps when repeatedly evaluated on a, remembering the number of steps it takes.

• steps : ℕ
• evals_in_steps : (flip bind f)^[self.steps] (some a) = b
• steps_le_m : self.steps ≤ m

def StateTransition.EvalsTo.refl {σ : Type u_1} (f : σ → Option σ) (a : σ) : EvalsTo f a (some a)

Reflexivity of EvalsTo in 0 steps.

Equations

• StateTransition.EvalsTo.refl f a = { steps := 0, evals_in_steps := ⋯ }

def StateTransition.EvalsTo.trans {σ : Type u_1} (f : σ → Option σ) (a b : σ) (c : Option σ) (h₁ : EvalsTo f a (some b)) (h₂ : EvalsTo f b c) : EvalsTo f a c

Transitivity of EvalsTo in the sum of the numbers of steps.

Equations

• StateTransition.EvalsTo.trans f a b c h₁ h₂ = { steps := h₂.steps + h₁.steps, evals_in_steps := ⋯ }

def StateTransition.EvalsToInTime.refl {σ : Type u_1} (f : σ → Option σ) (a : σ) : EvalsToInTime f a (some a) 0

Reflexivity of EvalsToInTime in 0 steps.

Equations

• StateTransition.EvalsToInTime.refl f a = { toEvalsTo := StateTransition.EvalsTo.refl f a, steps_le_m := StateTransition.EvalsToInTime.refl._proof_1 }

def StateTransition.EvalsToInTime.trans {σ : Type u_1} (f : σ → Option σ) (m₁ m₂ : ℕ) (a b : σ) (c : Option σ) (h₁ : EvalsToInTime f a (some b) m₁) (h₂ : EvalsToInTime f b c m₂) : EvalsToInTime f a c (m₂ + m₁)

Transitivity of EvalsToInTime in the sum of the numbers of steps.

Equations

• StateTransition.EvalsToInTime.trans f m₁ m₂ a b c h₁ h₂ = { toEvalsTo := StateTransition.EvalsTo.trans f a b c h₁.toEvalsTo h₂.toEvalsTo, steps_le_m := ⋯ }