Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/lean4 into joachim/csup-prop

Author: nomeata

src/Init/Grind/Ring/CommSolver.lean

@@ -180,6 +180,53 @@ where
         else
           .mult { x := pw₁.x, k := pw₁.k + pw₂.k } (go fuel m₁ m₂)
 
+noncomputable def Mon.mul_k : Mon → Mon → Mon :=
+  Nat.rec
+    (fun m₁ m₂ => concat m₁ m₂)
+    (fun _ ih m₁ m₂ =>
+      Mon.rec (t := m₂)
+        m₁
+        (fun pw₂ m₂' _ => Mon.rec (t := m₁)
+          m₂
+          (fun pw₁ m₁' _ =>
+            Bool.rec (t := pw₁.varLt pw₂)
+              (Bool.rec (t := pw₂.varLt pw₁)
+                (.mult { x := pw₁.x, k := Nat.add pw₁.k pw₂.k } (ih m₁' m₂'))
+                (.mult pw₂ (ih (.mult pw₁ m₁') m₂')))
+              (.mult pw₁ (ih m₁' (.mult pw₂ m₂'))))))
+    hugeFuel
+
+theorem Mon.mul_k_eq_mul : Mon.mul_k m₁ m₂ = Mon.mul m₁ m₂ := by
+  unfold mul_k mul
+  generalize hugeFuel = fuel
+  fun_induction mul.go
+  · rfl
+  · rfl
+  case case3 m₂ _ =>
+    cases m₂
+    · contradiction
+    · dsimp
+  case case4 fuel pw₁ m₁ pw₂ m₂ h ih =>
+    dsimp only
+    rw [h]
+    dsimp only
+    rw [ih]
+  case case5 fuel pw₁ m₁ pw₂ m₂ h₁ h₂ ih =>
+    dsimp only
+    rw [h₁]
+    dsimp only
+    rw [h₂]
+    dsimp only
+    rw [ih]
+  case case6 fuel pw₁ m₁ pw₂ m₂ h₁ h₂ ih =>
+    dsimp only
+    rw [h₁]
+    dsimp only
+    rw [h₂]
+    dsimp only
+    rw [ih]
+    rfl
+
 def Mon.mul_nc (m₁ m₂ : Mon) : Mon :=
   match m₁ with
   | .unit          => m₂
@@ -190,6 +237,28 @@ def Mon.degree : Mon → Nat
   | .unit => 0
   | .mult pw m => pw.k + degree m
 
+noncomputable def Mon.degree_k : Mon → Nat :=
+  Nat.rec
+    (fun m => m.degree)
+    (fun _ ih m =>
+      Mon.rec (t := m)
+        0
+        (fun pw m' _ => Nat.add pw.k (ih m')))
+    hugeFuel
+
+theorem Mon.degree_k_eq_degree : Mon.degree_k m = Mon.degree m := by
+  unfold degree_k
+  generalize hugeFuel = fuel
+  induction fuel generalizing m with
+  | zero => rfl
+  | succ fuel ih =>
+    conv => rhs; unfold degree
+    split
+    · rfl
+    · dsimp only
+      rw [← ih]
+      rfl
+
 def Var.revlex (x y : Var) : Ordering :=
   bif x.blt y then .gt
   else bif y.blt x then .lt
@@ -270,7 +339,7 @@ noncomputable def Mon.grevlex_k (m₁ m₂ : Mon) : Ordering :=
   Bool.rec
     (Bool.rec .gt .lt (Nat.blt m₁.degree m₂.degree))
     (revlex_k m₁ m₂)
-    (Nat.beq m₁.degree m₂.degree)
+    (Nat.beq m₁.degree_k m₂.degree_k)
 
 theorem Mon.revlex_k_eq_revlex (m₁ m₂ : Mon) : m₁.revlex_k m₂ = m₁.revlex m₂ := by
   unfold revlex_k revlex
@@ -302,18 +371,18 @@ theorem Mon.grevlex_k_eq_grevlex (m₁ m₂ : Mon) : m₁.grevlex_k m₂ = m₁.
   next h =>
     have h₁ : Nat.blt m₁.degree m₂.degree = true := by simp [h]
     have h₂ : Nat.beq m₁.degree m₂.degree = false := by rw [← Bool.not_eq_true, Nat.beq_eq]; omega
