Entailment in SPred.

One predicate P entails another predicate Q if Q is true in every state in which P is true. Unlike implication (SPred.imp), entailment is not itself an SPred, but is instead an ordinary proposition.

Logical equivalence of SPred.

Logically equivalent predicates are equal. Use SPred.bientails.to_eq to convert bi-entailment to equality.

term ::= ...
    | Entailment in `SPred`; sugar for `SPred.entails`. term ⊢ₛ term

Entailment in SPred; sugar for SPred.entails.

term ::= ...
    | Tautology in `SPred`; sugar for `SPred.entails ⌜True⌝`. ⊢ₛ term

Tautology in SPred; sugar for SPred.entails ⌜True⌝.

term ::= ...
    | Bi-entailment in `SPred`; sugar for `SPred.bientails`. term ⊣⊢ₛ term

Bi-entailment in SPred; sugar for SPred.bientails.

Std.Do.«termSpred(_)» : termAn embedding of the special syntax for `SPred` into ordinary terms that provides alternative interpretations of logical connectives and quantifiers. Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax. spred indicates that logical connectives and quantifiers should be understood as those pertaining to stateful predicates, while Std.Do.«termTerm(_)» : termEscapes from a surrounding `spred(...)` term, returning to the usual interpretations of quantifiers and connectives. term indicates that they should have the usual meaning.

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(term)

term ::= ...
    | Escapes from a surrounding `spred(...)` term, returning to the usual interpretations of quantifiers
and connectives.
term(term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.term ∧ term)

Syntactic sugar for SPred.and.

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(`Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two
constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`,
and you can use `match` or `cases` to destruct an `Or` assumption into the
two cases.


Conventions for notations in identifiers:

 * The recommended spelling of `∨` in identifiers is `or`.term ∨ term)

Syntactic sugar for SPred.or.

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.¬ term)

Syntactic sugar for SPred.not.

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(term → term)

Syntactic sugar for SPred.imp.

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.term ↔ term)

Syntactic sugar for SPred.iff.

Conjunction in SPred: states that satisfy P and satisfy Q satisfy spred(P ∧ Q).

Conjunction of a list of stateful predicates. A state satisfies conjunction env if it satisfies all predicates in env.

Disjunction in SPred: states that either satisfy P or satisfy Q satisfy spred(P ∨ Q).

Negation in SPred: states that do not satisfy P satisfy spred(¬ P).

Implication in SPred: states that satisfy Q whenever they satisfy P satisfy spred(P → Q).

Biimplication in SPred: states that either satisfy both P and Q or satisfy neither satisfy spred(P ↔ Q).

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ ident, term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ ident : term,  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
(ident (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole)* : term),  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_, term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_ : term,  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
(A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_ (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole)* : term),  term)

Each form of universal quantification is syntactic sugar for an invocation of SPred.forall on a function that takes the quantified variable as a parameter.

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident, term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident : term,  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ (`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
binderIdent* : term),  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_, term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_ : term,  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ (`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
binderIdent* : term),  term)

Each form of existential quantification is syntactic sugar for an invocation of SPred.exists on a function that takes the quantified variable as a parameter.

Universal quantifier in SPred.

Existential quantifier in SPred.

A value indexed by a curried tuple of states.

Example:

example : SVal [Nat, Bool] String = (Nat → Bool → String) := rfl

Gets the top-most state of type σ from an SVal.

A tuple capturing the whole state of an SVal.

Curries a function taking a StateTuple into an SVal.

Uncurries an SVal into a function taking a StateTuple.

A weakest precondition interpretation of a monadic program x : m α in terms of a predicate transformer PredTrans ps α. The monad m determines ps : PostShape.

For practical reasoning, an instance of WPMonad m ps is typically needed in addition to WP m ps.

Instance Constructor

Std.Do.WP.mk.{u, v}

Methods

wp : {α : Type u} → m α → PredTrans ps α

term ::= ...
    | `wp⟦x⟧ Q` is defined as `(WP.wp x).apply Q`. wp⟦term (: term)?⟧

wp⟦x⟧ Q is defined as (WP.wp x).apply Q.

A monad with weakest preconditions (WP) that is also a monad morphism, preserving pure and bind.

In practice, mvcgen is not useful for reasoning about programs in a monad that is without a WPMonad instance. The specification lemmas for Pure.pure and Bind.bind, as well as those for operators like Functor.map, require that their monad have a WPMonad instance.

Instance Constructor

Std.Do.WPMonad.mk.{u, v}

Extends

• LawfulMonad m
• WP m ps

Methods

map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β

id_map : ∀ {α : Type u} (x : m α), id <$> x = x

comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α), (h ∘ g) <$> x = h <$> g <$> x

seqLeft_eq : ∀ {α β : Type u} (x : m α) (y : m β), x <* y = Function.const β <$> x <*> y

seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), x *> y = Function.const α id <$> x <*> y

pure_seq : ∀ {α β : Type u} (g : α → β) (x : m α), pure g <*> x = g <$> x

map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)

seq_pure : ∀ {α β : Type u} (g : m (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g

seq_assoc : ∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)), h <*> (g <*> x) = Function.comp <$> h <*> g <*> x

bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α),
  (do
      let a ← x
      pure (f a)) =
    f <$> x

bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α),
  (do
      let x_1 ← f
      x_1 <$> x) =
    f <*> x

pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

wp : {α : Type u} → m α → PredTrans ps α

wp_pure : ∀ {α : Type u} (a : α), wp (pure a) = pure a

wp_bind : ∀ {α β : Type u} (x : m α) (f : α → m β),
  (wp do
      let a ← x
      f a) =
    do
    let a ← wp x
    wp (f a)

Adequacy lemma for Id.run. Useful if you want to prove a property about an expression x defined as Id.run prog and you want to use mvcgen to reason about prog.