Documentation

PGCL.OMDP

Operation MDP derived from SmallStep. #

Main definitions #

source
noncomputable def pGCL.๐’ฌ {ฯ– : Type u_1} [DecidableEq ฯ–] :
MDP (Conf ฯ–) Act
Equations
Instances For
    source
    @[simp]
    theorem pGCL.๐’ฌ.act_eq {ฯ– : Type u_1} [DecidableEq ฯ–] :
    ๐’ฌ.act = SmallStep.act
    source
    @[simp]
    theorem pGCL.๐’ฌ.succs_univ_eq {ฯ– : Type u_1} [DecidableEq ฯ–] :
    ๐’ฌ.succs_univ = fun (c : Conf ฯ–) => {c' : Conf ฯ– | โˆƒ (ฮฑ : Act) (p : ENNReal), c โคณ[ฮฑ,p] c'}
    source
    @[simp]
    theorem pGCL.๐’ฌ.P_eq {ฯ– : Type u_1} [DecidableEq ฯ–] :
    ๐’ฌ.P = fun (c : Conf ฯ–) (ฮฑ : Act) (c' : Conf ฯ–) => โˆ‘' (p : { p : ENNReal // c โคณ[ฮฑ,p] c' }), โ†‘p
    source
    theorem pGCL.๐’ฌ.P_support_eq_succs {ฯ– : Type u_1} [DecidableEq ฯ–] {c : Conf ฯ–} {ฮฑ : Act} :
    Function.support (๐’ฌ.P c ฮฑ) = SmallStep.succs c ฮฑ
    source
    instance pGCL.๐’ฌ.instFiniteBranchingConfAct {ฯ– : Type u_1} [DecidableEq ฯ–] :
    ๐’ฌ.FiniteBranching
    source
    @[irreducible]
    noncomputable def pGCL.๐’ฌ.cost {ฯ– : Type u_1} (X : Exp ฯ–) :
    Option (Option (pGCL ฯ–) ร— States ฯ–) โ†’ ENNReal
    Equations
    Instances For
      source
      @[simp]
      theorem pGCL.๐’ฌ.cost_X_of_pGCL {ฯ–โœ : Type u_2} {X : Exp ฯ–โœ} {C : pGCL ฯ–โœ} {ฯƒ : States ฯ–โœ} :
      cost X (ยทโŸจC,ฯƒโŸฉ) = cost 0 (ยทโŸจC,ฯƒโŸฉ)
      source
      @[simp]
      theorem pGCL.๐’ฌ.ฮฆ_simp {ฯ– : Type u_1} [DecidableEq ฯ–] {c f : ๐’ฌ.Costs} {C : Conf ฯ–} :
      (MDP.ฮฆ c) f C = c C + โจ… ฮฑ โˆˆ SmallStep.act C, โˆ‘' (s' : โ†‘(๐’ฌ.succs_univ C)), ๐’ฌ.P C ฮฑ โ†‘s' * f โ†‘s'
      source
      @[simp]
      theorem pGCL.๐’ฌ.bot_eq {ฯ– : Type u_1} [DecidableEq ฯ–] {i : โ„•} {X : Exp ฯ–} :
      (โ‡‘(MDP.ฮฆ (cost X)))^[i] โŠฅ none = 0
      source
      noncomputable instance pGCL.๐’ฌ.instDecidableMemConfSetSuccs_univAct {ฯ– : Type u_1} [DecidableEq ฯ–] {s s' : Conf ฯ–} :
      Decidable (s' โˆˆ ๐’ฌ.succs_univ s)
      Equations
      source
      theorem pGCL.๐’ฌ.tsum_succs_univ' {ฯ– : Type u_1} [DecidableEq ฯ–] {c : Conf ฯ–} (f : โ†‘(๐’ฌ.succs_univ c) โ†’ ENNReal) :
      โˆ‘' (s' : โ†‘(๐’ฌ.succs_univ c)), f s' = โˆ‘' (s' : Conf ฯ–), if h : s' โˆˆ ๐’ฌ.succs_univ c then f โŸจs', hโŸฉ else 0
      source
      @[simp]
      theorem pGCL.๐’ฌ.sink_eq {ฯ– : Type u_1} [DecidableEq ฯ–] {X : Exp ฯ–} {i : โ„•} {ฯƒ : States ฯ–} :
      (โ‡‘(MDP.ฮฆ (cost X)))^[i] โŠฅ (some (none, ฯƒ)) = if i = 0 then 0 else X ฯƒ
      source
      @[simp]
      theorem pGCL.๐’ฌ.lfp_ฮฆ_bot {ฯ– : Type u_1} [DecidableEq ฯ–] {X : Exp ฯ–} :
      MDP.lfp_ฮฆ (cost X) none = 0
      source
      @[simp]
      theorem pGCL.๐’ฌ.lfp_ฮฆ_sink {ฯ– : Type u_1} [DecidableEq ฯ–] {X : Exp ฯ–} {ฯƒ : States ฯ–} :
      MDP.lfp_ฮฆ (cost X) (some (none, ฯƒ)) = X ฯƒ
      source
      noncomputable def pGCL.๐’ฌ.ฯ‚ {ฯ– : Type u_1} [DecidableEq ฯ–] :
      (pGCL ฯ– โ†’ Exp ฯ– โ†’ Exp ฯ–) โ†’o pGCL ฯ– โ†’ Exp ฯ– โ†’ Exp ฯ–
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem pGCL.๐’ฌ.ฯ‚.skip {ฯ– : Type u_1} [DecidableEq ฯ–] {f : pGCL ฯ– โ†’ Exp ฯ– โ†’ Exp ฯ–} :
        ฯ‚ f pGCL.skip = fun (x1 : Exp ฯ–) (x2 : States ฯ–) => x1 x2
        source
        @[simp]
        theorem pGCL.๐’ฌ.ฯ‚.assign {ฯ– : Type u_1} [DecidableEq ฯ–] {f : pGCL ฯ– โ†’ Exp ฯ– โ†’ Exp ฯ–} {x : ฯ–} {e : Exp ฯ–} :
        ฯ‚ f (x ::= e) = fun (X : Exp ฯ–) (ฯƒ : States ฯ–) => f pGCL.skip X (ฯƒ[x โ†ฆ e ฯƒ])
        source
        @[simp]
        theorem pGCL.๐’ฌ.ฯ‚.tick {ฯ– : Type u_1} [DecidableEq ฯ–] {f : pGCL ฯ– โ†’ Exp ฯ– โ†’ Exp ฯ–} {r : Exp ฯ–} :
        ฯ‚ f (pGCL.tick r) = fun (X : Exp ฯ–) => r + f pGCL.skip X
        source
        @[simp]
        theorem pGCL.๐’ฌ.ฯ‚.prob {ฯ– : Type u_1} [DecidableEq ฯ–] {f : pGCL ฯ– โ†’ Exp ฯ– โ†’ Exp ฯ–} {Cโ‚ : pGCL ฯ–} {p : ProbExp ฯ–} {Cโ‚‚ : pGCL ฯ–} :
        ฯ‚ f (Cโ‚ ยท[p] Cโ‚‚) = fun (X : Exp ฯ–) => p.pick (f Cโ‚ X) (f Cโ‚‚ X)
        source
        @[simp]
        theorem pGCL.๐’ฌ.ฯ‚.nonDet {ฯ– : Type u_1} [DecidableEq ฯ–] {f : pGCL ฯ– โ†’ Exp ฯ– โ†’ Exp ฯ–} {Cโ‚ Cโ‚‚ : pGCL ฯ–} :
        ฯ‚ f (Cโ‚ ยท[] Cโ‚‚) = f Cโ‚ โŠ“ f Cโ‚‚
        source
        theorem pGCL.๐’ฌ.ฯ‚.loop {ฯ– : Type u_1} [DecidableEq ฯ–] {f : pGCL ฯ– โ†’ Exp ฯ– โ†’ Exp ฯ–} {b : BExpr ฯ–} {C : pGCL ฯ–} :
        ฯ‚ f (pGCL.loop b C) = fun (X : Exp ฯ–) => b.probOf * f (C ;; pGCL.loop b C) X + b.not.probOf * f pGCL.skip X
        source
        noncomputable def pGCL.op {ฯ– : Type u_1} [DecidableEq ฯ–] (C : pGCL ฯ–) (X : Exp ฯ–) :
        Exp ฯ–
        Equations
        Instances For
          source
          theorem pGCL.op_eq_iSup_ฮฆ {ฯ– : Type u_1} [DecidableEq ฯ–] :
          op = โจ† (n : โ„•), fun (C : pGCL ฯ–) (X : Exp ฯ–) (ฯƒ : States ฯ–) => (โ‡‘(MDP.ฮฆ (๐’ฌ.cost X)))^[n] โŠฅ (ยทโŸจC,ฯƒโŸฉ)
          source
          theorem pGCL.op_eq_iSup_succ_ฮฆ {ฯ– : Type u_1} [DecidableEq ฯ–] :
          op = โจ† (n : โ„•), fun (C : pGCL ฯ–) (X : Exp ฯ–) (ฯƒ : States ฯ–) => (โ‡‘(MDP.ฮฆ (๐’ฌ.cost X)))^[n + 1] โŠฅ (ยทโŸจC,ฯƒโŸฉ)
          source
          theorem pGCL.ฯ‚_op_eq_op {ฯ– : Type u_1} [DecidableEq ฯ–] :
          ๐’ฌ.ฯ‚ op = op
          source
          @[simp]
          theorem pGCL.op_skip {ฯ– : Type u_1} [DecidableEq ฯ–] :
          skip.op = fun (x1 : Exp ฯ–) (x2 : States ฯ–) => x1 x2
          source
          theorem pGCL.op_isLeast {ฯ– : Type u_1} [DecidableEq ฯ–] (b : pGCL ฯ– โ†’ Exp ฯ– โ†’ Exp ฯ–) (h : ๐’ฌ.ฯ‚ b โ‰ค b) :
          op โ‰ค b
          source
          theorem pGCL.lfp_ฯ‚_eq_op {ฯ– : Type u_1} [DecidableEq ฯ–] :
          OrderHom.lfp ๐’ฌ.ฯ‚ = op
          source
          theorem pGCL.op_le_seq {ฯ– : Type u_1} [DecidableEq ฯ–] {C C' : pGCL ฯ–} :
          C.op โˆ˜ C'.op โ‰ค (C ;; C').op
          source
          theorem pGCL.ฯ‚_wp_eq_wp {ฯ– : Type u_1} [DecidableEq ฯ–] :
          ๐’ฌ.ฯ‚ wp = wp
          source
          theorem pGCL.wp_le_op.loop {ฯ– : Type u_1} [DecidableEq ฯ–] {C : pGCL ฯ–} {b : BExpr ฯ–} (ih : C.wp โ‰ค C.op) :
          (pGCL.loop b C).wp โ‰ค (pGCL.loop b C).op
          source
          theorem pGCL.wp_le_op {ฯ– : Type u_1} [DecidableEq ฯ–] :
          wp โ‰ค op
          source
          theorem pGCL.op_eq_wp {ฯ– : Type u_1} [DecidableEq ฯ–] :
          op = wp