SatisfiesM.seq_pre
theorem SatisfiesM.seq_pre :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p₂ : α → Prop} {α_1 : Type u_1} {q : α_1 → Prop} {f : m (α → α_1)}
[inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM (fun f => ∀ {a : α}, p₂ a → q (f a)) f → SatisfiesM p₂ x → SatisfiesM q (Seq.seq f fun x_1 => x)
The theorem `SatisfiesM.seq_pre` states that the `SatisfiesM` function, which lifts propositions over a monad, distributes over the `Seq.seq` operation. More concretely, for any applicative functor `m`, types `α` and `α_1`, propositions `p₂` and `q`, a function `f` of type `m (α → α_1)` and a value `x` of type `m α`, if `f` satisfies the condition that for all `a` of type `α`, `p₂ a` implies `q (f a)`, and `x` satisfies `p₂`, then the result of sequencing `f` and `x` will satisfy `q`. This theorem is useful when `x` and the goal are known, and `f` is a subgoal.
More concisely: If `f` is a function from `α` to `α_1` in an applicative monad `m` such that `p₂(a)` implies `q(f(a))` for all `a` in `α` and `x` is an element of type `m α` satisfying `p₂(x)`, then `(f <$> x)` satisfies `q`.
|
SatisfiesM.map_pre
theorem SatisfiesM.map_pre :
∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p : α_1 → Prop} {f : α → α_1} [inst : Functor m]
[inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM (fun a => p (f a)) x → SatisfiesM p (f <$> x)
The theorem `SatisfiesM.map_pre` states that the `SatisfiesM` property, which asserts that a monadic value can act as if it has a postcondition, distributes over the functor map operation `<$>`. Specifically, if we have a monadic value `x` of type `m α`, a function `f` from `α` to `α_1`, and a property `p` over `α_1`, then if our `x` satisfies a precondition that, when `f` is applied to any value of `α`, it results in a value satisfying `p`, then we can equivalently say that the monadic value resulting from applying `f` to `x` (denoted `f <$> x`) satisfies `p`. This theorem is useful when reasoning backward from the goal, in a weakest precondition style.
More concisely: If `x : m α` satisfies `p` for all `α` such that `f(α) : α₁` also satisfies `p`, then `f <$> x : m (α₁)` satisfies `p`.
|
SatisfiesM.trivial
theorem SatisfiesM.trivial :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM (fun x => True) x
The theorem `SatisfiesM.trivial` states that if we have a proposition `p` that is always true (i.e., for every variable `x`, `p x` is `True`), then that proposition `p` is satisfied by any value `x` of an arbitrary type `α` in the context of any monad `m`. This is a variant of the general truth principle `of_true` under the perspective of strongest postconditions in the setting of monads, which means that when a proposition is always `True`, it is fulfilled by any value in the monadic context.
More concisely: For any proposition `p` that is always true and monad `m`, `p` is satisfied by any value `x` of type `α` in the context of `m`.
|
SatisfiesM.bind
theorem SatisfiesM.bind :
∀ {m : Type u_1 → Type u_2} {α β : Type u_1} {p : α → Prop} {x : m α} {q : β → Prop} [inst : Monad m]
[inst_1 : LawfulMonad m] {f : α → m β},
SatisfiesM p x → (∀ (a : α), p a → SatisfiesM q (f a)) → SatisfiesM q (x >>= f)
The theorem `SatisfiesM.bind` states that the `SatisfiesM` property, which is a way of expressing conditions on the values produced by a monadic computation, distributes over the bind operation (`>>=`) in a monad. More specifically, given a monad `m`, types `α` and `β`, a property `p` on `α`, a monadic computation `x` of type `m α`, another property `q` on `β`, and a function `f` of type `α → m β`, if `x` satisfies `p` (in the sense of `SatisfiesM`) and for all elements `a` of type `α` for which `p a` holds, the computation `f a` satisfies `q`, then the computation obtained by binding `x` to `f` (i.e., `x >>= f`) satisfies `q`. This theorem is a generalized version of the property that conditions on the values produced by a monadic computation are preserved under the bind operation.
More concisely: If `m` is a monad, `p` is a property on type `α`, `x` is an `m α` value satisfying `SatisfiesM p`, and for all `α` values `a` where `p a` holds, `f a` also satisfies `q`, then `x >>= f` satisfies `SatisfiesM q`.
|
SatisfiesM.map_post
theorem SatisfiesM.map_post :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {α_1 : Type u_1} {f : α → α_1} [inst : Functor m]
[inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM p x → SatisfiesM (fun b => ∃ a, p a ∧ b = f a) (f <$> x)
The theorem `SatisfiesM.map_post` states that for any functor `m`, types `α` and `α_1`, proposition `p` over `α`, and function `f` from `α` to `α_1`, if a monadic value `x` of type `m α` satisfies the proposition `p` (in the sense of the `SatisfiesM` definition), then the transformed value `f <$> x` of type `m α_1` satisfies the stronger proposition that there exists an `a` such that `p a` holds and `f a` equals the new value. Put simply, it says that if `x` satisfies `p`, then `f(x)` satisfies the existence of `p` and the function relationship, and this holds in the context of monadic computations. This theorem is particularly useful for forward reasoning from assumptions.
More concisely: For any functor `m`, types `α` and `α_1`, proposition `p` over `α`, and function `f` from `α` to `α_1`, if `x : m α` satisfies `p` and `p` implies the existence of `a` such that `f(a) = t`, then `f <$> x : m α_1` satisfies `∃a, p a ∧ f a = t`.
|
SatisfiesM.pure
theorem SatisfiesM.pure :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {a : α} [inst : Applicative m]
[inst_1 : LawfulApplicative m], p a → SatisfiesM p (pure a)
The theorem `SatisfiesM.pure` states that for any applicative monad `m`, a type `α`, a predicate `p` over `α`, and a value `a` of type `α`, if the predicate `p` holds for `a`, then `a` satisfies `p` in the context of the monad when we lift `a` into the monad using the `pure` function. This is a general form or weakest precondition version stating the property of how satisfaction (`SatisfiesM`) distributes over the `pure` function of a monad. It essentially says that `pure a` in the monad can be thought of as a value of the monad that satisfies the predicate `p` if `a` itself satisfies `p`.
More concisely: For any applicative monad `m`, predicate `p` over `α`, and value `a` of type `α`, if `p(a)` holds, then `pure a` satisfies `p` in the monad.
|
SatisfiesM.seqRight
theorem SatisfiesM.seqRight :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p₁ : α → Prop} {a : Type u_1} {p₂ : a → Prop} {y : m a} {q : a → Prop}
[inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM p₁ x →
SatisfiesM p₂ y → (∀ {a_1 : α} {b : a}, p₁ a_1 → p₂ b → q b) → SatisfiesM q (SeqRight.seqRight x fun x => y)
The theorem `SatisfiesM.seqRight` states that for any applicative functor `m`, types `α` and `a`, predicates `p₁` on `α` and `p₂` on `a`, monadic values `x` of type `m α` and `y` of type `m a`, and a predicate `q` on `a`, if `x` satisfies `p₁` and `y` satisfies `p₂`, and for any values `a_1` of type `α` and `b` of type `a`, if `p₁ a_1` and `p₂ b` implies `q b`, then the result of sequencing `x` and `y` (i.e., evaluating `x`, then `y`, and returning the result of `y`) satisfies `q`. In other words, the satisfaction property `SatisfiesM` distributes over the sequencing operation `*>` of applicative functors.
More concisely: If `m` is an applicative functor, `p₁` is a predicate on `α`, `p₂` is a predicate on `a`, `x` is a monadic value of type `m α` satisfying `p₁`, `y` is a monadic value of type `m a` satisfying `p₂`, and for all `α_1` and `a_1`, if `p₁ α_1` and `p₂ a_1` imply `q a_1`, then the result of sequencing `x` and `y` satisfies `q`.
|
SatisfiesM.seq_post
theorem SatisfiesM.seq_post :
∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {p₂ : α → Prop}
[inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM p₁ f → SatisfiesM p₂ x → SatisfiesM (fun c => ∃ f a, p₁ f ∧ p₂ a ∧ c = f a) (Seq.seq f fun x_1 => x)
The theorem `SatisfiesM.seq_post` states that, for any applicative monad `m`, any types `α` and `α_1`, propositions `p₁` over a function from `α` to `α_1` and `p₂` over `α`, a function `f` in the monad `m` from `α` to `α_1`, and a value `x` in the monad `m` of type `α`, if `f` satisfies `p₁` and `x` satisfies `p₂` (in the sense of the definition `SatisfiesM`), then the monadic value obtained by applying `f` to `x` using the sequence operator `<*>` (in a lazy perspective, meaning `x` is taken as a `Unit → m α` function) satisfies the proposition that there exist a function and a value such that the function satisfies `p₁`, the value satisfies `p₂`, and the output of the sequence operation equals to the application of the function to the value.
More concisely: For any applicative monad `m`, any types `α` and `α_1`, propositions `p₁` over `α → α_1` and `p₂` over `α`, a monadic function `f : m α → m α_1` satisfying `p₁`, a monadic value `x : m α` satisfying `p₂`, the sequence `x <*> f` in `m α_1` also satisfies the proposition `p₁ ∘ p₂`.
|
SatisfiesM.mapConst
theorem SatisfiesM.mapConst :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} {q : α → Prop} {α_1 : Type u_1} {p : α_1 → Prop} {a : α_1}
[inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α},
SatisfiesM q x → (∀ {b : α}, q b → p a) → SatisfiesM p (Functor.mapConst a x)
The theorem `SatisfiesM.mapConst` states that for any functor `m` and any types `α` and `α_1`, given properties `p` and `q` over `α_1` and `α` respectively, and a value `a` of type `α_1`, if a monadic value `x` of type `m α` satisfies the property `q`, and for all values `b` of type `α`, if `q b` holds then `p a` also holds, then the result of mapping the constant `a` over `x` using `Functor.mapConst` also satisfies the property `p`. Here, the notion of a monadic value 'satisfying a property' is defined by `SatisfiesM p x` to mean that there exists another monadic value which maps to `x` and only contains values satisfying `p`.
More concisely: If `m` is a functor, `α` and `α_1` are types, `p` is a property over `α_1`, `q` is a property over `α`, `a` is a value of type `α_1`, `x` is a monadic value of type `m α` satisfying `q`, and for all `b` of type `α`, if `q b` holds then `p a` holds, then `Functor.mapConst a x` satisfies property `p`.
|
SatisfiesM.seqLeft
theorem SatisfiesM.seqLeft :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p₁ : α → Prop} {a : Type u_1} {p₂ : a → Prop} {y : m a} {q : α → Prop}
[inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM p₁ x →
SatisfiesM p₂ y → (∀ {a_1 : α} {b : a}, p₁ a_1 → p₂ b → q a_1) → SatisfiesM q (SeqLeft.seqLeft x fun x => y)
This theorem, `SatisfiesM.seqLeft`, states that for any applicative monad `m`, given types `α` and `a`, predicates `p₁` over `α`, `p₂` over `a`, and `q` over `α`, if `x : m α` satisfies `p₁` and `y : m a` satisfies `p₂`, and for any `α_1 : α` and `b : a` the conjunction of `p₁ α_1` and `p₂ b` implies `q α_1`, then `SeqLeft.seqLeft x (fun x => y)` (which is a monadic operation that evaluates `x`, then `y`, and returns the result of `x`) satisfies `q`. This theorem essentially shows that the satisfaction property `SatisfiesM`, when applied to the `SeqLeft.seqLeft` operation, distributes over the conjunction of predicates.
More concisely: If `m` is an applicative monad, `α` and `a` are types, `p₁` is a predicate on `α`, `p₂` is a predicate on `a`, and `q` is a predicate on `α` such that `p₁(x)` and `p₂(y)` imply `q(x)` for all `x : α` and `y : a`, then `SeqLeft.seqLeft x (fun x => y)` satisfies `q` for any instances `x : m α` and `y : m a`.
|
SatisfiesM.seq
theorem SatisfiesM.seq :
∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {p₂ : α → Prop}
{q : α_1 → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM p₁ f →
SatisfiesM p₂ x → (∀ {f : α → α_1} {a : α}, p₁ f → p₂ a → q (f a)) → SatisfiesM q (Seq.seq f fun x_1 => x)
The theorem `SatisfiesM.seq` states that, given any applicative functor `m` and types `α`, `α_1`, if `f` is a monadic value of type `m (α → α_1)` that satisfies a property `p₁`, and `x` is a monadic value of type `m α` that satisfies another property `p₂`, then the result of sequencing `f` and `x` (i.e., `Seq.seq f fun _ => x`) satisfies a third property `q`, assuming that for any function `f` from `α` to `α_1` and any value `a` of type `α`, if `f` satisfies `p₁` and `a` satisfies `p₂`, then `f a` satisfies `q`. This theorem essentially states that the `SatisfiesM` property distributes over the sequencing operation `<*>` in a lawful applicative functor.
More concisely: Given an applicative functor `m`, if functions `f : α -> α_1` of type `m (α -> α_1)` satisfying `p₁` and values `x : m α` satisfying `p₂` imply that `f (x)` satisfies `q`, then `Seq.seq f fun _ => x` is a value of type `m α_1` satisfying property `q`.
|
SatisfiesM.imp
theorem SatisfiesM.imp :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p q : α → Prop} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α},
SatisfiesM p x → (∀ {a : α}, p a → q a) → SatisfiesM q x
The theorem `SatisfiesM.imp` describes the monotonicity of the `SatisfiesM p x` predicate in terms of `p`. More specifically, given a functor `m` of type `Type u_1 → Type u_2`, an arbitrary type `α`, and two propositions `p` and `q` over `α`, if `SatisfiesM p x` holds for some `x : m α` and every element `a : α` that satisfies `p` also satisfies `q`, then `SatisfiesM q x` also holds. In other words, if the monadic value `x` satisfies the postcondition `p` and `p` implies `q`, then `x` also satisfies the postcondition `q`.
More concisely: If `p` implies `q` and `SatisfiesM p x` holds for all `a` satisfying `p`, then `SatisfiesM q x`.
|
SatisfiesM.seq_pre'
theorem SatisfiesM.seq_pre' :
∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {q : α_1 → Prop}
[inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM p₁ f →
SatisfiesM (fun a => ∀ {f : α → α_1}, p₁ f → q (f a)) x → SatisfiesM q (Seq.seq f fun x_1 => x)
The theorem `SatisfiesM.seq_pre'` states that the function `SatisfiesM`, which lifts propositions over a monad to assert postconditions of monadic values, distributes over the sequence function `<*>`, in the weakest precondition sense. Specifically, given a monad `m`, types `α` and `α_1`, a predicate `p₁` on functions from `α` to `α_1`, a monadic function `f` of type `m (α → α_1)`, a predicate `q` on `α_1`, and a monadic value `x` of type `m α`, if `f` satisfies `p₁` and `x` satisfies the predicate that for all functions `f` from `α` to `α_1` that satisfy `p₁`, `q` holds for `f a`, then the sequenced application of `f` and `x` (written as `Seq.seq f fun x_1 => x`) satisfies `q`. This theorem can be used when `f` and the goal are known, and `x` is a subgoal.
More concisely: Given a monad `m`, types `α` and `α_1`, a predicate `p₁` on functions from `α` to `α_1`, a monadic function `f : m (α → α_1)`, a predicate `q` on `α_1`, and a monadic value `x : m α`, if `f` satisfies `p₁` and `x` satisfies the weakest precondition `∀g∣p₁(g), q(g ∘ x)`, then the sequenced application `Seq.seq f fun x_1 => x` satisfies `q`.
|
SatisfiesM.map
theorem SatisfiesM.map :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {α_1 : Type u_1} {q : α_1 → Prop} {f : α → α_1}
[inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α},
SatisfiesM p x → (∀ {a : α}, p a → q (f a)) → SatisfiesM q (f <$> x)
The theorem `SatisfiesM.map` states that for any functor `m`, types `α` and `α_1`, propositions `p` and `q` over `α` and `α_1` respectively, and a function `f` from `α` to `α_1`, if a monadic value `x` satisfies the proposition `p`, and for all `a` of type `α` where `p a` holds, `q (f a)` also holds, then the monadic value `f <$> x` satisfies the proposition `q`. This means that the property `SatisfiesM` distributes over a functor's fmap operation.
More concisely: If `m` is a functor, `α` and `α_1` are types, `p` is a proposition over `α`, `q` is a proposition over `α_1`, `f` is a function from `α` to `α_1`, and `x` is a monadic value of type `m α` satisfying `p`, then `f <$> x` satisfies `q` whenever `p a` implies `q (f a)` for all `a` of type `α`.
|
SatisfiesM.bind_pre
theorem SatisfiesM.bind_pre :
∀ {m : Type u_1 → Type u_2} {α β : Type u_1} {q : β → Prop} {x : m α} [inst : Monad m] [inst_1 : LawfulMonad m]
{f : α → m β}, SatisfiesM (fun a => SatisfiesM q (f a)) x → SatisfiesM q (x >>= f)
The theorem `SatisfiesM.bind_pre` states that for any monad `m`, types `α` and `β`, a proposition `q` over `β`, a monadic value `x` of type `m α`, and a function `f` from `α` to `m β`, if `x` satisfies the condition that for every `a` in `α`, `f(a)` satisfies the proposition `q`, then the result of binding `x` to `f` (denoted as `x >>= f`) also satisfies the proposition `q`. This describes how the `SatisfiesM` predicate, which lifts propositions over a monad, distributes over the bind operation `>>=` in a monadic context, in the sense of weakest preconditions.
More concisely: If `x: m α` satisfies `∀ a: α, f a belongs to q`, then `x >>= f` belongs to `q`.
|
SatisfiesM.of_true
theorem SatisfiesM.of_true :
∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m]
{x : m α}, (∀ (a : α), p a) → SatisfiesM p x
The theorem `SatisfiesM.of_true` states that for any applicative functor `m` mapping type `u_1` to type `u_2`, any type `α` of `u_1`, a proposition `p` over `α`, and any monadic value `x` with type `m α`, if the proposition `p` is true for all elements of type `α`, then the monadic value `x` satisfies the proposition `p`. This means there exists a monadic value of the subtype `{a // p a}` whose image under the functor is `x`. In other words, if a property is always true, then every monadic value has a version of it that satisfies the property.
More concisely: For any applicative functor `m`, proposition `p` over type `α`, and monadic value `x : m α`, if `p` holds for all elements of type `α`, then there exists `a : α` such that `p a` and `m.map p a = x`.
|