wip

This reverts commit 838d72436a61f64942ccf808317290624db0a736.

Blah.lean

@@ -0,0 +1,33 @@
+def SatisfiesM {m : Type u → Type v} {α} [Functor m] (p : α → Prop) (x : m α) : Prop :=
+  ∃ x' : m {a // p a}, Subtype.val <$> x' = x
+
+theorem SatisfiesM.and [Monad m] [LawfulMonad m] {x : m α} {p q : α → Prop}
+    (hp : SatisfiesM p x) (hq : SatisfiesM q x) : SatisfiesM (fun r => p r ∧ q r) x := by
+  obtain ⟨xsub_p, hsub_p⟩ := hp
+  obtain ⟨xsub_q, hsub_q⟩ := hq
+  subst x
+  have sdlfkj_p := Subtype.property <$> xsub_p
+  have sdlfkj_q := Subtype.property <$> xsub_q
+  constructor
+  case w => sorry
+  case w => sorry
+
+
+
+theorem SatisfiesM.imp [Functor m] [LawfulFunctor m] {x : m α}
+    (h : SatisfiesM p x) (H : ∀ {a}, p a → q a) : SatisfiesM q x :=
+  let ⟨x, h⟩ := h; ⟨(fun ⟨_, h⟩ => ⟨_, H h⟩) <$> x, by rw [← h, ← comp_map]; rfl⟩
+
+
+theorem SatisfiesM.split_step [Functor m] [LawfulFunctor m] {x : m (ForInStep β)}
+    {done : β → Prop} {yield : β → Prop}
+    (hyield : SatisfiesM (∀ b', · = .yield b' → yield b') x)
+    (hdone :  SatisfiesM (∀ b', · = .done b'  → done b') x) :
+    SatisfiesM (fun r => (∃ b', r = .yield b' ∧ yield b') ∨ (∃ b', r = .done b' ∧ done b')) x := by
+      obtain ⟨xsub_yld, hsub_yld⟩ := hyield
+      obtain ⟨xsub_dn, hsub_dn⟩ := hdone
+      subst x
+      constructor
+      case h =>
+      case w =>
+      exact ⟨(fun r => ⟨r,match r with | .yield b' => _ | .done b' => _⟩) <$> x, _⟩

Test.lean

@@ -0,0 +1,568 @@
+import Lean
+open Lean
+open Lean.Parser
+open Lean.Elab.Command
+open Lean.Elab
+open Lean.Elab.Tactic
+open Lean.Meta
+open Lean.SubExpr
+--open Std.Range
+
+def PredTransM α := (α → Prop) → Prop
+instance : Monad PredTransM where
+  pure x := fun p => p x
+  bind x f := fun p => x (fun a => f a p)
+instance : LawfulMonad PredTransM := sorry
+
+
+/-- Backward predicate transformer derived from a substitution property of monads.
+A generic effect observation that can be used to observe all monads.
+It is oblivious to any computations that happened before it, so `Obs.bind` loses information
+for non-pure monads.
+It is a suitable choice for the base layer of a specification monad stack if
+the observation does the right thing for your use case; see the equivalence lemmas such as
+`Obs_Id_eq`.
+More sophisticated observations can be built on top of `Obs` by wrapping suitable monad transformers such
+as `StateT` or `ExceptT`.
+-/
+def Obs {m : Type u → Type v} {α} [Monad m] (x : m α) : PredTransM α := fun p =>
+  ∀ {β} {f g : α → m β}, (∀ a, p a → f a = g a) → x >>= f = x >>= g
+
+notation "obs⟦" x "⟧" => Obs x
+
+theorem Obs.pure [Monad m] [LawfulMonad m]
+    (h : p a) : obs⟦pure (f:=m) a⟧ p := by
+  simp_all only [Obs, pure_bind, implies_true]
+
+--set_option pp.all true in
+--theorem repro {m : Type u → Type v} {p : α × σ → Prop} [Monad m] [LawfulMonad m] (hp : p (a, s)) :
+--  (do Obs (m := StateT σ m) (set s); Obs (m := StateT σ m) (Pure.pure (a, s))) p
+--  = Obs (m := StateT σ m) (set s) (fun _ => True)
+--  := by
+--    replace hp : Obs (m := StateT σ m) (Pure.pure (a, s)) p := (Obs.pure hp)
+--    set_option trace.Tactic.rewrites true in
+--    conv => lhs; arg 1; intro; rw [eq_true @hp]
+
+theorem Obs.bind [Monad m] [LawfulMonad m] {f : α → m β}
+    (hx : obs⟦x⟧ (fun a => obs⟦f a⟧ q)) :
+    obs⟦x >>= f⟧ q := by
+  intros γ f g hfg
+  simp only [bind_assoc]
+  exact hx fun a hq => hq hfg
+
+theorem Obs.subst [Monad m] [LawfulMonad m] {x : m α}
+  (hp : obs⟦x⟧ p) (hf : ∀ a, p a → f a = g a) : x >>= f = x >>= g := hp hf
+
+theorem Obs.subst_pre [Monad m] [LawfulMonad m] {x : m α} (hp : obs⟦x⟧ (fun r => f r = g r)) :
+  x >>= f = x >>= g := by apply hp; simp
+
+theorem Obs.conj [Monad m] [LawfulMonad m] {x : m α}
+    (hp : obs⟦x⟧ p) (hq : obs⟦x⟧ q) : obs⟦x⟧ (fun r => p r ∧ q r) := by
+  intros β f g hfg
+  open Classical in
+  calc x >>= f
+    _ = x >>= (fun r => if p r ∧ q r then f r else f r) := by simp
+    _ = x >>= (fun r => if p r ∧ q r then g r else f r) := by simp +contextual [hfg]
+    _ = x >>= (fun r => if q r then g r else f r) := hp (by simp +contextual)
+    _ = x >>= g := hq (by simp +contextual)
+
+theorem Obs.inf_conj [Monad m] [LawfulMonad m] {x : m α}
+    (hp : obs⟦x⟧ p) (hq : obs⟦x⟧ q) : obs⟦x⟧ (fun r => sInf { p ∈ ps // p r }) := by
+  intros β f g hfg
+  open Classical in
+  calc x >>= f
+    _ = x >>= (fun r => if p r ∧ q r then f r else f r) := by simp
+    _ = x >>= (fun r => if p r ∧ q r then g r else f r) := by simp +contextual [hfg]
+    _ = x >>= (fun r => if q r then g r else f r) := hp (by simp +contextual)
+    _ = x >>= g := hq (by simp +contextual)
+
+@[simp]
+theorem Monad.bind_unit {m : Type u → Type v} [Monad m] {x : m PUnit} {f : PUnit → m α} :
+  (do let a ← x; f a) = (do x; f ⟨⟩) := by simp only
+
+theorem Obs.split_unit {m : Type u → Type v} [Monad m] {x : m PUnit} (hp : p) :
+  obs⟦x⟧ (fun _ => p) := fun hfg =>
+    funext (fun u => hfg u hp) ▸ rfl
+
+def KimsObs {m : Type u → Type v} {α} [Functor m] (p : α → Prop) (x : m α) : Prop :=
+  (fun r => (r, p r)) <$> x = (fun r => (r, True)) <$> x
+
+def KimsObs_of_Obs {m : Type u → Type v} {α} [Monad m] [LawfulMonad m] (p : α → Prop) (x : m α)
+  (h : obs⟦x⟧ p) : KimsObs p x := by
+  unfold KimsObs
+  simp [← LawfulMonad.bind_pure_comp]
+  apply h
+  intros
+  simp [*]
+
+@[simp]
+theorem Obs_Id_eq : obs⟦x⟧ P ↔ P (Id.run x) := by
+  constructor
+  case mp =>
+    intro h
+    replace h := KimsObs_of_Obs P x h
+    simp [KimsObs] at h
+    injection h
+    simp[*, Id.run]
+  case mpr =>
+    intro h; apply Obs.pure; exact h
+
+theorem Obs.imp [Monad m] [LawfulMonad m] {p : Prop} {f : α → m β} :
+    obs⟦f a⟧ (fun r => p → q r) ↔ (p → obs⟦f a⟧ q) := by
+  if hp : p
+  then simp_all
+  else simp_all; intro _ _ _ h; simp[funext (fun a => h a ⟨⟩)]
+
+theorem Obs.mono [Monad m] [LawfulMonad m] {x : m a}
+    (h : obs⟦x⟧ p) (H : ∀ {a}, p a → q a) : obs⟦x⟧ q := by
+    intro _ _ _ hfg
+    apply h
+    simp_all only [implies_true]
+
+class LawfulMonadState (σ : semiOutParam (Type u)) (m : Type u → Type v) [Monad m] [LawfulMonad m] [MonadStateOf σ m] where
+  get_set : (do let s ← get; set s) = pure (f := m) ⟨⟩
+  set_get {k : σ → m β} : (do set s₁; let s₂ ← get; k s₂) = (do set s₁; k s₁)
+  set_set {s₁ s₂ : σ} : (do set s₁; set s₂) = set (m := m) s₂
+
+theorem LawfulMonadState.set_get_pure [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadState σ m] {s : σ} :
+  (do set s; get) = (do set (m := m) s; pure s) := by
+    calc (do set s; get)
+      _ = (do set s; let s' ← get; pure s') := by simp
+      _ = (do set s; pure s) := by rw [LawfulMonadState.set_get]
+attribute [simp] LawfulMonadState.get_set LawfulMonadState.set_get LawfulMonadState.set_set LawfulMonadState.set_get_pure
+
+instance [Monad m] [LawfulMonad m] : LawfulMonadState σ (StateT σ m) where
+  get_set := by intros; ext s; simp
+  set_get := by intros; ext s; simp
+  set_set := by intros; ext s; simp
+
+def SatisfiesSM {m : Type u → Type v} {α} [Monad m] (x : StateT σ m α) (p : α × σ → Prop) : Prop :=
+  obs⟦do let a ← x; let s ← get; pure (a, s)⟧ p
+
+theorem SatisfiesSM.subst [Monad m] [LawfulMonad m] {x : StateT σ m α}
+  {f g : α → StateT σ m β}
+  (hp : SatisfiesSM x p) (hf : ∀ a s, p (a, s) → (do set s; f a) = (do set s; g a)) :
+  x >>= f = x >>= g := by
+    suffices h : (do let (a,s) ← (do let a ← x; let s ← get; pure (a, s)); set s; f a) = (do let (a,s) ← (do let a ← x; let s ← get; pure (a, s)); set s; g a) by
+      simp at h
+      simp[← LawfulMonad.bind_assoc] at h
+      assumption
+    unfold SatisfiesSM at hp
+    apply hp.subst fun ⟨a, s⟩ => hf a s
+
+theorem Obs.split_step [Monad m] [LawfulMonad m] {x : m (ForInStep β)}
+    {done : β → Prop} {yield : β → Prop}
+    (hyield : obs⟦x⟧ (∀ b', · = .yield b' → yield b'))
+    (hdone :  obs⟦x⟧ (∀ b', · = .done b'  → done b')) :
+    obs⟦x⟧ (fun | .yield b' => yield b' | .done b' => done b') := by
+  apply Obs.mono (Obs.conj hyield hdone)
+  rintro a ⟨hyield, hdone⟩
+  split <;> solve_by_elim
+
+theorem Obs.forIn_list
+  [Monad m] [LawfulMonad m]
+  {xs : List α} {init : β} {f : α → β → m (ForInStep β)}
+  (inv : List α → β → Prop)                     -- user-supplied loop invariant
+  (hpre : inv xs init)                          -- pre⟦for {inv} xs init f⟧(p)
+  (hweaken : ∀ b, inv [] b → p b)               -- vc₁: weaken invariant to postcondition after loop exit
+  (hdone : ∀ {hd tl b}, inv (hd::tl) b →        -- vc₂: weaken invariant to precondition of loop body upon loop entry, done case
+          obs⟦f hd b⟧ (∀ b', · = .done b'  → inv [] b'))
+  (hyield : ∀ {hd tl b}, inv (hd::tl) b →       -- vc₃: weaken invariant to precondition of loop body upon loop entry, yield case
+          obs⟦f hd b⟧ (∀ b', · = .yield b' → inv tl b')) :
+  obs⟦forIn xs init f⟧ p := by
+    induction xs generalizing init
+    case nil => simp only [List.forIn_nil]; apply Obs.pure; apply hweaken; exact hpre
+    case cons hd tl h =>
+      simp only [List.forIn_cons]
+      apply Obs.bind
+      have : obs⟦f hd init⟧ (fun | .yield b' => inv tl b' | .done b' => inv [] b') :=
+        Obs.split_step (hyield hpre) (hdone hpre)
+      apply Obs.mono this
+      intro r hres
+      match r with
+      | .done b => apply Obs.pure; apply hweaken; assumption
+      | .yield b => simp; simp at hres; exact @h b hres
+
+theorem Obs.forIn_range
+  [Monad m] [LawfulMonad m]
+  {xs : Std.Range} {init : β} {f : Nat → β → m (ForInStep β)}
+  (inv : List Nat → β → Prop := fun _ => p)     -- user-supplied loop invariant
+  (hpre : inv (List.range' xs.start xs.size xs.step) init)                          -- pre⟦for {inv} xs init f⟧(p)
+  (hweaken : ∀ b, inv [] b → p b)               -- vc1: weaken invariant to postcondition after loop exit
+  (hdone : ∀ {hd tl b}, inv (hd::tl) b →        -- vc₂: weaken invariant to precondition of loop body upon loop entry, done case
+          obs⟦f hd b⟧ (∀ b', · = .done b'  → inv [] b'))
+  (hyield : ∀ {hd tl b}, inv (hd::tl) b →       -- vc₃: weaken invariant to precondition of loop body upon loop entry, yield case
+          obs⟦f hd b⟧ (∀ b', · = .yield b' → inv tl b')) :
+  obs⟦forIn xs init f⟧ p := by
+    rw [Std.Range.forIn_eq_forIn_range']
+    exact Obs.forIn_list inv hpre hweaken hdone hyield
+
+theorem Obs.forIn_loop
+  [Monad m] [LawfulMonad m]
+  {xs : Loop} {init : β} {f : Unit → β → m (ForInStep β)}
+  (inv : Bool → β → Prop := fun _ => p)     -- user-supplied loop invariant
+  (hpre : inv true init)                          -- pre⟦for {inv} xs init f⟧(p)
+  (hweaken : ∀ b, inv false b → p b)               -- vc1: weaken invariant to postcondition after loop exit
+  (hdone : ∀ {b}, inv true b →        -- vc₂: weaken invariant to precondition of loop body upon loop entry, done case
+          obs⟦f () b⟧ (∀ b', · = .done b'  → inv false b'))
+  (hyield : ∀ {b}, inv true b →       -- vc₃: weaken invariant to precondition of loop body upon loop entry, yield case
+          obs⟦f () b⟧ (∀ b', · = .yield b' → inv true b')) :
+  obs⟦forIn Loop.mk init f⟧ p := sorry
+
+elab "vcgen" /-("invariant " ilbls:ident ": " inv:term)*-/ : tactic => withMainContext <| do
+  let goal ← getMainGoal
+  let ctx ← mkSimpContext Syntax.missing (eraseLocal := false)
+  try
+    let goal := match ← dsimpGoal goal ctx.ctx with
+    | (some goal, _) => goal
+    | _              => goal
+    replaceMainGoal [goal]
+  catch _ => pure ()
+  let mut verification_conds := #[]
+  while true do
+    let goal :: goals ← getGoals | break
+    if ← goal.isAssigned then setGoals goals; continue
+    let (_xs, goal) ← goal.intros
+    let ty ← instantiateMVars (← goal.getType)
+    -- ty = @Obs m α [Functor m] prog post
+    if ¬(ty.isAppOfArity `Obs 5) then
+      logInfo m!"give up on {ty}"
+      verification_conds := verification_conds.push goal
+      setGoals goals
+      continue
+    let prog := ty.appFn!.appArg!
+    let α := ty.appFn!.appFn!.appFn!.appArg!
+    let m := ty.appFn!.appFn!.appFn!.appFn!.appArg!
+
+    -- Convention: ⟦P⟧(x) for Obs P x
+    if prog.isAppOfArity ``Pure.pure 4 then
+      -- prog = @pure m [Pure m] α (x : α)
+      -- ⟦P⟧(pure x)
+      -- <=={Satisfies.pure}
+      -- P x
+      let [goal] ← goal.applyConst ``Obs.pure | throwError "argh"
+      replaceMainGoal [goal]
+      continue
+    else if prog.isAppOfArity ``Bind.bind 6 then
+      -- prog = @bind m [Bind m] α β e f
+      -- ⟦P⟧(bind e f)
+      -- <=={Satisfies.bind}
+      -- P⟦fun r => ⟦P⟧(f r)⟧(e)
+      let [goal] ← goal.applyConst ``Obs.bind | throwError "argh"
+      replaceMainGoal [goal]
+      continue
+    else if prog.isAppOfArity ``ForIn.forIn 9 then
+      -- prog = @forIn {m} {ρ} {α} [ForIn m ρ α] {β} [Monad m] xs init f
+      -- ⟦P⟧(forIn xs init f)
+      -- <=={Obs.forIn_*} (depending on ρ)
+      -- ... a bunch of sub-goals, including the invariant
+      let ρ := prog.appFn!.appFn!.appFn!.appFn!.appFn!.appFn!.appFn!.appArg!;
+      if ρ.isConstOf ``Std.Range then
+        let goals ← goal.applyConst ``Obs.forIn_range
+        replaceMainGoal goals
+        continue
+      else if ρ.isConstOf ``List then
+        let goals ← goal.applyConst ``Obs.forIn_range
+        replaceMainGoal goals
+        continue
+      -- let name := match
+      replaceMainGoal [goal]
+      continue
+    else if prog.isLet then
+      -- C ⊢ ⟦P⟧(do let x : ty := val; prog)
+      -- <=={lift_let; intros}
+      -- C; let x : ty := val ⊢ ⟦P⟧(prog)
+      let ty ← instantiateMVars (← goal.getType)
+      let goal ← goal.change (← ty.liftLets mkLetFVars)
+      let (_xs, goal) ← goal.intros
+      replaceMainGoal [goal]
+      continue
+    else if prog.isIte then
+      -- ⟦P⟧((if b then prog₁ else prog₂))
+      -- <=={split}
+      -- (b → ⟦P⟧(prog₁) ∧ ((¬b) → ⟦P⟧(prog₂))
+      let some (tt,ff) ← splitIfTarget? goal | throwError "wlp failed"
+      replaceMainGoal [tt.mvarId, ff.mvarId]
+      continue
+    else if let .fvar fvarId := prog.getAppFn then -- inline locals
+      -- C; let __do_jp : ty := val ⊢ ⟦P⟧(__do_jp y x))
+      -- <=={dsimp only [__do_jp]}
+      -- C; let __do_jp : ty := val ⊢ ⟦P⟧(val y x))
+      try
+        -- Why can't I test fvarId.isLetVar? here, but zeta succeeds???
+        let goal ← zetaDeltaTarget goal fvarId
+        replaceMainGoal [goal]
+        continue
+      catch _ => pure ()
+    else if m.isConstOf ``Id then
+      -- Id x is definitionally equal to x, and we can apply Obs.pure in that case
+      -- prog = @pure m [Pure m] α (x : α)
+      -- ⟦P⟧(pure x)
+      -- <=={Satisfies.pure}
+      -- P x
+      let [goal] ← goal.applyConst ``Obs.pure | throwError "argh"
+      replaceMainGoal [goal]
+      continue
+    else if α.isConstOf ``PUnit then
+      -- If c : m PUnit, then the predicate is constant and can be pulled out
+      -- ⟦P⟧(c)
+      -- <=={Satisfies.split_unit}
+      -- P ⟨⟩
+      let [goal] ← goal.applyConst ``Obs.split_unit | throwError "argh"
+      replaceMainGoal [goal]
+      continue
+
+    logInfo m!"give up on {repr prog}"
+    verification_conds := verification_conds.push goal
+    setGoals goals
+    continue
+
+  setGoals verification_conds.toList
+
+theorem test_5 : Obs (m:=Id) (do let mut x := 0; for i in [1:5] do { x := x + i } return x) (fun r => r ≤ 25) := by
+  vcgen
+  case inv => exact (fun xs r => (∀ x, x ∈ xs → x ≤ 5) ∧ r + xs.length * 5 ≤ 25)
+  set_option trace.grind.debug true in
+  case hpre => simp_all; omega
+  case hweaken => simp_all
+  case hdone => simp_all
+  case hyield h => injection h; simp_all; omega
+
+theorem test_6 : Obs (m:=Id) (do let mut x := 0; let mut i := 0; while i < 4 do { x := x + i; i := i + 1 } return x) (fun r => r ≤ 1) := by
+  dsimp
+  vcgen
+  case inv => exact (fun xs r => (∀ x, x ∈ xs → x ≤ 5) ∧ r + xs.length * 5 ≤ 25)
+  case hpre => simp; omega
+  case hweaken => simp
+  case hdone => intros; apply Obs.pure; simp;
+  case hyield => intros; apply Obs.pure; simp_all; intro _ h; injection h; omega
+
+theorem test_1 : Obs (m:=Id) (do return 3) (fun r => r = 3) := by
+  vcgen
+  trivial
+
+theorem test_2 : Obs (m:=Id) (do let mut id := 5; id := 3; return id) (fun r => r = 3) := by
+  vcgen
+  trivial
+
+theorem test_3 [Monad m] [LawfulMonad m] (h : Obs e₁ (fun _ => Obs (m:=m) (do e₂; e₃) P)) : Obs (m:=m) (do e₁; e₂; e₃) P := by
+  vcgen
+  trivial
+
+theorem test_4 : Obs (m:=Id) (do let mut x := 5; if x > 1 then { x := 1 } else { x := x }; pure x) (fun r => r ≤ 1) := by
+  vcgen <;> simp; omega
+
+def fib_impl (n : Nat) := Id.run do
+  if n = 0 then return 0
+  let mut a := 0
+  let mut b := 0
+  b := b + 1
+  for _ in [1:n] do
+    let a' := a
+    a := b
+    b := a' + b
+  return b
+
+def fib_spec : Nat → Nat
+| 0 => 0
+| 1 => 1
+| n+2 => fib_spec n + fib_spec (n+1)
+
+theorem fib_correct {n} : fib_impl n = fib_spec n := Obs_Id_eq (P := fun r => r = fib_spec n) <| by
+  vcgen
+  case isTrue => simp_all[fib_spec]
+  case inv => exact (fun | xs, ⟨a, b⟩ => a = fib_spec (n - xs.length - 1) ∧ b = fib_spec (n - xs.length))
+  case hpre col _ h =>
+    simp_all[List.range']
+    have : 1 ≤ n := Nat.succ_le_of_lt (Nat.zero_lt_of_ne_zero h)
+    rw[Nat.div_one, Nat.sub_one_add_one h, Nat.sub_sub, Nat.sub_add_cancel this, Nat.sub_self, Nat.sub_sub_self this]
+    simp_all[fib_spec]
+    exact ⟨rfl, rfl⟩
+  case hweaken => apply Obs.pure; simp_all
+  case hdone.hx.h.h => simp_all
+  case hyield.hx.h.h b' h => injection h; subst b'; subst_vars; simp_all; rw[fib_spec] at ⊢;
+  -- The default simp set eliminates the binds generated by `do` notation,
+  -- and converts the `for` loop into a `List.foldl` over `List.range'`.
+  simp [fib_impl, Id.run]
+  match n with
+  | 0 => simp [fib_spec]
+  | n+1 =>
+    -- Note here that we have to use `⟨x, y⟩ : MProd _ _`, because these are not `Prod` products.
+    suffices ((List.range' 1 n).foldl (fun b a ↦ ⟨b.snd, b.fst + b.snd⟩) (⟨0, 1⟩ : MProd _ _)) =
+        ⟨fib_spec n, fib_spec (n + 1)⟩ by simp_all
+    induction n with
+    | zero => rfl
+    | succ n ih => simp [fib_spec, List.range'_1_concat, ih]
+/-
+https://lean-fro.zulipchat.com/#narrow/channel/398861-general/topic/baby.20steps.20towards.20monadic.20verification
+
+-/
+
+class MonadObserve (m : Type u₁ → Type u₂) [Monad com] [LawfulMonad com] [Monad spec] [LawfulMonad spec] where
+  observe : com α → spec α
+  pure_pure : ∀ {a : α} {p : α → prop}, p a → observe (pure a) p
+
+class MonadPost (m : Type u₁ → Type u₂) (prop : Type) [Monad m] [LawfulMonad m] where
+  Post : m α → Prop
+  pure {a : α} {p : α → prop} (hp : p a) : Post (pure a)
+  bind {α β} (x : m α) (f : α → m β) {p : β → prop} : Post x (fun a => Post (f a) p) → Post (x >>= f) p
+  forIn_list {α β} {xs : List α} {init : β} {f : α → β → m (ForInStep β)} {p : α → prop}
+    (inv : List α → β → Prop)                     -- user-supplied loop invariant
+    (hpre : inv xs init)                          -- pre⟦for {inv} xs init f⟧(p)
+    (hweaken : ∀ b, inv [] b → p b)               -- vc₁: weaken invariant to postcondition after loop exit
+    (hdone : ∀ {hd tl b}, inv (hd::tl) b →        -- vc₂: weaken invariant to precondition of loop body upon loop entry, done case
+            Post (f hd b) (∀ b', · = .done b'  → inv [] b'))
+    (hyield : ∀ {hd tl b}, inv (hd::tl) b →       -- vc₃: weaken invariant to precondition of loop body upon loop entry, yield case
+          Post (f hd b) (∀ b', · = .yield b' → inv tl b')) :
+      Post (forIn xs init f) p
+
+
+def StateT.observe {m : Type u → Type v} {α} [Monad m] (x : StateT σ m α) : StateT σ PredTransM α := fun s₁ p =>
+  Obs (do set s₁; let a ← x; let s₂ ← get; pure (a, s₂)) p
+
+theorem blah {a : α} {s : σ} : (fun p => p (a, s)) → (do s ← Obs get; Obs (Pure.pure (a, s))) := by
+  intro h
+  simp only [observe]
+  vcgen
+  assumption
+
+theorem StateT.observe.pure {m : Type u → Type v} {p : α × σ → Prop} [Monad m] [LawfulMonad m]
+  (hp : p (a, s)) : StateT.observe (m:=m) (pure a) s p := by
+  simp only [observe, pure_bind, LawfulMonadState.set_get]
+  vcgen
+  assumption
+
+theorem StateT.observe.get_pre {m : Type u → Type v} [Monad m] [LawfulMonad m] {p : σ × σ → Prop} (hp : p ⟨s, s⟩) :
+  StateT.observe (m:=m) get s p := by
+  simp only [observe, pure_bind, LawfulMonadState.set_get]
+  vcgen
+  assumption
+
+theorem StateT.observe.get {m : Type u → Type v} [Monad m] [LawfulMonad m] :
+  StateT.observe (m:=m) get s (· = ⟨s, s⟩) := StateT.observe.get_pre (by rfl)
+
+theorem StateT.observe.set_pre {m : Type u → Type v} [Monad m] [LawfulMonad m] {p : PUnit × σ → Prop} (hp : p ⟨⟨⟩, s₂⟩) :
+  StateT.observe (m:=m) (set s₂) s₁ p := by
+  simp only [observe, pure_bind, Monad.bind_unit]
+  simp only [← LawfulMonad.bind_assoc, LawfulMonadState.set_set]
+  simp only [LawfulMonadState.set_get_pure]
+  simp [-LawfulMonad.bind_pure_comp]
+  vcgen
+  assumption
+
+theorem StateT.observe.set {m : Type u → Type v} [Monad m] [LawfulMonad m] {s₂ : σ} :
+  StateT.observe (m:=m) (set s₂) s₁ (· = ⟨⟨⟩, s₂⟩) := StateT.observe.set_pre (by rfl)
+
+
+
+/-
+def fib_spec : Nat → Nat
+| 0 => 0
+| 1 => 1
+| n+2 => fib_spec n + fib_spec (n+1)
+
+theorem fib_spec_rec (h : n > 1) : fib_spec n = fib_spec (n-2) + fib_spec (n-1) := by
+  rw (occs := .pos [1]) [fib_spec.eq_def]
+  split
+  repeat omega
+  --omega
+  simp
+
+def fib_impl (n : Nat) := Id.run do
+  if n = 0 then return 0
+  let mut i := 1
+  let mut a := 0
+  let mut b := 0
+  b := b + 1
+  while@first_loop i < n do
+    let a' := a
+    a := b
+    b := a' + b
+    i := i + 1
+    if n > 15 then return 42
+  return b
+
+theorem blah : let i := 1; ¬(n = 0) → i ≤ n := by intro _ h; have : _ := Nat.succ_le_of_lt (Nat.zero_lt_of_ne_zero h); assumption
+
+theorem fib_correct : fib_impl n = fib_spec n := by
+  unfold fib_impl
+  split -- if_split n = 0
+  case isTrue  h => simp[h, fib_spec]; exact (Id.pure_eq 0)
+  case isFalse h =>
+  let_mut_intro i a b' -- i = 1, a = 0, b' = 0.
+  let_mut_upd b        -- b = b' + 1
+  while_inv (1 ≤ i ∧ i ≤ n ∧ a = fib_spec (i-1) ∧ b = fib_spec i)
+  case base => by
+    -- goal: show invariant
+    -- (weirdness: hcond and hind are not in scope here!
+    rw[Nat.sub_self, fib_spec, fib_spec]; sorry
+  case induct hcond hinv => by
+    -- hcond : i < n
+    -- hinv : ...
+    -- goal: new(hinv). Q: How do we display this in the goal view?
+    let_intro a' ha'  -- ha' : a' = a.     Very similar to intro?
+    let_mut_upd a ha  -- ha : a = b         (a' = a†, hcond = ..., hinv = ...)
+    let_mut_upd b hb  -- hb : b = a' + b†   (a = b†, ...)
+    let_mut_upd i hi  -- hi : i = i† + 1
+    -- Now:
+    -- hcond : i† < n
+    -- hinv : 1 ≤ i† ∧ i ≤ n ∧ a† = fib_spec (i†-1) ∧ b† = fib_spec i†
+    have hi1 : i > 1              := by ... hi ... hinv ...
+    have     : i ≤ n              := by ... hi ... hinv ...
+    have     : a = fib_spec (i-1) := by rw[ha, hinv, hi]
+    have     : b = fib_spec i     := by rw[hb, ha', hinv, hinv, (fib_spec_rec hi1).symm]
+    show 1 ≤ i ∧ i ≤ n ∧ a = fib_spec (i-1) ∧ b = fib_spec i
+    by ⟨by simp_arith[hi1], by assumption, by assumption, by assumption⟩
+  intro (hafter : ¬(i < n))
+  intro (hinv : ...)
+  have i = n          := by simp[hinv, hafter]
+  have b = fib_spec n := by simp[this, hinv]
+  return_post this
+
+theorem fib_correct_david : fib_impl n = fib_spec n := by
+  unfold fib_impl
+  do =>
+    if n = 0 then by simp[h, fib_spec]
+    let mut i a b'
+    b := _
+    while hcond -- : i < n
+          (n - i)
+          (hinv : 1 ≤ i ∧ i ≤ n ∧ a = fib_spec (i-1) ∧ b = fib_spec i)
+          (by grind ... /- show inv in base case; hinv not in scope here... -/) do
+      let a'
+      assume a = b;
+      a := _
+      ----
+
+      ---
+      b := _
+      i := _
+      continue (by ... : 1 ≤ i ∧ i ≤ n ∧ a = fib_spec (i-1) ∧ b = fib_spec i)  /- show inv in inductive case, using old(hinv) and hcond -/)
+    return (by ... : b = fib_spec n)
+
+def fib_correct_wlp  : fib_impl n = fib_spec n := Id.run_satisfies2 by
+  wlp
+    termination first_loop: ...
+    invariant   first_loop: 1 ≤ i ∧ i ≤ n ∧ a = fib_spec (i-1) ∧ b = fib_spec i
+    by
+      /- X goals -/
+      grind
+
+def fib_impl_intrinsic (n : Nat) := Id.run do
+  if n = 0 then return 0
+  let mut i := 1
+  let mut a := 0
+  let mut b := 0
+  b := b + 1
+  while i < n
+    invariant 1 ≤ i
+    invariant i ≤ n
+    invariant a = fib_spec (i-1)
+    invariant b = fib_spec i
+    do
+    let a' := a
+    a := b
+    b := a' + b
+    i := i + 1
+  return b
+-/

src/Init/Data/List/Lemmas.lean

@@ -2546,20 +2546,24 @@ theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : List
     simp only [filterMap_cons, foldr_cons]
     cases f a <;> simp [ih]
 
-theorem foldl_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
+theorem foldl_map_hom (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
     (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
     (l.map g).foldl f' (g a) = g (l.foldl f a) := by
   induction l generalizing a
   · simp
   · simp [*, h]
 
-theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
+@[deprecated foldl_map_hom (since := "2025-01-20")] abbrev foldl_map' := @foldl_map_hom
+
+theorem foldr_map_hom (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
     (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
     (l.map g).foldr f' (g a) = g (l.foldr f a) := by
   induction l generalizing a
   · simp
   · simp [*, h]
 
+@[deprecated foldr_map_hom (since := "2025-01-20")] abbrev foldr_map' := @foldr_map_hom
+
 @[simp] theorem foldrM_append [Monad m] [LawfulMonad m] (f : α → β → m β) (b) (l l' : List α) :
     (l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f := by
   induction l <;> simp [*]

src/Init/Data/Vector/Lemmas.lean

@@ -1866,6 +1866,222 @@ theorem flatMap_reverse {β} (l : Vector α n) (f : α → Vector β m) :
   rw [← toArray_inj]
   simp
 
+/-! ### extract -/
+
+@[simp] theorem getElem_extract {as : Vector α n} {start stop : Nat}
+    (h : i < min stop n - start) :
+    (as.extract start stop)[i] = as[start + i] := by
+  rcases as with ⟨as, rfl⟩
+  simp
+
+theorem getElem?_extract {as : Vector α n} {start stop : Nat} :
+    (as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none := by
+  rcases as with ⟨as, rfl⟩
+  simp [Array.getElem?_extract]
+
+@[simp] theorem extract_size (as : Vector α n) : as.extract 0 n = as.cast (by simp) := by
+  rcases as with ⟨as, rfl⟩
+  simp
+
+theorem extract_empty (start stop : Nat) :
+    (#v[] : Vector α 0).extract start stop = #v[].cast (by simp) := by
+  simp
+
+/-! ### foldlM and foldrM -/
+
+@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l : Vector α n) (l' : Vector α k) :
+    (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', rfl⟩
+  simp
+
+@[simp] theorem foldlM_empty [Monad m] (f : β → α → m β) (init : β) :
+    foldlM f init #v[] = return init := by
+  simp [foldlM]
+
+@[simp] theorem foldrM_empty [Monad m] (f : α → β → m β) (init : β) :
+    foldrM f init #v[] = return init := by
+  simp [foldrM]
+
+@[simp] theorem foldlM_push [Monad m] [LawfulMonad m] (l : Vector α n) (a : α) (f : β → α → m β) (b) :
+    (l.push a).foldlM f b = l.foldlM f b >>= fun b => f b a := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+theorem foldl_eq_foldlM (f : β → α → β) (b) (l : Vector α n) :
+    l.foldl f b = l.foldlM (m := Id) f b := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldl_eq_foldlM]
+
+theorem foldr_eq_foldrM (f : α → β → β) (b) (l : Vector α n) :
+    l.foldr f b = l.foldrM (m := Id) f b := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldr_eq_foldrM]
+
+@[simp] theorem id_run_foldlM (f : β → α → Id β) (b) (l : Vector α n) :
+    Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm
+
+@[simp] theorem id_run_foldrM (f : α → β → Id β) (b) (l : Vector α n) :
+    Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm
+
+@[simp] theorem foldlM_reverse [Monad m] (l : Vector α n) (f : β → α → m β) (b) :
+    l.reverse.foldlM f b = l.foldrM (fun x y => f y x) b := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldlM_reverse]
+
+@[simp] theorem foldrM_reverse [Monad m] (l : Vector α n) (f : α → β → m β) (b) :
+    l.reverse.foldrM f b = l.foldlM (fun x y => f y x) b := by
+  rcases l with ⟨l, rfl⟩
+  simp
+
+@[simp] theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Vector α n) (a : α) :
+    (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
+  rcases arr with ⟨arr, rfl⟩
+  simp [Array.foldrM_push]
+
+/-! ### foldl / foldr -/
+
+@[congr]
+theorem foldl_congr {as bs : Vector α n} (h₀ : as = bs) {f g : β → α → β} (h₁ : f = g)
+     {a b : β} (h₂ : a = b) :
+    as.foldl f a = bs.foldl g b := by
+  congr
+
+@[congr]
+theorem foldr_congr {as bs : Vector α n} (h₀ : as = bs) {f g : α → β → β} (h₁ : f = g)
+     {a b : β} (h₂ : a = b) :
+    as.foldr f a = bs.foldr g b := by
+  congr
+
+@[simp] theorem foldr_push (f : α → β → β) (init : β) (arr : Vector α n) (a : α) :
+    (arr.push a).foldr f init = arr.foldr f (f a init) := by
+  rcases arr with ⟨arr, rfl⟩
+  simp [Array.foldr_push]
+
+theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : Vector β₁ n) (init : α) :
+    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
+  cases l; simp [Array.foldl_map']
+
+theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : Vector α₁ n) (init : β) :
+    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
+  cases l; simp [Array.foldr_map']
+
+theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : Vector α n) (init : γ) :
+    (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldl_filterMap']
+  rfl
+
+theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : Vector α n) (init : γ) :
+    (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldr_filterMap']
+  rfl
+
+theorem foldl_map_hom (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : Vector α n)
+    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
+    (l.map g).foldl f' (g a) = g (l.foldl f a) := by
+  rcases l with ⟨l, rfl⟩
+  simp
+  rw [Array.foldl_map_hom' _ _ _ _ _ h rfl]
+
+theorem foldr_map_hom (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : Vector α n)
+    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
+    (l.map g).foldr f' (g a) = g (l.foldr f a) := by
+  rcases l with ⟨l, rfl⟩
+  simp
+  rw [Array.foldr_map_hom' _ _ _ _ _ h rfl]
+
+@[simp] theorem foldrM_append [Monad m] [LawfulMonad m] (f : α → β → m β) (b) (l : Vector α n) (l' : Vector α k) :
+    (l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f := by
+  rcases l with ⟨l, rfl⟩
+  rcases l' with ⟨l', rfl⟩
+  simp
+
+@[simp] theorem foldl_append {β : Type _} (f : β → α → β) (b) (l : Vector α n) (l' : Vector α k) :
+    (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
+
+@[simp] theorem foldr_append (f : α → β → β) (b) (l : Vector α n) (l' : Vector α k) :
+    (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
+
+@[simp] theorem foldl_flatten (f : β → α → β) (b : β) (L : Vector (Vector α m) n) :
+    (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
+  cases L using vector₂_induction
+  simp [Array.foldl_flatten', Array.foldl_map']
+
+@[simp] theorem foldr_flatten (f : α → β → β) (b : β) (L : Vector (Vector α m) n) :
+    (flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by
+  cases L using vector₂_induction
+  simp [Array.foldr_flatten', Array.foldr_map']
+
+@[simp] theorem foldl_reverse (l : Vector α n) (f : β → α → β) (b) :
+    l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
+
+@[simp] theorem foldr_reverse (l : Vector α n) (f : α → β → β) (b) :
+    l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
+  (foldl_reverse ..).symm.trans <| by simp
+
+theorem foldl_eq_foldr_reverse (l : Vector α n) (f : β → α → β) (b) :
+    l.foldl f b = l.reverse.foldr (fun x y => f y x) b := by simp
+
+theorem foldr_eq_foldl_reverse (l : Vector α n) (f : α → β → β) (b) :
+    l.foldr f b = l.reverse.foldl (fun x y => f y x) b := by simp
+
+theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] {l : Vector α n} {a₁ a₂} :
+     l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂) := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldl_assoc]
+
+@[simp] theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] {l : Vector α n} {a₁ a₂} :
+    l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂ := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.foldr_assoc]
+
+theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : Vector β n) (init : α₁)
+    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
+  rcases l with ⟨l, rfl⟩
+  simp
+  rw [Array.foldl_hom _ _ _ _ _ H]
+
+theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : Vector α n) (init : β₁)
+    (H : ∀ x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init) := by
+  cases l
+  simp
+  rw [Array.foldr_hom _ _ _ _ _ H]
+
+/--
+We can prove that two folds over the same array are related (by some arbitrary relation)
+if we know that the initial elements are related and the folding function, for each element of the array,
+preserves the relation.
+-/
+theorem foldl_rel {l : Array α} {f g : β → α → β} {a b : β} (r : β → β → Prop)
+    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
+    r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
+  rcases l with ⟨l⟩
+  simpa using List.foldl_rel r h (by simpa using h')
+
+/--
+We can prove that two folds over the same array are related (by some arbitrary relation)
+if we know that the initial elements are related and the folding function, for each element of the array,
+preserves the relation.
+-/
+theorem foldr_rel {l : Array α} {f g : α → β → β} {a b : β} (r : β → β → Prop)
+    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
+    r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
+  rcases l with ⟨l⟩
+  simpa using List.foldr_rel r h (by simpa using h')
+
+@[simp] theorem foldl_add_const (l : Array α) (a b : Nat) :
+    l.foldl (fun x _ => x + a) b = b + a * l.size := by
+  rcases l with ⟨l⟩
+  simp
+
+@[simp] theorem foldr_add_const (l : Array α) (a b : Nat) :
+    l.foldr (fun _ x => x + a) b = b + a * l.size := by
+  rcases l with ⟨l⟩
+  simp
+
+
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 @[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
@@ -1896,13 +2112,6 @@ defeq issues in the implicit size argument.
     subst h
     simp [back]
 
-/-! ### extract -/
-
-@[simp] theorem getElem_extract (a : Vector α n) (start stop) (i : Nat) (hi : i < min stop n - start) :
-    (a.extract start stop)[i] = a[start + i] := by
-  cases a
-  simp
-
 /-! ### zipWith -/
 
 @[simp] theorem getElem_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) (i : Nat)
@@ -1911,37 +2120,6 @@ defeq issues in the implicit size argument.
   cases b
   simp
 
-/-! ### foldlM and foldrM -/
-
-@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l : Vector α n) (l' : Vector α n') :
-    (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
-  cases l
-  cases l'
-  simp
-
-@[simp] theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (l : Vector α n) (a : α) :
-    (l.push a).foldrM f init = f a init >>= l.foldrM f := by
-  cases l
-  simp
-
-theorem foldl_eq_foldlM (f : β → α → β) (b) (l : Vector α n) :
-    l.foldl f b = l.foldlM (m := Id) f b := by
-  cases l
-  simp [Array.foldl_eq_foldlM]
-
-theorem foldr_eq_foldrM (f : α → β → β) (b) (l : Vector α n) :
-    l.foldr f b = l.foldrM (m := Id) f b := by
-  cases l
-  simp [Array.foldr_eq_foldrM]
-
-@[simp] theorem id_run_foldlM (f : β → α → Id β) (b) (l : Vector α n) :
-    Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm
-
-@[simp] theorem id_run_foldrM (f : α → β → Id β) (b) (l : Vector α n) :
-    Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm
-
-/-! ### foldl and foldr -/
-
 /-! ### take -/
 
 @[simp] theorem take_size (a : Vector α n) : a.take n = a.cast (by simp) := by

src/Init/Grind/Tactics.lean

@@ -11,12 +11,15 @@ namespace Lean.Parser.Attr
 syntax grindEq     := "="
 syntax grindEqBoth := atomic("_" "=" "_")
 syntax grindEqRhs  := atomic("=" "_")
+syntax grindEqBwd  := atomic("←" "=")
 syntax grindBwd    := "←"
 syntax grindFwd    := "→"
+syntax grindCases  := &"cases"
+syntax grindCasesEager := atomic(&"cases" &"eager")
 
-syntax grindThmMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindBwd <|> grindFwd
+syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindCasesEager <|> grindCases
 
-syntax (name := grind) "grind" (grindThmMod)? : attr
+syntax (name := grind) "grind" (grindMod)? : attr
 
 end Lean.Parser.Attr
 
@@ -64,7 +67,7 @@ namespace Lean.Parser.Tactic
 -/
 
 syntax grindErase := "-" ident
-syntax grindLemma := (Attr.grindThmMod)? ident
+syntax grindLemma := (Attr.grindMod)? ident
 syntax grindParam := grindErase <|> grindLemma
 
 syntax (name := grind)

src/Init/Grind/Util.lean

@@ -21,6 +21,9 @@ def doNotSimp {α : Sort u} (a : α) : α := a
 /-- Gadget for representing offsets `t+k` in patterns. -/
 def offset (a b : Nat) : Nat := a + b
 
+/-- Gadget for representing `a = b` in patterns for backward propagation. -/
+def eqBwdPattern (a b : α) : Prop := a = b
+
 /--
 Gadget for annotating the equalities in `match`-equations conclusions.
 `_origin` is the term used to instantiate the `match`-equation using E-matching.

src/Lean/Elab/Tactic/Grind.lean

@@ -51,41 +51,52 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
     match p with
     | `(Parser.Tactic.grindParam| - $id:ident) =>
       let declName ← realizeGlobalConstNoOverloadWithInfo id
-      if (← isInductivePredicate declName) then
-        throwErrorAt p "NIY"
+      if (← Grind.isCasesAttrCandidate declName false) then
+        params := { params with casesTypes := (← params.casesTypes.eraseDecl declName) }
       else
         params := { params with ematch := (← params.ematch.eraseDecl declName) }
-    | `(Parser.Tactic.grindParam| $[$mod?:grindThmMod]? $id:ident) =>
+    | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) =>
       let declName ← realizeGlobalConstNoOverloadWithInfo id
-      let kind ← if let some mod := mod? then Grind.getTheoremKindCore mod else pure .default
-      if (← isInductivePredicate declName) then
-        throwErrorAt p "NIY"
-      else
-        let info ← getConstInfo declName
-        match info with
-        | .thmInfo _ =>
-          if kind == .eqBoth then
-            params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqLhs) }
-            params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqRhs) }
-          else
-            params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind) }
-        | .defnInfo _ =>
-          if (← isReducible declName) then
-            throwErrorAt p "`{declName}` is a reducible definition, `grind` automatically unfolds them"
-          if kind != .eqLhs && kind != .default then
-            throwErrorAt p "invalid `grind` parameter, `{declName}` is a definition, the only acceptable (and redundant) modifier is '='"
-          let some thms ← Grind.mkEMatchEqTheoremsForDef? declName
-            | throwErrorAt p "failed to genereate equation theorems for `{declName}`"
-          params := { params with extra := params.extra ++ thms.toPArray' }
-        | _ =>
-          throwErrorAt p "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type"
+      let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer
+      match kind with
+      | .ematch kind =>
+        params ← withRef p <| addEMatchTheorem params declName kind
+      | .cases eager =>
+        withRef p <| Grind.validateCasesAttr declName eager
+        params := { params with casesTypes := params.casesTypes.insert declName eager }
+      | .infer =>
+        if (← Grind.isCasesAttrCandidate declName false) then
+          params := { params with casesTypes := params.casesTypes.insert declName false }
+        else
+          params ← withRef p <| addEMatchTheorem params declName .default
     | _ => throwError "unexpected `grind` parameter{indentD p}"
   return params
+where
+  addEMatchTheorem (params : Grind.Params) (declName : Name) (kind : Grind.TheoremKind) : MetaM Grind.Params := do
+    let info ← getConstInfo declName
+    match info with
+    | .thmInfo _ =>
+      if kind == .eqBoth then
+        let params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqLhs) }
+        return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqRhs) }
+      else
+        return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind) }
+    | .defnInfo _ =>
+      if (← isReducible declName) then
+        throwError "`{declName}` is a reducible definition, `grind` automatically unfolds them"
+      if kind != .eqLhs && kind != .default then
+        throwError "invalid `grind` parameter, `{declName}` is a definition, the only acceptable (and redundant) modifier is '='"
+      let some thms ← Grind.mkEMatchEqTheoremsForDef? declName
+        | throwError "failed to genereate equation theorems for `{declName}`"
+      return { params with extra := params.extra ++ thms.toPArray' }
+    | _ =>
+      throwError "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type"
 
 def mkGrindParams (config : Grind.Config) (only : Bool) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do
   let params ← Grind.mkParams config
   let ematch ← if only then pure {} else Grind.getEMatchTheorems
-  let params := { params with ematch }
+  let casesTypes ← if only then pure {} else Grind.getCasesTypes
+  let params := { params with ematch, casesTypes }
   elabGrindParams params ps
 
 def grind

src/Lean/Meta/Basic.lean

@@ -1264,7 +1264,7 @@ private def fvarsSizeLtMaxFVars (fvars : Array Expr) (maxFVars? : Option Nat) :
 
 mutual
   /--
-    `withNewLocalInstances isClassExpensive fvars j k` updates the vector or local instances
+    `withNewLocalInstances isClassExpensive fvars j k` updates the vector of local instances
     using free variables `fvars[j] ... fvars.back`, and execute `k`.
 
     - `isClassExpensive` is defined later.

src/Lean/Meta/Tactic.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Intro
+import Lean.Meta.Tactic.LiftLets
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.Tactic.Apply

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

@@ -4,12 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.Tactic.Simp.Attr
-import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Grind.EMatchTheorem
+import Lean.Meta.Tactic.Grind.Cases
 
 namespace Lean.Meta.Grind
-open Simp
-
+--- TODO: delete
 builtin_initialize grindCasesExt : SimpleScopedEnvExtension Name NameSet ←
   registerSimpleScopedEnvExtension {
     initial        := {}
@@ -59,5 +58,68 @@ builtin_initialize
       validateGrindCasesAttr declName
       grindCasesExt.add declName attrKind
   }
+--- END of TODO: detele
+
+inductive AttrKind where
+  | ematch (k : TheoremKind)
+  | cases (eager : Bool)
+  | infer
+
+/-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/
+def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do
+  match stx with
+  | `(Parser.Attr.grindMod| =) => return .ematch .eqLhs
+  | `(Parser.Attr.grindMod| →) => return .ematch .fwd
+  | `(Parser.Attr.grindMod| ←) => return .ematch .bwd
+  | `(Parser.Attr.grindMod| =_) => return .ematch .eqRhs
+  | `(Parser.Attr.grindMod| _=_) => return .ematch .eqBoth
+  | `(Parser.Attr.grindMod| ←=) => return .ematch .eqBwd
+  | `(Parser.Attr.grindMod| cases) => return .cases false
+  | `(Parser.Attr.grindMod| cases eager) => return .cases true
+  | _ => throwError "unexpected `grind` theorem kind: `{stx}`"
+
+/-- Return theorem kind for `stx` of the form `(Attr.grindMod)?` -/
+def getAttrKindFromOpt (stx : Syntax) : CoreM AttrKind := do
+  if stx[1].isNone then
+    return .infer
+  else
+    getAttrKindCore stx[1][0]
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name := `grind
+    descr :=
+      "The `[grind]` attribute is used to annotate declarations.\
+      \
+      When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`\
+      will mark the theorem for use in heuristic instantiations by the `grind` tactic,
+      using respectively the left-hand side, the right-hand side, or both sides of the theorem.\
+      When applied to a function, `[grind =]` automatically annotates the equational theorems associated with that function.\
+      When applied to a theorem `[grind ←]` will instantiate the theorem whenever it encounters the conclusion of the theorem
+      (that is, it will use the theorem for backwards reasoning).\
+      When applied to a theorem `[grind →]` will instantiate the theorem whenever it encounters sufficiently many of the propositional hypotheses
+      (that is, it will use the theorem for forwards reasoning).\
+      \
+      The attribute `[grind]` by itself will effectively try `[grind ←]` (if the conclusion is sufficient for instantiation) and then `[grind →]`.\
+      \
+      The `grind` tactic utilizes annotated theorems to add instances of matching patterns into the local context during proof search.\
+      For example, if a theorem `@[grind =] theorem foo_idempotent : foo (foo x) = foo x` is annotated,\
+      `grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`."
+    applicationTime := .afterCompilation
+    add := fun declName stx attrKind => MetaM.run' do
+      match (← getAttrKindFromOpt stx) with
+      | .ematch k => addEMatchAttr declName attrKind k
+      | .cases eager => addCasesAttr declName eager attrKind
+      | .infer =>
+        if (← isCasesAttrCandidate declName false) then
+          addCasesAttr declName false attrKind
+        else
+          addEMatchAttr declName attrKind .default
+    erase := fun declName => MetaM.run' do
+      if (← isCasesAttrCandidate declName false) then
+        eraseCasesAttr declName
+      else
+        eraseEMatchAttr declName
+  }
 
 end Lean.Meta.Grind

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

@@ -7,6 +7,79 @@ prelude
 import Lean.Meta.Tactic.Cases
 
 namespace Lean.Meta.Grind
+
+/-- Types that `grind` will case-split on. -/
+structure CasesTypes where
+  casesMap : PHashMap Name Bool := {}
+  deriving Inhabited
+
+structure CasesEntry where
+  declName : Name
+  eager : Bool
+  deriving Inhabited
+
+/-- Returns `true` if `s` contains a `declName`. -/
+def CasesTypes.contains (s : CasesTypes) (declName : Name) : Bool :=
+  s.casesMap.contains declName
+
+/-- Removes the given declaration from `s`. -/
+def CasesTypes.erase (s : CasesTypes) (declName : Name) : CasesTypes :=
+  { s with casesMap := s.casesMap.erase declName }
+
+def CasesTypes.insert (s : CasesTypes) (declName : Name) (eager : Bool) : CasesTypes :=
+  { s with casesMap := s.casesMap.insert declName eager }
+
+def CasesTypes.find? (s : CasesTypes) (declName : Name) : Option Bool :=
+  s.casesMap.find? declName
+
+builtin_initialize casesExt : SimpleScopedEnvExtension CasesEntry CasesTypes ←
+  registerSimpleScopedEnvExtension {
+    initial        := {}
+    addEntry       := fun s {declName, eager} => s.insert declName eager
+  }
+
+def getCasesTypes : CoreM CasesTypes :=
+  return casesExt.getState (← getEnv)
+
+private def getAlias? (value : Expr) : MetaM (Option Name) :=
+  lambdaTelescope value fun _ body => do
+    if let .const declName _ := body.getAppFn' then
+      return some declName
+    else
+      return none
+
+partial def isCasesAttrCandidate (declName : Name) (eager : Bool) : CoreM Bool := do
+  match (← getConstInfo declName) with
+  | .inductInfo info => return !info.isRec || !eager
+  | .defnInfo info =>
+    let some declName ← getAlias? info.value |>.run' {} {}
+      | return false
+    isCasesAttrCandidate declName eager
+  | _ => return false
+
+def validateCasesAttr (declName : Name) (eager : Bool) : CoreM Unit := do
+  unless (← isCasesAttrCandidate declName eager) do
+    if eager then
+      throwError "invalid `[grind cases eager]`, `{declName}` is not a non-recursive inductive datatype or an alias for one"
+    else
+      throwError "invalid `[grind cases]`, `{declName}` is not an inductive datatype or an alias for one"
+
+def addCasesAttr (declName : Name) (eager : Bool) (attrKind : AttributeKind) : CoreM Unit := do
+  validateCasesAttr declName eager
+  casesExt.add { declName, eager } attrKind
+
+def CasesTypes.eraseDecl (s : CasesTypes) (declName : Name) : CoreM CasesTypes := do
+  if s.contains declName then
+    return s.erase declName
+  else
+    throwError "`{declName}` is not marked with the `[grind]` attribute"
+
+def eraseCasesAttr (declName : Name) : CoreM Unit := do
+  let s := casesExt.getState (← getEnv)
+  let s ← s.eraseDecl declName
+  modifyEnv fun env => casesExt.modifyState env fun _ => s
+
+
 /--
 The `grind` tactic includes an auxiliary `cases` tactic that is not intended for direct use by users.
 This method implements it.

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

@@ -310,12 +310,44 @@ private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
           modify fun s => { s with choiceStack := [c] }
           processChoices
 
+/--
+Entry point for matching `lhs ←= rhs` patterns.
+It traverses disequalities `a = b`, and tries to solve two matching problems:
+1- match `lhs` with `a` and `rhs` with `b`
+2- match `lhs` with `b` and `rhs` with `a`
+-/
+private def matchEqBwdPat (p : Expr) : M Unit := do
+  let_expr Grind.eqBwdPattern pα plhs prhs := p | return ()
+  let numParams  := (← read).thm.numParams
+  let assignment := mkArray numParams unassigned
+  let useMT      := (← read).useMT
+  let gmt        := (← getThe Goal).gmt
+  let false      ← getFalseExpr
+  let mut curr   := false
+  repeat
+    if (← checkMaxInstancesExceeded) then return ()
+    let n ← getENode curr
+    if (n.heqProofs || n.isCongrRoot) &&
+       (!useMT || n.mt == gmt) then
+      let_expr Eq α lhs rhs := n.self | pure ()
+      if (← isDefEq α pα) then
+         let c₀ : Choice := { cnstrs := [], assignment, gen := n.generation }
+         let go (lhs rhs : Expr) : M Unit := do
+           let some c₁ ← matchArg? c₀ plhs lhs |>.run | return ()
+           let some c₂ ← matchArg? c₁ prhs rhs |>.run | return ()
+           modify fun s => { s with choiceStack := [c₂] }
+           processChoices
+         go lhs rhs
+         go rhs lhs
+    if isSameExpr n.next false then return ()
+    curr := n.next
+
 def ematchTheorem (thm : EMatchTheorem) : M Unit := do
   if (← checkMaxInstancesExceeded) then return ()
   withReader (fun ctx => { ctx with thm }) do
     let ps := thm.patterns
     match ps, (← read).useMT with
-    | [p],   _     => main p []
+    | [p],   _     => if isEqBwdPattern p then matchEqBwdPat p else main p []
     | p::ps, false => main p (ps.map (.continue ·))
     | _::_,  true  => tryAll ps []
     | _,     _     => unreachable!

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

@@ -39,6 +39,17 @@ def isOffsetPattern? (pat : Expr) : Option (Expr × Nat) := Id.run do
   let .lit (.natVal k) := k | none
   return some (pat, k)
 
+def mkEqBwdPattern (u : List Level) (α : Expr) (lhs rhs : Expr) : Expr :=
+  mkApp3 (mkConst ``Grind.eqBwdPattern u) α lhs rhs
+
+def isEqBwdPattern (e : Expr) : Bool :=
+  e.isAppOfArity ``Grind.eqBwdPattern 3
+
+def isEqBwdPattern? (e : Expr) : Option (Expr × Expr) :=
+  let_expr Grind.eqBwdPattern _ lhs rhs := e
+    | none
+  some (lhs, rhs)
+
 def preprocessPattern (pat : Expr) (normalizePattern := true) : MetaM Expr := do
   let pat ← instantiateMVars pat
   let pat ← unfoldReducible pat
@@ -131,7 +142,7 @@ def EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchThe
 def EMatchTheorems.contains (s : EMatchTheorems) (origin : Origin) : Bool :=
   s.origins.contains origin
 
-/-- Mark the theorm with the given origin as `erased` -/
+/-- Mark the theorem with the given origin as `erased` -/
 def EMatchTheorems.erase (s : EMatchTheorems) (origin : Origin) : EMatchTheorems :=
   { s with erased := s.erased.insert origin, origins := s.origins.erase origin }
 
@@ -314,7 +325,8 @@ private partial def go (pattern : Expr) (root := false) : M Expr := do
   let some f := getPatternFn? pattern
     | throwError "invalid pattern, (non-forbidden) application expected{indentExpr pattern}"
   assert! f.isConst || f.isFVar
-  saveSymbol f.toHeadIndex
+  unless f.isConstOf ``Grind.eqBwdPattern do
+   saveSymbol f.toHeadIndex
   let mut args := pattern.getAppArgs.toVector
   let supportMask ← getPatternSupportMask f args.size
   for h : i in [:args.size] do
@@ -481,6 +493,8 @@ Pattern variables are represented using de Bruijn indices.
 -/
 def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr) (patterns : List Expr) : MetaM EMatchTheorem := do
   let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns
+  if symbols.isEmpty then
+    throwError "invalid pattern for `{← origin.pp}`{indentD (patterns.map ppPattern)}\nthe pattern does not contain constant symbols for indexing"
   trace[grind.ematch.pattern] "{MessageData.ofConst proof}: {patterns.map ppPattern}"
   if let .missing pos ← checkCoverage proof numParams bvarFound then
      let pats : MessageData := m!"{patterns.map ppPattern}"
@@ -523,6 +537,14 @@ def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof :
     return (xs.size, pats)
   mkEMatchTheoremCore origin levelParams numParams proof patterns
 
+def mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) : MetaM EMatchTheorem := do
+  let (numParams, patterns) ← forallTelescopeReducing (← inferType proof) fun xs type => do
+    let_expr f@Eq α lhs rhs := type
+      | throwError "invalid E-matching `≠` theorem, conclusion must be an equality{indentExpr type}"
+    let pat ← preprocessPattern (mkEqBwdPattern f.constLevels! α lhs rhs)
+    return (xs.size, [pat.abstract xs])
+  mkEMatchTheoremCore origin levelParams numParams proof patterns
+
 /--
 Given theorem with name `declName` and type of the form `∀ (a_1 ... a_n), lhs = rhs`,
 creates an E-matching pattern for it using `addEMatchTheorem n [lhs]`
@@ -552,13 +574,14 @@ def getEMatchTheorems : CoreM EMatchTheorems :=
   return ematchTheoremsExt.getState (← getEnv)
 
 inductive TheoremKind where
-  | eqLhs | eqRhs | eqBoth | fwd | bwd | default
+  | eqLhs | eqRhs | eqBoth | eqBwd | fwd | bwd | default
   deriving Inhabited, BEq, Repr
 
 private def TheoremKind.toAttribute : TheoremKind → String
   | .eqLhs   => "[grind =]"
   | .eqRhs   => "[grind =_]"
   | .eqBoth  => "[grind _=_]"
+  | .eqBwd   => "[grind ←=]"
   | .fwd     => "[grind →]"
   | .bwd     => "[grind ←]"
   | .default => "[grind]"
@@ -567,6 +590,7 @@ private def TheoremKind.explainFailure : TheoremKind → String
   | .eqLhs   => "failed to find pattern in the left-hand side of the theorem's conclusion"
   | .eqRhs   => "failed to find pattern in the right-hand side of the theorem's conclusion"
   | .eqBoth  => unreachable! -- eqBoth is a macro
+  | .eqBwd   => "failed to use theorem's conclusion as a pattern"
   | .fwd     => "failed to find patterns in the antecedents of the theorem"
   | .bwd     => "failed to find patterns in the theorem's conclusion"
   | .default => "failed to find patterns"
@@ -656,6 +680,8 @@ def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof
     return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true))
   else if kind == .eqRhs then
     return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := false))
+  else if kind == .eqBwd then
+    return (← mkEMatchEqBwdTheoremCore origin levelParams proof)
   let type ← inferType proof
   forallTelescopeReducing type fun xs type => do
     let searchPlaces ← match kind with
@@ -679,23 +705,6 @@ where
       levelParams, origin
     }
 
-/-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/
-def getTheoremKindCore (stx : Syntax) : CoreM TheoremKind := do
-  match stx with
-  | `(Parser.Attr.grindThmMod| =) => return .eqLhs
-  | `(Parser.Attr.grindThmMod| →) => return .fwd
-  | `(Parser.Attr.grindThmMod| ←) => return .bwd
-  | `(Parser.Attr.grindThmMod| =_) => return .eqRhs
-  | `(Parser.Attr.grindThmMod| _=_) => return .eqBoth
-  | _ => throwError "unexpected `grind` theorem kind: `{stx}`"
-
-/-- Return theorem kind for `stx` of the form `(Attr.grindThmMod)?` -/
-def getTheoremKindFromOpt (stx : Syntax) : CoreM TheoremKind := do
-  if stx[1].isNone then
-    return .default
-  else
-    getTheoremKindCore stx[1][0]
-
 def mkEMatchTheoremForDecl (declName : Name) (thmKind : TheoremKind) : MetaM EMatchTheorem := do
   let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind
     | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
@@ -716,20 +725,6 @@ private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind
   else
     throwError s!"`{thmKind.toAttribute}` attribute can only be applied to equational theorems or function definitions"
 
-private def addGrindAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) : MetaM Unit := do
-  if thmKind == .eqLhs then
-    addGrindEqAttr declName attrKind thmKind (useLhs := true)
-  else if thmKind == .eqRhs then
-    addGrindEqAttr declName attrKind thmKind (useLhs := false)
-  else if thmKind == .eqBoth then
-    addGrindEqAttr declName attrKind thmKind (useLhs := true)
-    addGrindEqAttr declName attrKind thmKind (useLhs := false)
-  else if !(← getConstInfo declName).isTheorem then
-    addGrindEqAttr declName attrKind thmKind
-  else
-    let thm ← mkEMatchTheoremForDecl declName thmKind
-    ematchTheoremsExt.add thm attrKind
-
 def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMatchTheorems := do
   let throwErr {α} : MetaM α :=
     throwError "`{declName}` is not marked with the `[grind]` attribute"
@@ -747,47 +742,37 @@ def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMat
       throwErr
     return s.erase <| .decl declName
 
-builtin_initialize
-  registerBuiltinAttribute {
-    name := `grind
-    descr :=
-      "The `[grind]` attribute is used to annotate declarations.\
-      \
-      When applied to an equational theorem, `[grind =]`, `[grind =_]`, or `[grind _=_]`\
-      will mark the theorem for use in heuristic instantiations by the `grind` tactic,
-      using respectively the left-hand side, the right-hand side, or both sides of the theorem.\
-      When applied to a function, `[grind =]` automatically annotates the equational theorems associated with that function.\
-      When applied to a theorem `[grind ←]` will instantiate the theorem whenever it encounters the conclusion of the theorem
-      (that is, it will use the theorem for backwards reasoning).\
-      When applied to a theorem `[grind →]` will instantiate the theorem whenever it encounters sufficiently many of the propositional hypotheses
-      (that is, it will use the theorem for forwards reasoning).\
-      \
-      The attribute `[grind]` by itself will effectively try `[grind ←]` (if the conclusion is sufficient for instantiation) and then `[grind →]`.\
-      \
-      The `grind` tactic utilizes annotated theorems to add instances of matching patterns into the local context during proof search.\
-      For example, if a theorem `@[grind =] theorem foo_idempotent : foo (foo x) = foo x` is annotated,\
-      `grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`."
-    applicationTime := .afterCompilation
-    add := fun declName stx attrKind => do
-      addGrindAttr declName attrKind (← getTheoremKindFromOpt stx) |>.run' {}
-    erase := fun declName => MetaM.run' do
-      /-
-      Remark: consider the following example
-      ```
-      attribute [grind] foo  -- ok
-      attribute [-grind] foo.eqn_2  -- ok
-      attribute [-grind] foo  -- error
-      ```
-      One may argue that the correct behavior should be
-      ```
-      attribute [grind] foo  -- ok
-      attribute [-grind] foo.eqn_2  -- error
-      attribute [-grind] foo  -- ok
-      ```
-      -/
-      let s := ematchTheoremsExt.getState (← getEnv)
-      let s ← s.eraseDecl declName
-      modifyEnv fun env => ematchTheoremsExt.modifyState env fun _ => s
-  }
+def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) : MetaM Unit := do
+  if thmKind == .eqLhs then
+    addGrindEqAttr declName attrKind thmKind (useLhs := true)
+  else if thmKind == .eqRhs then
+    addGrindEqAttr declName attrKind thmKind (useLhs := false)
+  else if thmKind == .eqBoth then
+    addGrindEqAttr declName attrKind thmKind (useLhs := true)
+    addGrindEqAttr declName attrKind thmKind (useLhs := false)
+  else if !(← getConstInfo declName).isTheorem then
+    addGrindEqAttr declName attrKind thmKind
+  else
+    let thm ← mkEMatchTheoremForDecl declName thmKind
+    ematchTheoremsExt.add thm attrKind
+
+def eraseEMatchAttr (declName : Name) : MetaM Unit := do
+  /-
+  Remark: consider the following example
+  ```
+  attribute [grind] foo  -- ok
+  attribute [-grind] foo.eqn_2  -- ok
+  attribute [-grind] foo  -- error
+  ```
+  One may argue that the correct behavior should be
+  ```
+  attribute [grind] foo  -- ok
+  attribute [-grind] foo.eqn_2  -- error
+  attribute [-grind] foo  -- ok
+  ```
+  -/
+  let s := ematchTheoremsExt.getState (← getEnv)
+  let s ← s.eraseDecl declName
+  modifyEnv fun env => ematchTheoremsExt.modifyState env fun _ => s
 
 end Lean.Meta.Grind

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

@@ -17,15 +17,17 @@ import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.Split
 import Lean.Meta.Tactic.Grind.Solve
 import Lean.Meta.Tactic.Grind.SimpUtil
+import Lean.Meta.Tactic.Grind.Cases
 
 namespace Lean.Meta.Grind
 
 structure Params where
-  config    : Grind.Config
-  ematch    : EMatchTheorems := {}
-  extra     : PArray EMatchTheorem := {}
-  norm      : Simp.Context
-  normProcs : Array Simprocs
+  config     : Grind.Config
+  ematch     : EMatchTheorems := {}
+  casesTypes : CasesTypes := {}
+  extra      : PArray EMatchTheorem := {}
+  norm       : Simp.Context
+  normProcs  : Array Simprocs
   -- TODO: inductives to split
 
 def mkParams (config : Grind.Config) : MetaM Params := do

src/Lean/Meta/Tactic/LiftLets.lean

@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+
+import Lean.Elab.Tactic
+
+/-!
+# The `lift_lets` tactic
+
+This module defines a tactic `lift_lets` that can be used to pull `let` bindings as far out
+of an expression as possible.
+-/
+
+open Lean Elab Parser Meta Tactic
+
+/-- Configuration for `Lean.Expr.liftLets` and the `lift_lets` tactic. -/
+structure Lean.Expr.LiftLetsConfig where
+  /-- Whether to lift lets out of proofs. The default is not to. -/
+  proofs : Bool := false
+  /-- Whether to merge let bindings if they have the same type and value.
+  This test is by syntactic equality, not definitional equality.
+  The default is to merge. -/
+  merge : Bool := true
+
+/--
+Auxiliary definition for `Lean.Expr.liftLets`. Takes a list of the accumulated fvars.
+This list is used during the computation to merge let bindings.
+-/
+private partial def Lean.Expr.liftLetsAux (config : LiftLetsConfig) (e : Expr) (fvars : Array Expr)
+    (f : Array Expr → Expr → MetaM Expr) : MetaM Expr := do
+  if (e.find? Expr.isLet).isNone then
+    -- If `e` contains no `let` expressions, then we can avoid recursing into it.
+    return ← f fvars e
+  if !config.proofs then
+    if ← Meta.isProof e then
+      return ← f fvars e
+  match e with
+  | .letE n t v b _ =>
+    t.liftLetsAux config fvars fun fvars t' =>
+      v.liftLetsAux config fvars fun fvars v' => do
+        if config.merge then
+          -- Eliminate the let binding if there is already one of the same type and value.
+          let fvar? ← fvars.findM? (fun fvar => do
+            let decl ← fvar.fvarId!.getDecl
+            return decl.type == t' && decl.value? == some v')
+          if let some fvar' := fvar? then
+            return ← (b.instantiate1 fvar').liftLetsAux config fvars f
+        withLetDecl n t' v' fun fvar =>
+          (b.instantiate1 fvar).liftLetsAux config (fvars.push fvar) f
+  | .app x y =>
+    x.liftLetsAux config fvars fun fvars x' => y.liftLetsAux config fvars fun fvars y' =>
+      f fvars (.app x' y')
+  | .proj n idx s =>
+    s.liftLetsAux config fvars fun fvars s' => f fvars (.proj n idx s')
+  | .lam n t b i =>
+    t.liftLetsAux config fvars fun fvars t => do
+      -- Enter the binding, do liftLets, and lift out liftable lets
+      let e' ← withLocalDecl n i t fun fvar => do
+        (b.instantiate1 fvar).liftLetsAux config fvars fun fvars2 b => do
+          -- See which bindings can't be migrated out
+          let deps ← collectForwardDeps #[fvar] false
+          let fvars2 := fvars2[fvars.size:].toArray
+          let (fvars2, fvars2') := fvars2.partition deps.contains
+          mkLetFVars fvars2' (← mkLambdaFVars #[fvar] (← mkLetFVars fvars2 b))
+      -- Re-enter the new lets; we do it this way to keep the local context clean
+      insideLets e' fvars fun fvars e'' => f fvars e''
+  | .forallE n t b i =>
+    t.liftLetsAux config fvars fun fvars t => do
+      -- Enter the binding, do liftLets, and lift out liftable lets
+      let e' ← withLocalDecl n i t fun fvar => do
+        (b.instantiate1 fvar).liftLetsAux config fvars fun fvars2 b => do
+          -- See which bindings can't be migrated out
+          let deps ← collectForwardDeps #[fvar] false
+          let fvars2 := fvars2[fvars.size:].toArray
+          let (fvars2, fvars2') := fvars2.partition deps.contains
+          mkLetFVars fvars2' (← mkForallFVars #[fvar] (← mkLetFVars fvars2 b))
+      -- Re-enter the new lets; we do it this way to keep the local context clean
+      insideLets e' fvars fun fvars e'' => f fvars e''
+  | .mdata _ e => e.liftLetsAux config fvars f
+  | _ => f fvars e
+where
+  -- Like the whole `Lean.Expr.liftLets`, but only handles lets
+  insideLets {α} (e : Expr) (fvars : Array Expr) (f : Array Expr → Expr → MetaM α) : MetaM α := do
+    match e with
+    | .letE n t v b _ =>
+      withLetDecl n t v fun fvar => insideLets (b.instantiate1 fvar) (fvars.push fvar) f
+    | _ => f fvars e
+
+/-- Take all the `let`s in an expression and move them outwards as far as possible.
+All top-level `let`s are added to the local context, and then `f` is called with the list
+of local bindings (each an fvar) and the new expression.
+
+Let bindings are merged if they have the same type and value.
+
+Use `e.liftLets mkLetFVars` to get a defeq expression with all `let`s lifted as far as possible. -/
+def Lean.Expr.liftLets (e : Expr) (f : Array Expr → Expr → MetaM Expr)
+    (config : LiftLetsConfig := {}) : MetaM Expr :=
+  e.liftLetsAux config #[] f
+
+namespace Mathlib.Tactic
+
+declare_config_elab elabConfig Lean.Expr.LiftLetsConfig
+
+/--
+Lift all the `let` bindings in the type of an expression as far out as possible.
+
+When applied to the main goal, this gives one the ability to `intro` embedded `let` expressions.
+For example,
+```lean
+example : (let x := 1; x) = 1 := by
+  lift_lets
+  -- ⊢ let x := 1; x = 1
+  intro x
+  sorry
+```
+
+During the lifting process, let bindings are merged if they have the same type and value.
+-/
+syntax (name := lift_lets) "lift_lets" optConfig (ppSpace location)? : tactic
+
+elab_rules : tactic
+  | `(tactic| lift_lets $cfg:optConfig $[$loc:location]?) => do
+    let config ← elabConfig (mkOptionalNode cfg)
+    withLocation (expandOptLocation (Lean.mkOptionalNode loc))
+      (atLocal := fun h ↦ liftMetaTactic1 fun mvarId ↦ do
+        let hTy ← instantiateMVars (← h.getType)
+        mvarId.changeLocalDecl h (← hTy.liftLets mkLetFVars config))
+      (atTarget := liftMetaTactic1 fun mvarId ↦ do
+        let ty ← instantiateMVars (← mvarId.getType)
+        mvarId.change (← ty.liftLets mkLetFVars config))
+      (failed := fun _ ↦ throwError "lift_lets tactic failed")
+
+end Mathlib.Tactic

src/Lean/SubExpr.lean

@@ -105,7 +105,7 @@ def pushNaryFn (numArgs : Nat) (p : Pos) : Pos :=
   p.asNat * (maxChildren ^ numArgs)
 
 def pushNaryArg (numArgs argIdx : Nat) (p : Pos) : Pos :=
-  show Nat from p.asNat * (maxChildren ^ (numArgs - argIdx)) + 1
+  p.asNat * (maxChildren ^ (numArgs - argIdx)) + 1
 
 def pushNthBindingDomain : (binderIdx : Nat) → Pos → Pos
   | 0, p => p.pushBindingDomain

src/Std/Time/DateTime/PlainDateTime.lean

@@ -53,7 +53,7 @@ def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do
 
   let nanos := stamp.toNanosecondsSinceUnixEpoch
   let secs : Second.Offset := nanos.ediv 1000000000
-  let daysSinceEpoch : Day.Offset := secs.ediv 86400
+  let daysSinceEpoch : Day.Offset := secs.tdiv 86400
   let boundedDaysSinceEpoch := daysSinceEpoch
 
   let mut rawDays := boundedDaysSinceEpoch - leapYearEpoch
@@ -315,16 +315,26 @@ resulting month.
 def subYearsClip (dt : PlainDateTime) (years : Year.Offset) : PlainDateTime :=
   { dt with date := dt.date.subYearsClip years }
 
+/--
+Adds a `Nanosecond.Offset` to a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds overflow.
+-/
+@[inline]
+def addNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime :=
+  ofTimestampAssumingUTC (dt.toTimestampAssumingUTC + nanos)
+
+/--
+Subtracts a `Nanosecond.Offset` from a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds underflow.
+-/
+@[inline]
+def subNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime :=
+  addNanoseconds dt (-nanos)
 
 /--
 Adds an `Hour.Offset` to a `PlainDateTime`, adjusting the date if the hour overflows.
 -/
 @[inline]
 def addHours (dt : PlainDateTime) (hours : Hour.Offset) : PlainDateTime :=
-  let totalSeconds := dt.time.toSeconds + hours.toSeconds
-  let days := totalSeconds.ediv 86400
-  let newTime := dt.time.addSeconds (hours.toSeconds)
-  { dt with date := dt.date.addDays days, time := newTime }
+  addNanoseconds dt hours.toNanoseconds
 
 /--
 Subtracts an `Hour.Offset` from a `PlainDateTime`, adjusting the date if the hour underflows.
@@ -338,10 +348,7 @@ Adds a `Minute.Offset` to a `PlainDateTime`, adjusting the hour and date if the
 -/
 @[inline]
 def addMinutes (dt : PlainDateTime) (minutes : Minute.Offset) : PlainDateTime :=
-  let totalSeconds := dt.time.toSeconds + minutes.toSeconds
-  let days := totalSeconds.ediv 86400
-  let newTime := dt.time.addSeconds (minutes.toSeconds)
-  { dt with date := dt.date.addDays days, time := newTime }
+  addNanoseconds dt minutes.toNanoseconds
 
 /--
 Subtracts a `Minute.Offset` from a `PlainDateTime`, adjusting the hour and date if the minutes underflow.
@@ -355,10 +362,7 @@ Adds a `Second.Offset` to a `PlainDateTime`, adjusting the minute, hour, and dat
 -/
 @[inline]
 def addSeconds (dt : PlainDateTime) (seconds : Second.Offset) : PlainDateTime :=
-  let totalSeconds := dt.time.toSeconds + seconds
-  let days := totalSeconds.ediv 86400
-  let newTime := dt.time.addSeconds seconds
-  { dt with date := dt.date.addDays days, time := newTime }
+  addNanoseconds dt seconds.toNanoseconds
 
 /--
 Subtracts a `Second.Offset` from a `PlainDateTime`, adjusting the minute, hour, and date if the seconds underflow.
@@ -372,10 +376,7 @@ Adds a `Millisecond.Offset` to a `PlainDateTime`, adjusting the second, minute,
 -/
 @[inline]
 def addMilliseconds (dt : PlainDateTime) (milliseconds : Millisecond.Offset) : PlainDateTime :=
-  let totalMilliseconds := dt.time.toMilliseconds + milliseconds
-  let days := totalMilliseconds.ediv 86400000 -- 86400000 ms in a day
-  let newTime := dt.time.addMilliseconds milliseconds
-  { dt with date := dt.date.addDays days, time := newTime }
+  addNanoseconds dt milliseconds.toNanoseconds
 
 /--
 Subtracts a `Millisecond.Offset` from a `PlainDateTime`, adjusting the second, minute, hour, and date if the milliseconds underflow.
@@ -384,25 +385,6 @@ Subtracts a `Millisecond.Offset` from a `PlainDateTime`, adjusting the second, m
 def subMilliseconds (dt : PlainDateTime) (milliseconds : Millisecond.Offset) : PlainDateTime :=
   addMilliseconds dt (-milliseconds)
 
-/--
-Adds a `Nanosecond.Offset` to a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds overflow.
--/
-@[inline]
-def addNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime :=
-  let nano := Nanosecond.Offset.ofInt dt.time.nanosecond.val
-  let totalNanos := nano + nanos
-  let extraSeconds := totalNanos.ediv 1000000000
-  let nanosecond := Bounded.LE.byEmod totalNanos.val 1000000000 (by decide)
-  let newTime := dt.time.addSeconds extraSeconds
-  { dt with time := { newTime with nanosecond } }
-
-/--
-Subtracts a `Nanosecond.Offset` from a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds underflow.
--/
-@[inline]
-def subNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime :=
-  addNanoseconds dt (-nanos)
-
 /--
 Getter for the `Year` inside of a `PlainDateTime`.
 -/

src/Std/Time/Duration.lean

@@ -82,15 +82,21 @@ def ofSeconds (s : Second.Offset) : Duration := by
 Creates a new `Duration` out of `Nanosecond.Offset`.
 -/
 def ofNanoseconds (s : Nanosecond.Offset) : Duration := by
-  refine ⟨s.ediv 1000000000, Bounded.LE.byMod s.val 1000000000 (by decide), ?_⟩
+  refine ⟨s.tdiv 1000000000, Bounded.LE.byMod s.val 1000000000 (by decide), ?_⟩
+
   cases Int.le_total s.val 0
-  next n => exact Or.inr (And.intro (Int.ediv_le_ediv (by decide) n) (mod_nonpos 1000000000 n (by decide)))
-  next n => exact Or.inl (And.intro (Int.ediv_nonneg n (by decide)) (Int.tmod_nonneg 1000000000 n))
+  next n => exact Or.inr (And.intro (tdiv_neg n (by decide)) (mod_nonpos 1000000000 n (by decide)))
+  next n => exact Or.inl (And.intro (Int.tdiv_nonneg n (by decide)) (Int.tmod_nonneg 1000000000 n))
   where
     mod_nonpos : ∀ {a : Int} (b : Int), (a ≤ 0) → (b ≥ 0) → 0 ≥ a.tmod b
     | .negSucc m, .ofNat n, _, _ => Int.neg_le_neg (Int.tmod_nonneg (↑n) (Int.ofNat_le.mpr (Nat.zero_le (m + 1))))
     | 0, n, _, _ => Int.eq_iff_le_and_ge.mp (Int.zero_tmod n) |>.left
 
+    tdiv_neg {a b : Int} (Ha : a ≤ 0) (Hb : 0 ≤ b) : a.tdiv b ≤ 0 :=
+    match a, b, Ha with
+    | .negSucc _, .ofNat _, _ => Int.neg_le_neg (Int.ofNat_le.mpr (Nat.zero_le _))
+    | 0,  n, _ => Int.eq_iff_le_and_ge.mp (Int.zero_tdiv n) |>.left
+
 /--
 Creates a new `Duration` out of `Millisecond.Offset`.
 -/
@@ -142,14 +148,14 @@ Converts a `Duration` to a `Minute.Offset`
 -/
 @[inline]
 def toMinutes (tm : Duration) : Minute.Offset :=
-  tm.second.ediv 60
+  tm.second.tdiv 60
 
 /--
 Converts a `Duration` to a `Day.Offset`
 -/
 @[inline]
 def toDays (tm : Duration) : Day.Offset :=
-  tm.second.ediv 86400
+  tm.second.tdiv 86400
 
 /--
 Normalizes `Second.Offset` and `NanoSecond.span` in order to build a new `Duration` out of it.

src/Std/Time/Internal/UnitVal.lean

@@ -59,12 +59,21 @@ def mul (unit : UnitVal a) (factor : Int) : UnitVal (a / factor) :=
   ⟨unit.val * factor⟩
 
 /--
-Divides the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio.
+Divides the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio. Using the
+E-rounding convention (euclidean division)
 -/
 @[inline]
 def ediv (unit : UnitVal a) (divisor : Int) : UnitVal (a * divisor) :=
   ⟨unit.val.ediv divisor⟩
 
+/--
+Divides the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio. Using the
+"T-rounding" (Truncation-rounding) convention
+-/
+@[inline]
+def tdiv (unit : UnitVal a) (divisor : Int) : UnitVal (a * divisor) :=
+  ⟨unit.val.tdiv divisor⟩
+
 /--
 Divides the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio.
 -/

tests/lean/run/grind_cases.lean

@@ -27,3 +27,37 @@ attribute [grind_cases] And
 attribute [grind_cases] False
 
 attribute [grind_cases] Empty
+
+-- TODO: delete everything above
+
+/--
+error: invalid `[grind cases eager]`, `List` is not a non-recursive inductive datatype or an alias for one
+-/
+#guard_msgs (error) in
+attribute [grind cases eager] List
+
+attribute [grind cases] List
+
+attribute [grind] Prod
+
+/--
+error: invalid `[grind cases]`, `id` is not an inductive datatype or an alias for one
+-/
+#guard_msgs (error) in
+attribute [grind cases] id
+
+/--
+error: invalid `[grind cases eager]`, `id` is not a non-recursive inductive datatype or an alias for one
+-/
+#guard_msgs (error) in
+attribute [grind cases eager] id
+
+example : True := by
+  grind [-List]
+
+/--
+error: `Array` is not marked with the `[grind]` attribute
+-/
+#guard_msgs (error) in
+example : True := by
+  grind [-Array]

tests/lean/run/grind_eq_bwd.lean

@@ -0,0 +1,55 @@
+theorem dummy (x : Nat) : x = x :=
+  rfl
+
+/--
+error: invalid pattern for `dummy`
+  [@Lean.Grind.eqBwdPattern `[Nat] #0 #0]
+the pattern does not contain constant symbols for indexing
+-/
+#guard_msgs in
+attribute [grind ←=] dummy
+
+def α : Type := sorry
+def inv : α → α := sorry
+def mul : α → α → α := sorry
+def one : α := sorry
+
+theorem inv_eq {a b : α} (w : mul a b = one) : inv a = b := sorry
+
+/--
+info: [grind.ematch.pattern] inv_eq: [@Lean.Grind.eqBwdPattern `[α] (inv #2) #1]
+-/
+#guard_msgs in
+set_option trace.grind.ematch.pattern true in
+attribute [grind ←=] inv_eq
+
+example {a b : α} (w : mul a b = one) : inv a = b := by
+  grind
+
+structure S where
+  f : Bool → α
+  h : mul (f true) (f false) = one
+  h' : mul (f false) (f true) = one
+
+attribute [grind =] S.h S.h'
+
+example (s : S) : inv (s.f true) = s.f false := by
+  grind
+
+example (s : S) : s.f false = inv (s.f true) := by
+  grind
+
+example (s : S) : a = false → s.f a = inv (s.f true) := by
+  grind
+
+example (s : S) : a ≠ s.f false → a = inv (s.f true) → False := by
+  grind
+
+/--
+info: [grind.ematch.instance] inv_eq: mul (s.f true) (s.f false) = one → inv (s.f true) = s.f false
+[grind.ematch.instance] S.h: mul (s.f true) (s.f false) = one
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.instance true in
+example (s : S) : inv (s.f true) = s.f false := by
+  grind

tests/lean/run/timeAPI.lean

@@ -804,8 +804,8 @@ info: 1997-03-19T02:03:04.000000000[America/Sao_Paulo]
 1997-03-23T02:03:04.000000000[America/Sao_Paulo]
 1997-01-18T02:03:04.000000000[America/Sao_Paulo]
 1997-01-18T02:03:04.000000000[America/Sao_Paulo]
-0001-03-17T02:03:04.000000000[America/Sao_Paulo]
-0001-03-17T02:03:04.000000000[America/Sao_Paulo]
+0001-03-18T02:03:04.000000000[America/Sao_Paulo]
+0001-03-18T02:03:04.000000000[America/Sao_Paulo]
 97 1997 1997 1997 97 1997 1997 97 M
 false
 77

tests/lean/run/timeNegative.lean

@@ -0,0 +1,82 @@
+import Std.Time
+import Init
+open Std.Time
+
+/--
+info: Timestamp.ofNanosecondsSinceUnixEpoch -999999999
+-/
+#guard_msgs in
+#eval datetime("1969-12-31T23:59:59.000000001").toTimestampAssumingUTC
+
+/--
+info: Timestamp.ofNanosecondsSinceUnixEpoch -1000000000
+-/
+#guard_msgs in
+#eval datetime("1969-12-31T23:59:59.000000000").toTimestampAssumingUTC
+
+/--
+info: datetime("1969-12-31T23:59:59.000000001")
+-/
+#guard_msgs in
+#eval datetime("1969-12-31T23:59:59.000000001").toTimestampAssumingUTC.toPlainDateTimeAssumingUTC
+
+/--
+info: datetime("1969-12-31T23:59:59.000000000")
+-/
+#guard_msgs in
+#eval datetime("1969-12-31T23:59:59.000000000").toTimestampAssumingUTC.toPlainDateTimeAssumingUTC
+
+/--
+info: datetime("1969-12-31T23:59:59.000000001")
+-/
+#guard_msgs in
+#eval datetime("1969-12-31T23:59:59.000000000") + (1 : Nanosecond.Offset)
+
+/--
+info: datetime("1970-01-01T00:00:00.000000000")
+-/
+#guard_msgs in
+#eval datetime("1969-12-31T23:59:59.999999999") + (1 : Nanosecond.Offset)
+
+/--
+info: datetime("1970-01-01T00:00:01.000000000")
+-/
+#guard_msgs in
+#eval datetime("1970-01-01T00:00:00.999999999") + (1 : Nanosecond.Offset)
+
+/--
+info: Timestamp.ofNanosecondsSinceUnixEpoch -1
+-/
+#guard_msgs in
+#eval datetime("1969-12-31T23:59:59.999999999").toTimestampAssumingUTC
+
+/--
+info: Timestamp.ofNanosecondsSinceUnixEpoch 0
+-/
+#guard_msgs in
+#eval datetime("1969-12-31T23:59:59.999999999").toTimestampAssumingUTC + (1 : Nanosecond.Offset)
+
+
+/--
+info: datetime("1970-01-01T00:00:00.000000000")
+-/
+#guard_msgs in
+#eval PlainDateTime.ofTimestampAssumingUTC 0
+
+/--
+info: 121
+-/
+#guard_msgs in
+#eval datetime("1804-04-30T23:59:59.999999999").dayOfYear
+
+/--
+info: 35
+-/
+#guard_msgs in
+#eval datetime("1906-08-27T23:59:59.999999999").weekOfYear
+
+/--
+info: datetime("1906-08-27T23:59:59.999999999")
+-/
+#guard_msgs in
+#eval datetime("1906-08-27T23:59:59.999999999").toTimestampAssumingUTC.toPlainDateTimeAssumingUTC

tests/lean/run/timeParse.lean

@@ -84,7 +84,7 @@ info: "2024-08-16T01:28:00.000000000Z"
     ISO8601UTC.format t.toDateTime
 
 /--
-info: "0000-12-30T22:28:12.000000000+09:00"
+info: "0000-12-31T22:28:12.000000000+09:00"
 -/
 #guard_msgs in
 #eval
@@ -92,11 +92,11 @@ info: "0000-12-30T22:28:12.000000000+09:00"
     ISO8601UTC.format (t.toDateTime.convertTimeZone jpTZ)
 
 /--
-info: "0000-12-29T21:28:12.000000000-03:00"
+info: "0000-12-31T00:00:00.000000000-03:00"
 -/
 #guard_msgs in
 #eval
-    let t1 : ZonedDateTime := Time12Hour.parse! "12:28:12 AM"
+    let t1 : ZonedDateTime := Time12Hour.parse! "03:00:00 AM"
     ISO8601UTC.format (t1.toDateTime.convertTimeZone brTZ)
 
 /--