Documentation

Std.Do.PredTrans

Predicate transformers for arbitrary postcondition shapes #

This module defines the type PredTrans ps of predicate transformers for a given ps : PostShape. PredTrans forms the semantic domain of the weakest precondition interpretation WP in which we interpret monadic programs.

A predicate transformer x : PredTrans ps α is a function that takes a postcondition Q : PostCond α ps and returns a precondition x.apply Q : Assertion ps, with the additional monotonicity property that the precondition is stronger the stronger the postcondition is: Q₁ ⊢ₚ Q₂ → x.apply Q₁ ⊢ₛ x.apply Q₂.

Since PredTrans itself forms a monad, we can interpret monadic programs by writing a monad morphism into PredTrans; this is exactly what WP encodes. This module defines interpretations of common monadic operations, such as get, throw, liftM, etc.

def Std.Do.PredTrans.Monotonic {ps : PostShape} {α : Type} (t : PostCond α psAssertion ps) :

The stronger the postcondition, the stronger the transformed precondition.

Equations
Instances For
    def Std.Do.PredTrans.Conjunctive {ps : PostShape} {α : Type} (t : PostCond α psAssertion ps) :

    Transforming a conjunction of postconditions is the same as the conjunction of transformed postconditions.

    Equations
    Instances For

      Any predicate transformer that is conjunctive is also monotonic.

      Equations
      • =
      Instances For
        structure Std.Do.PredTrans (ps : PostShape) (α : Type) :

        The type of predicate transformers for a given ps : PostShape and return type α : Type. A predicate transformer x : PredTrans ps α is a function that takes a postcondition Q : PostCond α ps and returns a precondition x.apply Q : Assertion ps, with the additional monotonicity property that the precondition is stronger the stronger the postcondition is: Q₁ ⊢ₚ Q₂ → x.apply Q₁ ⊢ₛ x.apply Q₂.

        Instances For
          theorem Std.Do.PredTrans.ext_iff {ps : PostShape} {α : Type} {x y : PredTrans ps α} :
          x = y x.apply = y.apply
          theorem Std.Do.PredTrans.ext {ps : PostShape} {α : Type} {x y : PredTrans ps α} (apply : x.apply = y.apply) :
          x = y
          theorem Std.Do.PredTrans.mono {ps : PostShape} {α : Type} (t : PredTrans ps α) :
          def Std.Do.PredTrans.le {ps : PostShape} {α : Type} (x y : PredTrans ps α) :

          Given a fixed postcondition, the stronger predicate transformer will yield a weaker precondition.

          Equations
          Instances For
            def Std.Do.PredTrans.pure {ps : PostShape} {α : Type} (a : α) :
            PredTrans ps α
            Equations
            Instances For
              def Std.Do.PredTrans.bind {ps : PostShape} {α β : Type} (x : PredTrans ps α) (f : αPredTrans ps β) :
              PredTrans ps β
              Equations
              Instances For
                def Std.Do.PredTrans.const {ps : PostShape} {α : Type} (p : Assertion ps) :
                PredTrans ps α
                Equations
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  @[simp]
                  theorem Std.Do.PredTrans.pure_apply {ps : PostShape} {α : Type} (a : α) (Q : PostCond α ps) :
                  (pure a).apply Q = Q.fst a
                  @[simp]
                  theorem Std.Do.PredTrans.Pure_pure_apply {ps : PostShape} {α : Type} (a : α) (Q : PostCond α ps) :
                  (Pure.pure a).apply Q = Q.fst a
                  @[simp]
                  theorem Std.Do.PredTrans.map_apply {ps : PostShape} {α β : Type} (f : αβ) (x : PredTrans ps α) (Q : PostCond β ps) :
                  (f <$> x).apply Q = x.apply (fun (a : α) => Q.fst (f a), Q.snd)
                  @[simp]
                  theorem Std.Do.PredTrans.bind_apply {ps : PostShape} {α β : Type} (x : PredTrans ps α) (f : αPredTrans ps β) (Q : PostCond β ps) :
                  (x >>= f).apply Q = x.apply (fun (a : α) => (f a).apply Q, Q.snd)
                  @[simp]
                  theorem Std.Do.PredTrans.seq_apply {ps : PostShape} {α β : Type} (f : PredTrans ps (αβ)) (x : PredTrans ps α) (Q : PostCond β ps) :
                  (f <*> x).apply Q = f.apply (fun (g : αβ) => x.apply (fun (a : α) => Q.fst (g a), Q.snd), Q.snd)
                  theorem Std.Do.PredTrans.bind_mono {ps : PostShape} {α β : Type} {x y : PredTrans ps α} {f : αPredTrans ps β} (h : x y) :
                  x >>= f y >>= f
                  def Std.Do.PredTrans.pushArg {ps : PostShape} {σ α : Type} (x : StateT σ (PredTrans ps) α) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Std.Do.PredTrans.popArg {σ : Type} {ps : PostShape} {α : Type} (x : PredTrans (PostShape.arg σ ps) α) :
                    StateT σ (PredTrans ps) α
                    Equations
                    Instances For
                      def Std.Do.PredTrans.pushExcept {ps : PostShape} {α ε : Type} (x : ExceptT ε (PredTrans ps) α) :
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Std.Do.PredTrans.popExcept {ε : Type} {ps : PostShape} {α : Type} (x : PredTrans (PostShape.except ε ps) α) :
                        ExceptT ε (PredTrans ps) α
                        Equations
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Equations
                          • One or more equations did not get rendered due to their size.
                          @[simp]
                          def Std.Do.PredTrans.pushArg_apply {ps : PostShape} {α σ : Type} {Q : PostCond α (PostShape.arg σ ps)} (f : σPredTrans ps (α × σ)) :
                          (pushArg f).apply Q = fun (s : σ) => (f s).apply (fun (x : α × σ) => match x with | (a, s) => Q.fst a s, Q.snd)
                          Equations
                          • =
                          Instances For
                            @[simp]
                            def Std.Do.PredTrans.pushExcept_apply {ps : PostShape} {α ε : Type} {Q : PostCond α (PostShape.except ε ps)} (x : PredTrans ps (Except ε α)) :
                            (pushExcept x).apply Q = x.apply (fun (x : Except ε α) => match x with | Except.ok a => Q.fst a | Except.error e => Q.snd.fst e, Q.snd.snd)
                            Equations
                            • =
                            Instances For
                              def Std.Do.PredTrans.dite_apply {α : Type} {ps : PostShape} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : cPredTrans ps α) (e : ¬cPredTrans ps α) :
                              (if h : c then t h else e h).apply Q = if h : c then (t h).apply Q else (e h).apply Q
                              Equations
                              • =
                              Instances For
                                def Std.Do.PredTrans.ite_apply {α : Type} {ps : PostShape} {Q : PostCond α ps} (c : Prop) [Decidable c] (t e : PredTrans ps α) :
                                (if c then t else e).apply Q = if c then t.apply Q else e.apply Q
                                Equations
                                • =
                                Instances For
                                  @[simp]
                                  def Std.Do.PredTrans.monadLiftArg_apply {α σ : Type} {ps : PostShape} {Q : PostCond α (PostShape.arg σ ps)} (t : PredTrans ps α) :
                                  (MonadLift.monadLift t).apply Q = fun (s : σ) => t.apply (fun (a : α) => Q.fst a s, Q.snd)
                                  Equations
                                  • =
                                  Instances For
                                    @[simp]
                                    def Std.Do.PredTrans.monadLiftExcept_apply {α ε : Type} {ps : PostShape} {Q : PostCond α (PostShape.except ε ps)} (t : PredTrans ps α) :
                                    (MonadLift.monadLift t).apply Q = t.apply (fun (a : α) => Q.fst a, Q.snd.snd)
                                    Equations
                                    • =
                                    Instances For
                                      @[simp]
                                      def Std.Do.PredTrans.monadMapArg_apply {α σ : Type} {ps : PostShape} {Q : PostCond α (PostShape.arg σ ps)} (f : {β : Type} → PredTrans ps βPredTrans ps β) (t : PredTrans (PostShape.arg σ ps) α) :
                                      (MonadFunctor.monadMap (fun {β : Type} => f) t).apply Q = fun (s : σ) => (f (t.popArg s)).apply (fun (x : α × σ) => match x with | (a, s) => Q.fst a s, Q.snd)
                                      Equations
                                      • =
                                      Instances For
                                        @[simp]
                                        def Std.Do.PredTrans.monadMapExcept_apply {α ε : Type} {ps : PostShape} {Q : PostCond α (PostShape.except ε ps)} (f : {β : Type} → PredTrans ps βPredTrans ps β) (t : PredTrans (PostShape.except ε ps) α) :
                                        (MonadFunctor.monadMap (fun {β : Type} => f) t).apply Q = (f t.popExcept).apply (fun (x : Except ε α) => match x with | Except.ok a => Q.fst a | Except.error e => Q.snd.fst e, Q.snd.snd)
                                        Equations
                                        • =
                                        Instances For
                                          @[simp]
                                          def Std.Do.PredTrans.popArg_apply {α σ : Type} {s : σ} {ps : PostShape} {Q : PostCond (α × σ) ps} (t : PredTrans (PostShape.arg σ ps) α) :
                                          (t.popArg s).apply Q = t.apply (fun (a : α) (s : σ) => Q.fst (a, s), Q.snd) s
                                          Equations
                                          • =
                                          Instances For
                                            @[simp]
                                            def Std.Do.PredTrans.popExcept_apply {ε α : Type} {ps : PostShape} {Q : PostCond (Except ε α) ps} (t : PredTrans (PostShape.except ε ps) α) :
                                            t.popExcept.apply Q = t.apply (fun (a : α) => Q.fst (Except.ok a), fun (e : ε) => Q.fst (Except.error e), Q.snd)
                                            Equations
                                            • =
                                            Instances For
                                              @[simp]
                                              theorem Std.Do.PredTrans.pushArg_popArg {σ✝ : Type} {a✝ : PostShape} {α✝ : Type} {x : PredTrans (PostShape.arg σ✝ a✝) α✝} :
                                              @[simp]
                                              theorem Std.Do.PredTrans.popArg_pushArg {σ✝ : Type} {ps✝ : PostShape} {α✝ : Type} {f : StateT σ✝ (PredTrans ps✝) α✝} :
                                              @[simp]
                                              theorem Std.Do.PredTrans.pushExcept_popExcept {ε✝ : Type} {a✝ : PostShape} {α✝ : Type} {x : PredTrans (PostShape.except ε✝ a✝) α✝} :
                                              @[simp]
                                              theorem Std.Do.PredTrans.popExcept_pushExcept {ε✝ : Type} {ps✝ : PostShape} {α✝ : Type} {x : ExceptT ε✝ (PredTrans ps✝) α✝} :