Update to v4.28.0

Verbose/English/Since.lean

@@ -288,6 +288,9 @@ example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by
 example (P Q : Prop) (hPQ : P → Q) (hQP : Q → P) : P ↔ Q := by
   Since P → Q and Q → P we conclude that P ↔ Q
 
+
+configureAnonymousFactSplittingLemmas LogicElims
+
 example (P Q : Prop) (hPQ : P ↔ Q) : True := by
   Since P ↔ Q we get that P → Q and Q → P
   trivial
@@ -400,6 +403,9 @@ example (a b : ℝ) (h : a ≥ b) (h' : b > 0) : True := by
 example (a b : ℝ) (h : a ≥ b) (h' : b > 0) : |a| = a := by
   Since a ≥ b and b > 0 we get that a > 0 finally we conclude that |a| = a
 
+example (a b c d : ℝ) (h : a = b) (h': c = d) : a - c = b - d := by
+  Since a = b and c = d we conclude that a - c = b - d
+
 -- Regression tests for simpa exceeding heartbeats bug
-example (a b c : ℝ) (h : a = b) (h' : b = b * c) : b - a = b - b * c := by
-  Since a = b and b = b * c we conclude that b - a = b - b * c
+example (a b c : ℝ) (h : a = b) (h' : b = b * c) : b - b = b - b * c := by
+  Since b = b * c we conclude that b - b = b - b * c

Verbose/French/Since.lean

@@ -290,6 +290,8 @@ example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by
 example (P Q : Prop) (hPQ : P → Q) (hQP : Q → P) : P ↔ Q := by
   Comme P → Q et Q → P on conclut que P ↔ Q
 
+configureAnonymousFactSplittingLemmas LogicElims
+
 example (P Q : Prop) (hPQ : P ↔ Q) : True := by
   Comme P ↔ Q on obtient que P → Q et Q → P
   trivial
@@ -402,3 +404,6 @@ example (a b : ℝ) (h : a ≥ b) (h' : b > 0) : True := by
 
 example (a b : ℝ) (h : a ≥ b) (h' : b > 0) : |a| = a := by
   Comme a ≥ b et b > 0 on obtient que a > 0 enfin on conclut que |a| = a
+
+example (a b c d : ℝ) (h : a = b) (h': c = d) : a - c = b - d := by
+  Comme a = b et c = d on conclut que a - c = b - d

Verbose/Infrastructure/HelpInfrastructure.lean

@@ -496,7 +496,7 @@ initialize hypHelpExt : PersistentEnvExtension HypHelpEntry (HypHelpEntry × Hyp
     (List HypHelpEntry × DiscrTree HypHelpExt) ←
   -- we only need this to deduplicate entries in the DiscrTree
   have : BEq HypHelpExt := ⟨fun _ _ => false⟩
-  let insert kss v dt := kss.foldl (fun dt ks => dt.insertCore ks v) dt
+  let insert kss v dt := kss.foldl (fun dt ks => dt.insertKeyValue ks v) dt
   registerPersistentEnvExtension {
     mkInitial := pure ([], {})
     addImportedFn := fun s => do
@@ -557,7 +557,7 @@ initialize goalHelpExt : PersistentEnvExtension GoalHelpEntry (GoalHelpEntry ×
     (List GoalHelpEntry × DiscrTree GoalHelpExt) ←
   -- we only need this to deduplicate entries in the DiscrTree
   have : BEq GoalHelpExt := ⟨fun _ _ => false⟩
-  let insert kss v dt := kss.foldl (fun dt ks => dt.insertCore ks v) dt
+  let insert kss v dt := kss.foldl (fun dt ks => dt.insertKeyValue ks v) dt
   registerPersistentEnvExtension {
     mkInitial := pure ([], {})
     addImportedFn := fun s => do

Verbose/Tactics/Since.lean

@@ -1,5 +1,4 @@
 import Mathlib.Tactic.FieldSimp
-import Mathlib.Tactic.CC
 import Verbose.Tactics.Common
 import Verbose.Tactics.By
 import Verbose.FromMathlib.Rify
@@ -128,94 +127,6 @@ def tryLemma! (goal : MVarId) (lem : Name) (facts : List Term) (useAssumption :
     trace[Verbose] s!"could not apply lemma {lem}"
     return false
 
-section cc
-open Lean Meta Elab Tactic Std
-
-namespace Mathlib.Tactic.CC
-
-namespace CCState
-
-open CCM
-
-/-- Create a congruence closure state object from the given `config` using the given hypotheses in the
-current goal. This is variation on `mkUsingHsCore` from Mathlib. -/
-def mkUsingGivenCore (config : CCConfig) (hyps : Array FVarId) : MetaM CCState := do
-  let (_, c) ← CCM.run (hyps.forM fun fvar => do
-    let dcl ← fvar.getDecl
-    unless dcl.isImplementationDetail do
-      if ← isProp dcl.type then
-        CCM.add dcl.type dcl.toExpr) { mkCore config with }
-  return c.toCCState
-
-/-- Run the `cc` tactic but using only the provided hypotheses instead of the full local
-context. This a variation on `_root_.Lean.MVarId.cc` from Mathlib.-/
-def _root_.Lean.MVarId.ccWithHyps (m : MVarId) (hyps : Array FVarId) (cfg : CCConfig := {}) :
-    MetaM Unit := do
-  let (introsFVars, m) ← m.intros
-  m.withContext do
-    let s ← CCState.mkUsingGivenCore cfg (hyps ++ introsFVars)
-    let t ← m.getType >>= instantiateMVars
-    let s ← s.internalize t
-    if s.inconsistent then
-        let pr ← s.proofForFalse
-        mkAppOptM ``False.elim #[t, pr] >>= m.assign
-    else
-      let tr := Expr.const ``True []
-      let b ← s.isEqv t tr
-      if b then
-        let pr ← s.eqvProof t tr
-        mkAppM ``of_eq_true #[pr] >>= m.assign
-      else
-        let dbg ← getBoolOption `trace.Meta.Tactic.cc.failure false
-        if dbg then
-          throwError m!"cc tactic failed, equivalence classes: {s}"
-        else
-          throwError "cc tactic failed"
-
-end CCState
-end Mathlib.Tactic.CC
-
-/-- Try to close the current goal using `cc` with the given hypotheses and report
-whether it succeeded.
-The tactic state is preserved in case of failure.
--/
-def tryCC (goal : MVarId) (hyps : Array FVarId) : MetaM Bool := do
-  let state ← saveState
-  try
-    goal.ccWithHyps hyps
-  catch _ =>
-    restoreState state
-    return false
-  return true
-
-/-- Try to close the current goal using `cc` with the given hypotheses and report
-whether it succeeded. If the goal is an inequality, try to prove the corresponding equality
-using `cc` with the given hypotheses and report whether it succeeded.
-The tactic state is preserved in case of failure.
--/
-def tryCC! (goal : MVarId) (hyps : Array FVarId) : TacticM Bool := do
-  if ← tryCC goal hyps then
-    trace[Verbose] "cc worked"
-    return true
-  else
-    trace[Verbose] "Try to use `le_of_eq`"
-    let state ← saveState
-    let names ← liftMetaM <| hyps.mapM FVarId.getUserName
-    if let some [newGoal] ← tryLemma goal ``le_of_eq then
-      trace[Verbose] "le_of_eq applies. Will try to prove equality using cc"
-      let newHyps ← liftMetaM <| names.mapM getLocalDeclFromUserName
-      if ← tryCC newGoal (newHyps.map LocalDecl.fvarId) then
-        trace[Verbose] "le_of_eq applied"
-        return true
-      else
-        trace[Verbose] "le_of_eq failed"
-        restoreState state
-        return false
-    else
-      restoreState state
-      return false
-end cc
-
 /-- This function will be used to discharge side goals in rels using the given
 expressions hs. We only try to close the goal using each hypothesis. This
 is weaker than the default discharger, on purpose, since it does not call
@@ -334,14 +245,16 @@ def trySimpa (g : MVarId) (a b : Term) : TacticM Bool := g.withContext do
           state.restore
           return false))
 
-def trySimpOnly (g : MVarId) (hyp : Term) : TacticM Bool := g.withContext do
+def trySimpOnly (g : MVarId) (hyps : Array Term) : TacticM Bool := g.withContext do
   let goals ← getGoals
   let state ← saveState
   setGoals [g]
   -- Catching runtime exceptions, because heartbeat exceeded causes a runtime exception
   tryCatchRuntimeEx (do
-    evalTactic (← `(tactic| focus ((simp only [$hyp:term]; try apply le_rfl); done)))
+    let simpArgs ← hyps.mapM (fun t ↦ `(Lean.Parser.Tactic.simpLemma| $t:term))
+    evalTactic (← `(tactic| focus ((simp only [$simpArgs,*]; try apply le_rfl); done)))
     setGoals goals
+    trace[Verbose] s!"simp succeeded"
     return true)
    (fun e => do
     trace[Verbose] e.toMessageData
@@ -405,18 +318,14 @@ def tryAll_core (goal : MVarId) (factsT : Array Term) (factsFVar : Array FVarId)
     if ← (withTraceNode `Verbose (fun e ↦ do
         return s!"{emo e} Will now try simpa with {factsT}.") do
       trySimpa goal factsT[0]! factsT[1]!) then return
-  if factsFVar.size == 1 then
-    if ((← isEqEqv factsFVar[0]!) || goalType.isAppOf `Eq || goalType.isAppOf `Iff) then
+  if ((← factsFVar.allM isEqEqv) || goalType.isAppOf `Eq || goalType.isAppOf `Iff) then
     if ← (withTraceNode `Verbose (fun e ↦ do
-        return s!"{emo e} Will now try simp only with {factsT[0]!}.") do
-      trySimpOnly goal factsT[0]!) then return
+      return s!"{emo e} Will now try simp only with {factsT}.") do
+    trySimpOnly goal factsT) then return
   if factsFVar.size == 1 && goalType.containsConst (· == `HDiv.hDiv) then
     if ← (withTraceNode `Verbose (fun e ↦ do
         return s!"{emo e} Will now try field_simp only with {factsT[0]!}.") do
       tryFieldSimpOnly goal factsT[0]!) then return
-  if ← factsFVar.anyM isEqEqv then
-    if ← withTraceNode `Verbose (fun e ↦ do return s!"{emo e} Will now try cc") do
-      tryCC! goal factsFVar then return
   if factsT.size == 1 then
     let prf : Expr := .fvar factsFVar[0]!
     unless (← factsFVar[0]!.getType).isAppOf `And do
@@ -781,3 +690,9 @@ def sinceChooseTac (fact : Term) (news : Array MaybeTypedIdent) : TacticM Unit :
   replaceMainGoal [newGoal]
   newGoal.withContext do
   chooseTac newFVarsT[0]! news
+
+private lemma iff_def_mp {a b : Prop} : (a ↔ b) → (a → b) ∧ (b → a) := iff_def.mp
+
+private lemma iff_def_mpr {a b : Prop} : (a ↔ b) → (b → a) ∧ (a → b) := iff_def'.mp
+
+AnonymousFactSplittingLemmasList LogicElims := Iff.mp Iff.mpr iff_def_mp iff_def_mpr

basic-configuration.md

@@ -101,6 +101,7 @@ The fact splitting lemmas are lemmas that can be used to get several facts out
 of one. The tautological example would be splitting a conjunction, but the
 library actually has dedicated support for that. An actual typical example
 would be a lemma splitting `x ≥ max a b` into `x ≥ a` and `x ≥ b`.
+In addition, the `LogicElims` lemma list contains lemmas that prove any combination of `a → b` or `b → a` from an equivalence.
 
 ## Help and suggestion providers
 

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
+   "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.28.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
+   "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
+   "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c04225ee7c0585effbd933662b3151f01b600e40",
+   "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.85",
+   "inputRev": "v0.0.87",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
+   "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
+   "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
+   "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "55c37290ff6186e2e965d68cf853a57c0702db82",
+   "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.28.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "verbose",

lakefile.toml

@@ -10,7 +10,7 @@ pp.proofs.withType = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.27.0"
+rev = "v4.28.0"
 
 [[lean_lib]]
 name = "Verbose"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.28.0