Expand ↑-notation. (leanprover#37)

Mathlib.lean

@@ -25,6 +25,7 @@ import Mathlib.Set
 import Mathlib.SetNotation
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.Block
+import Mathlib.Tactic.Coe
 import Mathlib.Tactic.NoMatch
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.OpenPrivate

Mathlib/Data/Int/Basic.lean

@@ -9,6 +9,7 @@ Original file license:
 -/
 
 import Mathlib.Data.Nat.Basic
+import Mathlib.Tactic.Coe
 open Nat
 
 /- ## Additional notation -/
@@ -29,8 +30,6 @@ def nat_abs := @natAbs
 def to_nat := @toNat
 def nat_mod := @natMod
 
-protected lemma coe_nat_eq (n : ℕ) : ↑n = ofNat n := rfl
-
 -- TODO: use these to instantiate "has zero" and "has one" classes
 -- (which rn seem to be in Mathlib.Algebra.Group.Defs for some reason)
 protected def zero : ℤ := ofNat 0
@@ -76,9 +75,9 @@ protected lemma coe_nat_zero : ↑(0 : ℕ) = (0 : ℤ) := rfl
 protected lemma coe_nat_one : ↑(1 : ℕ) = (1 : ℤ) := rfl
 protected lemma coe_nat_succ (n : ℕ) : (↑(succ n) : ℤ) = (↑n : Int) + 1 := rfl
 
-protected lemma coe_nat_add_out (m n : ℕ) : ↑m + ↑n = (m + n : ℤ) := rfl
-protected lemma coe_nat_mul_out (m n : ℕ) : ↑m * ↑n = (↑(m * n) : ℤ) := rfl
-protected lemma coe_nat_add_one_out (n : ℕ) : ↑n + (1 : ℤ) = ↑(succ n) := rfl
+protected lemma coe_nat_add_out (m n : ℕ) : (↑m + ↑n : ℤ) = ↑(m + n) := rfl
+protected lemma coe_nat_mul_out (m n : ℕ) : (↑m * ↑n : ℤ) = ↑(m * n) := rfl
+protected lemma coe_nat_add_one_out (n : ℕ) : n + (1 : ℤ) = ↑(succ n) := rfl
 
 /- ## These are only for internal use -/
 
@@ -514,18 +513,17 @@ by rw [Int.sub_eq_add_neg, ← Int.neg_add]; rfl
 
 protected lemma coe_nat_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n := of_nat_sub
 
-attribute [local simp] Int.sub_eq_add_neg
-
-protected lemma sub_nat_nat_eq_coe {m n : ℕ} : sub_nat_nat m n = ↑m - ↑n :=
-sub_nat_nat_elim m n (λm n i => i = ↑m - ↑n)
-  (λi n => by
-    simp [Int.coe_nat_add, Int.add_left_comm, Int.add_assoc, Int.add_right_neg]
-    rfl)
-  (λi n => by
-    simp
-    rw [Int.coe_nat_add, Int.coe_nat_add, Int.coe_nat_one, Int.neg_succ_of_nat_eq,
-         Int.neg_add, Int.neg_add, Int.neg_add, ← Int.add_assoc,
-        ← Int.add_assoc, Int.add_right_neg, Int.zero_add])
+protected lemma sub_nat_nat_eq_coe {m n : ℕ} : sub_nat_nat m n = ↑m - ↑n := by
+  refine sub_nat_nat_elim m n (fun m n i => i = ↑m - ↑n) ?p ?n
+  case p =>
+    intros i n
+    simp only [Int.coe_nat_add, Int.add_left_comm, Int.add_assoc, Int.add_right_neg, Int.sub_eq_add_neg]
+    rfl
+  case n =>
+    intros i n
+    simp only [neg_succ_of_nat_coe, of_nat_add, Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc]
+    rw [← @Int.sub_eq_add_neg n, ← of_nat_sub, Nat.sub_self, of_nat_zero, Int.zero_add]
+    apply Nat.le_refl
 
 theorem to_nat_sub (m n : ℕ) : to_nat (m - n : ℕ) = m - n := rfl
 

Mathlib/Data/Subtype.lean

@@ -7,6 +7,7 @@ Authors: Johannes Hölzl
 import Mathlib.Function
 import Mathlib.Logic.Function.Basic
 import Mathlib.Tactic.Basic
+import Mathlib.Tactic.Coe
 
 open Function
 
@@ -19,8 +20,6 @@ def simps.coe (x: Subtype p) : α := x
   instead of `x.1`. A similar result is `Subtype.mem` in `data.set.basic`. -/
 lemma prop (x : Subtype p) : p x := x.2
 
-@[simp] lemma val_eq_coe {x : Subtype p} : x.1 = ↑x := rfl
-
 @[simp] protected theorem «forall» {q : {a // p a} → Prop} :
   (∀ x, q x) ↔ (∀ a b, q ⟨a, b⟩) :=
 ⟨λ h a b => h ⟨a, b⟩, λ h ⟨a, b⟩ => h a b⟩
@@ -171,8 +170,6 @@ namespace Subtype
 /-! Some facts about sets, which require that `α` is a type. -/
 variable {α : Type _} {β : Type _} {γ : Type _} {p : α → Prop}
 
-@[simp] lemma coe_prop {S : Set α} (a : {a // a ∈ S}) : ↑a ∈ S := a.prop
-
-lemma val_prop {S : Set α} (a : {a // a ∈ S}) : a.val ∈ S := a.property
+@[simp] lemma val_prop {S : Set α} (a : {a // a ∈ S}) : a.val ∈ S := a.property
 
 end Subtype

Mathlib/Tactic/Coe.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2021 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Gabriel Ebner
+-/
+import Lean
+
+open Lean Elab Term
+
+/-!
+Redefine the ↑-notation to elaborate in the same way as type annotations
+(i.e., unfolding the coercion instance).
+-/
+
+namespace Lean.Elab.Term.CoeImpl
+
+scoped elab "coe%" x:term : term <= expectedType => do
+  tryPostponeIfMVar expectedType
+  let x ← elabTerm x none
+  synthesizeSyntheticMVarsUsingDefault
+  ensureHasType expectedType x
+
+macro_rules
+  | `(↑ $x) => `(coe% $x)