-    simp [h₁, h₂]
+    simp [degree_k_eq_degree, h₁, h₂]
   next h =>
     split
     next h' =>
       have h₂ : Nat.beq m₁.degree m₂.degree = true := by rw [Nat.beq_eq, h']
-      simp [h₂]
+      simp [degree_k_eq_degree, h₂]
     next h' =>
       have h₁ : Nat.blt m₁.degree m₂.degree = false := by
         rw [← Bool.not_eq_true, Nat.blt_eq]; assumption
       have h₂ : Nat.beq m₁.degree m₂.degree = false := by
         rw [← Bool.not_eq_true, Nat.beq_eq]; assumption
-      simp [h₁, h₂]
+      simp [degree_k_eq_degree, h₁, h₂]
 
 inductive Poly where
   | num (k : Int)
@@ -481,7 +550,7 @@ noncomputable def Poly.mulMon_k (k : Int) (m : Mon) (p : Poly) : Poly :=
     (Bool.rec
       (Poly.rec
         (fun k' => Bool.rec (.add (Int.mul k k') m (.num 0)) (.num 0) (Int.beq' k' 0))
-        (fun k' m' _ ih => .add (Int.mul k k') (m.mul m') ih)
+        (fun k' m' _ ih => .add (Int.mul k k') (m.mul_k m') ih)
         p)
       (p.mulConst_k k)
       (Mon.beq' m .unit))
@@ -511,7 +580,7 @@ noncomputable def Poly.mulMon_k (k : Int) (m : Mon) (p : Poly) : Poly :=
         next =>
           have h : Int.beq' k 0 = false := by simp [*]
           simp [h]
-      next ih => simp [← ih]
+      next ih => simp [← ih, Mon.mul_k_eq_mul]
 
 def Poly.mulMon_nc (k : Int) (m : Mon) (p : Poly) : Poly :=
   bif k == 0 then

src/Init/Notation.lean

@@ -842,7 +842,7 @@ Position reporting:
   `#guard_msgs` appears.
 - `positions := false` does not report position info.
 
-For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and drop
+For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop
 everything else.
 
 The command elaborator has special support for `#guard_msgs` for linting.

src/Lean/Meta/Tactic/Grind/Parser.lean

@@ -35,6 +35,102 @@ def grindPatternCnstrs : Parser := leading_parser "where " >> many1Indent (ppLin
 /-!
 Builtin parsers for `grind` related commands
 -/
+
+/--
+The `grind_pattern` command can be used to manually select a pattern for theorem instantiation.
+Enabling the option `trace.grind.ematch.instance` causes `grind` to print a trace message for each
+theorem instance it generates, which can be helpful when determining patterns.
+
+When multiple patterns are specified together, all of them must match in the current context before
+`grind` attempts to instantiate the theorem. This is referred to as a *multi-pattern*.
+This is useful for theorems such as transitivity rules, where multiple premises must be simultaneously
+present for the rule to apply.
+
+In the following example, `R` is a transitive binary relation over `Int`.
+```
+opaque R : Int → Int → Prop
+axiom Rtrans {x y z : Int} : R x y → R y z → R x z
+```
+To use the fact that `R` is transitive, `grind` must already be able to satisfy both premises.
+This is represented using a multi-pattern:
+```
+grind_pattern Rtrans => R x y, R y z
+
+example {a b c d} : R a b → R b c → R c d → R a d := by
+  grind
+```
+The multi-pattern `R x y`, `R y z` instructs `grind` to instantiate `Rtrans` only when both `R x y`
+and `R y z` are available in the context. In the example, `grind` applies `Rtrans` to derive `R a c`
+from `R a b` and `R b c`, and can then repeat the same reasoning to deduce `R a d` from `R a c` and
+`R c d`.
+
+You can add constraints to restrict theorem instantiation. For example:
+```
+grind_pattern extract_extract => (as.extract i j).extract k l where
+  as =/= #[]
+```
+The constraint instructs `grind` to instantiate the theorem only if `as` is **not** definitionally equal
+to `#[]`.
+
+## Constraints
+
+- `x =/= term`: The term bound to `x` (one of the theorem parameters) is **not** definitionally equal to `term`.
+  The term may contain holes (i.e., `_`).
+
+- `x =?= term`: The term bound to `x` is definitionally equal to `term`.
+  The term may contain holes (i.e., `_`).
+
+- `size x < n`: The term bound to `x` has size less than `n`. Implicit arguments
+and binder types are ignored when computing the size.
+
+- `depth x < n`: The term bound to `x` has depth less than `n`.
+
+- `is_ground x`: The term bound to `x` does not contain local variables or meta-variables.
+
+- `is_value x`: The term bound to `x` is a value. That is, it is a constructor fully applied to value arguments,
+a literal (`Nat`, `Int`, `String`, etc.), or a lambda `fun x => t`.
+
+- `is_strict_value x`: Similar to `is_value`, but without lambdas.
+
+- `gen < n`: The theorem instance has generation less than `n`. Recall that each term is assigned a
+generation, and terms produced by theorem instantiation have a generation that is one greater than
+the maximal generation of all the terms used to instantiate the theorem. This constraint complements
+the `gen` option available in `grind`.
+
+- `max_insts < n`: A new instance is generated only if less than `n` instances have been generated so far.
+
+- `guard e`: The instantiation is delayed until `grind` learns that `e` is `true` in this state.
+
+- `check e`: Similar to `guard e`, but `grind` checks whether `e` is implied by its current state by
+assuming `¬ e` and trying to deduce an inconsistency.
+
+## Example
+
+Consider the following example where `f` is a monotonic function
+```
+opaque f : Nat → Nat
+axiom fMono : x ≤ y → f x ≤ f y
+```
+and you want to instruct `grind` to instantiate `fMono` for every pair of terms `f x` and `f y` when
+`x ≤ y` and `x` is **not** definitionally equal to `y`. You can use
+```
+grind_pattern fMono => f x, f y where
+  guard x ≤ y
+  x =/= y
+```
+Then, in the following example, only three instances are generated.
+```
+/--
+trace: [grind.ematch.instance] fMono: a ≤ f a → f a ≤ f (f a)
+[grind.ematch.instance] fMono: f a ≤ f (f a) → f (f a) ≤ f (f (f a))
+[grind.ematch.instance] fMono: a ≤ f (f a) → f a ≤ f (f (f a))
+-/
+#guard_msgs in
+example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
+  set_option trace.grind.ematch.instance true in
+  grind
+```
+-/
 @[builtin_command_parser] def grindPattern := leading_parser
   Term.attrKind >> "grind_pattern " >>  ident >> darrow >> sepBy1 termParser "," >> optional grindPatternCnstrs
 

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -12,6 +12,7 @@ public import Lean.Meta.Tactic.Simp.Diagnostics
 public import Lean.Meta.Match.Value
 public import Lean.Util.CollectLooseBVars
 import Lean.PrettyPrinter
+import Lean.ExtraModUses
 
 public section
 
@@ -1069,15 +1070,29 @@ def simpImpl (e : Expr) : SimpM Result := withIncRecDepth do
   else
     x
 
+/--
+For `rfl` theorems and simprocs, there might not be an explicit reference in the proof term, so
+we record (all non-builtin) usages explicitly.
+-/
+private def recordSimpUses (s : State) : MetaM Unit := do
+  for (thm, _) in s.usedTheorems.map do
+    if let .decl declName .. := thm then
+      if !(← isBuiltinSimproc declName) then
+        recordExtraModUseFromDecl (isMeta := false) declName
+
 def mainCore (e : Expr) (ctx : Context) (s : State := {}) (methods : Methods := {}) : MetaM (Result × State) := do
-  SimpM.run ctx s methods <| withCatchingRuntimeEx <| simp e
+  let (r, s) ← SimpM.run ctx s methods <| withCatchingRuntimeEx <| simp e
+  recordSimpUses s
+  return (r, s)
 
 def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do
   let (r, s) ← mainCore e ctx { stats with } methods
   return (r, { s with })
 
 def dsimpMainCore (e : Expr) (ctx : Context) (s : State := {}) (methods : Methods := {}) : MetaM (Expr × State) := do
-  SimpM.run ctx s methods <| withCatchingRuntimeEx <| dsimp e
+  let (r, s) ← SimpM.run ctx s methods <| withCatchingRuntimeEx <| dsimp e
+  recordSimpUses s
+  return (r, s)
 
 def dsimpMain (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Expr × Stats) := do
   let (r, s) ← dsimpMainCore e ctx { stats with } methods

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -12,7 +12,6 @@ public import Lean.Meta.Eqns
 public import Lean.Meta.Tactic.Simp.SimpTheorems
 public import Lean.Meta.Tactic.Simp.SimpCongrTheorems
 import Lean.Meta.Tactic.Replace
-import Lean.ExtraModUses
 
 public section
 
@@ -881,11 +880,6 @@ def SimpM.run (ctx : Context) (s : State := {}) (methods : Methods := {}) (k : S
     trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
     let stats ← updateUsedSimpsWithZetaDelta ctx { s with }
     let s := { s with diag := stats.diag, usedTheorems := stats.usedTheorems }
-    for (thm, _) in s.usedTheorems.map do
-      if let .decl declName .. := thm then
-        -- for `rfl` theorems and simprocs, there might not be an explicit reference in the proof
-        -- term
-        recordExtraModUseFromDecl (isMeta := false) declName
     return (r, s)
 
 end Simp

tests/lean/run/grind_ring_5.lean

@@ -1,7 +1,6 @@
 module
 open Lean.Grind
 
-
 example {α} [CommRing α] [IsCharP α 0] (d t c : α) (d_inv PSO3_inv : α)
   (Δ40 : d^2 * (d + t - d * t - 2) *
     (d + t + d * t) = 0)