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} (P : SPred σs) : P ⊢ₛ P

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

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

Equations

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

Bientailment

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

@[simp]

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

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

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

Equations

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

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

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

Pure

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

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

Conjunction

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

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

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

Disjunction

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

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

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

Implication

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

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

Quantifiers

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

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

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

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