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

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

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

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

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

Connectives

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Std.Do.SPred.exists_intro' {α : Sort u_1} {σs : List Type} {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} {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} {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} {P Q : SPred σs} (h : P ⊢ₛ ⌜False⌝) : P ⊢ₛ Q

Monotonicity and congruence

theorem Std.Do.SPred.and_mono {σs : List Type} {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} {P P' Q : SPred σs} (h : P ⊢ₛ P') : P ∧ Q ⊢ₛ P' ∧ Q

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

theorem Std.Do.SPred.and_congr {σs : List Type} {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} {P P' Q : SPred σs} (hp : P ⊣⊢ₛ P') : P ∧ Q ⊣⊢ₛ P' ∧ Q

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

theorem Std.Do.SPred.or_mono {σs : List Type} {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} {P P' Q : SPred σs} (h : P ⊢ₛ P') : P ∨ Q ⊢ₛ P' ∨ Q

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

theorem Std.Do.SPred.or_congr {σs : List Type} {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} {P P' Q : SPred σs} (hp : P ⊣⊢ₛ P') : P ∨ Q ⊣⊢ₛ P' ∨ Q

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

theorem Std.Do.SPred.imp_mono {σs : List Type} {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} {P P' Q : SPred σs} (h : P' ⊢ₛ P) : (P → Q) ⊢ₛ P' → Q

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

theorem Std.Do.SPred.imp_congr {σs : List Type} {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} {P P' Q : SPred σs} (h : P ⊣⊢ₛ P') : (P → Q) ⊣⊢ₛ P' → Q

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

theorem Std.Do.SPred.forall_mono {σs : List Type} {α : 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} {α : 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} {α : 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} {α : Sort u_1} {Φ Ψ : α → SPred σs} (h : ∀ (a : α), Φ a ⊣⊢ₛ Ψ a) : («exists» fun (a : α) => Φ a) ⊣⊢ₛ «exists» fun (a : α) => Ψ a

theorem Std.Do.SPred.and_imp {σs✝ : List Type} {P₁ P₂ Q₁ Q₂ : SPred σs✝} (hp : P₁ ⊢ₛ P₂) (hq : Q₁ ⊢ₛ Q₂) : P₁ ∧ Q₁ ⊢ₛ P₂ ∧ Q₂

theorem Std.Do.SPred.or_imp_left {σs : List Type} {Q P₁ P₂ : SPred σs} (hleft : P₁ ⊢ₛ P₂) : P₁ ∨ Q ⊢ₛ P₂ ∨ Q

theorem Std.Do.SPred.or_imp_right {σs : List Type} {P Q₁ Q₂ : SPred σs} (hright : Q₁ ⊢ₛ Q₂) : P ∨ Q₁ ⊢ₛ P ∨ Q₂

Boolean algebra

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Pure

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

theorem Std.Do.SPred.true_intro_simp_nil {Q : SPred []} : Q ⊢ₛ True ↔ True

Miscellaneous

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

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

Working with entailment

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

@[simp]

theorem Std.Do.SPred.entails_elim_nil (P Q : SPred []) : P ⊢ₛ Q ↔ P → Q

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

@[simp]

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

@[simp]

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

Tactic support

@[reducible, inline]

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

Tautology in SPred as a quotable definition.

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

• iff : φ ↔ ⊢ₛ P

instance Std.Do.SPred.Tactic.instPropAsSPredTautology {φ : Prop} : PropAsSPredTautology φ φ

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

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

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

• to_pure : P ⊣⊢ₛ ⌜φ⌝

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

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

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

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

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

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

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

instance Std.Do.SPred.Tactic.instIsPure_1 (P : Prop) : IsPure P P

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

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

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

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

instance Std.Do.SPred.Tactic.instIsAnd {σ : Type} (σs : List Type) (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} {P : SPred σs} {φ : Prop} [PropAsSPredTautology φ P] : (⊢ₛ P) → φ

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

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

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

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

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

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

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

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

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

theorem Std.Do.SPred.Tactic.SCases.exists {α : Sort u_1} {σs : List Type} {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} {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} {P P' A : SPred σs} (h : P ⊣⊢ₛ P' ∧ A) : P ⊢ₛ A

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

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

theorem Std.Do.SPred.Tactic.Focus.left {σs : List Type} {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} {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} {P Q R : SPred σs} (hrw : P ⊣⊢ₛ Q) (hgoal : Q ⊢ₛ R) : P ⊢ₛ R

theorem Std.Do.SPred.Tactic.Have.dup {σs : List Type} {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} {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} {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} {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (h : P ⊢ₛ T) : Q ⊢ₛ H → T

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

theorem Std.Do.SPred.Tactic.Pure.intro {σs : List Type} {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} {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} {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} {φ : Prop} {P Q R : SPred σs} [PropAsSPredTautology φ Q] (h : φ) : P ∧ (Q → R) ⊢ₛ P ∧ R

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

theorem Std.Do.SPred.Tactic.Specialize.pure_start {σs : List Type} {φ : 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} {φ : Prop} {P : SPred σs} [IsPure P φ] (h : φ) : ⊢ₛ P

theorem Std.Do.SPred.Tactic.Specialize.focus {σs : List Type} {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} (P Q : SPred σs) (PQ : outParam (SPred σs)) : Prop

• simp_and : P ∧ Q ⊣⊢ₛ PQ

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

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

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

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

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

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

instance Std.Do.SPred.Tactic.instHasFrameAndOfSimpAnd {φ : Prop} (σs : List Type) (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) (P P' Q' PQ : SPred σs) [HasFrame P' Q' φ] [SimpAnd P Q' PQ] : HasFrame spred(P ∧ P') PQ φ

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

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

instance Std.Do.SPred.Tactic.instHasFrameAndAndOfSimpAnd {φ ψ : Prop} (σs : List Type) (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.instHasFrameAndCurryAnd {φ ψ : Prop} (σs : List Type) (P Q : SPred σs) [HasFrame P Q ψ] : HasFrame spred(⌜φ⌝ ∧ P) Q (φ ∧ ψ)

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

instance Std.Do.SPred.Tactic.instHasFrameCurryTrue_1 {P : Prop} : HasFrame P ⌜True⌝ P

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