refactor(library): move 'cast' to init folder

library/init/logic.lean

@@ -130,6 +130,15 @@ attribute eq.refl [refl]
 attribute eq.trans [trans]
 attribute eq.symm [symm]
 
+definition cast {A B : Type} (H : A = B) (a : A) : B :=
+eq.rec a H
+
+theorem cast_proof_irrel {A B : Type} (H₁ H₂ : A = B) (a : A) : cast H₁ a = cast H₂ a :=
+rfl
+
+theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a :=
+rfl
+
 /- ne -/
 
 definition ne [reducible] {A : Type} (a b : A) := ¬(a = b)

library/logic/cast.lean

@@ -9,22 +9,6 @@ Casts and heterogeneous equality. See also init.datatypes and init.logic.
 import logic.eq logic.quantifiers
 open eq.ops
 
-section
-  universe variable u
-  variables {A B : Type.{u}}
-  definition cast (H : A = B) (a : A) : B :=
-  eq.rec a H
-
-  theorem cast_refl (a : A) : cast (eq.refl A) a = a :=
-  rfl
-
-  theorem cast_proof_irrel (H₁ H₂ : A = B) (a : A) : cast H₁ a = cast H₂ a :=
-  rfl
-
-  theorem cast_eq (H : A = A) (a : A) : cast H a = a :=
-  rfl
-end
-
 namespace heq
   universe variable u
   variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}

src/library/constants.cpp

@@ -18,6 +18,7 @@ name const * g_bit1 = nullptr;
 name const * g_bool = nullptr;
 name const * g_bool_ff = nullptr;
 name const * g_bool_tt = nullptr;
+name const * g_cast = nullptr;
 name const * g_char = nullptr;
 name const * g_char_mk = nullptr;
 name const * g_classical = nullptr;
@@ -282,6 +283,7 @@ void initialize_constants() {
     g_bool = new name{"bool"};
     g_bool_ff = new name{"bool", "ff"};
     g_bool_tt = new name{"bool", "tt"};
+    g_cast = new name{"cast"};
     g_char = new name{"char"};
     g_char_mk = new name{"char", "mk"};
     g_classical = new name{"classical"};
@@ -547,6 +549,7 @@ void finalize_constants() {
     delete g_bool;
     delete g_bool_ff;
     delete g_bool_tt;
+    delete g_cast;
     delete g_char;
     delete g_char_mk;
     delete g_classical;
@@ -811,6 +814,7 @@ name const & get_bit1_name() { return *g_bit1; }
 name const & get_bool_name() { return *g_bool; }
 name const & get_bool_ff_name() { return *g_bool_ff; }
 name const & get_bool_tt_name() { return *g_bool_tt; }
+name const & get_cast_name() { return *g_cast; }
 name const & get_char_name() { return *g_char; }
 name const & get_char_mk_name() { return *g_char_mk; }
 name const & get_classical_name() { return *g_classical; }

src/library/constants.h

@@ -20,6 +20,7 @@ name const & get_bit1_name();
 name const & get_bool_name();
 name const & get_bool_ff_name();
 name const & get_bool_tt_name();
+name const & get_cast_name();
 name const & get_char_name();
 name const & get_char_mk_name();
 name const & get_classical_name();

src/library/constants.txt

@@ -13,6 +13,7 @@ bit1
 bool
 bool.ff
 bool.tt
+cast
 char
 char.mk
 classical

tests/lean/run/cases_bug.lean

@@ -1,4 +1,4 @@
 import logic.cast
 
 theorem cast_heq : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
-| A A (eq.refl A) a := heq_of_eq (cast_refl a)
+| A A (eq.refl A) a := heq_of_eq !cast_eq