feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes

library/data/bool.lean

@@ -10,9 +10,6 @@ inductive bool : Type :=
   ff : bool,
   tt : bool
 namespace bool
-  protected definition rec_on {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b :=
-  rec H₁ H₂ b
-
   protected definition cases_on {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b :=
   rec H₁ H₂ b
 

library/data/list/basic.lean

@@ -29,10 +29,6 @@ protected theorem cases_on {P : list T → Prop} (l : list T) (Hnil : P nil)
     (Hcons : ∀ (x : T) (l : list T), P (x::l)) : P l :=
 induction_on l Hnil (take x l IH, Hcons x l)
 
-protected definition rec_on {A : Type} {C : list A → Type} (l : list A)
-    (H1 : C nil) (H2 : Π (h : A) (t : list A), C t → C (h::t)) : C l :=
-  rec H1 H2 l
-
 -- Concat
 -- ------
 

library/data/nat/basic.lean

@@ -34,9 +34,6 @@ protected theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P zero) (H2 :
   P a :=
 nat.rec H1 H2 a
 
-protected definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n :=
-nat.rec H1 H2 n
-
 protected definition is_inhabited [instance] : inhabited nat :=
 inhabited.mk zero
 

library/data/num.lean

@@ -22,10 +22,6 @@ namespace pos_num
       (H₁ : P one) (H₂ : ∀ (n : pos_num), P n → P (bit1 n)) (H₃ : ∀ (n : pos_num), P n → P (bit0 n)) : P a :=
   rec H₁ H₂ H₃ a
 
-  protected definition rec_on {P : pos_num → Type} (a : pos_num)
-      (H₁ : P one) (H₂ : ∀ (n : pos_num), P n → P (bit1 n)) (H₃ : ∀ (n : pos_num), P n → P (bit0 n)) : P a :=
-  rec H₁ H₂ H₃ a
-
   definition succ (a : pos_num) : pos_num :=
   rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n)
 
@@ -133,10 +129,6 @@ namespace num
       (H₁ : P zero) (H₂ : ∀ (p : pos_num), P (pos p)) : P a :=
   rec H₁ H₂ a
 
-  protected definition rec_on {P : num → Type} (a : num)
-      (H₁ : P zero) (H₂ : ∀ (p : pos_num), P (pos p)) : P a :=
-  rec H₁ H₂ a
-
   definition succ (a : num) : num :=
   rec_on a (pos one) (λp, pos (succ p))
 

library/data/option.lean

@@ -14,10 +14,6 @@ namespace option
     (H1 : p none) (H2 : ∀a, p (some a)) : p o :=
   rec H1 H2 o
 
-  protected definition rec_on {A : Type} {C : option A → Type} (o : option A)
-    (H1 : C none) (H2 : ∀a, C (some a)) : C o :=
-  rec H1 H2 o
-
   definition is_none {A : Type} (o : option A) : Prop :=
   rec true (λ a, false) o
 

library/data/quotient/basic.lean

@@ -115,17 +115,17 @@ R_intro Q Ha Hc Hac
 
 definition rec {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (Q : is_quotient R abs rep) {C : B → Type} (f : forall (a : A), C (abs a)) (b : B) : C b :=
-eq.rec_on (abs_rep Q b) (f (rep b))
+eq.drec_on (abs_rep Q b) (f (rep b))
 
 theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (Q : is_quotient R abs rep) {C : B → Type} {f : forall (a : A), C (abs a)}
-  (H : forall (r s : A) (H' : R r s), eq.rec_on (eq_abs Q H') (f r) = f s)
+  (H : forall (r s : A) (H' : R r s), eq.drec_on (eq_abs Q H') (f r) = f s)
   {a : A} (Ha : R a a) : rec Q f (abs a) = f a :=
 have H2 [visible] : R a (rep (abs a)), from R_rep_abs Q Ha,
 calc
-  rec Q f (abs a) =  eq.rec_on _ (f (rep (abs a))) : rfl
+  rec Q f (abs a) =  eq.drec_on _ (f (rep (abs a))) : rfl
-    ... = eq.rec_on _ (eq.rec_on _ (f a)) : {(H _ _ H2)⁻¹}
+    ... = eq.drec_on _ (eq.drec_on _ (f a)) : {(H _ _ H2)⁻¹}
-    ... = eq.rec_on _ (f a) : eq.rec_on_compose (eq_abs Q H2) _ _
+    ... = eq.drec_on _ (f a) : eq.rec_on_compose (eq_abs Q H2) _ _
     ... = f a : eq.rec_on_id (eq.trans (eq_abs Q H2) (abs_rep Q (abs a))) _
 
 definition rec_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}

library/data/sigma.lean

@@ -25,12 +25,12 @@ namespace sigma
   theorem dpair_ext (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p :=
   destruct p (take a b, rfl)
 
-  theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
+  theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂) :
     dpair a₁ b₁ = dpair a₂ b₂ :=
   congr_arg2_dep dpair H₁ H₂
 
   protected theorem equal {p₁ p₂ : Σx : A, B x} :
-    ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.rec_on H₁ (dpr2 p₁) = dpr2 p₂), p₁ = p₂ :=
+    ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.drec_on H₁ (dpr2 p₁) = dpr2 p₂), p₁ = p₂ :=
   destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, dpair_eq H₁ H₂))
 
   protected definition is_inhabited [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) :
