Derived laws of SPred

This module contains some laws about SPred that are derived from the laws in Std.Do.Laws.

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

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

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

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

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

Connectives

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

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

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

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

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

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

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

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

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

theorem Std.Do.SPred.entails.trans' {σs : List (Type u)} {P Q R : SPred σs} (h₁ : P ⊢ₛ Q) (h₂ : P ∧ Q ⊢ₛ R) : P ⊢ₛ R

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

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

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

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

theorem Std.Do.SPred.false_elim {σs : List (Type u)} {P : SPred σs} : ⌜False⌝ ⊢ₛ P

theorem Std.Do.SPred.true_intro {σs : List (Type u)} {P : SPred σs} : P ⊢ₛ ⌜True⌝

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

theorem Std.Do.SPred.and_or_elim_l {σs : List (Type u)} {P Q R T : SPred σs} (hleft : P ∧ R ⊢ₛ T) (hright : Q ∧ R ⊢ₛ T) : (P ∨ Q) ∧ R ⊢ₛ T

theorem Std.Do.SPred.and_or_elim_r {σs : List (Type u)} {P Q R T : SPred σs} (hleft : P ∧ Q ⊢ₛ T) (hright : P ∧ R ⊢ₛ T) : P ∧ (Q ∨ R) ⊢ₛ T

theorem Std.Do.SPred.exfalso {σs : List (Type u)} {P Q : SPred σs} (h : P ⊢ₛ ⌜False⌝) : P ⊢ₛ Q

Monotonicity and congruence

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

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

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

theorem Std.Do.SPred.and_congr {σs : List (Type u)} {P P' Q Q' : SPred σs} (hp : P ⊣⊢ₛ P') (hq : Q ⊣⊢ₛ Q') : P ∧ Q ⊣⊢ₛ P' ∧ Q'

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

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

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

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

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

theorem Std.Do.SPred.or_congr {σs : List (Type u)} {P P' Q Q' : SPred σs} (hp : P ⊣⊢ₛ P') (hq : Q ⊣⊢ₛ Q') : P ∨ Q ⊣⊢ₛ P' ∨ Q'

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

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

