Documentation

PGCL.OperationalSemantics

source
@[simp]
theorem pGCL.ProbExp.pick_same {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} {Οƒ : State Ξ“} {x : ENNReal} {p : ProbExp Ξ“} :
p Οƒ * x + (1 - p Οƒ) * x = x
source
noncomputable def pGCL.cost_t {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} :
(State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def pGCL.cost_t' {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} :
    (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[irreducible]
      noncomputable def pGCL.cost_p {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} :
      pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal
      Equations
      Instances For
        source
        noncomputable def pGCL.cost_p' {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} :
        pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal
        Equations
        Instances For
          source
          noncomputable instance pGCL.π•Š {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) :
          SmallStepSemantics (pGCL Ξ“) (State Ξ“) Termination Act
          Equations
          • pGCL.π•Š cT cP = { r := pGCL.SmallStep, relation_p_pos := β‹―, succs_sum_to_one := β‹―, progress := β‹―, cost_p := cP, cost_t := cT }
          source
          noncomputable instance pGCL.instSmallStepSemanticsStateTerminationAct {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] :
          SmallStepSemantics (pGCL Ξ“) (State Ξ“) Termination Act
          Equations
          source
          @[reducible, inline]
          noncomputable abbrev pGCL.π’ͺ {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) :
          MDP (Conf (pGCL Ξ“) (State Ξ“) Termination) (Option Act)
          Equations
          Instances For
            source
            instance pGCL.instFiniteBranchingStateTerminationAct {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] :
            SmallStepSemantics.FiniteBranching (pGCL Ξ“) (State Ξ“) Termination Act
            source
            @[simp]
            theorem pGCL.act_eq_SmallStep_act {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) {C : pGCL Ξ“} {Οƒ : State Ξ“} :
            SmallStepSemantics.act (Conf.prog C Οƒ) = (fun (x : Act) => some x) '' SmallStep.act (C, Οƒ)
            source
            @[simp]
            theorem pGCL.act_seq {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) {C : pGCL Ξ“} {Οƒ : State Ξ“} {C' : pGCL Ξ“} :
            SmallStepSemantics.act (Conf.prog (pgcl {@C ; @C'}) Οƒ) = SmallStepSemantics.act (Conf.prog C Οƒ)
            source
            def pGCL.cP' {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} (f : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) :
            pGCL Ξ“ β†’ (State Ξ“ β†’ ENNReal) β†’o State Ξ“ β†’ ENNReal
            Equations
            Instances For
              source
              @[simp]
              theorem pGCL.cP'_apply {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} {C : pGCL Ξ“} {X : State Ξ“ β†’ ENNReal} {f : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal} :
              (cP' f C) X = fun (Οƒ : State Ξ“) => f (C, Οƒ)
              source
              @[simp]
              theorem pGCL.ΞΎ.skip {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) {f : pGCL Ξ“ β†’ (State Ξ“ β†’ ENNReal) β†’o State Ξ“ β†’ ENNReal} {O : Optimization} :
              (SmallStepSemantics.ΞΎ O) f (pgcl {skip}) = { toFun := fun (X : State Ξ“ β†’ ENNReal) (Οƒ : State Ξ“) => cP (pgcl {skip}, Οƒ) + cT X (Termination.term, Οƒ), monotone' := β‹― }
              source
              @[simp]
              theorem pGCL.ΞΎ.assign {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) {f : pGCL Ξ“ β†’ (State Ξ“ β†’ ENNReal) β†’o State Ξ“ β†’ ENNReal} {O : Optimization} {x : 𝒱} {e : State Ξ“ β†’ Ξ“ x} :
              (SmallStepSemantics.ΞΎ O) f (pgcl {@x := @e}) = { toFun := fun (X : State Ξ“ β†’ ENNReal) (Οƒ : State Ξ“) => cP (pgcl {@x := @e}, Οƒ) + cT X (Termination.term, Οƒ[x ↦ e Οƒ]), monotone' := β‹― }
              source
              @[simp]
              theorem pGCL.ΞΎ.tick {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) {f : pGCL Ξ“ β†’ (State Ξ“ β†’ ENNReal) β†’o State Ξ“ β†’ ENNReal} {O : Optimization} {t : State Ξ“ β†’ ENNReal} :
              (SmallStepSemantics.ΞΎ O) f pgcl {tick(@t)} = { toFun := fun (X : State Ξ“ β†’ ENNReal) (Οƒ : State Ξ“) => cP (pgcl {tick(@t)}, Οƒ) + cT X (Termination.term, Οƒ), monotone' := β‹― }
              source
              @[simp]
              theorem pGCL.ΞΎ.observe {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) {f : pGCL Ξ“ β†’ (State Ξ“ β†’ ENNReal) β†’o State Ξ“ β†’ ENNReal} {b : BExpr Ξ“} {O : Optimization} :
              (SmallStepSemantics.ΞΎ O) f pgcl {observe(@b)} = { toFun := fun (X : State Ξ“ β†’ ENNReal) (Οƒ : State Ξ“) => cP (pgcl {observe(@b)}, Οƒ) + i[b] Οƒ * cT X (Termination.term, Οƒ) + (1 - i[b] Οƒ) * cT X (Termination.fault, Οƒ), monotone' := β‹― }
              source
              @[simp]
              theorem pGCL.ΞΎ.prob {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) {f : pGCL Ξ“ β†’ (State Ξ“ β†’ ENNReal) β†’o State Ξ“ β†’ ENNReal} {O : Optimization} {C₁ : pGCL Ξ“} {p : ProbExp Ξ“} {Cβ‚‚ : pGCL Ξ“} :
              (SmallStepSemantics.ΞΎ O) f pgcl {{ @C₁ } [@p] { @Cβ‚‚ }} = cP' cP pgcl {{ @C₁ } [@p] { @Cβ‚‚ }} + p.pick' (f C₁) (f Cβ‚‚)
              source
              @[simp]
              theorem pGCL.ΞΎ.nonDet {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) {f : pGCL Ξ“ β†’ (State Ξ“ β†’ ENNReal) β†’o State Ξ“ β†’ ENNReal} {O : Optimization} {C₁ Cβ‚‚ : pGCL Ξ“} :
              (SmallStepSemantics.ΞΎ O) f pgcl {{ @C₁ } [] { @Cβ‚‚ }} = cP' cP pgcl {{ @C₁ } [] { @Cβ‚‚ }} + O.opt (f C₁) (f Cβ‚‚)
              source
              theorem pGCL.ΞΎ.loop {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) {f : pGCL Ξ“ β†’ (State Ξ“ β†’ ENNReal) β†’o State Ξ“ β†’ ENNReal} {C : pGCL Ξ“} {b : BExpr Ξ“} {O : Optimization} :
              (SmallStepSemantics.ΞΎ O) f pgcl {while @b { @C }} = cP' cP pgcl {while @b { @C }} + { toFun := fun (X : State Ξ“ β†’ ENNReal) => ((Ξ¨[f (pgcl {@C ; while @b { @C }})] b) fun (x : State Ξ“) => cT X (Termination.term, x)) X, monotone' := β‹― }
              source
              theorem pGCL.tsum_succs_univ' {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) {C : pGCL Ξ“} {Οƒ : State Ξ“} {Ξ± : Act} (f : ↑(SmallStepSemantics.psucc C Οƒ Ξ±) β†’ ENNReal) :
              βˆ‘' (s' : ↑(SmallStepSemantics.psucc C Οƒ Ξ±)), f s' = βˆ‘' (s' : ENNReal Γ— (pGCL Ξ“ βŠ• Termination) Γ— State Ξ“), if h : s' ∈ SmallStepSemantics.psucc C Οƒ Ξ± then f ⟨s', h⟩ else 0
              source
              theorem pGCL.tsum_succs_univ'' {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) {C : pGCL Ξ“} {Οƒ : State Ξ“} {Ξ± : Act} (f : ↑(SmallStepSemantics.psucc C Οƒ Ξ±) β†’ ENNReal) :
              βˆ‘' (s' : ↑(SmallStepSemantics.psucc C Οƒ Ξ±)), f s' = βˆ‘' (s' : ENNReal Γ— (pGCL Ξ“ βŠ• Termination) Γ— State Ξ“), if h : s' ∈ SmallStepSemantics.psucc C Οƒ Ξ± then f ⟨s', h⟩ else 0
              source
              theorem pGCL.ΞΎ.seq {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] {O : Optimization} {C₁ Cβ‚‚ : pGCL Ξ“} (ih₁ : (SmallStepSemantics.ΞΎ O) (wp O) C₁ = wp[O]⟦@Cβ‚βŸ§) :
              (SmallStepSemantics.ΞΎ O) (wp O) (pgcl {@C₁ ; @Cβ‚‚}) = wp[O]⟦@Cβ‚βŸ§.comp wp[O]⟦@Cβ‚‚βŸ§
              source
              theorem pGCL.ΞΎ.seq' {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] {O : Optimization} {C₁ Cβ‚‚ : pGCL Ξ“} (ih₁ : (SmallStepSemantics.ΞΎ O) (wfp O) C₁ = wfp[O]⟦@Cβ‚βŸ§) :
              (SmallStepSemantics.ΞΎ O) (wfp O) (pgcl {@C₁ ; @Cβ‚‚}) = wfp[O]⟦@Cβ‚βŸ§.comp wfp[O]⟦@Cβ‚‚βŸ§
              source
              theorem pGCL.op_le_seq {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] (cT : (State Ξ“ β†’ ENNReal) β†’o Termination Γ— State Ξ“ β†’ ENNReal) (cP : pGCL Ξ“ Γ— State Ξ“ β†’ ENNReal) {C : pGCL Ξ“} {O : Optimization} {C' : pGCL Ξ“} [SmallStepSemantics.mdp.FiniteBranching] (t_const : State Ξ“ β†’ ENNReal) (hp : βˆ€ (C C' : pGCL Ξ“) (Οƒ : State Ξ“), cP (pgcl {@C ; @C'}, Οƒ) = cP (C, Οƒ)) (ht : βˆ€ (X : State Ξ“ β†’ ENNReal) (Οƒ : State Ξ“), cT X (Termination.term, Οƒ) ≀ X Οƒ) (ht' : βˆ€ (X : State Ξ“ β†’ ENNReal) (Οƒ : State Ξ“), cT X (Termination.fault, Οƒ) = t_const Οƒ) :
              ⇑(SmallStepSemantics.op O C) ∘ ⇑(SmallStepSemantics.op O C') ≀ ⇑(SmallStepSemantics.op O (pgcl {@C ; @C'}))
              source
              theorem pGCL.wp_le_op.loop {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] {C : pGCL Ξ“} {b : BExpr Ξ“} {O : Optimization} (ih : wp[O]⟦@C⟧ ≀ SmallStepSemantics.op O C) :
              wp[O]⟦while @b { @C }⟧ ≀ SmallStepSemantics.op O pgcl {while @b { @C }}
              source
              @[simp]
              theorem pGCL.Exp.mk_zero_eq {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} :
              (fun (x : State Ξ“) => 0) = 0
              source
              instance pGCL.instET {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] {O : Optimization} :
              (π•Š cost_t cost_p).ET O (wp O)
              source
              theorem pGCL.wp_eq_op {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] {O : Optimization} {C : pGCL Ξ“} :
              wp[O]⟦@C⟧ = SmallStepSemantics.op O C
              source
              noncomputable instance pGCL.instSmallStepSemanticsStateTerminationAct_1 {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] :
              SmallStepSemantics (pGCL Ξ“) (State Ξ“) Termination Act
              Equations
              source
              instance pGCL.instFiniteBranchingStateTerminationAct_1 {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] :
              SmallStepSemantics.FiniteBranching (pGCL Ξ“) (State Ξ“) Termination Act
              source
              theorem pGCL.wfp_le_op.loop {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] {C : pGCL Ξ“} {b : BExpr Ξ“} {O : Optimization} (ih : wfp[O]⟦@C⟧ ≀ SmallStepSemantics.op O C) :
              wfp[O]⟦while @b { @C }⟧ ≀ SmallStepSemantics.op O pgcl {while @b { @C }}
              source
              instance pGCL.instET' {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] {O : Optimization} :
              (π•Š cost_t' cost_p').ET O (wfp O)
              source
              theorem pGCL.wfp_eq_op {𝒱 : Type u_1} {Ξ“ : 𝒱 β†’ Type u_2} [DecidableEq 𝒱] {O : Optimization} {C : pGCL Ξ“} :
              wfp[O]⟦@C⟧ = SmallStepSemantics.op O C