feat: implement Std.Do.Triple.mp (#9931)

This PR implements `Std.Do.Triple.mp`, enabling users to compose two
specifications for the same program.

src/Std/Do/PostCond.lean

@@ -124,7 +124,7 @@ def ExceptConds.entails {ps : PostShape.{u}} (x y : ExceptConds ps) : Prop :=
   | .arg _ ps => @entails ps x y
   | .except _ ps => (∀ e, x.1 e ⊢ₛ y.1 e) ∧ @entails ps x.2 y.2
 
-scoped infix:25 " ⊢ₑ " => ExceptConds.entails
+scoped infixr:25 " ⊢ₑ " => ExceptConds.entails
 
 @[refl, simp]
 theorem ExceptConds.entails.refl {ps : PostShape} (x : ExceptConds ps) : x ⊢ₑ x := by
@@ -146,7 +146,6 @@ theorem ExceptConds.entails_false {x : ExceptConds ps} : ExceptConds.false ⊢
 theorem ExceptConds.entails_true {x : ExceptConds ps} : x ⊢ₑ ExceptConds.true := by
   induction ps <;> simp_all [true, const, entails]
 
-@[simp]
 def ExceptConds.and {ps : PostShape.{u}} (x : ExceptConds ps) (y : ExceptConds ps) : ExceptConds ps :=
   match ps with
   | .pure => ⟨⟩
@@ -155,6 +154,12 @@ def ExceptConds.and {ps : PostShape.{u}} (x : ExceptConds ps) (y : ExceptConds p
 
 infixr:35 " ∧ₑ " => ExceptConds.and
 
+@[simp]
+theorem ExceptConds.fst_and {x₁ x₂ : ExceptConds (.except ε ps)} : (x₁ ∧ₑ x₂).fst = fun e => spred(x₁.fst e ∧ x₂.fst e) := rfl
+
+@[simp]
+theorem ExceptConds.snd_and {x₁ x₂ : ExceptConds (.except ε ps)} : (x₁ ∧ₑ x₂).snd = (x₁.snd ∧ₑ x₂.snd) := rfl
+
 @[simp]
 theorem ExceptConds.and_true {x : ExceptConds ps} : x ∧ₑ ExceptConds.true ⊢ₑ x := by
   induction ps
@@ -202,6 +207,55 @@ theorem ExceptConds.and_eq_left {ps : PostShape} {p q : ExceptConds ps} (h : p
     · ext a; exact (SPred.and_eq_left.mp (h.1 a)).to_eq
     · exact ih h.2
 
+def ExceptConds.imp {ps : PostShape.{u}} (x : ExceptConds ps) (y : ExceptConds ps) : ExceptConds ps :=
+  match ps with
+  | .pure => ⟨⟩
+  | .arg _ ps => @ExceptConds.imp ps x y
+  | .except _ _ => (fun e => SPred.imp (x.1 e) (y.1 e), ExceptConds.imp x.2 y.2)
+
+infixr:25 " →ₑ " => ExceptConds.imp
+
+@[simp]
+theorem ExceptConds.fst_imp {x₁ x₂ : ExceptConds (.except ε ps)} : (x₁ →ₑ x₂).fst = fun e => spred(x₁.fst e → x₂.fst e) := rfl
+
+@[simp]
+theorem ExceptConds.snd_imp {x₁ x₂ : ExceptConds (.except ε ps)} : (x₁ →ₑ x₂).snd = (x₁.snd →ₑ x₂.snd) := rfl
+
+theorem ExceptConds.imp_intro {P Q R : ExceptConds ps} (h : P ∧ₑ Q ⊢ₑ R) : P ⊢ₑ Q →ₑ R := by
+  induction ps
+  case pure => trivial
+  case arg ih => exact ih h
+  case except ε ps ih => simp_all [entails, SPred.imp_intro]
+
+theorem ExceptConds.imp_elim {P Q R : ExceptConds ps} (h : P ⊢ₑ (Q →ₑ R)) : P ∧ₑ Q ⊢ₑ R := by
+  induction ps
+  case pure => trivial
+  case arg ih => exact ih h
+  case except ε ps ih => simp_all [entails, SPred.imp_elim]
+
+@[simp]
+theorem ExceptConds.true_imp {x : ExceptConds ps} : (ExceptConds.true →ₑ x) = x := by
+  induction ps
+  case pure => trivial
+  case arg ih => exact ih
+  case except ε ps ih =>
+    cases x
+    simp only [ih, imp, fst_true, snd_true, SPred.true_imp.to_eq]
+
+@[simp]
+theorem ExceptConds.false_imp {x : ExceptConds ps} : (ExceptConds.false →ₑ x) = ExceptConds.true := by
+  induction ps
+  case pure => trivial
+  case arg ih => exact ih
+  case except ε ps ih =>
+    simp only [true, const, ih, imp, fst_false, snd_false, SPred.false_imp.to_eq]
+
+theorem ExceptConds.and_imp {x₁ x₂ : ExceptConds ps} : (x₁ ∧ₑ (x₁ →ₑ x₂)) ⊢ₑ x₁ ∧ₑ x₂ := by
+  induction ps
+  case pure => trivial
+  case arg ih => exact ih
+  case except ε ps ih => simp_all [and, imp, entails, SPred.and_imp]
+
 /--
 A postcondition for the given predicate shape, with one `Assertion` for the terminating case and
 one `Assertion` for each `.except` layer in the predicate shape.
@@ -254,7 +308,7 @@ instance : Inhabited (PostCond α ps) where
 def PostCond.entails (p q : PostCond α ps) : Prop :=
   (∀ a, SPred.entails (p.1 a) (q.1 a)) ∧ ExceptConds.entails p.2 q.2
 
-scoped infix:25 " ⊢ₚ " => PostCond.entails
+scoped infixr:25 " ⊢ₚ " => PostCond.entails
 
 @[refl, simp]
 theorem PostCond.entails.refl (Q : PostCond α ps) : Q ⊢ₚ Q := ⟨fun a => SPred.entails.refl (Q.1 a), ExceptConds.entails.refl Q.2⟩
@@ -276,7 +330,15 @@ abbrev PostCond.and (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :
 
 scoped infixr:35 " ∧ₚ " => PostCond.and
 
-theorem PostCond.and_eq_left {p q : PostCond α ps} (h : p ⊢ₚ q) :
+abbrev PostCond.imp (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
+  (fun a => SPred.imp (p.1 a) (q.1 a), ExceptConds.imp p.2 q.2)
+
+scoped infixr:25 " →ₚ " => PostCond.imp
+
+theorem PostCond.and_imp : P' ∧ₚ (P' →ₚ Q') ⊢ₚ P' ∧ₚ Q' := by
+  simp [SPred.and_imp, ExceptConds.and_imp]
+
+theorem PostCond.and_left_of_entails {p q : PostCond α ps} (h : p ⊢ₚ q) :
     p = (p ∧ₚ q) := by
   ext
   · exact (SPred.and_eq_left.mp (h.1 _)).to_eq

src/Std/Do/PredTrans.lean

@@ -47,7 +47,7 @@ def PredTrans.Conjunctive (t : PostCond α ps → Assertion ps) : Prop :=
 /-- Any predicate transformer that is conjunctive is also monotonic. -/
 def PredTrans.Conjunctive.mono (t : PostCond α ps → Assertion ps) (h : PredTrans.Conjunctive t) : PredTrans.Monotonic t := by
   intro Q₁ Q₂ hq
-  replace hq : Q₁ = (Q₁ ∧ₚ Q₂) := PostCond.and_eq_left hq
+  replace hq : Q₁ = (Q₁ ∧ₚ Q₂) := PostCond.and_left_of_entails hq
   rw [hq, (h Q₁ Q₂).to_eq]
   exact SPred.and_elim_r
 
@@ -137,7 +137,7 @@ def pushArg {σ : Type u} (x : StateT σ (PredTrans ps) α) : PredTrans (.arg σ
       intro Q₁ Q₂
       apply SPred.bientails.of_eq
       ext s
-      dsimp
+      dsimp only [SPred.and_cons, ExceptConds.and]
       rw [← ((x s).conjunctive _ _).to_eq]
   }
 

src/Std/Do/SPred/DerivedLaws.lean

@@ -79,10 +79,6 @@ theorem forall_congr {Φ Ψ : α → SPred σs} (h : ∀ a, Φ a ⊣⊢ₛ Ψ a)
 theorem exists_mono {Φ Ψ : α → SPred σs} (h : ∀ a, Φ a ⊢ₛ Ψ a) : (∃ a, Φ a) ⊢ₛ ∃ a, Ψ a := exists_elim fun a => (h a).trans (exists_intro a)
 theorem exists_congr {Φ Ψ : α → SPred σs} (h : ∀ a, Φ a ⊣⊢ₛ Ψ a) : (∃ a, Φ a) ⊣⊢ₛ ∃ a, Ψ a := bientails.iff.mpr ⟨exists_mono fun a => (h a).mp, exists_mono fun a => (h a).mpr⟩
 
-theorem and_imp (hp : P₁ ⊢ₛ P₂) (hq : Q₁ ⊢ₛ Q₂) : (P₁ ∧ Q₁) ⊢ₛ (P₂ ∧ Q₂) := and_intro (and_elim_l' hp) (and_elim_r' hq)
-theorem or_imp_left (hleft : P₁ ⊢ₛ P₂) : (P₁ ∨ Q) ⊢ₛ (P₂ ∨ Q) := or_elim (or_intro_l' hleft) or_intro_r
-theorem or_imp_right (hright : Q₁ ⊢ₛ Q₂) : (P ∨ Q₁) ⊢ₛ (P ∨ Q₂) := or_elim or_intro_l (or_intro_r' hright)
-
 /-! # Boolean algebra -/
 
 theorem and_self : P ∧ P ⊣⊢ₛ P := bientails.iff.mpr ⟨and_elim_l, and_intro .rfl .rfl⟩
@@ -100,7 +96,7 @@ theorem and_or_left : P ∧ (Q ∨ R) ⊣⊢ₛ (P ∧ Q) ∨ (P ∧ R) :=
   bientails.iff.mpr ⟨and_or_elim_r or_intro_l or_intro_r,
                      or_elim (and_intro and_elim_l (or_intro_l' and_elim_r)) (and_intro and_elim_l (or_intro_r' and_elim_r))⟩
 theorem or_and_left : P ∨ (Q ∧ R) ⊣⊢ₛ (P ∨ Q) ∧ (P ∨ R) :=
-  bientails.iff.mpr ⟨or_elim (and_intro or_intro_l or_intro_l) (and_imp or_intro_r or_intro_r),
+  bientails.iff.mpr ⟨or_elim (and_intro or_intro_l or_intro_l) (and_mono or_intro_r or_intro_r),
                      and_or_elim_l (or_intro_l' and_elim_l) (and_or_elim_r (or_intro_l' and_elim_r) or_intro_r)⟩
 theorem or_and_right : (P ∨ Q) ∧ R ⊣⊢ₛ (P ∧ R) ∨ (Q ∧ R) := and_comm.trans (and_or_left.trans (or_congr and_comm and_comm))
 theorem and_or_right : (P ∧ Q) ∨ R ⊣⊢ₛ (P ∨ R) ∧ (Q ∨ R) := or_comm.trans (or_and_left.trans (and_congr or_comm or_comm))
@@ -120,6 +116,10 @@ theorem imp_self_simp : (Q ⊢ₛ P → P) ↔ True := iff_true_intro imp_self
 theorem imp_trans : (P → Q) ∧ (Q → R) ⊢ₛ P → R := imp_intro' <| and_assoc.mpr.trans <| (and_mono_l imp_elim_r).trans imp_elim_r
 theorem false_imp : (⌜False⌝ → P) ⊣⊢ₛ ⌜True⌝ := bientails.iff.mpr ⟨true_intro, imp_intro <| and_elim_r.trans false_elim⟩
 
+-- Sort-of modus ponens:
+theorem and_imp : P' ∧ (P' → Q') ⊢ₛ P' ∧ Q' := and_intro and_elim_l (and_comm.mp.trans (imp_elim .rfl))
+theorem of_and_imp (hp : P ⊢ₛ P') (hq : Q ⊢ₛ (P' → Q')) : P ∧ Q ⊢ₛ P' ∧ Q' := (and_mono hp hq).trans and_imp
+
 /-! # Pure -/
 
 theorem pure_elim {φ : Prop} (h1 : Q ⊢ₛ ⌜φ⌝) (h2 : φ → Q ⊢ₛ R) : Q ⊢ₛ R :=

src/Std/Do/Triple/Basic.lean

@@ -66,4 +66,7 @@ theorem bind [Monad m] [WPMonad m ps] {α β : Type u} {P : Assertion ps} {Q :
 theorem and [WP m ps] (x : m α) (h₁ : Triple x P₁ Q₁) (h₂ : Triple x P₂ Q₂) : Triple x spred(P₁ ∧ P₂) (Q₁ ∧ₚ Q₂) :=
   (SPred.and_mono h₁ h₂).trans ((wp x).conjunctive Q₁ Q₂).mpr
 
+theorem mp [WP m ps] (x : m α) (h₁ : Triple x P₁ Q₁) (h₂ : Triple x P₂ (Q₁ →ₚ Q₂)) : Triple x spred(P₁ ∧ P₂) (Q₁ ∧ₚ Q₂) :=
+  SPred.and_mono h₁ h₂ |>.trans ((wp x).conjunctive Q₁ (Q₁ →ₚ Q₂)).mpr |>.trans ((wp x).mono _ _ PostCond.and_imp)
+
 end Triple

src/Std/Do/Triple/SpecLemmas.lean

@@ -23,10 +23,6 @@ namespace Std.Range
 abbrev toList (r : Std.Range) : List Nat :=
   List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step
 
-theorem toList_range' (r : Std.Range) (h : r.step = 1) :
-    toList r = List.range' r.start (r.stop - r.start) := by
-  simp [toList, h]
-
 end Std.Range
 
 namespace List