feat(kernel/inductive): improve how induction hypotheses are named

See doc/changes.md

doc/changes.md

@@ -56,6 +56,12 @@ master branch (aka work in progress branch)
 
 - The automatically generated recursor `C.rec` for an inductive datatype
   now uses `ih` to name induction hypotheses instead of `ih_1` if there is only one.
+  If there is more than one induction hypotheses, the name is generated by concatenating `ih_`
+  before the constructor field name. For example, for the constructor
+  ```
+  | node (left right : tree) (val : A) : tree
+  ```
+  The induction hypotheses are now named: `ih_left` and `ih_right`.
   This change only affects tactical proofs where explicit names are not provided
   to `induction` and `cases` tactics.
 

library/data/rbtree/basic.lean

@@ -75,8 +75,8 @@ begin
   case leaf { cases hs, assumption },
   all_goals {
     cases hs,
-    have h₁ := t_ih_1 hs_hs₁,
-    have h₂ := t_ih_2 hs_hs₂,
+    have h₁ := t_ih_lchild hs_hs₁,
+    have h₂ := t_ih_rchild hs_hs₂,
     cases lo with lo; cases hi with hi; simp [lift] at *,
     apply trans_of lt h₁ h₂,
   }
@@ -88,42 +88,42 @@ lemma is_searchable_of_is_searchable_of_incomp [is_strict_weak_order α lt] {t}
 begin
   induction t; intros; is_searchable_tactic,
   { cases lo; simp [lift, *] at *, apply lt_of_lt_of_incomp, assumption, exact ⟨hc.2, hc.1⟩ },
-  all_goals { apply t_ih_2 hc hs_hs₂ }
+  all_goals { apply t_ih_rchild hc hs_hs₂ }
 end
 
 lemma is_searchable_of_incomp_of_is_searchable [is_strict_weak_order α lt] {t} : ∀ {lo lo' hi} (hc : ¬ lt lo' lo ∧ ¬ lt lo lo') (hs : is_searchable lt t (some lo) hi), is_searchable lt t (some lo') hi :=
 begin
   induction t; intros; is_searchable_tactic,
   { cases hi; simp [lift, *] at *, apply lt_of_incomp_of_lt, assumption, assumption },