theorem Std.Do.SPred.imp_mono {σs : List (Type u)} {P P' Q Q' : SPred σs} (h1 : Q ⊢ₛ P) (h2 : P' ⊢ₛ Q') : (P → P') ⊢ₛ Q → Q'

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

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

theorem Std.Do.SPred.imp_congr {σs : List (Type u)} {P P' Q Q' : SPred σs} (h1 : P ⊣⊢ₛ Q) (h2 : P' ⊣⊢ₛ Q') : (P → P') ⊣⊢ₛ Q → Q'

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

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

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

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

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

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

Boolean algebra

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Std.Do.SPred.true_and {σs : List (Type u)} {P : SPred σs} : ⌜True⌝ ∧ P ⊣⊢ₛ P

theorem Std.Do.SPred.and_true {σs : List (Type u)} {P : SPred σs} : P ∧ ⌜True⌝ ⊣⊢ₛ P

theorem Std.Do.SPred.false_and {σs : List (Type u)} {P : SPred σs} : ⌜False⌝ ∧ P ⊣⊢ₛ ⌜False⌝

theorem Std.Do.SPred.and_false {σs : List (Type u)} {P : SPred σs} : P ∧ ⌜False⌝ ⊣⊢ₛ ⌜False⌝

theorem Std.Do.SPred.true_or {σs : List (Type u)} {P : SPred σs} : ⌜True⌝ ∨ P ⊣⊢ₛ ⌜True⌝

theorem Std.Do.SPred.or_true {σs : List (Type u)} {P : SPred σs} : P ∨ ⌜True⌝ ⊣⊢ₛ ⌜True⌝

theorem Std.Do.SPred.false_or {σs : List (Type u)} {P : SPred σs} : ⌜False⌝ ∨ P ⊣⊢ₛ P

theorem Std.Do.SPred.or_false {σs : List (Type u)} {P : SPred σs} : P ∨ ⌜False⌝ ⊣⊢ₛ P

theorem Std.Do.SPred.true_imp {σs : List (Type u)} {P : SPred σs} : (⌜True⌝ → P) ⊣⊢ₛ P

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

theorem Std.Do.SPred.imp_self_simp {σs : List (Type u)} {P Q : SPred σs} : Q ⊢ₛ P → P ↔ True

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

theorem Std.Do.SPred.false_imp {σs : List (Type u)} {P : SPred σs} : (⌜False⌝ → P) ⊣⊢ₛ ⌜True⌝

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

theorem Std.Do.SPred.of_and_imp {σs : List (Type u)} {P P' Q Q' : SPred σs} (hp : P ⊢ₛ P') (hq : Q ⊢ₛ P' → Q') : P ∧ Q ⊢ₛ P' ∧ Q'

Pure

theorem Std.Do.SPred.pure_elim {σs : List (Type u)} {Q R : SPred σs} {φ : Prop} (h1 : Q ⊢ₛ ⌜φ⌝) (h2 : φ → Q ⊢ₛ R) : Q ⊢ₛ R

theorem Std.Do.SPred.pure_mono {σs : List (Type u)} {φ₁ φ₂ : Prop} (h : φ₁ → φ₂) : ⌜φ₁⌝ ⊢ₛ ⌜φ₂⌝

theorem Std.Do.SPred.pure_congr {σs : List (Type u)} {φ₁ φ₂ : Prop} (h : φ₁ ↔ φ₂) : ⌜φ₁⌝ ⊣⊢ₛ ⌜φ₂⌝

theorem Std.Do.SPred.pure_elim_l {σs : List (Type u)} {Q R : SPred σs} {φ : Prop} (h : φ → Q ⊢ₛ R) : ⌜φ⌝ ∧ Q ⊢ₛ R

theorem Std.Do.SPred.pure_elim_r {σs : List (Type u)} {Q R : SPred σs} {φ : Prop} (h : φ → Q ⊢ₛ R) : Q ∧ ⌜φ⌝ ⊢ₛ R

theorem Std.Do.SPred.pure_true {σs : List (Type u)} {φ : Prop} (h : φ) : ⌜φ⌝ ⊣⊢ₛ ⌜True⌝

theorem Std.Do.SPred.pure_and {σs : List (Type u)} {φ₁ φ₂ : Prop} : ⌜φ₁⌝ ∧ ⌜φ₂⌝ ⊣⊢ₛ ⌜φ₁ ∧ φ₂⌝

theorem Std.Do.SPred.pure_or {σs : List (Type u)} {φ₁ φ₂ : Prop} : ⌜φ₁⌝ ∨ ⌜φ₂⌝ ⊣⊢ₛ ⌜φ₁ ∨ φ₂⌝

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

theorem Std.Do.SPred.pure_imp {σs : List (Type u)} {φ₁ φ₂ : Prop} : (⌜φ₁⌝ → ⌜φ₂⌝) ⊣⊢ₛ ⌜φ₁ → φ₂⌝

theorem Std.Do.SPred.pure_forall_2 {σs : List (Type u)} {α : Sort u_1} {φ : α → Prop} : ⌜∀ (x : α), φ x⌝ ⊢ₛ «forall» fun (x : α) => ⌜φ x⌝

theorem Std.Do.SPred.pure_forall {σs : List (Type u)} {α : Sort u_1} {φ : α → Prop} : («forall» fun (x : α) => ⌜φ x⌝) ⊣⊢ₛ ⌜∀ (x : α), φ x⌝

theorem Std.Do.SPred.pure_exists {σs : List (Type u)} {α : Sort u_1} {φ : α → Prop} : («exists» fun (x : α) => ⌜φ x⌝) ⊣⊢ₛ ⌜∃ (x : α), φ x⌝

@[simp]

theorem Std.Do.SPred.true_intro_simp {σs : List (Type u)} {Q : SPred σs} : Q ⊢ₛ ⌜True⌝ ↔ True

@[simp]

theorem ULift.down_dite {α : Type u_1} {φ : Prop} [Decidable φ] (t : φ → α) (e : ¬φ → α) : (if h : φ then { down := t h } else { down := e h }).down = if h : φ then t h else e h

@[simp]

theorem ULift.down_ite {α : Type u_1} {φ : Prop} [Decidable φ] (t e : α) : (if φ then { down := t } else { down := e }).down = if φ then t else e

Miscellaneous

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

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

Working with entailment

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

theorem Std.Do.SPred.entails_pure_elim_cons {σs : List (Type u)} {σ : Type u} [Inhabited σ] (P Q : Prop) : ⌜P⌝ ⊢ₛ ⌜Q⌝ ↔ ⌜P⌝ ⊢ₛ ⌜Q⌝

@[simp]

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

@[simp]

theorem Std.Do.SPred.entails_1 {σ : Type u_1} {P Q : SPred [σ]} : (P ⊢ₛ Q) = ∀ (s : σ), (P s).down → (Q s).down

@[simp]

theorem Std.Do.SPred.entails_2 {σ₁ σ₂ : Type u_1} {P Q : SPred [σ₁, σ₂]} : (P ⊢ₛ Q) = ∀ (s₁ : σ₁) (s₂ : σ₂), (P s₁ s₂).down → (Q s₁ s₂).down

@[simp]

theorem Std.Do.SPred.entails_3 {σ₁ σ₂ σ₃ : Type u_1} {P Q : SPred [σ₁, σ₂, σ₃]} : (P ⊢ₛ Q) = ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃), (P s₁ s₂ s₃).down → (Q s₁ s₂ s₃).down

@[simp]

theorem Std.Do.SPred.entails_4 {σ₁ σ₂ σ₃ σ₄ : Type u_1} {P Q : SPred [σ₁, σ₂, σ₃, σ₄]} : (P ⊢ₛ Q) = ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄), (P s₁ s₂ s₃ s₄).down → (Q s₁ s₂ s₃ s₄).down

@[simp]

theorem Std.Do.SPred.entails_5 {σ₁ σ₂ σ₃ σ₄ σ₅ : Type u_1} {P Q : SPred [σ₁, σ₂, σ₃, σ₄, σ₅]} : (P ⊢ₛ Q) = ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄) (s₅ : σ₅), (P s₁ s₂ s₃ s₄ s₅).down → (Q s₁ s₂ s₃ s₄ s₅).down

