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) : Type

A predicate indexed by a list of states.

example : SPred [Nat, Bool] = (Nat → Bool → Prop) := rfl

Equations

• Std.Do.SPred σs = Std.Do.SVal σs Prop

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

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

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

Entailment in SPred.

Equations

• (P_2 ⊢ₛ Q_2) = (P_2 → Q_2)
• (P_2 ⊢ₛ Q_2) = ∀ (s : σ), P_2 s ⊢ₛ Q_2 s

@[simp]

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

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

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

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

Equivalence relation on SPred. Convert to Eq via bientails.to_eq.

Equations

• (P_2 ⊣⊢ₛ Q_2) = (P_2 ↔ Q_2)
• (P_2 ⊣⊢ₛ Q_2) = ∀ (s : σ), P_2 s ⊣⊢ₛ Q_2 s

@[simp]

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

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

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

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

Conjunction in SPred.

Equations

• spred(P_2 ∧ Q_2) = (P_2 ∧ Q_2)
• spred(P_2 ∧ Q_2) = fun (s : σ) => spred(P_2 s ∧ Q_2 s)

@[simp]

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

@[simp]

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

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

Disjunction in SPred.

Equations

• spred(P_2 ∨ Q_2) = (P_2 ∨ Q_2)
• spred(P_2 ∨ Q_2) = fun (s : σ) => spred(P_2 s ∨ Q_2 s)

@[simp]

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

@[simp]

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

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

Negation in SPred.

Equations

• spred(¬P_2) = ¬P_2
• spred(¬P_2) = fun (s : σ) => spred(¬P_2 s)

@[simp]

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

@[simp]

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

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

Implication in SPred.

Equations

• spred(P_2 → Q_2) = (P_2 → Q_2)
• spred(P_2 → Q_2) = fun (s : σ) => spred(P_2 s → Q_2 s)

@[simp]

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

@[simp]

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

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

Biconditional in SPred.

Equations

• spred(P_2 ↔ Q_2) = (P_2 ↔ Q_2)
• spred(P_2 ↔ Q_2) = fun (s : σ) => spred(P_2 s ↔ Q_2 s)

@[simp]

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

@[simp]

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

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

Existential quantifier in SPred.

Equations

• Std.Do.SPred.exists P_2 = ∃ (a : α), P_2 a
• Std.Do.SPred.exists P_2 = fun (s : σ) => Std.Do.SPred.exists fun (a : α) => P_2 a s

@[simp]

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

@[simp]

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

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

Universal quantifier in SPred.

Equations

• Std.Do.SPred.forall P_2 = ∀ (a : α), P_2 a
• Std.Do.SPred.forall P_2 = fun (s : σ) => Std.Do.SPred.forall fun (a : α) => P_2 a s

@[simp]

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

@[simp]

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

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

Conjunction of a list of SPred.

Equations

• Std.Do.SPred.conjunction [] = Std.Do.SPred.pure✝ True
• Std.Do.SPred.conjunction (P :: env_2) = spred(P ∧ Std.Do.SPred.conjunction env_2)

@[simp]

theorem Std.Do.SPred.conjunction_nil {σs : List Type} : conjunction [] = Std.Do.SPred.pure✝ True

@[simp]

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

@[simp]

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