From dce86b3a847bfd43f707f4c05b8abb44d1ef2ccd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Jun 2015 17:16:10 -0700
Subject: [PATCH] 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   | 10 +++++++---
 src/library/constants.cpp |  4 ++++
 src/library/constants.h   |  1 +
 src/library/constants.txt |  1 +
 4 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/library/init/logic.lean b/library/init/logic.lean
index 8711443ee0..a4275a13ce 100644
--- a/library/init/logic.lean
+++ b/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₂ :=
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index b7b3c73329..c129232822 100644
--- a/src/library/constants.cpp
+++ b/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; }
diff --git a/src/library/constants.h b/src/library/constants.h
index a628fc32cb..aca24202da 100644
--- a/src/library/constants.h
+++ b/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();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 50d25426eb..c2426595d2 100644
--- a/src/library/constants.txt
+++ b/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