Tactic support

@[reducible, inline]

abbrev Std.Do.SPred.Tactic.tautological {σs : List (Type u)} (Q : SPred σs) : Prop

Tautology in SPred as a quotable definition.

Equations

• Std.Do.SPred.Tactic.tautological Q = (⊢ₛ Q)

class Std.Do.SPred.Tactic.PropAsSPredTautology (φ : Prop) {σs : outParam (List (Type u))} (P : outParam (SPred σs)) : Prop

• iff : φ ↔ ⊢ₛ P

instance Std.Do.SPred.Tactic.instPropAsSPredTautologyDown {φ : SPred []} : PropAsSPredTautology φ.down φ

instance Std.Do.SPred.Tactic.instPropAsSPredTautologyEntailsImp {σs : List (Type u)} {P Q : SPred σs} : PropAsSPredTautology (P ⊢ₛ Q) spred(P → Q)

instance Std.Do.SPred.Tactic.instPropAsSPredTautologyEntailsPureTrue {σs : List (Type u)} {P : SPred σs} : PropAsSPredTautology (⊢ₛ P) P

class Std.Do.SPred.Tactic.IsPure {σs : List (Type u)} (P : SPred σs) (φ : outParam Prop) : Prop

• to_pure : P ⊣⊢ₛ ⌜φ⌝

