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

A mapping from propositions to SPred tautologies that are known to be logically equivalent. This is used to rewrite proof goals into a form that is suitable for use with mvcgen.

• iff : φ ↔ ⊢ₛ P

  A proof that φ and P are logically equivalent.

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

A mapping from SPred to pure propositions that are known to be equivalent.

• to_pure : P ⊣⊢ₛ ⌜φ⌝

  A proof that P and φ are equivalent.

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

A decomposition of a stateful predicate into the conjunction of two other stateful predicates.

Decomposing assertions in postconditions into conjunctions of simpler predicates increases the chance that automation will be able to prove the entailment of the postcondition and the next precondition.

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

  A proof the the decomposition is logically equivalent to the original predicate.

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 φ] (hφ : φ) : 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

Expresses that the conjunction of P and Q is equivalent to spred(P ∧ Q), but potentially simpler.

• simp_and : P ∧ Q ⊣⊢ₛ PQ

  A proof that spred(P ∧ Q) is logically equivalent to 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

Provides a decomposition of a stateful predicate (P) into stateful and pure components (P' and φ, respectively).

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

  A proof that the original stateful predicate is equivalent to the decomposed form.

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