feat(library/init/logic): add 'eq.drec' (in standard Lean) with a signature very similar to eq.rec in the HoTT library

library/init/logic.lean

@@ -40,10 +40,17 @@ theorem rfl {A : Type} {a : A} : a = a := eq.refl a
 theorem proof_irrel {a : Prop} (H₁ H₂ : a) : H₁ = H₂ :=
 rfl
 
+-- Remark: we provide the universe levels explicitly to make sure `eq.drec` has the same type of `eq.rec` in the HoTT library
+protected theorem eq.drec.{l₁ l₂} {A : Type.{l₂}} {a : A} {C : Π (x : A), a = x → Type.{l₁}} (h₁ : C a (eq.refl a)) {b : A} (h₂ : a = b) : C b h₂ :=
+eq.rec (λh₂ : a = a, show C a h₂, from h₁) h₂ h₂
+
 namespace eq
   variables {A : Type}
   variables {a b c a': A}
 
+  protected theorem drec_on {a : A} {C : Π (x : A), a = x → Type} {b : A} (h₂ : a = b) (h₁ : C a (refl a)) : C b h₂ :=
+  eq.drec h₁ h₂
+
   theorem subst {P : A → Prop} (H₁ : a = b) (H₂ : P a) : P b :=
   eq.rec H₂ H₁
 
@@ -58,9 +65,6 @@ namespace eq
     notation H1 ⬝ H2 := trans H1 H2
     notation H1 ▸ H2 := subst H1 H2
   end ops
-
-  protected theorem drec_on {B : Πa' : A, a = a' → Type} (H₁ : a = a') (H₂ : B a (refl a)) : B a' H₁ :=
-  eq.rec (λH₁ : a = a, show B a H₁, from H₂) H₁ H₁
 end eq
 
 theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=

src/library/constants.cpp

@@ -21,6 +21,7 @@ name const * g_eq = nullptr;
 name const * g_eq_elim_inv_inv = nullptr;
 name const * g_eq_intro = nullptr;
 name const * g_eq_rec = nullptr;
+name const * g_eq_drec = nullptr;
 name const * g_eq_rec_eq = nullptr;
 name const * g_eq_refl = nullptr;
 name const * g_eq_symm = nullptr;
@@ -157,6 +158,7 @@ void initialize_constants() {
     g_eq_elim_inv_inv = new name{"eq", "elim_inv_inv"};
     g_eq_intro = new name{"eq", "intro"};
     g_eq_rec = new name{"eq", "rec"};
+    g_eq_drec = new name{"eq", "drec"};
     g_eq_rec_eq = new name{"eq_rec_eq"};
     g_eq_refl = new name{"eq", "refl"};
     g_eq_symm = new name{"eq", "symm"};
@@ -294,6 +296,7 @@ void finalize_constants() {
     delete g_eq_elim_inv_inv;
     delete g_eq_intro;
     delete g_eq_rec;
+    delete g_eq_drec;
     delete g_eq_rec_eq;
     delete g_eq_refl;
     delete g_eq_symm;
@@ -430,6 +433,7 @@ name const & get_eq_name() { return *g_eq; }
 name const & get_eq_elim_inv_inv_name() { return *g_eq_elim_inv_inv; }
 name const & get_eq_intro_name() { return *g_eq_intro; }
 name const & get_eq_rec_name() { return *g_eq_rec; }
+name const & get_eq_drec_name() { return *g_eq_drec; }
 name const & get_eq_rec_eq_name() { return *g_eq_rec_eq; }
 name const & get_eq_refl_name() { return *g_eq_refl; }
 name const & get_eq_symm_name() { return *g_eq_symm; }

src/library/constants.h

@@ -23,6 +23,7 @@ name const & get_eq_name();
 name const & get_eq_elim_inv_inv_name();
 name const & get_eq_intro_name();
 name const & get_eq_rec_name();
+name const & get_eq_drec_name();
 name const & get_eq_rec_eq_name();
 name const & get_eq_refl_name();
 name const & get_eq_symm_name();

src/library/constants.txt

@@ -16,6 +16,7 @@ eq
 eq.elim_inv_inv
 eq.intro
 eq.rec
+eq.drec
 eq_rec_eq
 eq.refl
 eq.symm