# Derived laws of `SPred` #

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

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

# Connectives #

source
theorem Std.Do.SPred.and_intro_l {σs : List (Type u)} {P Q : SPred σs} (h : P ⊢ₛ Q) :
P ⊢ₛ Q ∧ P
source
theorem Std.Do.SPred.and_intro_r {σs : List (Type u)} {P Q : SPred σs} (h : P ⊢ₛ Q) :
P ⊢ₛ P ∧ Q
source
theorem Std.Do.SPred.and_elim_l' {σs : List (Type u)} {P Q R : SPred σs} (h : P ⊢ₛ R) :
P ∧ Q ⊢ₛ R
source
theorem Std.Do.SPred.and_elim_r' {σs : List (Type u)} {P Q R : SPred σs} (h : Q ⊢ₛ R) :
P ∧ Q ⊢ₛ R
source
theorem Std.Do.SPred.or_intro_l' {σs : List (Type u)} {P Q R : SPred σs} (h : P ⊢ₛ Q) :
P ⊢ₛ Q ∨ R
source
theorem Std.Do.SPred.or_intro_r' {σs : List (Type u)} {P Q R : SPred σs} (h : P ⊢ₛ R) :
P ⊢ₛ Q ∨ R
source
theorem Std.Do.SPred.and_symm {σs : List (Type u)} {P Q : SPred σs} :
P ∧ Q ⊢ₛ Q ∧ P
source
theorem Std.Do.SPred.or_symm {σs : List (Type u)} {P Q : SPred σs} :
P ∨ Q ⊢ₛ Q ∨ P
source
theorem Std.Do.SPred.imp_intro' {σs : List (Type u)} {P Q R : SPred σs} (h : Q ∧ P ⊢ₛ R) :
P ⊢ₛ Q → R
source
theorem Std.Do.SPred.entails.trans' {σs : List (Type u)} {P Q R : SPred σs} (h₁ : P ⊢ₛ Q) (h₂ : P ∧ Q ⊢ₛ R) :
P ⊢ₛ R
source
theorem Std.Do.SPred.mp {σs : List (Type u)} {P Q R : SPred σs} (h₁ : P ⊢ₛ Q → R) (h₂ : P ⊢ₛ Q) :
P ⊢ₛ R
source
theorem Std.Do.SPred.imp_elim' {σs : List (Type u)} {P Q R : SPred σs} (h : Q ⊢ₛ P → R) :
P ∧ Q ⊢ₛ R
source
theorem Std.Do.SPred.imp_elim_l {σs : List (Type u)} {P Q : SPred σs} :
(P → Q) ∧ P ⊢ₛ Q
source
theorem Std.Do.SPred.imp_elim_r {σs : List (Type u)} {P Q : SPred σs} :
P ∧ (P → Q) ⊢ₛ Q
source
theorem Std.Do.SPred.false_elim {σs : List (Type u)} {P : SPred σs} :
⌜False⌝ ⊢ₛ P
source
theorem Std.Do.SPred.true_intro {σs : List (Type u)} {P : SPred σs} :
P ⊢ₛ ⌜True⌝
source
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
source
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
source
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
source
theorem Std.Do.SPred.exfalso {σs : List (Type u)} {P Q : SPred σs} (h : P ⊢ₛ ⌜False⌝) :
P ⊢ₛ Q

# Monotonicity and congruence #