@@ -49,19 +49,19 @@ namespace sigma
   definition dpr4  (x : Σ a b c, D a b c) := dpr2 (dpr2 (dpr2 x))
 
   theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
-      (H₁ : a₁ = a₂)  (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) :
+      (H₁ : a₁ = a₂)  (H₂ : eq.drec_on H₁ b₁ = b₂) (H₃ : eq.drec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) :
     dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
   congr_arg3_dep dtrip H₁ H₂ H₃
 
   theorem dtrip_eq_ndep {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
       {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂)  (H₂ : b₁ = b₂)
-      (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
+      (H₃ : eq.drec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
     dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
   congr_arg3_ndep_dep dtrip H₁ H₂ H₃
 
   theorem trip.equal_ndep {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
       ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : dpr2' p₁ = dpr2' p₂)
-      (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) (dpr3 p₁) = dpr3 p₂), p₁ = p₂ :=
+      (H₃ : eq.drec_on (congr_arg2 C H₁ H₂) (dpr3 p₁) = dpr3 p₂), p₁ = p₂ :=
   destruct p₁ (take a₁ q₁, destruct q₁ (take b₁ c₁, destruct p₂ (take a₂ q₂, destruct q₂
     (take b₂ c₂ H₁ H₂ H₃, dtrip_eq_ndep H₁ H₂ H₃))))
 

library/data/sum.lean

@@ -20,9 +20,6 @@ namespace sum
 
   variables {A B : Type}
   variables {a a₁ a₂ : A} {b b₁ b₂ : B}
-  protected definition rec_on {C : (A ⊎ B) → Type} (s : A ⊎ B) (H₁ : ∀a : A, C (inl B a)) (H₂ : ∀b : B, C (inr A b)) : C s :=
-  rec H₁ H₂ s
-
   protected definition cases_on {P : (A ⊎ B) → Prop} (s : A ⊎ B) (H₁ : ∀a : A, P (inl B a)) (H₂ : ∀b : B, P (inr A b)) : P s :=
   rec H₁ H₂ s
 

library/data/vector.lean

@@ -15,10 +15,6 @@ namespace vector
   section sc_vector
   variable {T : Type}
 
-  protected theorem rec_on {C : ∀ (n : ℕ), vector T n → Type} {n : ℕ} (v : vector T n) (Hnil : C 0 nil)
-    (Hcons : ∀(x : T) {n : ℕ} (w : vector T n), C n w → C (succ n) (cons x w)) : C n v :=
-  rec Hnil Hcons v
-
   protected theorem induction_on {C : ∀ (n : ℕ), vector T n → Prop} {n : ℕ} (v : vector T n) (Hnil : C 0 nil)
     (Hcons : ∀(x : T) {n : ℕ} (w : vector T n), C n w → C (succ n) (cons x w)) : C n v :=
   rec_on v Hnil Hcons

library/hott/equiv.lean

@@ -126,7 +126,7 @@ namespace IsEquiv
 
   --TODO: Maybe wait until rewrite rules are available.
   definition inv_closed (Hf : IsEquiv f) : (IsEquiv (inv Hf)) :=
-    IsEquiv_mk sorry sorry sorry sorry
+    sorry -- IsEquiv_mk sorry sorry sorry sorry
 
   definition cancel_R (Hf : IsEquiv f) (Hgf : IsEquiv (g ∘ f)) : (IsEquiv g) :=
     homotopic (comp_closed (inv_closed Hf) Hgf) (λb, ap g (retr Hf b))

library/logic/cast.lean

@@ -23,11 +23,11 @@ refl : heq a a
 infixl `==`:50 := heq
 
 namespace heq
-  theorem rec_on {A B : Type} {a : A} {b : B} {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ :=
+  theorem drec_on {A B : Type} {a : A} {b : B} {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ :=
   rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁
 
   theorem subst {A B : Type} {a : A} {b : B} {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b :=
-  rec H₂ H₁
+  rec_on H₁ H₂
 
   theorem symm {A B : Type} {a : A} {b : B} (H : a == b) : b == a :=
   subst H (refl a)
@@ -48,7 +48,7 @@ namespace heq
   trans (from_eq H₁) H₂
 
   theorem to_cast_eq {A B : Type} {a : A} {b : B} (H : a == b) : cast (type_eq H) a = b :=
-  rec_on H !cast_eq
+  drec_on H !cast_eq
 
   theorem to_eq {A : Type} {a b : A} (H : a == b) : a = b :=
   calc a = cast (eq.refl A) a : !cast_eq⁻¹

library/logic/decidable.lean

@@ -19,11 +19,6 @@ namespace decidable
   protected theorem induction_on {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
   decidable.rec H1 H2 H
 
-  protected definition rec_on {C : decidable p → Type} (H : decidable p)
-    (H1 : Π(a : p), C (inl a)) (H2 : Π(a : ¬p), C (inr a)) :
-    C H :=
-  decidable.rec H1 H2 H
-
   definition rec_on_true [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : p) (H4 : H1 H3)
       : rec_on H H1 H2 :=
   rec_on H (λh, H4) (λh, false.rec_type _ (h H3))

library/logic/eq.lean

@@ -53,31 +53,31 @@ calc_trans eq.trans
 open eq.ops
 
 namespace eq
-  definition rec_on {A : Type} {a a' : A} {B : Πa' : A, a = a' → Type} (H₁ : a = a') (H₂ : B a (refl a)) : B a' H₁ :=
+  definition drec_on {A : Type} {a a' : A} {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₁
 
-  theorem rec_on_id {A : Type} {a : A} {B : Πa' : A, a = a' → Type} (H : a = a) (b : B a H) : rec_on H b = b :=
+  theorem rec_on_id {A : Type} {a : A} {B : Πa' : A, a = a' → Type} (H : a = a) (b : B a H) : drec_on H b = b :=
   rfl
 
-  theorem rec_on_constant {A : Type} {a a' : A} {B : Type} (H : a = a') (b : B) : rec_on H b = b :=
+  theorem rec_on_constant {A : Type} {a a' : A} {B : Type} (H : a = a') (b : B) : drec_on H b = b :=
-  rec_on H (λ(H' : a = a), rec_on_id H' b) H
+  drec_on H (λ(H' : a = a), rec_on_id H' b) H
 
   theorem rec_on_constant2 {A : Type} {a₁ a₂ a₃ a₄ : A} {B : Type} (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) :
-                           rec_on H₁ b = rec_on H₂ b :=
+                           drec_on H₁ b = drec_on H₂ b :=
   rec_on_constant H₁ b ⬝ (rec_on_constant H₂ b)⁻¹
 
   theorem rec_on_irrel {A B : Type} {a a' : A} {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) :
-                       rec_on H b = rec_on H' b :=
+                       drec_on H b = drec_on H' b :=
-  rec_on H (λ(H : a = a) (H' : f a = f a), rec_on_id H b ⬝ rec_on_id H' b⁻¹) H H'
+  drec_on H (λ(H : a = a) (H' : f a = f a), rec_on_id H b ⬝ rec_on_id H' b⁻¹) H H'
 
   theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec b H = b :=
   rfl
 
   theorem rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c)
           (u : P a) :
-    rec_on H₂ (rec_on H₁ u) = rec_on (trans H₁ H₂) u :=
+    drec_on H₂ (drec_on H₁ u) = drec_on (trans H₁ H₂) u :=
-    (show ∀ H₂ : b = c, rec_on H₂ (rec_on H₁ u) = rec_on (trans H₁ H₂) u,
+    (show ∀ H₂ : b = c, drec_on H₂ (drec_on H₁ u) = drec_on (trans H₁ H₂) u,
-      from rec_on H₂ (take (H₂ : b = b), rec_on_id H₂ _))
+      from drec_on H₂ (take (H₂ : b = b), rec_on_id H₂ _))
     H₂
 end eq
 
@@ -131,21 +131,21 @@ section
             {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
             {d₁ : D a₁ b₁ c₁} {d₂ : D a₂ b₂ c₂}
 
-  theorem congr_arg2_dep (f : Πa, B a → R) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂)
+  theorem congr_arg2_dep (f : Πa, B a → R) (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂)
       : f a₁ b₁ = f a₂ b₂ :=
-  eq.rec_on H₁
+  eq.drec_on H₁
-    (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.rec_on H₁ b₁ = b₂),
+    (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.drec_on H₁ b₁ = b₂),
       calc
-        f a₁ b₁ = f a₁ (eq.rec_on H₁ b₁) : {(eq.rec_on_id H₁ b₁)⁻¹}
+        f a₁ b₁ = f a₁ (eq.drec_on H₁ b₁) : {(eq.rec_on_id H₁ b₁)⁻¹}
             ... = f a₁ b₂                : {H₂})
     b₂ H₁ H₂
 
-  theorem congr_arg3_dep (f : Πa b, C a b → R) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂)
+  theorem congr_arg3_dep (f : Πa b, C a b → R) (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂)
-      (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) : f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
+      (H₃ : eq.drec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) : f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
-  eq.rec_on H₁
+  eq.drec_on H₁
     (λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂)
-      (H₃ : (rec_on (congr_arg2_dep C (refl a₁) H₂) c₁) = c₂),
+      (H₃ : (drec_on (congr_arg2_dep C (refl a₁) H₂) c₁) = c₂),
-      have H₃' : eq.rec_on H₂ c₁ = c₂, from rec_on_irrel H₂ _ c₁ ⬝ H₃,
+      have H₃' : eq.drec_on H₂ c₁ = c₂, from rec_on_irrel H₂ _ c₁ ⬝ H₃,
       congr_arg2_dep (f a₁) H₂ H₃')
     b₂ H₂ c₂ H₃
 
@@ -164,7 +164,7 @@ end
 section
   variables {A B : Type} {C : A → B → Type} {R : Type}
   variables {a₁ a₂ : A} {b₁ b₂ : B} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
-  theorem congr_arg3_ndep_dep (f : Πa b, C a b → R) (H₁ : a₁ = a₂) (H₂ : b₁ = b₂) (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
+  theorem congr_arg3_ndep_dep (f : Πa b, C a b → R) (H₁ : a₁ = a₂) (H₂ : b₁ = b₂) (H₃ : eq.drec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
                               f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
   congr_arg3_dep f H₁ (rec_on_constant H₁ b₁ ⬝ H₂) H₃
 end

src/CMakeLists.txt

@@ -306,6 +306,8 @@ add_subdirectory(library)
 set(LEAN_LIBS ${LEAN_LIBS} library)
 add_subdirectory(library/tactic)
 set(LEAN_LIBS ${LEAN_LIBS} tactic)
+add_subdirectory(library/definitional)
+set(LEAN_LIBS ${LEAN_LIBS} definitional)
 add_subdirectory(library/error_handling)
 set(LEAN_LIBS ${LEAN_LIBS} error_handling)
 add_subdirectory(frontends/lean)

src/frontends/lean/inductive_cmd.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "library/protected.h"
 #include "library/explicit.h"
 #include "library/reducible.h"
+#include "library/definitional/rec_on.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/class.h"
@@ -646,6 +647,13 @@ struct inductive_cmd_fn {
         return env;
     }
 
+    environment mk_aux_decls(environment env, buffer<inductive_decl> const & decls) {
+        for (inductive_decl const & d : decls) {
+            env = mk_rec_on(env, inductive_decl_name(d));
+        }
+        return env;
+    }
+
     /** \brief Auxiliary method used for debugging */
     void display(std::ostream & out, buffer<inductive_decl> const & decls) {
         if (!m_levels.empty()) {
@@ -681,7 +689,8 @@ struct inductive_cmd_fn {
         environment env = module::add_inductive(m_p.env(), ls, m_num_params, to_list(decls.begin(), decls.end()));
         update_declaration_index(env);
         env = add_aliases(env, ls, locals, decls);
-        return apply_modifiers(env);
+        env = apply_modifiers(env);
+        return mk_aux_decls(env, decls);
     }
 };
 

src/library/definitional/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_library(definitional rec_on.cpp)
+
+target_link_libraries(definitional ${LEAN_LIBS})

src/library/definitional/rec_on.cpp

@@ -0,0 +1,57 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/environment.h"
+#include "kernel/instantiate.h"
+#include "kernel/abstract.h"
+#include "kernel/type_checker.h"
+#include "kernel/inductive/inductive.h"
+#include "library/module.h"
+#include "library/protected.h"
+
+namespace lean {
+environment mk_rec_on(environment const & env, name const & n) {
+    name rec_on_name(n, "rec_on");
+    name_generator ngen;
+    declaration rec_decl = env.get(inductive::get_elim_name(n));
+
+    buffer<expr> locals;
+    expr rec_type = rec_decl.get_type();
+    while (is_pi(rec_type)) {
+        expr local = mk_local(ngen.next(), binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type));
+        rec_type   = instantiate(binding_body(rec_type), local);
+        locals.push_back(local);
+    }
+
+    // locals order
+    //   A C minor_premises indices major-premise
+
+    // new_locals order
+    //   A C indices major-premise minor-premises
+    buffer<expr> new_locals;
+    unsigned idx_major_sz = *inductive::get_num_indices(env, n) + 1;
+    unsigned minor_sz     = *inductive::get_num_minor_premises(env, n);
+    unsigned AC_sz        = locals.size() - minor_sz - idx_major_sz;
+    for (unsigned i = 0; i < AC_sz; i++)
+        new_locals.push_back(locals[i]);
+    for (unsigned i = 0; i < idx_major_sz; i++)
+        new_locals.push_back(locals[AC_sz + minor_sz + i]);
+    for (unsigned i = 0; i < minor_sz; i++)
+        new_locals.push_back(locals[AC_sz + i]);
+    expr rec_on_type = Pi(new_locals, rec_type);
+
+    levels ls = param_names_to_levels(rec_decl.get_univ_params());
+    expr rec  = mk_constant(rec_decl.get_name(), ls);
+    expr rec_on_val = Fun(new_locals, mk_app(rec, locals));
+
+    bool opaque       = false;
+    bool use_conv_opt = true;
+    environment new_env = module::add(env,
+                                      check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(), rec_on_type, rec_on_val,
+                                                               opaque, rec_decl.get_module_idx(), use_conv_opt)));
+    return add_protected(new_env, rec_on_name);
+}
+}

src/library/definitional/rec_on.h

@@ -0,0 +1,17 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+
+namespace lean {
+/** \brief Given an inductive datatype \c n in \c env, add
+    <tt>n.rec_on</tt> to the environment.
+
+    \remark <tt>rec_on</tt> is based on <tt>n.rec</tt>
+*/
+environment mk_rec_on(environment const & env, name const & n);
+}

src/util/name_generator.cpp

@@ -9,6 +9,9 @@ Author: Leonardo de Moura
 #include "util/name_generator.h"
 
 namespace lean {
+static name * g_tmp_prefix = nullptr;
+name_generator::name_generator():name_generator(*g_tmp_prefix) {}
+
 name name_generator::next() {
     if (m_next_idx == std::numeric_limits<unsigned>::max()) {
         // avoid overflow
@@ -26,7 +29,6 @@ void swap(name_generator & a, name_generator & b) {
 }
 
 DECL_UDATA(name_generator)
-static name * g_tmp_prefix = nullptr;
 static int mk_name_generator(lua_State * L) {
     if (lua_gettop(L) == 0)
         return push_name_generator(L, name_generator(*g_tmp_prefix));

src/util/name_generator.h

@@ -21,6 +21,7 @@ class name_generator {
     unsigned m_next_idx;
 public:
     name_generator(name const & prefix):m_prefix(prefix), m_next_idx(0) { lean_assert(!prefix.is_anonymous()); }
+    name_generator();
 
     name const & prefix() const { return m_prefix; }
 

tests/lean/interactive/eq2.input.expected.out

@@ -75,7 +75,7 @@ H₃
 C a₁ b₂
 -- ACK
 -- SYNTH|134|53
-rec_on (congr_arg2_dep C (refl a₁) H₂) c₁
+drec_on (congr_arg2_dep C (refl a₁) H₂) c₁
 -- ACK
 -- SYMBOL|134|53
 _

tests/lean/interactive/eq2.lean

@@ -55,29 +55,29 @@ namespace eq
   -- definition rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
   -- eq.rec H2 H1
 
-  definition rec_on {A : Type} {a a' : A} {B : Πa' : A, a = a' → Type} (H1 : a = a') (H2 : B a (refl a)) : B a' H1 :=
+  definition drec_on {A : Type} {a a' : A} {B : Πa' : A, a = a' → Type} (H1 : a = a') (H2 : B a (refl a)) : B a' H1 :=
   eq.rec (λH1 : a = a, show B a H1, from H2) H1 H1
 
-  theorem rec_on_id {A : Type} {a : A} {B : Πa' : A, a = a' → Type} (H : a = a) (b : B a H) : rec_on H b = b :=
+  theorem drec_on_id {A : Type} {a : A} {B : Πa' : A, a = a' → Type} (H : a = a) (b : B a H) : drec_on H b = b :=
-  refl (rec_on rfl b)
+  refl (drec_on rfl b)
 
-  theorem rec_on_constant {A : Type} {a a' : A} {B : Type} (H : a = a') (b : B) : rec_on H b = b :=
+  theorem drec_on_constant {A : Type} {a a' : A} {B : Type} (H : a = a') (b : B) : drec_on H b = b :=
-  rec_on H (λ(H' : a = a), rec_on_id H' b) H
+  drec_on H (λ(H' : a = a), drec_on_id H' b) H
 
-  theorem rec_on_constant2 {A : Type} {a₁ a₂ a₃ a₄ : A} {B : Type} (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : rec_on H₁ b = rec_on H₂ b :=
+  theorem drec_on_constant2 {A : Type} {a₁ a₂ a₃ a₄ : A} {B : Type} (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : drec_on H₁ b = drec_on H₂ b :=
-  rec_on_constant H₁ b ⬝ rec_on_constant H₂ b ⁻¹
+  drec_on_constant H₁ b ⬝ drec_on_constant H₂ b ⁻¹
 
-  theorem rec_on_irrel {A B : Type} {a a' : A} {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) : rec_on H b = rec_on H' b :=
+  theorem drec_on_irrel {A B : Type} {a a' : A} {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) : drec_on H b = drec_on H' b :=
-  rec_on H (λ(H : a = a) (H' : f a = f a), rec_on_id H b ⬝ rec_on_id H' b⁻¹) H H'
+  drec_on H (λ(H : a = a) (H' : f a = f a), drec_on_id H b ⬝ drec_on_id H' b⁻¹) H H'
 
   theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec b H = b :=
   id_refl H⁻¹ ▸ refl (eq.rec b (refl a))
 
-  theorem rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)
+  theorem drec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)
           (u : P a) :
-    rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u :=
+    drec_on H2 (drec_on H1 u) = drec_on (trans H1 H2) u :=
-    (show ∀(H2 : b = c), rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u,
+    (show ∀(H2 : b = c), drec_on H2 (drec_on H1 u) = drec_on (trans H1 H2) u,
-      from rec_on H2 (take (H2 : b = b), rec_on_id H2 _))
+      from drec_on H2 (take (H2 : b = b), drec_on_id H2 _))
     H2
 end eq
 
@@ -118,29 +118,29 @@ theorem congr5 {A B C D E F : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D}
 Hf ▸ congr_arg5 f Ha Hb Hc Hd He
 
 theorem congr_arg2_dep {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A}
-    {b₁ : B a₁} {b₂ : B a₂} (f : Πa, B a → C) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
+    {b₁ : B a₁} {b₂ : B a₂} (f : Πa, B a → C) (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂) :
     f a₁ b₁ = f a₂ b₂ :=
-  eq.rec_on H₁
+  eq.drec_on H₁
-    (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.rec_on H₁ b₁ = b₂),
+    (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.drec_on H₁ b₁ = b₂),
       calc
-        f a₁ b₁ = f a₁ (eq.rec_on H₁ b₁) : {(eq.rec_on_id H₁ b₁)⁻¹}
+        f a₁ b₁ = f a₁ (eq.drec_on H₁ b₁) : {(eq.drec_on_id H₁ b₁)⁻¹}
             ... = f a₁ b₂                : {H₂})
     b₂ H₁ H₂
 
 theorem congr_arg3_dep {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Type} {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (f : Πa b, C a b → D)
-    (H₁ : a₁ = a₂)  (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) :
+    (H₁ : a₁ = a₂)  (H₂ : eq.drec_on H₁ b₁ = b₂) (H₃ : eq.drec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) :
   f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
-eq.rec_on H₁
+eq.drec_on H₁
   (λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂) (H₃ : _ = c₂),
-    have H₃' : eq.rec_on H₂ c₁ = c₂,
+    have H₃' : eq.drec_on H₂ c₁ = c₂,
-      from (rec_on_irrel H₂ (congr_arg2_dep C (refl a₁) H₂) c₁⁻¹) ▸ H₃,
+      from (drec_on_irrel H₂ (congr_arg2_dep C (refl a₁) H₂) c₁⁻¹) ▸ H₃,
     congr_arg2_dep (f a₁) H₂ H₃')
   b₂ H₂ c₂ H₃
 
 theorem congr_arg3_ndep_dep {A B : Type} {C : A → B → Type} {D : Type} {a₁ a₂ : A} {b₁ b₂ : B} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (f : Πa b, C a b → D)
-    (H₁ : a₁ = a₂)  (H₂ : b₁ = b₂) (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
+    (H₁ : a₁ = a₂)  (H₂ : b₁ = b₂) (H₃ : eq.drec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
   f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
-congr_arg3_dep f H₁ (rec_on_constant H₁ b₁ ⬝ H₂) H₃
+congr_arg3_dep f H₁ (drec_on_constant H₁ b₁ ⬝ H₂) H₃
 
 theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
 take x, congr_fun H x

tests/lean/interactive/findp.input.expected.out

@@ -4,6 +4,7 @@
 false|Prop
 false.rec|∀ (C : Prop), false → C
 false_elim|false → ?c
+false.rec_on|∀ (C : Prop), false → C
 not_false_trivial|¬ false
 true_ne_false|¬ true = false
 p_ne_false|?p → ?p ≠ false

tests/lean/interactive/num2.input.expected.out

@@ -10,6 +10,7 @@ pos_num.bit1|pos_num → pos_num
 pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
 pos_num.one|pos_num
 pos_num.num_bits|pos_num → pos_num
+pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num|Type
 -- ENDFINDP
 -- BEGINWAIT
@@ -24,6 +25,7 @@ pos_num.inc|pos_num → pos_num
 pos_num.bit1|pos_num → pos_num
 pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
 pos_num.one|pos_num
+pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num|Type
 -- ENDFINDP
 -- BEGINFINDP
@@ -34,5 +36,6 @@ pos_num.inc|pos_num → pos_num
 pos_num.bit1|pos_num → pos_num
 pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
 pos_num.one|pos_num
+pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num|Type
 -- ENDFINDP

tests/lean/run/sum_bug.lean

@@ -13,9 +13,6 @@ namespace sum
 reserve infixr `+`:25
 infixr `+` := sum
 
-definition rec_on {A B : Type} {C : (A + B) → Type} (s : A + B)
-  (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
-sum.rec H1 H2 s
 open eq
 
 theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 :=

tests/lean/run/tree.lean

@@ -15,8 +15,6 @@ namespace tree
     variables {A : Type} {C : tree A → Type}
     definition cases_on  (t : tree A) (e₁ : Πa, C (leaf a)) (e₂ : Πt₁ t₂, C (node t₁ t₂)) : C t :=
     rec e₁ (λt₁ t₂ r₁ r₂, e₂ t₁ t₂) t
-    definition rec_on (t : tree A) (e₁ : Πa, C (leaf a)) (e₂ : Πt₁ t₂ r₁ r₂, C (node t₁ t₂)) : C t :=
-    rec e₁ e₂ t
   end
 
   section

tests/lean/slow/nat_bug2.lean

@@ -39,9 +39,6 @@ theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m))
 theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) : P a
 := nat.rec H1 H2 a
 
-definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P 0) (H2 : ∀m, P m → P (succ m)) : P n
-:= nat.rec H1 H2 n
-
 -------------------------------------------------- succ pred
 
 theorem succ_ne_zero (n : ℕ) : succ n ≠ 0

tests/lean/slow/nat_wo_hints.lean

@@ -34,9 +34,6 @@ theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m))
 theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) : P a
 := nat.rec H1 H2 a
 
-definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P 0) (H2 : ∀m, P m → P (succ m)) : P n
-:= nat.rec H1 H2 n
-
 -------------------------------------------------- succ pred
 
 theorem succ_ne_zero (n : ℕ) : succ n ≠ 0