chore: upstream NatCast and IntCast (#3347)

This upstreams NatCast and IntCast alone independent of norm_cast in
#3322.

This will allow more efficiently upstreaming parts of Std.Data.Int
relevant for omega.

---------

Co-authored-by: Scott Morrison <[email protected]>

src/Init/Data.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Basic
 import Init.Data.Nat
+import Init.Data.Cast
 import Init.Data.Char
 import Init.Data.String
 import Init.Data.List

src/Init/Data/Cast.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2014 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Gabriel Ebner
+-/
+prelude
+import Init.Coe
+
+/-!
+# `NatCast`
+
+We introduce the typeclass `NatCast R` for a type `R` with a "canonical
+homomorphism" `Nat → R`. The typeclass carries the data of the function,
+but no required axioms.
+
+This typeclass was introduced to support a uniform `simp` normal form
+for such morphisms.
+
+Without such a typeclass, we would have specific coercions such as
+`Int.ofNat`, but also later the generic coercion from `Nat` into any
+Mathlib semiring (including `Int`), and we would need to use `simp` to
+move between them. However `simp` lemmas expressed using a non-normal
+form on the LHS would then not fire.
+
+Typically different instances of this class for the same target type `R`
+are definitionally equal, and so differences in the instance do not
+block `simp` or `rw`.
+
+This logic also applies to `Int` and so we also introduce `IntCast` alongside
+`Int.
+
+## Note about coercions into arbitrary types:
+
+Coercions such as `Nat.cast` that go from a concrete structure such as
+`Nat` to an arbitrary type `R` should be set up as follows:
+```lean
+instance : CoeTail Nat R where coe := ...
+instance : CoeHTCT Nat R where coe := ...
+```
+
+It needs to be `CoeTail` instead of `Coe` because otherwise type-class
+inference would loop when constructing the transitive coercion `Nat →
+Nat → Nat → ...`. Sometimes we also need to declare the `CoeHTCT`
+instance if we need to shadow another coercion.
+-/
+
+/-- Type class for the canonical homomorphism `Nat → R`. -/
+class NatCast (R : Type u) where
+  /-- The canonical map `Nat → R`. -/
+  protected natCast : Nat → R
+
+instance : NatCast Nat where natCast n := n
+
+/--
+Canonical homomorphism from `Nat` to a type `R`.
+
+It contains just the function, with no axioms.
+In practice, the target type will likely have a (semi)ring structure,
+and this homomorphism should be a ring homomorphism.
+
+The prototypical example is `Int.ofNat`.
+
+This class and `IntCast` exist to allow different libraries with their own types that can be notated as natural numbers to have consistent `simp` normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with `NatCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus a `NatCast R` instance) whenever `R` is an additive monoid with a `1`.
+-/
+@[coe, reducible, match_pattern] protected def Nat.cast {R : Type u} [NatCast R] : Nat → R :=
+  NatCast.natCast
+
+-- see the notes about coercions into arbitrary types in the module doc-string
+instance [NatCast R] : CoeTail Nat R where coe := Nat.cast
+
+-- see the notes about coercions into arbitrary types in the module doc-string
+instance [NatCast R] : CoeHTCT Nat R where coe := Nat.cast

src/Init/Data/Int/Basic.lean

@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 The integers, with addition, multiplication, and subtraction.
 -/
 prelude
-import Init.Coe
+import Init.Data.Cast
 import Init.Data.Nat.Div
 import Init.Data.List.Basic
 set_option linter.missingDocs true -- keep it documented
@@ -47,7 +47,7 @@ inductive Int : Type where
 attribute [extern "lean_nat_to_int"] Int.ofNat
 attribute [extern "lean_int_neg_succ_of_nat"] Int.negSucc
 
-instance : Coe Nat Int := ⟨Int.ofNat⟩
+instance : NatCast Int where natCast n := Int.ofNat n
 
 instance instOfNat : OfNat Int n where
   ofNat := Int.ofNat n
@@ -359,3 +359,27 @@ instance : Min Int := minOfLe
 instance : Max Int := maxOfLe
 
 end Int