source
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'
source
theorem Std.Do.SPred.and_mono_l {σs : List (Type u)} {P P' Q : SPred σs} (h : P ⊢ₛ P') :
P ∧ Q ⊢ₛ P' ∧ Q
source
theorem Std.Do.SPred.and_mono_r {σs : List (Type u)} {P Q Q' : SPred σs} (h : Q ⊢ₛ Q') :
P ∧ Q ⊢ₛ P ∧ Q'
source
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'
source
theorem Std.Do.SPred.and_congr_l {σs : List (Type u)} {P P' Q : SPred σs} (hp : P ⊣⊢ₛ P') :
P ∧ Q ⊣⊢ₛ P' ∧ Q
source
theorem Std.Do.SPred.and_congr_r {σs : List (Type u)} {P Q Q' : SPred σs} (hq : Q ⊣⊢ₛ Q') :
P ∧ Q ⊣⊢ₛ P ∧ Q'
source
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'
source
theorem Std.Do.SPred.or_mono_l {σs : List (Type u)} {P P' Q : SPred σs} (h : P ⊢ₛ P') :
P ∨ Q ⊢ₛ P' ∨ Q
source
theorem Std.Do.SPred.or_mono_r {σs : List (Type u)} {P Q Q' : SPred σs} (h : Q ⊢ₛ Q') :
P ∨ Q ⊢ₛ P ∨ Q'
source
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'
source
theorem Std.Do.SPred.or_congr_l {σs : List (Type u)} {P P' Q : SPred σs} (hp : P ⊣⊢ₛ P') :
P ∨ Q ⊣⊢ₛ P' ∨ Q
source
theorem Std.Do.SPred.or_congr_r {σs : List (Type u)} {P Q Q' : SPred σs} (hq : Q ⊣⊢ₛ Q') :
P ∨ Q ⊣⊢ₛ P ∨ Q'
source
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'
source
theorem Std.Do.SPred.imp_mono_l {σs : List (Type u)} {P P' Q : SPred σs} (h : P' ⊢ₛ P) :
(P → Q) ⊢ₛ P' → Q
source
theorem Std.Do.SPred.imp_mono_r {σs : List (Type u)} {P Q Q' : SPred σs} (h : Q ⊢ₛ Q') :
(P → Q) ⊢ₛ P → Q'
source
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'
source
theorem Std.Do.SPred.imp_congr_l {σs : List (Type u)} {P P' Q : SPred σs} (h : P ⊣⊢ₛ P') :
(P → Q) ⊣⊢ₛ P' → Q
source
theorem Std.Do.SPred.imp_congr_r {σs : List (Type u)} {P Q Q' : SPred σs} (h : Q ⊣⊢ₛ Q') :
(P → Q) ⊣⊢ₛ P → Q'
source
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
source
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
source
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
source
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 #