-  all_goals { apply t_ih_1 hc hs_hs₁ }
+  all_goals { apply t_ih_lchild hc hs_hs₁ }
 end
 
 lemma is_searchable_some_low_of_is_searchable_of_lt {t} [is_trans α lt] : ∀ {lo hi lo'} (hlt : lt lo' lo) (hs : is_searchable lt t (some lo) hi), is_searchable lt t (some lo') hi :=
 begin
   induction t; intros; is_searchable_tactic,
   { cases hi; simp [lift, *] at *, apply trans_of lt hlt, assumption },
-  all_goals { apply t_ih_1 hlt hs_hs₁ }
+  all_goals { apply t_ih_lchild hlt hs_hs₁ }
 end
 
 lemma is_searchable_none_low_of_is_searchable_some_low {t} : ∀ {y hi} (hlt : is_searchable lt t (some y) hi), is_searchable lt t none hi :=
 begin
   induction t; intros; is_searchable_tactic,
   { simp [lift] },
-  all_goals { apply t_ih_1 hlt_hs₁ }
+  all_goals { apply t_ih_lchild hlt_hs₁ }
 end
 
 lemma is_searchable_some_high_of_is_searchable_of_lt {t} [is_trans α lt] : ∀ {lo hi hi'} (hlt : lt hi hi') (hs : is_searchable lt t lo (some hi)), is_searchable lt t lo (some hi') :=
 begin
   induction t; intros; is_searchable_tactic,
   { cases lo; simp [lift, *] at *, apply trans_of lt, assumption, assumption},
-  all_goals { apply t_ih_2 hlt hs_hs₂ }
+  all_goals { apply t_ih_rchild hlt hs_hs₂ }
 end
 
 lemma is_searchable_none_high_of_is_searchable_some_high {t} : ∀ {lo y} (hlt : is_searchable lt t lo (some y)), is_searchable lt t lo none :=
 begin
   induction t; intros; is_searchable_tactic,
   { cases lo; simp [lift] },
-  all_goals { apply t_ih_2 hlt_hs₂ }
+  all_goals { apply t_ih_rchild hlt_hs₂ }
 end
 
 lemma range [is_strict_weak_order α lt] {t : rbnode α} {x} : ∀ {lo hi}, is_searchable lt t lo hi → mem lt x t → lift lt lo (some x) ∧ lift lt (some x) hi :=
@@ -137,7 +137,7 @@ begin
     have lo_val : lift lt lo (some t_val), { apply lo_lt_hi, assumption },
     blast_disjs,
     {
-      have h₃ : lift lt lo (some x) ∧ lift lt (some x) (some t_val), { apply t_ih_1, assumption, assumption },
+      have h₃ : lift lt lo (some x) ∧ lift lt (some x) (some t_val), { apply t_ih_lchild, assumption, assumption },
       cases h₃ with lo_x x_val,
       split,
       show lift lt lo (some x), { assumption },
@@ -156,7 +156,7 @@ begin
       { apply lt_of_incomp_of_lt _ val_hi, simp [*] }
     },
     {
-      have h₃ : lift lt (some t_val) (some x) ∧ lift lt (some x) hi, { apply t_ih_2, assumption, assumption },
+      have h₃ : lift lt (some t_val) (some x) ∧ lift lt (some x) hi, { apply t_ih_rchild, assumption, assumption },
       cases h₃ with val_x x_hi,
       cases lo with lo; cases hi with hi; simp [lift] at *,
       { assumption },
@@ -232,8 +232,8 @@ begin
     apply succ_le_succ,
     apply max_le; assumption },
   case black_rb {
-    have : depth max h_l ≤ 2*h_n + 1, from le_trans h_ih_1 (upper_le _ _),
-    have : depth max h_r ≤ 2*h_n + 1, from le_trans h_ih_2 (upper_le _ _),
+    have : depth max h_l ≤ 2*h_n + 1, from le_trans h_ih_rb_l (upper_le _ _),
+    have : depth max h_r ≤ 2*h_n + 1, from le_trans h_ih_rb_r (upper_le _ _),
     suffices new : max (depth max h_l) (depth max h_r) + 1 ≤ 2 * h_n + 2*1,
     { simp [depth, upper, succ_eq_add_one, left_distrib, *] at * },
     apply succ_le_succ, apply max_le; assumption

library/data/rbtree/find.lean

@@ -80,7 +80,7 @@ end
 lemma mem_of_mem_exact {lt} [is_irrefl α lt] {x t} : mem_exact x t → mem lt x t :=
 begin
   induction t; simp [mem_exact, mem]; intro h,
-  all_goals { blast_disjs, simp [t_ih_1 h], simp [h, irrefl_of lt t_val], simp [t_ih_2 h] }
+  all_goals { blast_disjs, simp [t_ih_lchild h], simp [h, irrefl_of lt t_val], simp [t_ih_rchild h] }
 end
 
 lemma find_correct_exact {t : rbnode α} {lt x} [decidable_rel lt] [is_strict_weak_order α lt] : ∀ {lo hi} (hs : is_searchable lt t lo hi), mem_exact x t ↔ find lt t x = some x :=

library/data/rbtree/main.lean

@@ -48,9 +48,9 @@ lemma mem_of_mem_of_eqv [is_strict_weak_order α lt] {t : rbtree α lt} {a b :
 begin
   cases t with n p; simp [has_mem.mem, rbtree.mem]; clear p; induction n; simp [rbnode.mem, strict_weak_order.equiv]; intros h₁ h₂; blast_disjs,
   iterate 2 {
-    { have : rbnode.mem lt b n_lchild := n_ih_1 h₁ h₂, simp [this] },
+    { have : rbnode.mem lt b n_lchild := n_ih_lchild h₁ h₂, simp [this] },
     { simp [incomp_trans_of lt h₂.swap h₁] },
-    { have : rbnode.mem lt b n_rchild := n_ih_2 h₁ h₂, simp [this] } }
+    { have : rbnode.mem lt b n_rchild := n_ih_rchild h₁ h₂, simp [this] } }
 end
 
 variables [decidable_rel lt]

library/data/rbtree/min_max.lean

@@ -16,7 +16,7 @@ begin
    all_goals {
      cases t_lchild; simp [rbnode.min]; intro h,
      { injection h, subst t_val, simp [mem, irrefl_of lt a] },
-     all_goals { rw [mem], simp [t_ih_1 h] } }
+     all_goals { rw [mem], simp [t_ih_lchild h] } }
 end
 
 lemma mem_of_max_eq (lt : α → α → Prop) [is_irrefl α lt] {a : α} {t : rbnode α} : t.max = some a → mem lt a t :=
@@ -26,7 +26,7 @@ begin
    all_goals {
      cases t_rchild; simp [rbnode.max]; intro h,
      { injection h, subst t_val, simp [mem, irrefl_of lt a] },
-     all_goals { rw [mem], simp [t_ih_2 h] } }
+     all_goals { rw [mem], simp [t_ih_rchild h] } }
 end
 
 variables [decidable_rel lt] [is_strict_weak_order α lt]
@@ -38,7 +38,7 @@ begin
   all_goals {
     cases t_lchild; simp [rbnode.min]; intro h,
     { contradiction },
-    all_goals { have := t_ih_1 h, contradiction } }
+    all_goals { have := t_ih_lchild h, contradiction } }
 end
 
 lemma eq_leaf_of_max_eq_none {t : rbnode α} : t.max = none → t = leaf :=
