State-indexed predicates

This module provides a type SPred σs of predicates indexed by a list of states. This type forms the basis for the notion of assertion in Std.Do; see Std.Do.Assertion.

@[reducible, inline]

abbrev Std.Do.SPred (σs : List (Type u)) : Type u

A predicate over states, where each state is defined by a list of component state types.

Example:

SPred [Nat, Bool] = (Nat → Bool → ULift Prop)

theorem Std.Do.SPred.ext_nil {P Q : SPred []} (h : P.down ↔ Q.down) : P = Q

theorem Std.Do.SPred.ext_nil_iff {P Q : SPred []} : P = Q ↔ (P.down ↔ Q.down)

theorem Std.Do.SPred.ext_cons {σs : List (Type u)} {σ : Type u} {P Q : SPred (σ :: σs)} : (∀ (s : σ), P s = Q s) → P = Q

theorem Std.Do.SPred.ext_cons_iff {σs : List (Type u)} {σ : Type u} {P Q : SPred (σ :: σs)} : P = Q ↔ ∀ (s : σ), P s = Q s

def Std.Do.SPred.pure {σs : List (Type u)} (P : Prop) : SPred σs

A pure proposition P : Prop embedded into SPred. Prefer to use notation ⌜P⌝.

theorem Std.Do.SPred.pure_nil {P : Prop} : ⌜P⌝ = { down := P }

theorem Std.Do.SPred.pure_cons {σs : List (Type u)} {σ : Type u} {P : Prop} : ⌜P⌝ = fun (x : σ) => ⌜P⌝

def Std.Do.SPred.entails {σs : List (Type u)} (P Q : SPred σs) : Prop

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.

@[simp]

theorem Std.Do.SPred.entails_nil {P Q : SPred []} : (P ⊢ₛ Q) = (P.down → Q.down)

theorem Std.Do.SPred.entails_cons {σs : List (Type u)} {σ : Type u} {P Q : SPred (σ :: σs)} : (P ⊢ₛ Q) = ∀ (s : σ), P s ⊢ₛ Q s

theorem Std.Do.SPred.entails_cons_intro {σs : List (Type u)} {σ : Type u} {P Q : SPred (σ :: σs)} : (∀ (s : σ), P s ⊢ₛ Q s) → P ⊢ₛ Q

def Std.Do.SPred.bientails {σs : List (Type u)} (P Q : SPred σs) : Prop

Logical equivalence of SPred.

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

@[simp]

theorem Std.Do.SPred.bientails_nil {P Q : SPred []} : (P ⊣⊢ₛ Q) = (P.down ↔ Q.down)

theorem Std.Do.SPred.bientails_cons {σs : List (Type u)} {σ : Type u} {P Q : SPred (σ :: σs)} : (P ⊣⊢ₛ Q) = ∀ (s : σ), P s ⊣⊢ₛ Q s

theorem Std.Do.SPred.bientails_cons_intro {σs : List (Type u)} {σ : Type u} {P Q : SPred (σ :: σs)} : (∀ (s : σ), P s ⊣⊢ₛ Q s) → P ⊣⊢ₛ Q

def Std.Do.SPred.and {σs : List (Type u)} (P Q : SPred σs) : SPred σs

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

@[simp]

theorem Std.Do.SPred.and_nil {P Q : SPred []} : spred(P ∧ Q) = { down := P.down ∧ Q.down }

@[simp]

theorem Std.Do.SPred.and_cons {σs : List (Type u)} {σ : Type u} {s : σ} {P Q : SPred (σ :: σs)} : spred(P ∧ Q) s = spred(P s ∧ Q s)

def Std.Do.SPred.or {σs : List (Type u)} (P Q : SPred σs) : SPred σs

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

@[simp]

theorem Std.Do.SPred.or_nil {P Q : SPred []} : spred(P ∨ Q) = { down := P.down ∨ Q.down }

@[simp]

theorem Std.Do.SPred.or_cons {σs : List (Type u)} {σ : Type u} {s : σ} {P Q : SPred (σ :: σs)} : spred(P ∨ Q) s = spred(P s ∨ Q s)

def Std.Do.SPred.not {σs : List (Type u)} (P : SPred σs) : SPred σs

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

@[simp]

theorem Std.Do.SPred.not_nil {P : SPred []} : spred(¬P) = { down := ¬P.down }

@[simp]

theorem Std.Do.SPred.not_cons {σs : List (Type u)} {σ : Type u} {s : σ} {P : SPred (σ :: σs)} : spred(¬P) s = spred(¬P s)

def Std.Do.SPred.imp {σs : List (Type u)} (P Q : SPred σs) : SPred σs

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

@[simp]

theorem Std.Do.SPred.imp_nil {P Q : SPred []} : spred(P → Q) = { down := P.down → Q.down }

@[simp]

theorem Std.Do.SPred.imp_cons {σs : List (Type u)} {σ : Type u} {s : σ} {P Q : SPred (σ :: σs)} : spred(P → Q) s = spred(P s → Q s)

def Std.Do.SPred.iff {σs : List (Type u)} (P Q : SPred σs) : SPred σs

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

@[simp]

theorem Std.Do.SPred.iff_nil {P Q : SPred []} : spred(P ↔ Q) = { down := P.down ↔ Q.down }

@[simp]

theorem Std.Do.SPred.iff_cons {σs : List (Type u)} {σ : Type u} {s : σ} {P Q : SPred (σ :: σs)} : spred(P ↔ Q) s = spred(P s ↔ Q s)

def Std.Do.SPred.exists {α : Sort u} {σs : List (Type v)} (P : α → SPred σs) : SPred σs

Existential quantifier in SPred.

@[simp]

theorem Std.Do.SPred.exists_nil {α : Sort u_1} {P : α → SPred []} : «exists» P = { down := ∃ (a : α), (P a).down }

@[simp]

theorem Std.Do.SPred.exists_cons {σs : List (Type u)} {σ : Type u} {s : σ} {α : Sort u_1} {P : α → SPred (σ :: σs)} : «exists» P s = «exists» fun (a : α) => P a s

def Std.Do.SPred.forall {α : Sort u} {σs : List (Type v)} (P : α → SPred σs) : SPred σs

Universal quantifier in SPred.

@[simp]

theorem Std.Do.SPred.forall_nil {α : Sort u_1} {P : α → SPred []} : «forall» P = { down := ∀ (a : α), (P a).down }

@[simp]

theorem Std.Do.SPred.forall_cons {σs : List (Type u)} {σ : Type u} {s : σ} {α : Sort u_1} {P : α → SPred (σ :: σs)} : «forall» P s = «forall» fun (a : α) => P a s

def Std.Do.SPred.conjunction {σs : List (Type u)} (env : List (SPred σs)) : SPred σs

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

@[simp]

theorem Std.Do.SPred.conjunction_nil {σs : List (Type u)} : conjunction [] = ⌜True⌝

@[simp]

theorem Std.Do.SPred.conjunction_cons {σs : List (Type u)} {P : SPred σs} {env : List (SPred σs)} : conjunction (P :: env) = spred(P ∧ conjunction env)

@[simp]

theorem Std.Do.SPred.conjunction_apply {σs : List (Type u)} {σ : Type u} {s : σ} {env : List (SPred (σ :: σs))} : conjunction env s = conjunction (List.map (fun (x : SPred (σ :: σs)) => x s) env)