instance Std.Do.SPred.Tactic.instIsPurePure {φ : Prop} (σs : List (Type u_1)) : IsPure ⌜φ⌝ φ

instance Std.Do.SPred.Tactic.instIsPureImpPureForall {φ ψ : Prop} (σs : List (Type u_1)) : IsPure spred(⌜φ⌝ → ⌜ψ⌝) (φ → ψ)

instance Std.Do.SPred.Tactic.instIsPureAndPureAnd {φ ψ : Prop} (σs : List (Type u_1)) : IsPure spred(⌜φ⌝ ∧ ⌜ψ⌝) (φ ∧ ψ)

instance Std.Do.SPred.Tactic.instIsPureOrPureOr {φ ψ : Prop} (σs : List (Type u_1)) : IsPure spred(⌜φ⌝ ∨ ⌜ψ⌝) (φ ∨ ψ)

instance Std.Do.SPred.Tactic.instIsPureExistsPureExists {α : Sort u_1} (σs : List (Type u_2)) (P : α → Prop) : IsPure («exists» fun (x : α) => ⌜P x⌝) (∃ (x : α), P x)

instance Std.Do.SPred.Tactic.instIsPureForallPureForall {α : Sort u_1} (σs : List (Type u_2)) (P : α → Prop) : IsPure («forall» fun (x : α) => ⌜P x⌝) (∀ (x : α), P x)

instance Std.Do.SPred.Tactic.instIsPure {φ : Prop} {σ : Type u_1} {s : σ} (σs : List (Type u_1)) (P : SPred (σ :: σs)) [inst : IsPure P φ] : IsPure (P s) φ

instance Std.Do.SPred.Tactic.instIsPure_1 {φ : Prop} {σ : Type u_1} (σs : List (Type u_1)) (P : SPred σs) [inst : IsPure P φ] : IsPure (fun (x : σ) => P) φ

instance Std.Do.SPred.Tactic.instIsPurePure_1 (φ : Prop) : IsPure ⌜φ⌝ φ

instance Std.Do.SPred.Tactic.instIsPureDown (P : SPred []) : IsPure P P.down

class Std.Do.SPred.Tactic.IsAnd {σs : List (Type u)} (P : SPred σs) (Q₁ Q₂ : outParam (SPred σs)) : Prop

• to_and : P ⊣⊢ₛ Q₁ ∧ Q₂

instance Std.Do.SPred.Tactic.instIsAndAnd (σs : List (Type u_1)) (Q₁ Q₂ : SPred σs) : IsAnd spred(Q₁ ∧ Q₂) Q₁ Q₂

instance Std.Do.SPred.Tactic.instIsAndPureAnd {p q : Prop} (σs : List (Type u_1)) : IsAnd ⌜p ∧ q⌝ ⌜p⌝ ⌜q⌝

instance Std.Do.SPred.Tactic.instIsAnd {σ : Type u_1} (σs : List (Type u_1)) (P Q₁ Q₂ : σ → SPred σs) [base : ∀ (s : σ), IsAnd (P s) (Q₁ s) (Q₂ s)] : IsAnd P Q₁ Q₂

theorem Std.Do.SPred.Tactic.ProofMode.start_entails {σs : List (Type u)} {P : SPred σs} {φ : Prop} [PropAsSPredTautology φ P] : (⊢ₛ P) → φ

theorem Std.Do.SPred.Tactic.ProofMode.elim_entails {σs : List (Type u)} {P : SPred σs} {φ : Prop} [PropAsSPredTautology φ P] : φ → ⊢ₛ P

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

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

