Laws of SPred

This module contains lemmas about SPred that need to be proved by induction on σs. That is, they need to proved by appealing to the model of SPred and cannot be derived without doing so.

Std.Do.SPred.DerivedLaws has some more laws that are derivative of what follows.

Entailment

@[simp]

theorem Std.Do.SPred.entails.refl {σs : List (Type u)} (P : SPred σs) : P ⊢ₛ P

theorem Std.Do.SPred.entails.trans {σs : List (Type u)} {P Q R : SPred σs} : (P ⊢ₛ Q) → (Q ⊢ₛ R) → P ⊢ₛ R

@[implicit_reducible]

instance Std.Do.SPred.instTransEntails {σs : List (Type u)} : Trans entails entails entails

Equations

• Std.Do.SPred.instTransEntails = { trans := ⋯ }

Bientailment

theorem Std.Do.SPred.bientails.iff {σs : List (Type u)} {P Q : SPred σs} : P ⊣⊢ₛ Q ↔ (P ⊢ₛ Q) ∧ (Q ⊢ₛ P)

@[simp]

theorem Std.Do.SPred.bientails.refl {σs : List (Type u)} (P : SPred σs) : P ⊣⊢ₛ P

theorem Std.Do.SPred.bientails.trans {σs : List (Type u)} {P Q R : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊣⊢ₛ R) → P ⊣⊢ₛ R

@[implicit_reducible]

instance Std.Do.SPred.instTransBientails {σs : List (Type u)} : Trans bientails bientails bientails

Equations

• Std.Do.SPred.instTransBientails = { trans := ⋯ }

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

theorem Std.Do.SPred.bientails.to_eq {σs : List (Type u)} {P Q : SPred σs} (h : P ⊣⊢ₛ Q) : P = Q

Pure

@[simp]

theorem Std.Do.SPred.down_pure {φ : Prop} : ⌜φ⌝.down = φ

@[simp]

theorem Std.Do.SPred.apply_pure {σs : List (Type u)} {σ : Type u} {s : σ} {φ : Prop} : ⌜φ⌝ s = ⌜φ⌝

theorem Std.Do.SPred.pure_intro {σs : List (Type u)} {φ : Prop} {P : SPred σs} : φ → P ⊢ₛ ⌜φ⌝

theorem Std.Do.SPred.pure_elim' {σs : List (Type u)} {φ : Prop} {P : SPred σs} : (φ → ⊢ₛ P) → ⌜φ⌝ ⊢ₛ P

Conjunction

theorem Std.Do.SPred.and_intro {σs : List (Type u)} {P Q R : SPred σs} (h1 : P ⊢ₛ Q) (h2 : P ⊢ₛ R) : P ⊢ₛ Q ∧ R

theorem Std.Do.SPred.and_elim_l {σs : List (Type u)} {P Q : SPred σs} : P ∧ Q ⊢ₛ P

theorem Std.Do.SPred.and_elim_r {σs : List (Type u)} {P Q : SPred σs} : P ∧ Q ⊢ₛ Q

Disjunction

theorem Std.Do.SPred.or_intro_l {σs : List (Type u)} {P Q : SPred σs} : P ⊢ₛ P ∨ Q

theorem Std.Do.SPred.or_intro_r {σs : List (Type u)} {P Q : SPred σs} : Q ⊢ₛ P ∨ Q

theorem Std.Do.SPred.or_elim {σs : List (Type u)} {P Q R : SPred σs} (h1 : P ⊢ₛ R) (h2 : Q ⊢ₛ R) : P ∨ Q ⊢ₛ R

Implication

theorem Std.Do.SPred.imp_intro {σs : List (Type u)} {P Q R : SPred σs} (h : P ∧ Q ⊢ₛ R) : P ⊢ₛ Q → R

theorem Std.Do.SPred.imp_elim {σs : List (Type u)} {P Q R : SPred σs} (h : P ⊢ₛ Q → R) : P ∧ Q ⊢ₛ R

Quantifiers

theorem Std.Do.SPred.forall_intro {σs : List (Type u)} {α : Sort u_1} {P : SPred σs} {Ψ : α → SPred σs} (h : ∀ (a : α), P ⊢ₛ Ψ a) : P ⊢ₛ «forall» fun (a : α) => Ψ a

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

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

theorem Std.Do.SPred.exists_elim {σs : List (Type u)} {α : Sort u_1} {Φ : α → SPred σs} {Q : SPred σs} (h : ∀ (a : α), Φ a ⊢ₛ Q) : («exists» fun (a : α) => Φ a) ⊢ₛ Q

Curry

theorem Std.Do.SPred.and_curry {σs : List (Type u)} {P Q : SVal.StateTuple σs → Prop} : ((SVal.curry fun (t : SVal.StateTuple σs) => { down := P t }) ∧ SVal.curry fun (t : SVal.StateTuple σs) => { down := Q t }) ⊣⊢ₛ SVal.curry fun (t : SVal.StateTuple σs) => { down := P t ∧ Q t }

theorem Std.Do.SPred.or_curry {σs : List (Type u)} {P Q : SVal.StateTuple σs → Prop} : ((SVal.curry fun (t : SVal.StateTuple σs) => { down := P t }) ∨ SVal.curry fun (t : SVal.StateTuple σs) => { down := Q t }) ⊣⊢ₛ SVal.curry fun (t : SVal.StateTuple σs) => { down := P t ∨ Q t }

theorem Std.Do.SPred.imp_curry {σs : List (Type u)} {P Q : SVal.StateTuple σs → Prop} : ((SVal.curry fun (t : SVal.StateTuple σs) => { down := P t }) → SVal.curry fun (t : SVal.StateTuple σs) => { down := Q t }) ⊣⊢ₛ SVal.curry fun (t : SVal.StateTuple σs) => { down := P t → Q t }

evalsTo — relate an SVal to a pure value

def Std.Do.SVal.evalsTo {α : Type u} {σs : List (Type u)} (f : SVal σs α) (a : α) : SPred σs

Relates a stateful value to a pure value, lifting equality through the state layers.

Equations

• f.evalsTo a = Std.Do.SVal.curry fun (t : Std.Do.SVal.StateTuple σs) => ⌜a = f.uncurry t⌝

@[simp]

theorem Std.Do.SVal.evalsTo_nil {α : Type u_1} {f : SVal [] α} {a : α} : f.evalsTo a = ⌜a = f⌝

@[simp]

theorem Std.Do.SVal.evalsTo_cons {α σ : Type u} {σs : List (Type u)} {f : SVal (σ :: σs) α} {a : α} {s : σ} : f.evalsTo a s = (f s).evalsTo a

theorem Std.Do.SVal.evalsTo_total {σs : List (Type u_1)} {α : Type u_1} {P : SPred σs} (f : SVal σs α) : P ⊢ₛ SPred.exists fun (m : α) => f.evalsTo m