# 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 #

source
@[simp]
theorem Std.Do.SPred.entails.refl {σs : List (Type u)} (P : SPred σs) :
P ⊢ₛ P
source
theorem Std.Do.SPred.entails.trans {σs : List (Type u)} {P Q R : SPred σs} :
(P ⊢ₛ Q) → (Q ⊢ₛ R) → P ⊢ₛ R
source
instance Std.Do.SPred.instTransEntails {σs : List (Type u)} :
Trans entails entails entails
Equations

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

# Bientailment #

source
theorem Std.Do.SPred.bientails.iff {σs : List (Type u)} {P Q : SPred σs} :
P ⊣⊢ₛ Q ↔ (P ⊢ₛ Q) ∧ (Q ⊢ₛ P)
source
@[simp]
theorem Std.Do.SPred.bientails.refl {σs : List (Type u)} (P : SPred σs) :
P ⊣⊢ₛ P
source
theorem Std.Do.SPred.bientails.trans {σs : List (Type u)} {P Q R : SPred σs} :
(P ⊣⊢ₛ Q) → (Q ⊣⊢ₛ R) → P ⊣⊢ₛ R
source
instance Std.Do.SPred.instTransBientails {σs : List (Type u)} :
Trans bientails bientails bientails
Equations

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

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

# Pure #

source
@[simp]
theorem Std.Do.SPred.down_pure {φ : Prop} :
⌜φ⌝.down = φ
source
@[simp]
theorem Std.Do.SPred.apply_pure {σs : List (Type u)} {σ : Type u} {s : σ} {φ : Prop} :
⌜φ⌝ s = ⌜φ⌝
source
theorem Std.Do.SPred.pure_intro {σs : List (Type u)} {φ : Prop} {P : SPred σs} :
φ → P ⊢ₛ ⌜φ⌝
source
theorem Std.Do.SPred.pure_elim' {σs : List (Type u)} {φ : Prop} {P : SPred σs} :
(φ → ⊢ₛ P) → ⌜φ⌝ ⊢ₛ P
source
theorem Std.Do.SPred.and_pure {σs : List (Type u)} {P Q : Prop} :
⌜P⌝ ∧ ⌜Q⌝ ⊣⊢ₛ ⌜P ∧ Q⌝
source
theorem Std.Do.SPred.or_pure {σs : List (Type u)} {P Q : Prop} :
⌜P⌝ ∨ ⌜Q⌝ ⊣⊢ₛ ⌜P ∨ Q⌝
source
theorem Std.Do.SPred.imp_pure {σs : List (Type u)} {P Q : Prop} :
(⌜P⌝ → ⌜Q⌝) ⊣⊢ₛ ⌜P → Q⌝

# Conjunction #

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

# Disjunction #

source
theorem Std.Do.SPred.or_intro_l {σs : List (Type u)} {P Q : SPred σs} :
P ⊢ₛ P ∨ Q
source
theorem Std.Do.SPred.or_intro_r {σs : List (Type u)} {P Q : SPred σs} :
Q ⊢ₛ P ∨ Q
source
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 #

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

# Quantifiers #

source
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
source
theorem Std.Do.SPred.forall_elim {σs : List (Type u)} {α : Sort u_1} {Ψ : α → SPred σs} (a : α) :
(«forall» fun (a : α) => Ψ a) ⊢ₛ Ψ a
source
theorem Std.Do.SPred.exists_intro {σs : List (Type u)} {α : Sort u_1} {Ψ : α → SPred σs} (a : α) :
Ψ a ⊢ₛ «exists» fun (a : α) => Ψ a
source
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 #

source
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 }
source
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 }
source
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 }