theorem Std.Do.SPred.Tactic.Cases.add_goal {σs : List (Type u_1)} {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (hgoal : P ⊢ₛ T) : Q ∧ H ⊢ₛ T

theorem Std.Do.SPred.Tactic.Cases.clear {σs : List (Type u_1)} {Q H T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) : Q ∧ H ⊢ₛ T

theorem Std.Do.SPred.Tactic.Cases.pure {σs : List (Type u_1)} {Q T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) : Q ⊢ₛ T

theorem Std.Do.SPred.Tactic.Cases.and_1 {σs : List (Type u_1)} {Q H₁' H₂' H₁₂' T : SPred σs} (hand : H₁' ∧ H₂' ⊣⊢ₛ H₁₂') (hgoal : Q ∧ H₁₂' ⊢ₛ T) : (Q ∧ H₁') ∧ H₂' ⊢ₛ T

theorem Std.Do.SPred.Tactic.Cases.and_2 {σs : List (Type u_1)} {Q H₁' H₂ T : SPred σs} (hgoal : (Q ∧ H₁') ∧ H₂ ⊢ₛ T) : (Q ∧ H₂) ∧ H₁' ⊢ₛ T

theorem Std.Do.SPred.Tactic.Cases.and_3 {σs : List (Type u_1)} {Q H₁ H₂ H T : SPred σs} (hand : H ⊣⊢ₛ H₁ ∧ H₂) (hgoal : (Q ∧ H₂) ∧ H₁ ⊢ₛ T) : Q ∧ H ⊢ₛ T

theorem Std.Do.SPred.Tactic.Cases.exists {σs : List (Type u)} {α : Sort u_1} {Q : SPred σs} {ψ : α → SPred σs} {T : SPred σs} (h : ∀ (a : α), Q ∧ ψ a ⊢ₛ T) : (Q ∧ SPred.exists fun (a : α) => ψ a) ⊢ₛ T