source
theorem Std.Do.SPred.and_self {σs : List (Type u)} {P : SPred σs} :
P ∧ P ⊣⊢ₛ P
source
theorem Std.Do.SPred.or_self {σs : List (Type u)} {P : SPred σs} :
P ∨ P ⊣⊢ₛ P
source
theorem Std.Do.SPred.and_comm {σs : List (Type u)} {P Q : SPred σs} :
P ∧ Q ⊣⊢ₛ Q ∧ P
source
theorem Std.Do.SPred.or_comm {σs : List (Type u)} {P Q : SPred σs} :
P ∨ Q ⊣⊢ₛ Q ∨ P
source
theorem Std.Do.SPred.and_assoc {σs : List (Type u)} {P Q R : SPred σs} :
(P ∧ Q) ∧ R ⊣⊢ₛ P ∧ Q ∧ R
source
theorem Std.Do.SPred.or_assoc {σs : List (Type u)} {P Q R : SPred σs} :
(P ∨ Q) ∨ R ⊣⊢ₛ P ∨ Q ∨ R
source
theorem Std.Do.SPred.and_eq_right {σs : List (Type u)} {P Q : SPred σs} :
P ⊢ₛ Q ↔ P ⊣⊢ₛ Q ∧ P
source
theorem Std.Do.SPred.and_eq_left {σs : List (Type u)} {P Q : SPred σs} :
P ⊢ₛ Q ↔ P ⊣⊢ₛ P ∧ Q
source
theorem Std.Do.SPred.or_eq_left {σs : List (Type u)} {P Q : SPred σs} :
P ⊢ₛ Q ↔ Q ⊣⊢ₛ Q ∨ P
source
theorem Std.Do.SPred.or_eq_right {σs : List (Type u)} {P Q : SPred σs} :
P ⊢ₛ Q ↔ Q ⊣⊢ₛ P ∨ Q
source
theorem Std.Do.SPred.and_or_left {σs : List (Type u)} {P Q R : SPred σs} :
P ∧ (Q ∨ R) ⊣⊢ₛ P ∧ Q ∨ P ∧ R
source
theorem Std.Do.SPred.or_and_left {σs : List (Type u)} {P Q R : SPred σs} :
P ∨ Q ∧ R ⊣⊢ₛ (P ∨ Q) ∧ (P ∨ R)
source
theorem Std.Do.SPred.or_and_right {σs : List (Type u)} {P Q R : SPred σs} :
(P ∨ Q) ∧ R ⊣⊢ₛ P ∧ R ∨ Q ∧ R
source
theorem Std.Do.SPred.and_or_right {σs : List (Type u)} {P Q R : SPred σs} :
P ∧ Q ∨ R ⊣⊢ₛ (P ∨ R) ∧ (Q ∨ R)
source
theorem Std.Do.SPred.true_and {σs : List (Type u)} {P : SPred σs} :
⌜True⌝ ∧ P ⊣⊢ₛ P
source
theorem Std.Do.SPred.and_true {σs : List (Type u)} {P : SPred σs} :
P ∧ ⌜True⌝ ⊣⊢ₛ P
source
theorem Std.Do.SPred.false_and {σs : List (Type u)} {P : SPred σs} :
⌜False⌝ ∧ P ⊣⊢ₛ ⌜False⌝
source
theorem Std.Do.SPred.and_false {σs : List (Type u)} {P : SPred σs} :
P ∧ ⌜False⌝ ⊣⊢ₛ ⌜False⌝
source
theorem Std.Do.SPred.true_or {σs : List (Type u)} {P : SPred σs} :
⌜True⌝ ∨ P ⊣⊢ₛ ⌜True⌝
source
theorem Std.Do.SPred.or_true {σs : List (Type u)} {P : SPred σs} :
P ∨ ⌜True⌝ ⊣⊢ₛ ⌜True⌝
source
theorem Std.Do.SPred.false_or {σs : List (Type u)} {P : SPred σs} :
⌜False⌝ ∨ P ⊣⊢ₛ P
source
theorem Std.Do.SPred.or_false {σs : List (Type u)} {P : SPred σs} :
P ∨ ⌜False⌝ ⊣⊢ₛ P
source
theorem Std.Do.SPred.true_imp {σs : List (Type u)} {P : SPred σs} :
(⌜True⌝ → P) ⊣⊢ₛ P
source
theorem Std.Do.SPred.imp_self {σs : List (Type u)} {P Q : SPred σs} :
Q ⊢ₛ P → P
source
theorem Std.Do.SPred.imp_self_simp {σs : List (Type u)} {P Q : SPred σs} :
Q ⊢ₛ P → P ↔ True
source
theorem Std.Do.SPred.imp_trans {σs : List (Type u)} {P Q R : SPred σs} :
(P → Q) ∧ (Q → R) ⊢ₛ P → R
source
theorem Std.Do.SPred.false_imp {σs : List (Type u)} {P : SPred σs} :
(⌜False⌝ → P) ⊣⊢ₛ ⌜True⌝
source
theorem Std.Do.SPred.and_imp {σs : List (Type u)} {P' Q' : SPred σs} :
P' ∧ (P' → Q') ⊢ₛ P' ∧ Q'
source
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 #

