structure MDP.Path {State : Type u_1} {Act : Type u_2} (M : MDP State Act) : Type u_1

• states : List State
• nonempty : self.states ≠ []
• property (i : ℕ) (h : i < self.states.length - 1) : self.states[i + 1] ∈ M.succs_univ self.states[i]

instance MDP.Path.instDecidableEq {State : Type u_1} {Act : Type u_2} {M : MDP State Act} [DecidableEq State] : DecidableEq M.Path

Equations

• a.instDecidableEq b = if h : a.states = b.states then isTrue ⋯ else isFalse ⋯

def MDP.Path.length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : ℕ

Equations

• ‖π‖ = π.states.length

def MDP.Path.«term‖_‖» : Lean.ParserDescr

Equations

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

instance MDP.Path.instSingleton {State : Type u_1} {Act : Type u_2} {M : MDP State Act} : Singleton State M.Path

Equations

• MDP.Path.instSingleton = { singleton := fun (s : State) => { states := [s], nonempty := ⋯, property := ⋯ } }

instance MDP.Path.instGetElem {State : Type u_1} {Act : Type u_2} {M : MDP State Act} : GetElem M.Path ℕ State fun (π : M.Path) (i : ℕ) => i < ‖π‖

Equations

• MDP.Path.instGetElem = { getElem := fun (π : M.Path) (i : ℕ) (x : i < ‖π‖) => π.states[i] }

@[simp]

