From d427423917ce113d56008fffd6755f918336a2a6 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 29 Oct 2025 08:26:24 +0100 Subject: [PATCH] chore: remove duplicate lemmas in `Std.Do.SPred` (#11006) This PR removes the duplicate lemmas `Std.Do.SPred.{and_pure,or_pure,imp_pure,entails_pure_intro}`. --- src/Std/Do/SPred/DerivedLaws.lean | 4 +--- src/Std/Do/SPred/Laws.lean | 15 --------------- 2 files changed, 1 insertion(+), 18 deletions(-) diff --git a/src/Std/Do/SPred/DerivedLaws.lean b/src/Std/Do/SPred/DerivedLaws.lean index 29f1b62269..0eb5369ebe 100644 --- a/src/Std/Do/SPred/DerivedLaws.lean +++ b/src/Std/Do/SPred/DerivedLaws.lean @@ -163,8 +163,6 @@ theorem and_right_comm : (P ∧ Q) ∧ R ⊣⊢ₛ (P ∧ R) ∧ Q := and_assoc. /-! # Working with entailment -/ -theorem entails_pure_intro (P Q : Prop) (h : P → Q) : entails ⌜P⌝ (σs := σs) ⌜Q⌝ := pure_elim' fun hp => pure_intro (h hp) - -- 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] @[simp] theorem entails_true_intro (P Q : SPred σs) : (⊢ₛ P → Q) = (P ⊢ₛ Q) := propext <| Iff.intro (fun h => (and_intro true_intro .rfl).trans (imp_elim h)) (fun h => imp_intro (and_elim_r.trans h)) @@ -268,7 +266,7 @@ class HasFrame (P : SPred σs) (P' : outParam (SPred σs)) (φ : outParam Prop) reassoc : P ⊣⊢ₛ P' ∧ ⌜φ⌝ instance (σs) (P P' Q QP : SPred σs) [HasFrame P Q φ] [SimpAnd Q P' QP]: HasFrame (σs:=σs) spred(P ∧ P') QP φ where reassoc := ((and_congr_l HasFrame.reassoc).trans and_right_comm).trans (and_congr_l SimpAnd.simp_and) instance (σs) (P P' Q' PQ : SPred σs) [HasFrame P' Q' φ] [SimpAnd P Q' PQ]: HasFrame (σs:=σs) spred(P ∧ P') PQ φ where reassoc := ((and_congr_r HasFrame.reassoc).trans and_assoc.symm).trans (and_congr_l SimpAnd.simp_and) -instance (σs) (P P' : Prop) (Q : SPred σs) [HasFrame spred(⌜P⌝ ∧ ⌜P'⌝) Q φ] : HasFrame (σs:=σs) ⌜P ∧ P'⌝ Q φ where reassoc := and_pure.symm.trans HasFrame.reassoc +instance (σs) (P P' : Prop) (Q : SPred σs) [HasFrame spred(⌜P⌝ ∧ ⌜P'⌝) Q φ] : HasFrame (σs:=σs) ⌜P ∧ P'⌝ Q φ where reassoc := pure_and.symm.trans HasFrame.reassoc instance (σs) (P P' : SVal.StateTuple σs → Prop) (Q : SPred σs) [HasFrame spred(SVal.curry (fun t => ⟨P t⟩) ∧ SVal.curry (fun t => ⟨P' t⟩)) Q φ] : HasFrame (σs:=σs) (SVal.curry fun t => ⟨P t ∧ P' t⟩) Q φ where reassoc := and_curry.symm.trans HasFrame.reassoc instance (σs) (P : SPred σs) : HasFrame (σs:=σs) spred(⌜φ⌝ ∧ P) P φ where reassoc := and_comm instance (σs) (P : SPred σs) : HasFrame (σs:=σs) spred(P ∧ ⌜φ⌝) P φ where reassoc := .rfl diff --git a/src/Std/Do/SPred/Laws.lean b/src/Std/Do/SPred/Laws.lean index a07165ab7e..8cca033a8d 100644 --- a/src/Std/Do/SPred/Laws.lean +++ b/src/Std/Do/SPred/Laws.lean @@ -89,21 +89,6 @@ theorem pure_elim' {φ : Prop} {P : SPred σs} : (φ → ⌜True⌝ ⊢ₛ P) -- theorem pure_elim' {φ : Prop} : SPred.entails (σs:=σs) ⌜True⌝ ⌜φ⌝ → φ -- Unfortunately, this is only true if all `σs` are Inhabited. -theorem and_pure {P Q : Prop} : ⌜P⌝ ∧ ⌜Q⌝ ⊣⊢ₛ (⌜P ∧ Q⌝ : SPred σs) := by - induction σs - case nil => rfl - case cons σ σs ih => intro s; simp only [and_cons]; exact ih - -theorem or_pure {P Q : Prop} : ⌜P⌝ ∨ ⌜Q⌝ ⊣⊢ₛ (⌜P ∨ Q⌝ : SPred σs) := by - induction σs - case nil => rfl - case cons σ σs ih => intro s; simp only [or_cons]; exact ih - -theorem imp_pure {P Q : Prop} : (⌜P⌝ → ⌜Q⌝) ⊣⊢ₛ (⌜P → Q⌝ : SPred σs) := by - induction σs - case nil => rfl - case cons σ σs ih => intro s; simp only [imp_cons]; exact ih - /-! # Conjunction -/ theorem and_intro {P Q R : SPred σs} (h1 : P ⊢ₛ Q) (h2 : P ⊢ₛ R) : P ⊢ₛ Q ∧ R := by