theorem Std.Do.SPred.Tactic.Clear.clear {σs : List (Type u)} {P P' A Q : SPred σs} (hfocus : P ⊣⊢ₛ P' ∧ A) (h : P' ⊢ₛ Q) : P ⊢ₛ Q

theorem Std.Do.SPred.Tactic.Exact.assumption {σs : List (Type u)} {P P' A : SPred σs} (h : P ⊣⊢ₛ P' ∧ A) : P ⊢ₛ A

theorem Std.Do.SPred.Tactic.Exact.from_tautology {σs : List (Type u)} {φ : Prop} {P T : SPred σs} [PropAsSPredTautology φ T] (h : φ) : P ⊢ₛ T

theorem Std.Do.SPred.Tactic.Focus.this {σs : List (Type u)} {P : SPred σs} : P ⊣⊢ₛ ⌜True⌝ ∧ P

theorem Std.Do.SPred.Tactic.Focus.left {σs : List (Type u)} {P P' Q C R : SPred σs} (h₁ : P ⊣⊢ₛ P' ∧ R) (h₂ : P' ∧ Q ⊣⊢ₛ C) : P ∧ Q ⊣⊢ₛ C ∧ R

theorem Std.Do.SPred.Tactic.Focus.right {σs : List (Type u)} {P Q Q' C R : SPred σs} (h₁ : Q ⊣⊢ₛ Q' ∧ R) (h₂ : P ∧ Q' ⊣⊢ₛ C) : P ∧ Q ⊣⊢ₛ C ∧ R

theorem Std.Do.SPred.Tactic.Focus.rewrite_hyps {σs : List (Type u_1)} {P Q R : SPred σs} (hrw : P ⊣⊢ₛ Q) (hgoal : Q ⊢ₛ R) : P ⊢ₛ R

theorem Std.Do.SPred.Tactic.Have.dup {σs : List (Type u)} {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (hgoal : P ∧ H ⊢ₛ T) : P ⊢ₛ T

theorem Std.Do.SPred.Tactic.Have.have {σs : List (Type u)} {P H PH T : SPred σs} (hand : P ∧ H ⊣⊢ₛ PH) (hhave : P ⊢ₛ H) (hgoal : PH ⊢ₛ T) : P ⊢ₛ T

theorem Std.Do.SPred.Tactic.Have.replace {σs : List (Type u)} {P H H' PH PH' T : SPred σs} (hfoc : PH ⊣⊢ₛ P ∧ H) (hand : P ∧ H' ⊣⊢ₛ PH') (hhave : PH ⊢ₛ H') (hgoal : PH' ⊢ₛ T) : PH ⊢ₛ T

theorem Std.Do.SPred.Tactic.Intro.intro {σs : List (Type u)} {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (h : P ⊢ₛ T) : Q ⊢ₛ H → T

theorem Std.Do.SPred.Tactic.Revert.and_pure_intro_r {σs : List (Type u)} {φ : Prop} {P P' Q : SPred σs} (h₁ : φ) (hand : P ∧ ⌜φ⌝ ⊣⊢ₛ P') (h₂ : P' ⊢ₛ Q) : P ⊢ₛ Q

theorem Std.Do.SPred.Tactic.Pure.thm {σs : List (Type u)} {P Q T : SPred σs} {φ : Prop} [IsPure Q φ] (h : φ → P ⊢ₛ T) : P ∧ Q ⊢ₛ T

theorem Std.Do.SPred.Tactic.Pure.intro {σs : List (Type u)} {P Q : SPred σs} {φ : Prop} [IsPure Q φ] (hp : φ) : P ⊢ₛ Q

A generalization of pure_intro exploiting IsPure.

theorem Std.Do.SPred.Tactic.Revert.revert {σs : List (Type u)} {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (h : Q ⊢ₛ H → T) : P ⊢ₛ T

theorem Std.Do.SPred.Tactic.Specialize.imp_stateful {σs : List (Type u)} {P P' Q R : SPred σs} (hrefocus : P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q) : P ∧ (Q → R) ⊢ₛ P ∧ R

theorem Std.Do.SPred.Tactic.Specialize.imp_pure {σs : List (Type u)} {φ : Prop} {P Q R : SPred σs} [PropAsSPredTautology φ Q] (h : φ) : P ∧ (Q → R) ⊢ₛ P ∧ R

theorem Std.Do.SPred.Tactic.Specialize.forall {α : Sort u_1} {σs : List (Type u_2)} {ψ : α → SPred σs} {P : SPred σs} (a : α) : (P ∧ SPred.forall fun (x : α) => ψ x) ⊢ₛ P ∧ ψ a

theorem Std.Do.SPred.Tactic.Specialize.pure_start {σs : List (Type u)} {φ : Prop} {H P T : SPred σs} [PropAsSPredTautology φ H] (hpure : φ) (hgoal : P ∧ H ⊢ₛ T) : P ⊢ₛ T

theorem Std.Do.SPred.Tactic.Specialize.pure_taut {σs : List (Type u_1)} {φ : Prop} {P : SPred σs} [IsPure P φ] (h : φ) : ⊢ₛ P

theorem Std.Do.SPred.Tactic.Specialize.focus {σs : List (Type u)} {P P' Q R : SPred σs} (hfocus : P ⊣⊢ₛ P' ∧ Q) (hnew : P' ∧ Q ⊢ₛ R) : P ⊢ₛ R

class Std.Do.SPred.Tactic.SimpAnd {σs : List (Type u)} (P Q : SPred σs) (PQ : outParam (SPred σs)) : Prop

• simp_and : P ∧ Q ⊣⊢ₛ PQ

instance Std.Do.SPred.Tactic.instSimpAndAnd (σs : List (Type u_1)) (P Q : SPred σs) : SimpAnd P Q spred(P ∧ Q)

instance Std.Do.SPred.Tactic.instSimpAndPureTrue (σs : List (Type u_1)) (P : SPred σs) : SimpAnd P ⌜True⌝ P

instance Std.Do.SPred.Tactic.instSimpAndPureTrue_1 (σs : List (Type u_1)) (P : SPred σs) : SimpAnd ⌜True⌝ P P

class Std.Do.SPred.Tactic.HasFrame {σs : List (Type u)} (P : SPred σs) (P' : outParam (SPred σs)) (φ : outParam Prop) : Prop

• reassoc : P ⊣⊢ₛ P' ∧ ⌜φ⌝

instance Std.Do.SPred.Tactic.instHasFrameAndOfSimpAnd {φ : Prop} (σs : List (Type u_1)) (P P' Q QP : SPred σs) [HasFrame P Q φ] [SimpAnd Q P' QP] : HasFrame spred(P ∧ P') QP φ

instance Std.Do.SPred.Tactic.instHasFrameAndOfSimpAnd_1 {φ : Prop} (σs : List (Type u_1)) (P P' Q' PQ : SPred σs) [HasFrame P' Q' φ] [SimpAnd P Q' PQ] : HasFrame spred(P ∧ P') PQ φ

instance Std.Do.SPred.Tactic.instHasFramePureAndOfAnd {φ : Prop} (σs : List (Type u_1)) (P P' : Prop) (Q : SPred σs) [HasFrame spred(⌜P⌝ ∧ ⌜P'⌝) Q φ] : HasFrame ⌜P ∧ P'⌝ Q φ

instance Std.Do.SPred.Tactic.instHasFrameCurryULiftPropUpAndOfAnd {φ : Prop} (σs : List (Type u_1)) (P P' : SVal.StateTuple σs → Prop) (Q : SPred σs) [HasFrame spred((SVal.curry fun (t : SVal.StateTuple σs) => { down := P t }) ∧ SVal.curry fun (t : SVal.StateTuple σs) => { down := P' t }) Q φ] : HasFrame (SVal.curry fun (t : SVal.StateTuple σs) => { down := P t ∧ P' t }) Q φ

instance Std.Do.SPred.Tactic.instHasFrameAndPure {φ : Prop} (σs : List (Type u_1)) (P : SPred σs) : HasFrame spred(⌜φ⌝ ∧ P) P φ

instance Std.Do.SPred.Tactic.instHasFrameAndPure_1 {φ : Prop} (σs : List (Type u_1)) (P : SPred σs) : HasFrame spred(P ∧ ⌜φ⌝) P φ

instance Std.Do.SPred.Tactic.instHasFrameAndAndOfSimpAnd {φ ψ : Prop} (σs : List (Type u_1)) (P P' Q Q' QQ : SPred σs) [HasFrame P Q φ] [HasFrame P' Q' ψ] [SimpAnd Q Q' QQ] : HasFrame spred(P ∧ P') QQ (φ ∧ ψ)

instance Std.Do.SPred.Tactic.instHasFrameAndPureAnd {φ ψ : Prop} (σs : List (Type u_1)) (P Q : SPred σs) [HasFrame P Q ψ] : HasFrame spred(⌜φ⌝ ∧ P) Q (φ ∧ ψ)

instance Std.Do.SPred.Tactic.instHasFrameAndPureAnd_1 {φ ψ : Prop} (σs : List (Type u_1)) (P Q : SPred σs) [HasFrame P Q ψ] : HasFrame spred(P ∧ ⌜φ⌝) Q (ψ ∧ φ)

instance Std.Do.SPred.Tactic.instHasFramePureTrue {φ : Prop} (σs : List (Type u_1)) : HasFrame ⌜φ⌝ ⌜True⌝ φ

instance Std.Do.SPred.Tactic.instHasFramePureTrueDown {P : SPred []} : HasFrame P ⌜True⌝ P.down

theorem Std.Do.SPred.Tactic.Frame.frame {σs : List (Type u)} {P Q T : SPred σs} {φ : Prop} [HasFrame P Q φ] (h : φ → Q ⊢ₛ T) : P ⊢ₛ T