theorem MDP.Path.states_getElem_eq_getElem {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (i : Fin ‖π‖) : π.states[i] = π[i]

@[simp]

theorem MDP.Path.states_getElem_eq_getElem_Nat {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (i : ℕ) (h : i < ‖π‖) : π.states[i] = π[i]

@[simp]

theorem MDP.Path.singleton_getElem_nat {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {i : ℕ} {s : State} (h : i < 1) : {s}[i] = s

@[simp]

theorem MDP.Path.singleton_getElem {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} (i : Fin 1) : {s}[i] = s

@[simp]

theorem MDP.Path.states_length_eq_length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π.states.length = ‖π‖

@[simp]

theorem MDP.Path.states_nonempty {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π.states ≠ []

@[simp]

theorem MDP.Path.length_pos {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : 0 < ‖π‖

@[simp]

theorem MDP.Path.length_pos' {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : 1 ≤ ‖π‖

@[simp]

theorem MDP.Path.length_ne_zero {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : ¬‖π‖ = 0

@[simp]

theorem MDP.Path.length_pred_succ {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : ‖π‖ - 1 + 1 = ‖π‖

@[simp]

theorem MDP.Path.fin_succ_le_length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (i : Fin (‖π‖ - 1)) : ↑i + 1 < ‖π‖

@[reducible, inline]

abbrev MDP.Path.last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : State

Equations

• π.last = π[‖π‖ - 1]

@[simp]

theorem MDP.Path.succs_succs {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (i : Fin (‖π‖ - 1)) : π[↑i + 1] ∈ M.succs_univ π[i]

@[simp]

theorem MDP.Path.succs_succs_nat {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {i : ℕ} (h : i < ‖π‖ - 1) : π[i + 1] ∈ M.succs_univ π[i]

def MDP.Path.take {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (n : ℕ) : M.Path

Equations

• π.take n = { states := List.take (n + 1) π.states, nonempty := ⋯, property := ⋯ }

def MDP.Path.prev {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : M.Path

Equations

• π.prev = { states := if ‖π‖ = 1 then π.states else π.states.dropLast, nonempty := ⋯, property := ⋯ }

def MDP.Path.extend {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (s : ↑(M.succs_univ π.last)) : M.Path

Equations

• π.extend s = { states := π.states ++ [↑s], nonempty := ⋯, property := ⋯ }

def MDP.Path.succs_univ {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : Set M.Path

Equations

• π.succs_univ = {π' : M.Path | π'.prev = π ∧ 1 < ‖π'‖}

@[simp]

theorem MDP.Path.last_if_singleton {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (h : ‖π‖ = 1) : π.last = π[0]

@[simp]

theorem MDP.Path.length_ne_one_iff {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : ¬‖π‖ = 1 ↔ 1 < ‖π‖

@[simp]

theorem MDP.Path.length_sub_add_eq {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (h : 1 < ‖π‖) : ‖π‖ - 2 + 1 = ‖π‖ - 1

@[simp]

theorem MDP.Path.last_mem_succs {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (h : 1 < ‖π‖) : π.last ∈ M.succs_univ π[‖π‖ - 2]

@[simp]

theorem MDP.Path.mem_succs_univ_prev {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {π π' : M.Path} (h : π' ∈ π.succs_univ) : π'.prev = π

@[simp]

theorem MDP.Path.succs_univ_prev {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (π' : ↑π.succs_univ) : (↑π').prev = π

@[simp]

theorem MDP.Path.mem_prev_succs_univ {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (h : 1 < ‖π‖) : π ∈ π.prev.succs_univ

def MDP.Path.act {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : Set Act

Equations

• π.act = M.act π.last

def MDP.Path.tail {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : M.Path

Equations

• π.tail = { states := if ‖π‖ = 1 then π.states else π.states.tail, nonempty := ⋯, property := ⋯ }

def MDP.Path.prepend {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (s : ↑(M.prev_univ π[0])) : M.Path

Equations

• π.prepend s = { states := ↑s :: π.states, nonempty := ⋯, property := ⋯ }

theorem MDP.Path.ext {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {π₁ π₂ : M.Path} (h₁ : ‖π₁‖ = ‖π₂‖) (h₂ : ∀ (i : ℕ) (x : i < ‖π₁‖) (x_1 : i < ‖π₂‖), π₁[i] = π₂[i]) : π₁ = π₂

theorem MDP.Path.ext_iff {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {π₁ π₂ : M.Path} : π₁ = π₂ ↔ ‖π₁‖ = ‖π₂‖ ∧ ∀ (i : ℕ) (x : i < ‖π₁‖) (x_1 : i < ‖π₂‖), π₁[i] = π₂[i]

theorem MDP.Path.ext_states {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {π₁ π₂ : M.Path} (h : π₁.states = π₂.states) : π₁ = π₂

@[simp]

theorem MDP.Path.mk_states {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (states : List State) {h₁ : states ≠ []} {h₂ : ∀ (i : ℕ) (h : i < states.length - 1), states[i + 1] ∈ M.succs_univ states[i]} : { states := states, nonempty := h₁, property := h₂ }.states = states

@[simp]

theorem MDP.Path.mk_length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (states : List State) {h₁ : states ≠ []} {h₂ : ∀ (i : ℕ) (h : i < states.length - 1), states[i + 1] ∈ M.succs_univ states[i]} : ‖{ states := states, nonempty := h₁, property := h₂ }‖ = states.length

@[simp]

theorem MDP.Path.mk_last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (states : List State) {h₁ : states ≠ []} {h₂ : ∀ (i : ℕ) (h : i < states.length - 1), states[i + 1] ∈ M.succs_univ states[i]} : { states := states, nonempty := h₁, property := h₂ }.last = states[states.length - 1]

@[simp]

theorem MDP.Path.mk_getElem {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {i : ℕ} (states : List State) {h₁ : states ≠ []} {h₂ : ∀ (i : ℕ) (h : i < states.length - 1), states[i + 1] ∈ M.succs_univ states[i]} (hi : i < states.length) : { states := states, nonempty := h₁, property := h₂ }[i] = states[i]

@[simp]

theorem MDP.Path.extend_prev {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} : (π.extend s).prev = π

@[simp]

theorem MDP.Path.tail_getElem_zero {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π.tail[0] = if h : ‖π‖ = 1 then π[0] else π[1]

@[simp]

theorem MDP.Path.mem_succs_univ {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (h : 1 < ‖π‖) : π[1] ∈ M.succs_univ π[0]

@[simp]

theorem MDP.Path.mem_prev_univ {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (h : 1 < ‖π‖) : π[0] ∈ M.prev_univ π[1]

@[simp]

theorem MDP.Path.mem_succs_univ_of_prev_univ {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (s : ↑(M.prev_univ π[0])) : π[0] ∈ M.succs_univ ↑s

@[simp]

theorem MDP.Path.prepend_tail {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.prev_univ π[0])} : (π.prepend s).tail = π

@[simp]

theorem MDP.Path.tail_prepend {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (h : 1 < ‖π‖) : π.tail.prepend ⟨π[0], ⋯⟩ = π

@[simp]

theorem MDP.Path.tail_prepend' {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : State} (h : 1 < ‖π‖) (h' : π[0] = s) : π.tail.prepend ⟨s, ⋯⟩ = π

@[simp]

theorem MDP.Path.singleton_first {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} : {s}[0] = s

@[simp]

theorem MDP.Path.extend_first {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} : (π.extend s)[0] = π[0]

@[simp]

theorem MDP.Path.prepend_first {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.prev_univ π[0])} : (π.prepend s)[0] = ↑s

@[simp]

theorem MDP.Path.tail_first {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π.tail[0] = if h : ‖π‖ = 1 then π[0] else π[1]

@[simp]

theorem MDP.Path.prev_first {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π.prev[0] = π[0]

@[simp]

theorem MDP.Path.take_first {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {n : ℕ} : (π.take n)[0] = π[0]

@[simp]

theorem MDP.Path.succs_first {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (π' : ↑π.succs_univ) : (↑π')[0] = π[0]

@[simp]

theorem MDP.Path.singleton_last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} : {s}.last = s

@[simp]

theorem MDP.Path.extend_last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} : (π.extend s).last = ↑s

@[simp]

theorem MDP.Path.prepend_last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.prev_univ π[0])} : (π.prepend s).last = π.last

@[simp]

theorem MDP.Path.tail_last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π.tail.last = π.last

@[simp]

theorem MDP.Path.prev_last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π.prev.last = π[‖π‖ - 2]

theorem MDP.Path.take_last_nat {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {n : ℕ} : (π.take n).last = π[min n (‖π‖ - 1)]

@[simp]

theorem MDP.Path.take_last_nat' {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {n : ℕ} (h : n < ‖π‖) : (π.take n).last = π[n]

@[simp]

theorem MDP.Path.take_last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (n : Fin ‖π‖) : (π.take ↑n).last = π[n]

@[simp]

theorem MDP.Path.take_last' {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (n : Fin (‖π‖ - 1)) : (π.take ↑n).last = π[n]

@[simp]

theorem MDP.Path.succs_last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (π' : ↑π.succs_univ) : (↑π').last ∈ M.succs_univ π.last

@[simp]

theorem MDP.Path.singleton_length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} : ‖{s}‖ = 1

@[simp]

theorem MDP.Path.extend_length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} : ‖π.extend s‖ = ‖π‖ + 1

@[simp]

theorem MDP.Path.prepend_length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.prev_univ π[0])} : ‖π.prepend s‖ = ‖π‖ + 1

@[simp]

theorem MDP.Path.tail_length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : ‖π.tail‖ = if 1 < ‖π‖ then ‖π‖ - 1 else ‖π‖

@[simp]

theorem MDP.Path.prev_length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : ‖π.prev‖ = if 1 < ‖π‖ then ‖π‖ - 1 else ‖π‖

@[simp]

theorem MDP.Path.take_length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {n : ℕ} : ‖π.take n‖ = min (n + 1) ‖π‖

@[simp]

theorem MDP.Path.succs_length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (π' : ↑π.succs_univ) : ‖↑π'‖ = ‖π‖ + 1

theorem MDP.Path.take_prepend {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {i : ℕ} {s : ↑(M.prev_univ (π.take i)[0])} : (π.take i).prepend s = (π.prepend ⟨↑s, ⋯⟩).take (i + 1)

@[simp]

theorem MDP.Path.take_zero {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π.take 0 = {π[0]}

@[simp]

theorem MDP.Path.getElem_length_pred_eq_last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π[‖π‖ - 1] = π.last

@[simp]

theorem MDP.Path.extend_getElem_length_pred_eq_last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} : (π.extend s)[‖π‖ - 1] = π.last

@[simp]

theorem MDP.Path.take_length_pred_eq_prev {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π.take (‖π‖ - 2) = π.prev

@[simp]

theorem MDP.Path.extend_take_length_pred_eq_prev {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} : (π.extend s).take (‖π‖ - 1) = π

@[simp]

theorem MDP.Path.extend_take {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} (i : Fin ‖π‖) : (π.extend s).take ↑i = π.take ↑i

@[simp]

theorem MDP.Path.extend_take' {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} (i : Fin (‖π‖ - 1)) : (π.extend s).take ↑i = π.take ↑i

@[simp]

theorem MDP.Path.extend_getElem {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} (i : Fin ‖π‖) : (π.extend s)[i] = π[i]

@[simp]

theorem MDP.Path.extend_getElem' {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} (i : Fin (‖π‖ - 1)) : (π.extend s)[i] = π[i]

@[simp]

theorem MDP.Path.extend_getElem_nat {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {i : ℕ} {s : ↑(M.succs_univ π.last)} (h : i < ‖π‖) : (π.extend s)[i] = π[i]

@[simp]

theorem MDP.Path.extend_getElem_nat' {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {i : ℕ} {s : ↑(M.succs_univ π.last)} (h : i < ‖π‖ - 1) : (π.extend s)[i] = π[i]

@[simp]

theorem MDP.Path.extend_getElem_length {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} : (π.extend s)[‖π‖] = ↑s

@[simp]

theorem MDP.Path.extend_getElem_succ {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} (i : Fin ‖π‖) : (π.extend s)[↑i + 1] = if h : ‖π‖ - 1 = ↑i then ↑s else π[↑i + 1]

@[simp]

theorem MDP.Path.extend_getElem_succ' {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : ↑(M.succs_univ π.last)} (i : Fin (‖π‖ - 1)) : (π.extend s)[↑i + 1] = π[↑i + 1]

@[simp]

theorem MDP.Path.tail_getElem {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (i : Fin (‖π‖ - 1)) : π.tail[i] = π[↑i + 1]

@[simp]

theorem MDP.Path.tail_getElem_nat {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (i : ℕ) (h : i < ‖π‖ - 1) : π.tail[i] = π[i + 1]

@[simp]

theorem MDP.Path.tail_getElem_nat_succ {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (i : ℕ) (h : i < ‖π‖ - 2) : π.tail[i] = π[i + 1]

@[simp]

theorem MDP.Path.tail_getElem_nat_succ' {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (i : ℕ) (h : i < ‖π‖ - 2) : π.tail[i + 1] = π[i + 2]

@[simp]

theorem MDP.Path.prepend_getElem_one {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (s : ↑(M.prev_univ π[0])) : (π.prepend s)[1] = π[0]

@[simp]

theorem MDP.Path.prepend_getElem_succ {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (s : ↑(M.prev_univ π[0])) (i : Fin ‖π‖) : (π.prepend s)[↑i + 1] = π[i]

@[simp]

theorem MDP.Path.prepend_getElem_succ' {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (s : ↑(M.prev_univ π[0])) (i : Fin (‖π‖ - 1)) : (π.prepend s)[↑i + 1] = π[i]

@[simp]

theorem MDP.Path.prepend_injective {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : Function.Injective π.prepend

@[simp]

theorem MDP.Path.prepend_inj_right {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π π' : M.Path) {s : ↑(M.prev_univ π[0])} (h : π[0] = π'[0]) : π.prepend s = π'.prepend ⟨↑s, ⋯⟩ ↔ π = π'

@[simp]

theorem MDP.Path.last_mem_succs_univ_prev_last {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (h : 1 < ‖π‖) : π.last ∈ M.succs_univ π.prev.last

@[simp]

theorem MDP.Path.prev_extend {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (h : 1 < ‖π‖) : π.prev.extend ⟨π.last, ⋯⟩ = π

theorem MDP.Path.succs_univ_eq_extend_range {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π.succs_univ = Set.range π.extend

theorem MDP.Path.induction_on {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {P : M.Path → Prop} (π : M.Path) (single : P {π[0]}) (extend : ∀ (π : M.Path) (s' : ↑(M.succs_univ π.last)), P π → P (π.extend s')) : P π