@@ -48,7 +48,7 @@ begin
   all_goals {
     cases t_rchild; simp [rbnode.max]; intro h,
     { contradiction },
-    all_goals { have := t_ih_2 h, contradiction } }
+    all_goals { have := t_ih_rchild h, contradiction } }
 end
 
 lemma min_is_minimal {a : α} {t : rbnode α} : ∀ {lo hi}, is_searchable lt t lo hi → t.min = some a → ∀ {b}, mem lt b t → a ≈[lt] b ∨ lt a b :=
@@ -66,7 +66,7 @@ begin
       have hs' := hs,
       cases hs, simp [rbnode.min] at hmin,
       rw [mem] at hmem, blast_disjs,
-      { exact t_ih_1 hs_hs₁ hmin hmem },
+      { exact t_ih_lchild hs_hs₁ hmin hmem },
       { have hmm       := mem_of_min_eq lt hmin,
         have a_lt_val  := lt_of_mem_left hs' (by constructor) hmm,
         have a_lt_b    := lt_of_lt_of_incomp a_lt_val hmem.swap,
@@ -98,7 +98,7 @@ begin
         have val_lt_a  := lt_of_mem_right hs' (by constructor) hmm,
         have a_lt_b    := lt_of_incomp_of_lt hmem val_lt_a,
         right, assumption },
-      { exact t_ih_2 hs_hs₂ hmax hmem } } }
+      { exact t_ih_rchild hs_hs₂ hmax hmem } } }
 end
 
 end rbnode

src/kernel/inductive/inductive.cpp

@@ -599,8 +599,14 @@ struct add_inductive_fn {
                 }
                 expr v_i_ty = Pi(xs, C_app);
                 name ih("ih");
-                if (u.size() > 1)
-                    ih = ih.append_after(i+1);
+                if (u.size() > 1) {
+                    name const & u_i_name = mlocal_pp_name(u_i);
+                    if (u_i_name.is_atomic() && u_i_name.is_string()) {
+                        ih = ih.append_after("_").append_after(u_i_name.get_string());
+                    } else {
+                        ih = ih.append_after(i+1);
+                    }
+                }
                 expr v_i    = mk_local(mk_fresh_name(), ih, v_i_ty, binder_info());
                 v.push_back(v_i);
             }

tests/lean/induction_naming2.lean

@@ -0,0 +1,12 @@
+inductive tree
+| leaf : tree
+| node (left : tree) (val : nat) (right : tree) : tree
+
+constant foo : tree → tree
+
+example (a : tree) : foo a = a :=
+begin
+  induction a,
+  trace_state,
+  repeat { admit }
+end

tests/lean/induction_naming2.lean.expected.out

@@ -0,0 +1,9 @@
+⊢ foo tree.leaf = tree.leaf
+
+a_left : tree,
+a_val : ℕ,
+a_right : tree,
+a_ih_left : foo a_left = a_left,
+a_ih_right : foo a_right = a_right
+⊢ foo (tree.node a_left a_val a_right) = tree.node a_left a_val a_right
+induction_naming2.lean:7:0: warning: declaration '[anonymous]' uses sorry