source
theorem Std.Do.SPred.pure_elim {σs : List (Type u)} {Q R : SPred σs} {φ : Prop} (h1 : Q ⊢ₛ ⌜φ⌝) (h2 : φ → Q ⊢ₛ R) :
Q ⊢ₛ R
source
theorem Std.Do.SPred.pure_mono {σs : List (Type u)} {φ₁ φ₂ : Prop} (h : φ₁ → φ₂) :
⌜φ₁⌝ ⊢ₛ ⌜φ₂⌝
source
theorem Std.Do.SPred.pure_congr {σs : List (Type u)} {φ₁ φ₂ : Prop} (h : φ₁ ↔ φ₂) :
⌜φ₁⌝ ⊣⊢ₛ ⌜φ₂⌝
source
theorem Std.Do.SPred.pure_elim_l {σs : List (Type u)} {Q R : SPred σs} {φ : Prop} (h : φ → Q ⊢ₛ R) :
⌜φ⌝ ∧ Q ⊢ₛ R
source
theorem Std.Do.SPred.pure_elim_r {σs : List (Type u)} {Q R : SPred σs} {φ : Prop} (h : φ → Q ⊢ₛ R) :
Q ∧ ⌜φ⌝ ⊢ₛ R
source
theorem Std.Do.SPred.pure_true {σs : List (Type u)} {φ : Prop} (h : φ) :
⌜φ⌝ ⊣⊢ₛ ⌜True⌝
source
theorem Std.Do.SPred.pure_and {σs : List (Type u)} {φ₁ φ₂ : Prop} :
⌜φ₁⌝ ∧ ⌜φ₂⌝ ⊣⊢ₛ ⌜φ₁ ∧ φ₂⌝
source
theorem Std.Do.SPred.pure_or {σs : List (Type u)} {φ₁ φ₂ : Prop} :
⌜φ₁⌝ ∨ ⌜φ₂⌝ ⊣⊢ₛ ⌜φ₁ ∨ φ₂⌝
source
theorem Std.Do.SPred.pure_imp_2 {σs : List (Type u)} {φ₁ φ₂ : Prop} :
⌜φ₁ → φ₂⌝ ⊢ₛ ⌜φ₁⌝ → ⌜φ₂⌝
source
theorem Std.Do.SPred.pure_imp {σs : List (Type u)} {φ₁ φ₂ : Prop} :
(⌜φ₁⌝ → ⌜φ₂⌝) ⊣⊢ₛ ⌜φ₁ → φ₂⌝
source
theorem Std.Do.SPred.pure_forall_2 {σs : List (Type u)} {α : Sort u_1} {φ : α → Prop} :
⌜∀ (x : α), φ x⌝ ⊢ₛ «forall» fun (x : α) => ⌜φ x⌝
source
theorem Std.Do.SPred.pure_forall {σs : List (Type u)} {α : Sort u_1} {φ : α → Prop} :
(«forall» fun (x : α) => ⌜φ x⌝) ⊣⊢ₛ ⌜∀ (x : α), φ x⌝
source
theorem Std.Do.SPred.pure_exists {σs : List (Type u)} {α : Sort u_1} {φ : α → Prop} :
(«exists» fun (x : α) => ⌜φ x⌝) ⊣⊢ₛ ⌜∃ (x : α), φ x⌝
source
@[simp]
theorem Std.Do.SPred.true_intro_simp {σs : List (Type u)} {Q : SPred σs} :
Q ⊢ₛ ⌜True⌝ ↔ True
source
@[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
source
@[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 #

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

source
theorem Std.Do.SPred.entails_pure_intro {σs : List (Type u)} (P Q : Prop) (h : P → Q) :
⌜P⌝ ⊢ₛ ⌜Q⌝
source
theorem Std.Do.SPred.entails_pure_elim_cons {σs : List (Type u)} {σ : Type u} [Inhabited σ] (P Q : Prop) :
⌜P⌝ ⊢ₛ ⌜Q⌝ ↔ ⌜P⌝ ⊢ₛ ⌜Q⌝
source
@[simp]
theorem Std.Do.SPred.entails_true_intro {σs : List (Type u)} (P Q : SPred σs) :
(⊢ₛ P → Q) = (P ⊢ₛ Q)
source
@[simp]
theorem Std.Do.SPred.entails_1 {σ : Type u_1} {P Q : SPred [σ]} :
(P ⊢ₛ Q) = ∀ (s : σ), (P s).down → (Q s).down
source
@[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
source
@[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
source
@[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
source
@[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 #

source
@[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)

Instances For

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

- iff : φ ↔ ⊢ₛ P

Instances

source
instance Std.Do.SPred.Tactic.instPropAsSPredTautologyDown {φ : SPred []} :
PropAsSPredTautology φ.down φ
source
instance Std.Do.SPred.Tactic.instPropAsSPredTautologyEntailsImp {σs : List (Type u)} {P Q : SPred σs} :
PropAsSPredTautology (P ⊢ₛ Q) spred(P → Q)
source
instance Std.Do.SPred.Tactic.instPropAsSPredTautologyEntailsPureTrue {σs : List (Type u)} {P : SPred σs} :
PropAsSPredTautology (⊢ₛ P) P
source
class Std.Do.SPred.Tactic.IsPure {σs : List (Type u)} (P : SPred σs) (φ : outParam Prop) :
Prop

- to_pure : P ⊣⊢ₛ ⌜φ⌝

Instances

source
instance Std.Do.SPred.Tactic.instIsPurePure {φ : Prop} (σs : List (Type u_1)) :
IsPure ⌜φ⌝ φ
source
instance Std.Do.SPred.Tactic.instIsPureImpPureForall {φ ψ : Prop} (σs : List (Type u_1)) :
IsPure spred(⌜φ⌝ → ⌜ψ⌝) (φ → ψ)
source
instance Std.Do.SPred.Tactic.instIsPureAndPureAnd {φ ψ : Prop} (σs : List (Type u_1)) :
IsPure spred(⌜φ⌝ ∧ ⌜ψ⌝) (φ ∧ ψ)
source
instance Std.Do.SPred.Tactic.instIsPureOrPureOr {φ ψ : Prop} (σs : List (Type u_1)) :
IsPure spred(⌜φ⌝ ∨ ⌜ψ⌝) (φ ∨ ψ)
source
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)
source
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)
source
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) φ
source
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) φ
source
instance Std.Do.SPred.Tactic.instIsPurePure_1 (φ : Prop) :
IsPure ⌜φ⌝ φ
source
instance Std.Do.SPred.Tactic.instIsPureDown (P : SPred []) :
IsPure P P.down
source
class Std.Do.SPred.Tactic.IsAnd {σs : List (Type u)} (P : SPred σs) (Q₁ Q₂ : outParam (SPred σs)) :
Prop

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

Instances

source
instance Std.Do.SPred.Tactic.instIsAndAnd (σs : List (Type u_1)) (Q₁ Q₂ : SPred σs) :
IsAnd spred(Q₁ ∧ Q₂) Q₁ Q₂
source
instance Std.Do.SPred.Tactic.instIsAndPureAnd {p q : Prop} (σs : List (Type u_1)) :
IsAnd ⌜p ∧ q⌝ ⌜p⌝ ⌜q⌝
source
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₂
source
theorem Std.Do.SPred.Tactic.ProofMode.start_entails {σs : List (Type u)} {P : SPred σs} {φ : Prop} [PropAsSPredTautology φ P] :
(⊢ₛ P) → φ
source
theorem Std.Do.SPred.Tactic.ProofMode.elim_entails {σs : List (Type u)} {P : SPred σs} {φ : Prop} [PropAsSPredTautology φ P] :
φ → ⊢ₛ P
source
theorem Std.Do.SPred.Tactic.Assumption.left {σs : List (Type u)} {P Q R : SPred σs} (h : P ⊢ₛ R) :
P ∧ Q ⊢ₛ R
source
theorem Std.Do.SPred.Tactic.Assumption.right {σs : List (Type u)} {P Q R : SPred σs} (h : Q ⊢ₛ R) :
P ∧ Q ⊢ₛ R
source
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
source
theorem Std.Do.SPred.Tactic.Cases.clear {σs : List (Type u_1)} {Q H T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) :
Q ∧ H ⊢ₛ T
source
theorem Std.Do.SPred.Tactic.Cases.pure {σs : List (Type u_1)} {Q T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) :
Q ⊢ₛ T
source
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
source
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
source
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
source
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
source
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
source
theorem Std.Do.SPred.Tactic.Exact.assumption {σs : List (Type u)} {P P' A : SPred σs} (h : P ⊣⊢ₛ P' ∧ A) :
P ⊢ₛ A
source
theorem Std.Do.SPred.Tactic.Exact.from_tautology {σs : List (Type u)} {φ : Prop} {P T : SPred σs} [PropAsSPredTautology φ T] (h : φ) :
P ⊢ₛ T
source
theorem Std.Do.SPred.Tactic.Focus.this {σs : List (Type u)} {P : SPred σs} :
P ⊣⊢ₛ ⌜True⌝ ∧ P
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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`.

source
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
source
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
source
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
source
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
source
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
source
theorem Std.Do.SPred.Tactic.Specialize.pure_taut {σs : List (Type u_1)} {φ : Prop} {P : SPred σs} [IsPure P φ] (h : φ) :
⊢ₛ P
source
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
source
class Std.Do.SPred.Tactic.SimpAnd {σs : List (Type u)} (P Q : SPred σs) (PQ : outParam (SPred σs)) :
Prop

- simp_and : P ∧ Q ⊣⊢ₛ PQ

Instances

source
instance Std.Do.SPred.Tactic.instSimpAndAnd (σs : List (Type u_1)) (P Q : SPred σs) :
SimpAnd P Q spred(P ∧ Q)
source
instance Std.Do.SPred.Tactic.instSimpAndPureTrue (σs : List (Type u_1)) (P : SPred σs) :
SimpAnd P ⌜True⌝ P
source
instance Std.Do.SPred.Tactic.instSimpAndPureTrue_1 (σs : List (Type u_1)) (P : SPred σs) :
SimpAnd ⌜True⌝ P P
source
class Std.Do.SPred.Tactic.HasFrame {σs : List (Type u)} (P : SPred σs) (P' : outParam (SPred σs)) (φ : outParam Prop) :
Prop

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

Instances

source
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 φ
source
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 φ
source
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 φ
source
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 φ
source
instance Std.Do.SPred.Tactic.instHasFrameAndPure {φ : Prop} (σs : List (Type u_1)) (P : SPred σs) :
HasFrame spred(⌜φ⌝ ∧ P) P φ
source
instance Std.Do.SPred.Tactic.instHasFrameAndPure_1 {φ : Prop} (σs : List (Type u_1)) (P : SPred σs) :
HasFrame spred(P ∧ ⌜φ⌝) P φ
source
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 (φ ∧ ψ)
source
instance Std.Do.SPred.Tactic.instHasFrameAndPureAnd {φ ψ : Prop} (σs : List (Type u_1)) (P Q : SPred σs) [HasFrame P Q ψ] :
HasFrame spred(⌜φ⌝ ∧ P) Q (φ ∧ ψ)
source
instance Std.Do.SPred.Tactic.instHasFrameAndPureAnd_1 {φ ψ : Prop} (σs : List (Type u_1)) (P Q : SPred σs) [HasFrame P Q ψ] :
HasFrame spred(P ∧ ⌜φ⌝) Q (ψ ∧ φ)
source
instance Std.Do.SPred.Tactic.instHasFramePureTrue {φ : Prop} (σs : List (Type u_1)) :
HasFrame ⌜φ⌝ ⌜True⌝ φ
source
instance Std.Do.SPred.Tactic.instHasFramePureTrueDown {P : SPred []} :
HasFrame P ⌜True⌝ P.down
source
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