+
+/--
+The canonical homomorphism `Int → R`.
+In most use cases `R` will have a ring structure and this will be a ring homomorphism.
+-/
+class IntCast (R : Type u) where
+  /-- The canonical map `Int → R`. -/
+  protected intCast : Int → R
+
+instance : IntCast Int where intCast n := n
+
+/--
+Apply the canonical homomorphism from `Int` to a type `R` from an `IntCast R` instance.
+
+In Mathlib there will be such a homomorphism whenever `R` is an additive group with a `1`.
+-/
+@[coe, reducible, match_pattern] protected def Int.cast {R : Type u} [IntCast R] : Int → R :=
+  IntCast.intCast
+
+-- see the notes about coercions into arbitrary types in the module doc-string
+instance [IntCast R] : CoeTail Int R where coe := Int.cast
+
+-- see the notes about coercions into arbitrary types in the module doc-string
+instance [IntCast R] : CoeHTCT Int R where coe := Int.cast

src/Lean/Server/Utils.lean

@@ -117,7 +117,7 @@ def publishDiagnostics (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) (
     method := "textDocument/publishDiagnostics"
     param  := {
       uri         := m.uri
-      version?    := m.version
+      version?    := some m.version
       diagnostics := diagnostics
       : PublishDiagnosticsParams
     }

tests/lean/1298.lean

@@ -4,12 +4,12 @@ class Semiring (R : Type u) extends Add R, HPow R Nat R, Mul R where
 instance [Semiring R] : OfNat R n where
   ofNat := Semiring.zero
 
-def Nat.cast [Semiring R] (n : Nat) : R := let _ := n = n; Semiring.zero
+def Nat.castTest [Semiring R] (n : Nat) : R := let _ := n = n; Semiring.zero
 
 @[default_instance high] instance [Semiring R] : HPow R Nat R := inferInstance
 
 instance [Semiring R] : CoeTail Nat R where
-  coe n := n.cast
+  coe n := n.castTest
 
 variable (R) [Semiring R]
 #check (8 + 2 ^ 2 * 3 : R) = 20

tests/lean/binopInfoTree.lean.expected.out

@@ -25,10 +25,9 @@
                     • 1 : Nat @ ⟨5, 7⟩-⟨5, 8⟩ @ Lean.Elab.Term.elabNumLit
                     • 2 : Nat @ ⟨5, 11⟩-⟨5, 12⟩ @ Lean.Elab.Term.elabNumLit
               • 3 : Nat @ ⟨5, 15⟩-⟨5, 16⟩ @ Lean.Elab.Term.elabNumLit
-fun n m l => Int.ofNat n + (Int.ofNat m + Int.ofNat l) : Nat → Nat → Nat → Int
+fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int
 [Elab.info] • command @ ⟨7, 0⟩-⟨7, 48⟩ @ Lean.Elab.Command.elabCheck
-      • fun n m l =>
-          Int.ofNat n + (Int.ofNat m + Int.ofNat l) : Nat → Nat → Nat → Int @ ⟨7, 7⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabFun
+      • fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int @ ⟨7, 7⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabFun
         • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent
           • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩
           • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩
@@ -41,34 +40,32 @@ fun n m l => Int.ofNat n + (Int.ofNat m + Int.ofNat l) : Nat → Nat → Nat →
           • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩
           • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩
         • l (isBinder := true) : Nat @ ⟨7, 16⟩-⟨7, 17⟩
-        • Int.ofNat n + (Int.ofNat m + Int.ofNat l) : Int @ ⟨7, 28⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabTypeAscription
+        • ↑n + (↑m + ↑l) : Int @ ⟨7, 28⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabTypeAscription
           • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ @ Lean.Elab.Term.elabIdent
             • [.] Int : some Sort.{?_uniq} @ ⟨7, 44⟩-⟨7, 47⟩
             • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩
-          • Int.ofNat n +
-              (Int.ofNat m + Int.ofNat l) : Int @ ⟨7, 29⟩-⟨7, 41⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
+          • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩-⟨7, 41⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
             • Macro expansion
               n + (m +' l)
               ===>
               binop% HAdd.hAdd✝ n (m +' l)
-              • Int.ofNat n + (Int.ofNat m + Int.ofNat l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† @ Lean.Elab.Term.Op.elabBinOp
-                • Int.ofNat n + (Int.ofNat m + Int.ofNat l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩†
+              • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† @ Lean.Elab.Term.Op.elabBinOp
+                • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩†
                   • [.] HAdd.hAdd✝ : none @ ⟨7, 29⟩†-⟨7, 41⟩†
                   • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ @ Lean.Elab.Term.elabIdent
                     • [.] n : none @ ⟨7, 29⟩-⟨7, 30⟩
                     • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩
-                  • Int.ofNat m + Int.ofNat l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_binopInfoTree___macroRules_term_+'__1»
+                  • ↑m + ↑l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_binopInfoTree___macroRules_term_+'__1»
                     • Macro expansion
                       m +' l
                       ===>
                       m + l
-                      • Int.ofNat m +
-                          Int.ofNat l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† @ «_aux_Init_Notation___macroRules_term_+__2»
+                      • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† @ «_aux_Init_Notation___macroRules_term_+__2»
                         • Macro expansion
                           m + l
                           ===>
                           binop% HAdd.hAdd✝ m l
-                          • Int.ofNat m + Int.ofNat l : Int @ ⟨7, 34⟩†-⟨7, 40⟩†
+                          • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩†
                             • [.] HAdd.hAdd✝ : none @ ⟨7, 34⟩†-⟨7, 40⟩†
                             • m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ @ Lean.Elab.Term.elabIdent
                               • [.] m : none @ ⟨7, 34⟩-⟨7, 35⟩

tests/lean/binopIssues.lean.expected.out

@@ -1,4 +1,4 @@
 def f1 : Int → Nat → Nat → Int :=
-fun a b c => a + (Int.ofNat b - Int.ofNat c)
+fun a b c => a + (↑b - ↑c)
 def f2 : Int → Nat → Nat → Int :=
-fun a b c => Int.ofNat b - Int.ofNat c + a
+fun a b c => ↑b - ↑c + a

tests/lean/binrel_binop.lean.expected.out

@@ -1,6 +1,6 @@
 binrel_binop.lean:1:8-1:11: warning: declaration uses 'sorry'
-ex1 (a : Int) (b c : Nat) : a = Int.ofNat b - Int.ofNat c
+ex1 (a : Int) (b c : Nat) : a = ↑b - ↑c
 binrel_binop.lean:5:8-5:11: warning: declaration uses 'sorry'
-ex2 (a : Int) (b c : Nat) : a = Int.ofNat b - Int.ofNat c
+ex2 (a : Int) (b c : Nat) : a = ↑b - ↑c
 binrel_binop.lean:9:8-9:11: warning: declaration uses 'sorry'
-ex3 (a : Int) (b c : Nat) : a = Int.ofNat (b - c)
+ex3 (a : Int) (b c : Nat) : a = ↑(b - c)

tests/lean/hpow.lean.expected.out

@@ -1,9 +1,9 @@
-Int.ofNat n ^ 2 + m ^ 2 : Int
+↑n ^ 2 + m ^ 2 : Int
 n ^ 2 + 1 : Nat
-Int.ofNat n ^ 2 + 1 : Int
-Int.ofNat n ^ 2 + Int.ofNat 1 : Int
+↑n ^ 2 + 1 : Int
+↑n ^ 2 + ↑1 : Int
 q ^ n + 1 : Rat
 q ^ m + 1 : Rat
-q ^ Int.ofNat n + 1 : Rat
+q ^ ↑n + 1 : Rat
 12 * q + 1 ≤ 13 * q ^ 2 : Prop
 12 * q + 1 ≤ 13 * q ^ 2 : Prop

tests/lean/run/constProp.lean

@@ -8,8 +8,11 @@ inductive Val where
 instance : Coe Bool Val where
   coe b := .bool b
 
-instance : Coe Int Val where
-  coe i := .int i
+instance : NatCast Val where
+  natCast i := .int i
+
+instance : IntCast Val where
+  intCast i := .int i
 
 instance : OfNat Val n where
   ofNat := .int n

tests/lean/run/mathlibetaissue.lean

@@ -25,13 +25,6 @@ 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 NatCast (R : Type u) where
-class IntCast (R : Type u) where
-
-end Std.Classes.Cast
-
 section Std.Data.Int.Lemmas
 
 namespace Int

tests/lean/run/rational.lean

@@ -17,8 +17,15 @@ instance : Add Rat where
     pos := sorry
   }
 
-instance : Coe Int Rat where
-  coe n := {
+instance : NatCast Rat where
+  natCast n := {
+    num := n
+    den := 1
+    pos := by decide
+  }
+
+instance : IntCast Rat where
+  intCast n := {
     num := n
     den := 1
     pos := by decide