chore: missing [coe] attributes, review comments, fix tests

test: `norm_cast` and `push_cast`

chore: fix tests

Update src/Init/Data/Cast.lean

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

Apply suggestions from code review

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

use arxiv URL

move arxiv links out of doc-strings, into module-doc

remove inherit_doc; builtin_tactic already does this

src/Init/Conv.lean

@@ -308,4 +308,7 @@ Basic forms:
 -- refer to the syntax category instead of this syntax
 syntax (name := conv) "conv" (" at " ident)? (" in " (occs)? term)? " => " convSeq : tactic
 
+/-- `norm_cast` tactic in `conv` mode. -/
+syntax (name := normCast) "norm_cast" : conv
+
 end Lean.Parser.Tactic.Conv

src/Init/Data.lean

@@ -32,3 +32,4 @@ import Init.Data.Prod
 import Init.Data.AC
 import Init.Data.Queue
 import Init.Data.Channel
+import Init.Data.Cast

src/Init/Data/Array/Subarray.lean

@@ -143,6 +143,7 @@ def toSubarray (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Suba
      else
        { as := as, start := as.size, stop := as.size, h₁ := Nat.le_refl _, h₂ := Nat.le_refl _ }
 
+@[coe]
 def ofSubarray (s : Subarray α) : Array α := Id.run do
   let mut as := mkEmpty (s.stop - s.start)
   for a in s do

src/Init/Notation.lean

@@ -484,6 +484,9 @@ instance : Coe Syntax (TSyntax `rawStx) where
 /-- `with_annotate_term stx e` annotates the lexical range of `stx : Syntax` with term info for `e`. -/
 scoped syntax (name := withAnnotateTerm) "with_annotate_term " rawStx ppSpace term : term
 
+/-- Normalize casts in an expression using the same method as the `norm_cast` tactic. -/
+syntax (name := modCast) "mod_cast " term : term
+
 /--
 The attribute `@[deprecated]` on a declaration indicates that the declaration
 is discouraged for use in new code, and/or should be migrated away from in

src/Init/Prelude.lean

@@ -1814,6 +1814,8 @@ structure Fin (n : Nat) where
   /-- If `i : Fin n`, then `i.2` is a proof that `i.1 < n`. -/
   isLt : LT.lt val n
 
+attribute [coe] Fin.val
+
 theorem Fin.eq_of_val_eq {n} : ∀ {i j : Fin n}, Eq i.val j.val → Eq i j
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 

src/Init/Tactics.lean

@@ -1018,7 +1018,6 @@ macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_
 /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
 macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)
 
-
 /--
 The `omega` tactic, for resolving integer and natural linear arithmetic problems.
 
@@ -1052,6 +1051,74 @@ Currently, all of these are on by default.
 -/
 syntax (name := omega) "omega" (config)? : tactic
 
+/-- Implementation of `norm_cast` (the full `norm_cast` calls `trivial` afterwards). -/
+syntax (name := normCast0) "norm_cast0" (location)? : tactic
+
+/-- `assumption_mod_cast` is a variant of `assumption` that solves the goal
+using a hypothesis. Unlike `assumption`, it first pre-processes the goal and
+each hypothesis to move casts as far outwards as possible, so it can be used
+in more situations.
+
+Concretely, it runs `norm_cast` on the goal. For each local hypothesis `h`, it also
+normalizes `h` with `norm_cast` and tries to use that to close the goal. -/
+macro "assumption_mod_cast" : tactic => `(tactic| norm_cast0 at * <;> assumption)
+
+/--
+The `norm_cast` family of tactics is used to normalize casts inside expressions.
+It is basically a `simp` tactic with a specific set of lemmas to move casts
+upwards in the expression.
+Therefore even in situations where non-terminal `simp` calls are discouraged (because of fragility),
+`norm_cast` is considered safe.
+It also has special handling of numerals.
+
+For instance, given an assumption
+```lean
+a b : ℤ
+h : ↑a + ↑b < (10 : ℚ)
+```
+
+writing `norm_cast at h` will turn `h` into
+```lean
+h : a + b < 10
+```
+
+There are also variants of `exact`, `apply`, `rw`, and `assumption` that
+work modulo `norm_cast` - in other words, they apply `norm_cast` to make
+them more flexible. They are called `exact_mod_cast`, `apply_mod_cast`,
+`rw_mod_cast`, and `assumption_mod_cast`, respectively.
+Writing `exact_mod_cast h` and `apply_mod_cast h` will normalize casts
+in the goal and `h` before using `exact h` or `apply h`.
+Writing `assumption_mod_cast` will normalize casts in the goal and, for
+every hypothesis `h` in the context, it will try to normalize casts in `h` and use
+`exact h`.
+`rw_mod_cast` acts like the `rw` tactic but it applies `norm_cast` between steps.
+
+See also `push_cast`, which moves casts inwards rather than lifting them outwards.
+-/
+macro "norm_cast" loc:(location)? : tactic =>
+  `(tactic| norm_cast0 $[$loc]? <;> try trivial)
+
+/--
+`push_cast` rewrites the goal to move casts inward, toward the leaf nodes.
+This uses `norm_cast` lemmas in the forward direction.
+For example, `↑(a + b)` will be written to `↑a + ↑b`.
+It is equivalent to `simp only with push_cast`.
+It can also be used at hypotheses with `push_cast at h`
+and with extra simp lemmas with `push_cast [int.add_zero]`.
+
+```lean
+example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
+  ((a + b : ℕ) : ℤ) = 10 :=
+begin
+  push_cast,
+  push_cast at h1,
+  push_cast [int.add_zero] at h2,
+end
+```
+-/
+syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
+  (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
+
 end Tactic
 
 namespace Attr
@@ -1099,6 +1166,59 @@ If there are several with the same priority, it is uses the "most recent one". E
 ```
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
+
+
+/-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
+syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"
+
+/--
+The `norm_cast` attribute should be given to lemmas that describe the
+behaviour of a coercion with respect to an operator, a relation, or a particular
+function.
+
+It only concerns equality or iff lemmas involving `↑`, `⇑` and `↥`, describing the behavior of
+the coercion functions.
+It does not apply to the explicit functions that define the coercions.
+
+Examples:
+```lean
+@[norm_cast] theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n
+
+@[norm_cast] theorem coe_int_denom (n : ℤ) : (n : ℚ).denom = 1
+
+@[norm_cast] theorem cast_id : ∀ n : ℚ, ↑n = n
+
+@[norm_cast] theorem coe_nat_add (m n : ℕ) : (↑(m + n) : ℤ) = ↑m + ↑n
+
+@[norm_cast] theorem cast_coe_nat (n : ℕ) : ((n : ℤ) : α) = n
+
+@[norm_cast] theorem cast_one : ((1 : ℚ) : α) = 1
+```
+
+Lemmas tagged with `@[norm_cast]` are classified into three categories: `move`, `elim`, and
+`squash`. They are classified roughly as follows:
+
+* elim lemma:   LHS has 0 head coes and ≥ 1 internal coe
+* move lemma:   LHS has 1 head coe and 0 internal coes,    RHS has 0 head coes and ≥ 1 internal coes
+* squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
+
+`norm_cast` uses `move` and `elim` lemmas to factor coercions toward the root of an expression
+and to cancel them from both sides of an equation or relation. It uses `squash` lemmas to clean
+up the result.
+
+It is typically not necessary to specify these categories, as `norm_cast` lemmas are
+automatically classified by default. The automatic classification can be overridden by
+giving an optional `elim`, `move`, or `squash` parameter to the attribute.
+
+```lean
+@[simp, norm_cast elim] lemma nat_cast_re (n : ℕ) : (n : ℂ).re = n := by
+  rw [← of_real_nat_cast, of_real_re]
+```
+
+Don't do this unless you understand what you are doing.
+-/
+syntax (name := norm_cast) "norm_cast" (ppSpace normCastLabel)? (ppSpace num)? : attr
+
 end Attr
 
 end Parser

src/Init/TacticsExtra.lean

@@ -63,4 +63,24 @@ macro_rules
     | 0 => `(tactic| skip)
     | n+1 => `(tactic| ($seq:tacticSeq); iterate $(quote n) $seq:tacticSeq)
 
+/--
+Rewrites with the given rules, normalizing casts prior to each step.
+-/
+syntax "rw_mod_cast" (config)? rwRuleSeq (location)? : tactic
+macro_rules
+  | `(tactic| rw_mod_cast $[$config]? [$rules,*] $[$loc]?) => do
+    let tacs ← rules.getElems.mapM fun rule =>
+      `(tactic| (norm_cast at *; rw $[$config]? [$rule] $[$loc]?))
+    `(tactic| ($[$tacs]*))
+
+/--
+Normalize casts in the goal and the given expression, then close the goal with `exact`.
+-/
+macro "exact_mod_cast " e:term : tactic => `(tactic| exact mod_cast ($e : _))
+
+/--
+Normalize casts in the goal and the given expression, then `apply` the expression to the goal.
+-/
+macro "apply_mod_cast " e:term : tactic => `(tactic| apply mod_cast ($e : _))
+
 end Lean.Parser.Tactic

src/Lean/Elab/Tactic.lean

@@ -32,3 +32,4 @@ import Lean.Elab.Tactic.Change
 import Lean.Elab.Tactic.FalseOrByContra
 import Lean.Elab.Tactic.Omega
 import Lean.Elab.Tactic.Simpa
+import Lean.Elab.Tactic.NormCast

src/Lean/Elab/Tactic/NormCast.lean

@@ -0,0 +1,265 @@
+/-
+Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
+-/
+import Lean.Meta.Tactic.NormCast
+import Lean.Elab.Tactic.Conv.Simp
+import Lean.Elab.ElabRules
+
+/-!
+# The `norm_cast` family of tactics.
+
+A full description of the tactic, and the use of each theorem category, can be found at
+<https://arxiv.org/abs/2001.10594>.
+-/
+namespace Lean.Elab.Tactic.NormCast
+open Lean Meta Simp NormCast
+
+-- TODO: trace name consistency
+builtin_initialize registerTraceClass `Tactic.norm_cast
+
+/-- Proves `a = b` using the given simp set. -/
+def proveEqUsing (s : SimpTheorems) (a b : Expr) : MetaM (Option Simp.Result) := do
+  let go : SimpM (Option Simp.Result) := do
+    let a' ← Simp.simp a
+    let b' ← Simp.simp b
+    unless ← isDefEq a'.expr b'.expr do return none
+    a'.mkEqTrans (← b'.mkEqSymm b)
+  withReducible do
+    (go (← Simp.mkDefaultMethods).toMethodsRef
+      { simpTheorems := #[s], congrTheorems := ← Meta.getSimpCongrTheorems }).run' {}
+
+/-- Proves `a = b` by simplifying using move and squash lemmas. -/
+def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
+  withTraceNode `Tactic.norm_cast (return m!"{exceptOptionEmoji ·} proving: {← mkEq a b}") do
+  proveEqUsing (← normCastExt.down.getTheorems) a b
+
+/-- Constructs the expression `(e : ty)`. -/
+def mkCoe (e : Expr) (ty : Expr) : MetaM Expr := do
+  let .some e' ← coerce? e ty | failure
+  return e'
+
+/--
+Checks whether an expression is the coercion of some other expression,
+and if so returns that expression.
+-/
+def isCoeOf? (e : Expr) : MetaM (Option Expr) := do
+  if let Expr.const fn .. := e.getAppFn then
+    if let some info ← getCoeFnInfo? fn then
+      if e.getAppNumArgs == info.numArgs then
+        return e.getArg! info.coercee
+  return none
+
+/--
+Checks whether an expression is a numeral in some type,
+and if so returns that type and the natural number.
+-/
+def isNumeral? (e : Expr) : Option (Expr × Nat) :=
+  -- TODO: cleanup, and possibly remove duplicate
+  if e.isConstOf ``Nat.zero then
+    (mkConst ``Nat, 0)
+  else if let Expr.app (Expr.app (Expr.app (Expr.const ``OfNat.ofNat ..) α ..)
+      (Expr.lit (Literal.natVal n) ..) ..) .. := e then
+    some (α, n)
+  else
+    none
+
+/--
+This is the main heuristic used alongside the elim and move lemmas.
+The goal is to help casts move past operators by adding intermediate casts.
+An expression of the shape:
+```
+op (↑(x : α) : γ) (↑(y : β) : γ)
+```
+is rewritten to:
+```
+op (↑(↑(x : α) : β) : γ) (↑(y : β) : γ)
+```
+when
+```
+(↑(↑(x : α) : β) : γ) = (↑(x : α) : γ)
+```
+can be proven with a squash lemma
+-/
+def splittingProcedure (expr : Expr) : MetaM Simp.Result := do
+  let Expr.app (Expr.app op x ..) y .. := expr | return {expr}
+
+  let Expr.forallE _ γ (Expr.forallE _ γ' ty ..) .. ← inferType op | return {expr}
+  if γ'.hasLooseBVars || ty.hasLooseBVars then return {expr}
+  unless ← isDefEq γ γ' do return {expr}
+
+  let msg := m!"splitting {expr}"
+  let msg
+    | .error _ => return m!"{bombEmoji} {msg}"
+    | .ok r => return if r.expr == expr then m!"{crossEmoji} {msg}" else
+      m!"{checkEmoji} {msg} to {r.expr}"
+  withTraceNode `Tactic.norm_cast msg do
+
+  try
+    let some x' ← isCoeOf? x | failure
+    let some y' ← isCoeOf? y | failure
+    let α ← inferType x'
+    let β ← inferType y'
+
+    -- TODO: fast timeout
+    (try
+      let x2 ← mkCoe (← mkCoe x' β) γ
+      let some x_x2 ← proveEqUsingDown x x2 | failure
+      Simp.mkCongrFun (← Simp.mkCongr {expr := op} x_x2) y
+    catch _ =>
+      let y2 ← mkCoe (← mkCoe y' α) γ
+      let some y_y2 ← proveEqUsingDown y y2 | failure
+      Simp.mkCongr {expr := mkApp op x} y_y2)
+  catch _ => try
+    let some (_, n) := isNumeral? y | failure
+    let some x' ← isCoeOf? x | failure
+    let α ← inferType x'
+    let y2 ← mkCoe (← mkNumeral α n) γ
+    let some y_y2 ← proveEqUsingDown y y2 | failure
+    Simp.mkCongr {expr := mkApp op x} y_y2
+  catch _ => try
+    let some (_, n) := isNumeral? x | failure
+    let some y' ← isCoeOf? y | failure
+    let β ← inferType y'
+    let x2 ← mkCoe (← mkNumeral β n) γ
+    let some x_x2 ← proveEqUsingDown x x2 | failure
+    Simp.mkCongrFun (← Simp.mkCongr {expr := op} x_x2) y
+  catch _ =>
+    return {expr}
+
+/--
+Discharging function used during simplification in the "squash" step.
+-/
+-- TODO: normCast takes a list of expressions to use as lemmas for the discharger
+-- TODO: a tactic to print the results the discharger fails to prove
+def prove (e : Expr) : SimpM (Option Expr) := do
+  withTraceNode `Tactic.norm_cast (return m!"{exceptOptionEmoji ·} discharging: {e}") do
+  return (← findLocalDeclWithType? e).map mkFVar
+
+/--
+Core rewriting function used in the "squash" step, which moves casts upwards
+and eliminates them.
+
+It tries to rewrite an expression using the elim and move lemmas.
+On failure, it calls the splitting procedure heuristic.
+-/
+partial def upwardAndElim (up : SimpTheorems) (e : Expr) : SimpM Simp.Step := do
+  let r ← withDischarger prove do
+    Simp.rewrite? e up.post up.erased (tag := "squash") (rflOnly := false)
+  let r := r.getD { expr := e }
+  let r ← r.mkEqTrans (← splittingProcedure r.expr)
+  if r.expr == e then return Simp.Step.done {expr := e}
+  return Simp.Step.visit r
+
+/--
+If possible, rewrites `(n : α)` to `(Nat.cast n : α)` where `n` is a numeral and `α ≠ ℕ`.
+Returns a pair of the new expression and proof that they are equal.
+-/
+def numeralToCoe (e : Expr) : MetaM Simp.Result := do
+  let some (α, n) := isNumeral? e | failure
+  if (← whnf α).isConstOf ``Nat then failure
+  let newE ← mkAppOptM ``Nat.cast #[α, none, toExpr n]
+  let some pr ← proveEqUsingDown e newE | failure
+  return pr
+
+/--
+The core simplification routine of `normCast`.
+-/
+def derive (e : Expr) : MetaM Simp.Result := do
+  withTraceNode `Tactic.norm_cast (fun _ => return m!"{e}") do
+  let e ← instantiateMVars e
+
+  let config : Simp.Config := {
+    zeta := false
+    beta := false
+    eta  := false
+    proj := false
+    iota := false
+  }
+  let congrTheorems ← Meta.getSimpCongrTheorems
+
+  let r : Simp.Result := { expr := e }
+
+  let withTrace phase := withTraceNode `Tactic.norm_cast fun
+    | .ok r => return m!"{r.expr} (after {phase})"
+    | .error _ => return m!"{bombEmoji} {phase}"
+
+  -- step 1: pre-processing of numerals
+  let r ← withTrace "pre-processing numerals" do
+    let post e := return Simp.Step.done (← try numeralToCoe e catch _ => pure {expr := e})
+    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
+
+  -- step 2: casts are moved upwards and eliminated
+  let r ← withTrace "moving upward, splitting and eliminating" do
+    let post := upwardAndElim (← normCastExt.up.getTheorems)
+    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
+
+  -- step 3: casts are squashed
+  let r ← withTrace "squashing" do
+    let simpTheorems := #[← normCastExt.squash.getTheorems]
+    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems }).1
+
+  return r
+
+open Term
+@[builtin_term_elab modCast] def elabModCast : TermElab := fun stx expectedType? => do
+  match stx with
+  | `(mod_cast $e:term) =>
+    withExpectedType expectedType? fun expectedType => do
+    if (← instantiateMVars expectedType).hasExprMVar then tryPostpone
+    let expectedType' ← derive expectedType
+    let e ← Term.elabTerm e expectedType'.expr
+    synthesizeSyntheticMVars
+    let eTy ← instantiateMVars (← inferType e)
+    if eTy.hasExprMVar then tryPostpone
+    let eTy' ← derive eTy
+    unless ← isDefEq eTy'.expr expectedType'.expr do
+      throwTypeMismatchError "mod_cast" expectedType'.expr eTy'.expr e
+    let eTy_eq_expectedType ← eTy'.mkEqTrans (← expectedType'.mkEqSymm expectedType )
+    eTy_eq_expectedType.mkCast e
+  | _ => throwUnsupportedSyntax
+
+/-- Implementation of the `norm_cast` tactic when operating on the main goal. -/
+def normCastTarget : TacticM Unit :=
+  liftMetaTactic1 fun goal => do
+    let tgt ← instantiateMVars (← goal.getType)
+    let prf ← derive tgt
+    applySimpResultToTarget goal tgt prf
+
+/-- Implementation of the `norm_cast` tactic when operating on a hypothesis. -/
+def normCastHyp (fvarId : FVarId) : TacticM Unit :=
+  liftMetaTactic1 fun goal => do
+    let hyp ← instantiateMVars (← fvarId.getDecl).type
+    let prf ← derive hyp
+    return (← applySimpResultToLocalDecl goal fvarId prf false).map (·.snd)
+
+@[builtin_tactic normCast0]
+def evalNormCast0 : Tactic := fun stx => do
+  match stx with
+  | `(tactic| norm_cast0 $[$loc?]?) =>
+    let loc := if let some loc := loc? then expandLocation loc else Location.targets #[] true
+    withMainContext do
+      match loc with
+      | Location.targets hyps target =>
+        if target then normCastTarget
+        (← getFVarIds hyps).forM normCastHyp
+      | Location.wildcard =>
+        normCastTarget
+        (← (← getMainGoal).getNondepPropHyps).forM normCastHyp
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.Conv.normCast]
+def evalConvNormCast : Tactic :=
+  open Elab.Tactic.Conv in fun _ => withMainContext do
+    applySimpResult (← derive (← getLhs))
+
+@[builtin_tactic pushCast]
+def evalPushCast : Tactic := fun stx => do
+  let { ctx, simprocs, dischargeWrapper } ← withMainContext do
+    mkSimpContext (simpTheorems := pushCastExt.getTheorems) stx (eraseLocal := false)
+  let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
+  dischargeWrapper.with fun discharge? =>
+    discard <| simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
+
+end Lean.Elab.Tactic.NormCast

src/Lean/Meta/Tactic.lean

@@ -32,3 +32,4 @@ import Lean.Meta.Tactic.AC
 import Lean.Meta.Tactic.Refl
 import Lean.Meta.Tactic.Congr
 import Lean.Meta.Tactic.Repeat
+import Lean.Meta.Tactic.NormCast

src/Lean/Meta/Tactic/NormCast.lean

@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
+-/
+import Lean.Meta.CongrTheorems
+import Lean.Meta.Tactic.Simp.SimpTheorems
+import Lean.Meta.CoeAttr
+
+namespace Lean.Meta.NormCast
+/--
+`Label` is a type used to classify `norm_cast` lemmas.
+* elim lemma:   LHS has 0 head coes and ≥ 1 internal coe
+* move lemma:   LHS has 1 head coe and 0 internal coes,    RHS has 0 head coes and ≥ 1 internal coes
+* squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
+-/
+inductive Label
+  /-- elim lemma: LHS has 0 head coes and ≥ 1 internal coe -/
+  | elim
+  /-- move lemma: LHS has 1 head coe and 0 internal coes,
+  RHS has 0 head coes and ≥ 1 internal coes -/
+  | move
+  /-- squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes -/
+  | squash
+  deriving DecidableEq, Repr, Inhabited
+
+/-- Assuming `e` is an application, returns the list of subterms that `simp` will rewrite in. -/
+def getSimpArgs (e : Expr) : MetaM (Array Expr) := do
+  match ← mkCongrSimp? e.getAppFn with
+  | none => return e.getAppArgs
+  | some {argKinds, ..} =>
+    let mut args := #[]
+    for a in e.getAppArgs, k in argKinds do
+      if k matches .eq then
+        args := args.push a
+    return args
+
+/-- Counts how many coercions are at the head of the expression. -/
+partial def countHeadCoes (e : Expr) : MetaM Nat := do
+  if let Expr.const fn .. := e.getAppFn then
+    if let some info ← getCoeFnInfo? fn then
+      if e.getAppNumArgs >= info.numArgs then
+        return (← countHeadCoes (e.getArg! info.coercee)) + 1
+  return 0
+
+/-- Counts how many coercions are inside the expression, including the head ones. -/
+partial def countCoes (e : Expr) : MetaM Nat :=
+  lambdaTelescope e fun _ e => do
+    if let Expr.const fn .. := e.getAppFn then
+      if let some info ← getCoeFnInfo? fn then
+        if e.getAppNumArgs >= info.numArgs then
+          let mut coes := (← countHeadCoes (e.getArg! info.coercee)) + 1
+          for i in [info.numArgs:e.getAppNumArgs] do
+            coes := coes + (← countCoes (e.getArg! i))
+          return coes
+    return (← (← getSimpArgs e).mapM countCoes).foldl (·+·) 0
+
+/-- Counts how many coercions are inside the expression, excluding the head ones. -/
+def countInternalCoes (e : Expr) : MetaM Nat :=
+  return (← countCoes e) - (← countHeadCoes e)
+
+/-- Classifies a declaration of type `ty` as a `norm_cast` rule. -/
+def classifyType (ty : Expr) : MetaM Label :=
+  forallTelescopeReducing ty fun _ ty => do
+    let ty ← whnf ty
+    let (lhs, rhs) ←
+      if ty.isAppOfArity ``Eq 3 then pure (ty.getArg! 1, ty.getArg! 2)
+      else if ty.isAppOfArity ``Iff 2 then pure (ty.getArg! 0, ty.getArg! 1)
+      else throwError "norm_cast: lemma must be = or ↔, but is{indentExpr ty}"
+    let lhsCoes ← countCoes lhs
+    if lhsCoes = 0 then
+      throwError "norm_cast: badly shaped lemma, lhs must contain at least one coe{indentExpr lhs}"
+    let lhsHeadCoes ← countHeadCoes lhs
+    let rhsHeadCoes ← countHeadCoes rhs
+    let rhsInternalCoes ← countInternalCoes rhs
+    if lhsHeadCoes = 0 then
+      return Label.elim
+    else if lhsHeadCoes = 1 then do
+      unless rhsHeadCoes = 0 do
+        throwError "norm_cast: badly shaped lemma, rhs can't start with coe{indentExpr rhs}"
+      if rhsInternalCoes = 0 then
+        return Label.squash
+      else
+        return Label.move
+    else if rhsHeadCoes < lhsHeadCoes then do
+      return Label.squash
+    else do
+      throwError "\
+        norm_cast: badly shaped shaped squash lemma, \
+        rhs must have fewer head coes than lhs{indentExpr ty}"
+
+/-- The `push_cast` simp attribute. -/
+initialize pushCastExt : SimpExtension ←
+  registerSimpAttr `push_cast "\
+    The `push_cast` simp attribute uses `norm_cast` lemmas \
+    to move casts toward the leaf nodes of the expression."
+
+/--  The `norm_cast` attribute stores a simp set for each of the three types of `norm_cast` lemma. -/
+structure NormCastExtension where
+  /-- A simp set which lifts coercions to the top level. -/
+  up : SimpExtension
+  /-- A simp set which pushes coercions to the leaves. -/
+  down : SimpExtension
+  /-- A simp set which simplifies transitive coercions. -/
+  squash : SimpExtension
+deriving Inhabited
+
+/-- The `norm_cast` extension data. -/
+builtin_initialize normCastExt : NormCastExtension ← pure {
+  up := ← mkSimpExt (decl_name% ++ `up)
+  down := ← mkSimpExt (decl_name% ++ `down)
+  squash := ← mkSimpExt (decl_name% ++ `squash)
+}
+
+/-- `addElim decl` adds `decl` as an `elim` lemma to be used by `norm_cast`. -/
+def addElim (decl : Name)
+    (kind := AttributeKind.global) (prio := eval_prio default) : MetaM Unit :=
+  addSimpTheorem normCastExt.up decl (post := true) (inv := false) kind prio
+
+/-- `addMove decl` adds `decl` as a `move` lemma to be used by `norm_cast`. -/
+def addMove (decl : Name)
+    (kind := AttributeKind.global) (prio := eval_prio default) : MetaM Unit := do
+  addSimpTheorem pushCastExt decl (post := true) (inv := false) kind prio
+  addSimpTheorem normCastExt.up decl (post := true) (inv := true) kind prio
+  addSimpTheorem normCastExt.down decl (post := true) (inv := false) kind prio
+
+/-- `addSquash decl` adds `decl` as a `squash` lemma to be used by `norm_cast`. -/
+def addSquash (decl : Name)
+    (kind := AttributeKind.global) (prio := eval_prio default) : MetaM Unit := do
+  addSimpTheorem pushCastExt decl (post := true) (inv := false) kind prio
+  addSimpTheorem normCastExt.squash decl (post := true) (inv := false) kind prio
+  addSimpTheorem normCastExt.down decl (post := true) (inv := false) kind prio
+
+/-- `addInfer decl` infers the label of `decl` (`elim`, `move`, or `squash`) and arranges for it to
+be used by `norm_cast`.
+
+* elim lemma:   LHS has 0 head coes and ≥ 1 internal coe
+* move lemma:   LHS has 1 head coe and 0 internal coes,    RHS has 0 head coes and ≥ 1 internal coes
+* squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
+-/
+def addInfer (decl : Name)
+    (kind := AttributeKind.global) (prio := eval_prio default) : MetaM Unit := do
+  let ty := (← getConstInfo decl).type
+  match ← classifyType ty with
+  | Label.elim => addElim decl kind prio
+  | Label.squash => addSquash decl kind prio
+  | Label.move => addMove decl kind prio
+
+builtin_initialize registerBuiltinAttribute {
+  name := `norm_cast
+  descr := "attribute for norm_cast"
+  add := fun decl stx kind => MetaM.run' do
+    let `(attr| norm_cast $[$label:normCastLabel]? $[$prio]?) := stx | unreachable!
+    let prio := (prio.bind (·.1.isNatLit?)).getD (eval_prio default)
+    match label.bind (·.1.isStrLit?) with
+    | "elim" => addElim decl kind prio
+    | "move" => addMove decl kind prio
+    | "squash" => addSquash decl kind prio
+    | none => addInfer decl kind prio
+    | _ => unreachable!
+}
+
+end Lean.Meta.NormCast

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

@@ -37,6 +37,13 @@ def mkEqTransOptProofResult (h? : Option Expr) (cache : Bool) (r : Result) : Met
 def Result.mkEqTrans (r₁ r₂ : Result) : MetaM Result :=
   mkEqTransOptProofResult r₁.proof? r₁.cache r₂
 
+/-- Flip the proof in a `Simp.Result`. -/
+def Result.mkEqSymm (e : Expr) (r : Simp.Result) : MetaM Simp.Result :=
+  ({ expr := e, proof? := · }) <$>
+  match r.proof? with
+  | none => pure none
+  | some p => some <$> Meta.mkEqSymm p
+
 abbrev Cache := ExprMap Result
 
 abbrev CongrCache := ExprMap (Option CongrTheorem)
@@ -277,6 +284,10 @@ def Result.getProof' (source : Expr) (r : Result) : MetaM Expr := do
          are not definitionally equal at `TransparencyMode.reducible` -/
       mkExpectedTypeHint (← mkEqRefl r.expr) (← mkEq source r.expr)
 
+/-- Construct the `Expr` `cast h e`, from a `Simp.Result` with proof `h`. -/
+def Result.mkCast (r : Simp.Result) (e : Expr) : MetaM Expr := do
+  mkAppM ``cast #[← r.getProof, e]
+
 def mkCongrFun (r : Result) (a : Expr) : MetaM Result :=
   match r.proof? with
   | none   => return { expr := mkApp r.expr a, proof? := none }

tests/lean/delabProjectionApp.lean

@@ -47,13 +47,16 @@ set_option pp.structureProjections false
 
 end
 
-structure Fin' extends Fin 5
+structure Fin0 where
+  val : Nat
 
-structure Fin'' (n : Nat) extends Fin n
+structure Fin' extends Fin0
+
+structure Fin'' (n : Nat) extends Fin0
 
 structure D (n : Nat) extends A
 
-variable (x : Fin 5) (y : Fin') (z : Fin'' 5) (d : D 5)
+variable (x : Fin0) (y : Fin') (z : Fin'' 5) (d : D 5)
 
 section
 /-!
@@ -72,7 +75,7 @@ section
 Check handling of parameters when `pp.explicit` is true.
 -/
 set_option pp.explicit true
-
+-- TODO: double check whether the following outputs are the expected ones
 #check c.x
 #check x.val
 #check y.val

tests/lean/delabProjectionApp.lean.expected.out

@@ -15,8 +15,8 @@ y.val : Nat
 z.val : Nat
 d.x : Nat
 c.x : Nat
-@Fin.val 5 x : Nat
-@Fin.val 5 y.toFin : Nat
-@Fin.val 5 (@Fin''.toFin 5 z) : Nat
+x.val : Nat
+y.val : Nat
+(@Fin''.toFin0 5 z).val : Nat
 (@D.toA 5 d).x : Nat
 f.toFun 0 : Int

tests/lean/keyAttrErase.lean.expected.out

@@ -1,2 +1,2 @@
-theorem ex : ∀ {n : Nat} {i j : Fin n}, i = j → i.val = j.val :=
+theorem ex : ∀ {n : Nat} {i j : Fin n}, i = j → ↑i = ↑j :=
 fun {n} {i j} h => h ▸ rfl

tests/lean/run/mathlibetaissue.lean

@@ -25,6 +25,13 @@ This file is minimised in the sense that:
 Section titles correspond to the files the material came from the mathlib4/std4.
 -/
 
+section Std.Classes.Cast
+
+class NatCast2 (R : Type u) where
+class IntCast2 (R : Type u) where
+
+end Std.Classes.Cast
+
 section Std.Data.Int.Lemmas
 
 end Std.Data.Int.Lemmas
@@ -96,14 +103,14 @@ end Mathlib.Algebra.GroupWithZero.Defs
 
 section Mathlib.Data.Nat.Cast.Defs
 
-class AddMonoidWithOne (R : Type u) extends NatCast R, AddMonoid R, One R where
+class AddMonoidWithOne (R : Type u) extends NatCast2 R, AddMonoid R, One R where
 class AddCommMonoidWithOne (R : Type _) extends AddMonoidWithOne R, AddCommMonoid R
 
 end Mathlib.Data.Nat.Cast.Defs
 
 section Mathlib.Data.Int.Cast.Defs
 
-class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGroup R where
+class AddGroupWithOne (R : Type u) extends IntCast2 R, AddMonoidWithOne R, AddGroup R where
 
 end Mathlib.Data.Int.Cast.Defs
 

tests/lean/run/norm_cast.lean

@@ -0,0 +1,21 @@
+@[coe] def Bool.toNat' : Bool → Nat
+  | true => 1
+  | false => 0
+
+instance : Coe Bool Nat where
+  coe := Bool.toNat'
+
+@[norm_cast] theorem ofNat_band (a b : Bool) : (↑(a && b) : Nat) = ↑a &&& ↑b := by
+  cases a <;> cases b <;> rfl
+
+example (a b c : Bool) (n : Nat) (h : n = a &&& b &&& c)
+        : (↑(a && b && c) : Nat) = n := by
+  push_cast
+  guard_target =ₛ(↑a &&& ↑b &&& ↑c) = n
+  rw [h]
+
+example (a b c : Bool) (n : Nat) (h : n = (a && b && c))
+        : (↑a &&& ↑b &&& ↑c) = n := by
+  norm_cast
+  guard_target =ₛ ↑(a && b && c) = n
+  rw [h]