feat: add SPred and PostCond entailment lemmas (#13582)

This PR adds several entailment-related lemmas to `Std.Do.SPred` and
`Std.Do.PostCond`, intended for goal-decomposition during program
verification proof automation.

- `SPred.down_pure_nil` and `SPred.apply_pure_cons` (existing `rfl`
lemmas) become `@[simp, grind =]`. Drops the now-redundant `pure_cons`
argument from `simp` in `conjunction_apply`.
- New `SPred.entails_nil_intro` and `SPred.entails_nil_pure_intro`:
introduction forms for `entails` at `SPred []`, mirroring the existing
`entails_cons_intro`.
- New `SPred.down_pure_intro`: derive `(pure φ).down` from `φ`.
- New `SPred.apply_pure_cons_entails_l`/`_r`: peel a state argument from
`pure (σ::σs) φ s` on either side of `⊢ₛ`.
- New `Std.Do.ExceptConds.entails.pure`: closes any `⊢ₑ` goal at
`PostShape.pure`, where `ExceptConds.entails` reduces to `True`.

src/Std/Do/PostCond.lean

@@ -177,6 +177,8 @@ theorem ExceptConds.entails.refl {ps : PostShape} (x : ExceptConds ps) : x ⊢
 
 theorem ExceptConds.entails.rfl {ps : PostShape} {x : ExceptConds ps} : x ⊢ₑ x := refl x
 
+theorem ExceptConds.entails.pure {x y : ExceptConds PostShape.pure} : x ⊢ₑ y := True.intro
+
 theorem ExceptConds.entails.trans {ps : PostShape} {x y z : ExceptConds ps} : (x ⊢ₑ y) → (y ⊢ₑ z) → x ⊢ₑ z := by
   induction ps
   case pure => intro _ _; trivial

src/Std/Do/SPred/DerivedLaws.lean

@@ -156,6 +156,8 @@ theorem pure_forall {φ : α → Prop} : (∀ x, (⌜φ x⌝ : SPred σs)) ⊣
 
 theorem pure_exists {φ : α → Prop} : (∃ x, ⌜φ x⌝ : SPred σs) ⊣⊢ₛ ⌜∃ x, φ x⌝ := bientails.iff.mpr ⟨exists_elim fun a => pure_mono (⟨a, ·⟩), pure_elim' fun ⟨x, h⟩ => (pure_intro h).trans (exists_intro' x .rfl)⟩
 
+theorem down_pure_intro {φ : Prop} (h : φ) : (pure (σs:=[]) φ).down := by simp [h]
+
 @[simp, grind =] theorem true_intro_simp : (Q ⊢ₛ ⌜True⌝) ↔ True := iff_true_intro true_intro
 
 @[simp] theorem _root_.ULift.down_dite {φ : Prop} [Decidable φ] (t : φ → α) (e : ¬φ → α) : (ULift.down (if h : φ then ⟨t h⟩ else ⟨e h⟩)) = if h : φ then t h else e h := apply_dite _ _ _ _
@@ -170,6 +172,9 @@ theorem and_right_comm : (P ∧ Q) ∧ R ⊣⊢ₛ (P ∧ R) ∧ Q := and_assoc.
 
 -- NB: We cannot currently make the following lemma @[grind =]; we are blocked on #9623.
 theorem entails_pure_elim_cons {σ : Type u} [Inhabited σ] (P Q : Prop) : entails ⌜P⌝ (σs := σ::σs) ⌜Q⌝ ↔ entails ⌜P⌝ (σs := σs) ⌜Q⌝ := by simp [entails]
+theorem apply_pure_cons_entails_l {σ : Type u} {s : σ} (h : pure (σs:=σs) φ ⊢ₛ Q) : pure (σs:=σ::σs) φ s ⊢ₛ Q := by simpa using h
+theorem apply_pure_cons_entails_r {σ : Type u} {s : σ} (h : P ⊢ₛ pure (σs:=σs) φ) : P ⊢ₛ pure (σs:=σ::σs) φ s := by simpa using h
+
 @[simp] theorem entails_true_intro (P Q : SPred σs) : (⊢ₛ P → Q) ↔ (P ⊢ₛ Q) := Iff.intro (fun h => (and_intro true_intro .rfl).trans (imp_elim h)) (fun h => imp_intro (and_elim_r.trans h))
 -- The following lemmas work around a DefEq incompleteness that would be fixed by #9015.
 @[simp] theorem entails_1 {P Q : SPred [σ]} : SPred.entails P Q ↔ (∀ s, (P s).down → (Q s).down) := iff_of_eq rfl

src/Std/Do/SPred/SPred.lean

@@ -54,6 +54,8 @@ def pure {σs : List (Type u)} (P : Prop) : SPred σs := match σs with
   | _ :: _ => fun _ => pure P
 theorem pure_nil : pure (σs:=[]) P = ULift.up P := rfl
 theorem pure_cons : pure (σs:=σ::σs) P = fun _ => pure P := rfl
+@[simp, grind =] theorem down_pure_nil : (pure (σs:=[]) P).down = P := rfl
+@[simp, grind =] theorem apply_pure_cons : pure (σs:=σ::σs) P s = pure P := rfl
 
 /--
 Entailment in `SPred`.
@@ -66,6 +68,8 @@ def entails {σs : List (Type u)} (P Q : SPred σs) : Prop := match σs with
   | [] => P.down → Q.down
   | σ :: _ => ∀ (s : σ), entails (P s) (Q s)
 @[simp, grind =] theorem entails_nil {P Q : SPred []} : entails P Q = (P.down → Q.down) := rfl
+theorem entails_nil_intro {P Q : SPred []} : (P.down → Q.down) → entails P Q := by simp only [entails_nil, imp_self]
+theorem entails_nil_pure_intro {φ : Prop} {Q : SPred []} : (φ → Q.down) → entails (SPred.pure φ) Q := by simp only [entails_nil, pure_nil, imp_self]
 -- We would like to make `entails_cons` @[simp], but that has no effect until we merge #9015.
 -- Until then, we have `entails_<n>` for n ∈ [1:5] in DerivedLaws.lean.
 theorem entails_cons {P Q : SPred (σ::σs)} : entails P Q = (∀ s, entails (P s) (Q s)) := rfl
@@ -150,4 +154,4 @@ def conjunction {σs : List (Type u)} (env : List (SPred σs)) : SPred σs := ma
 @[simp, grind =] theorem conjunction_nil : conjunction ([] : List (SPred σs)) = pure True := rfl
 @[simp, grind =] theorem conjunction_cons {P : SPred σs} {env : List (SPred σs)} : conjunction (P::env) = P.and (conjunction env) := rfl
 @[simp, grind =] theorem conjunction_apply {env : List (SPred (σ::σs))} : conjunction env s = conjunction (env.map (· s)) := by
-  induction env <;> simp [conjunction, pure_cons, *]
+  induction env <;> simp [conjunction, *]