From eaef8dae20bd3237d792747b369fa0179cc34cf5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 7 Oct 2016 16:09:14 -0700
Subject: [PATCH] chore(library/init/core): remove unnecessary annotations

---
 library/init/core.lean                        | 79 ++++++++++++-------
 .../lean/defeq_simp_lemmas1.lean.expected.out | 15 ----
 .../lean/defeq_simp_lemmas2.lean.expected.out | 45 -----------
 tests/lean/run/converter.lean                 |  2 +
 4 files changed, 53 insertions(+), 88 deletions(-)

diff --git a/library/init/core.lean b/library/init/core.lean
index 0a4d9c2249..fb60948d17 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -454,90 +454,113 @@ From now on, the inductive compiler will automatically generate sizeof instances
 instance default_has_sizeof (A : Type u) : has_sizeof A :=
 ⟨λ a, nat.zero⟩
 
-attribute [simp, defeq, simp.sizeof]
+/- TODO(Leo): the [simp.sizeof] annotations are not really necessary.
+   What we need is a robust way of unfolding sizeof definitions. -/
+attribute [simp.sizeof]
 def default_has_sizeof_eq (A : Type u) (a : A) : @sizeof A (default_has_sizeof A) a = 0 :=
 rfl
 
-instance : has_sizeof nat := ⟨λ a, a⟩
+instance : has_sizeof nat :=
+⟨λ a, a⟩
 
-attribute [simp, defeq, simp.sizeof]
+attribute [simp.sizeof]
 def sizeof_nat_eq (a : nat) : sizeof a = a :=
 rfl
 
-instance (A : Type u) (B : Type v) [has_sizeof A] [has_sizeof B] : has_sizeof (prod A B) :=
-⟨λ p, prod.cases_on p (λ a b, 1 + sizeof a + sizeof b)⟩
+protected def prod.sizeof {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] : (prod A B) → nat
+| ⟨a, b⟩ := 1 + sizeof a + sizeof b
 
-attribute [simp, defeq, simp.sizeof]
+instance (A : Type u) (B : Type v) [has_sizeof A] [has_sizeof B] : has_sizeof (prod A B) :=
+⟨prod.sizeof⟩
+
+attribute [simp.sizeof]
 def sizeof_prod_eq {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] (a : A) (b : B) : sizeof (prod.mk a b) = 1 + sizeof a + sizeof b :=
 rfl
 
-instance (A : Type u) (B : Type v) [has_sizeof A] [has_sizeof B] : has_sizeof (sum A B) :=
-⟨λ s, sum.cases_on s (λ a, 1 + sizeof a) (λ b, 1 + sizeof b)⟩
+protected def sum.sizeof {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] : (sum A B) → nat
+| (sum.inl a) := 1 + sizeof a
+| (sum.inr b) := 1 + sizeof b
 
-attribute [simp, defeq, simp.sizeof]
+instance (A : Type u) (B : Type v) [has_sizeof A] [has_sizeof B] : has_sizeof (sum A B) :=
+⟨sum.sizeof⟩
+
+attribute [simp.sizeof]
 def sizeof_sum_eq_left {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] (a : A) : sizeof (@sum.inl A B a) = 1 + sizeof a :=
 rfl
 
-attribute [simp, defeq, simp.sizeof]
+attribute [simp.sizeof]
 def sizeof_sum_eq_right {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] (b : B) : sizeof (@sum.inr A B b) = 1 + sizeof b :=
 rfl
 
-instance (A : Type u) (B : A → Type v) [has_sizeof A] [∀ a, has_sizeof (B a)] : has_sizeof (sigma B) :=
-⟨λ p, sigma.cases_on p (λ a b, 1 + sizeof a + sizeof b)⟩
+protected def sigma.sizeof {A : Type u} {B : A → Type v} [has_sizeof A] [∀ a, has_sizeof (B a)] : sigma B → nat
+| ⟨a, b⟩ := 1 + sizeof a + sizeof b
 
-attribute [simp, defeq, simp.sizeof]
+instance (A : Type u) (B : A → Type v) [has_sizeof A] [∀ a, has_sizeof (B a)] : has_sizeof (sigma B) :=
+⟨sigma.sizeof⟩
+
+attribute [simp.sizeof]
 def sizeof_sigma_eq {A : Type u} {B : A → Type v} [has_sizeof A] [∀ a, has_sizeof (B a)] (a : A) (b : B a) : sizeof (@sigma.mk A B a b) = 1 + sizeof a + sizeof b :=
 rfl
 
 instance : has_sizeof unit := ⟨λ u, 1⟩
 
-attribute [simp, defeq, simp.sizeof]
+attribute [simp.sizeof]
 def sizeof_unit_eq (u : unit) : sizeof u = 1 :=
 rfl
 
 instance : has_sizeof poly_unit := ⟨λ u, 1⟩
 
-attribute [simp, defeq, simp.sizeof]
+attribute [simp.sizeof]
 def sizeof_poly_unit_eq (u : poly_unit) : sizeof u = 1 :=
 rfl
 
 instance : has_sizeof bool := ⟨λ u, 1⟩
 
-attribute [simp, defeq, simp.sizeof]
+attribute [simp.sizeof]
 def sizeof_bool_eq (b : bool) : sizeof b = 1 :=
 rfl
 
-instance : has_sizeof pos_num := ⟨λ p, nat.of_pos_num p⟩
+instance : has_sizeof pos_num :=
+⟨nat.of_pos_num⟩
 
-attribute [simp, defeq, simp.sizeof]
+attribute [simp.sizeof]
 def sizeof_pos_num_eq (p : pos_num) : sizeof p = nat.of_pos_num p :=
 rfl
 
-instance : has_sizeof num := ⟨λ p, nat.of_num p⟩
+instance : has_sizeof num :=
+⟨nat.of_num⟩
 
-attribute [simp, defeq, simp.sizeof]
+attribute [simp.sizeof]
 def sizeof_num_eq (n : num) : sizeof n = nat.of_num n :=
 rfl
 
-instance (A : Type u) [has_sizeof A] : has_sizeof (option A) :=
-⟨λ o, option.cases_on o 1 (λ a, 1 + sizeof a)⟩
+protected def option.sizeof {A : Type u} [has_sizeof A] : option A → nat
+| none     := 1
+| (some a) := 1 + sizeof a
 
-attribute [simp, defeq, simp.sizeof]
+instance (A : Type u) [has_sizeof A] : has_sizeof (option A) :=
+⟨option.sizeof⟩
+
+attribute [simp.sizeof]
 def sizeof_option_none_eq (A : Type u) [has_sizeof A] : sizeof (@none A) = 1 :=
 rfl
 
-attribute [simp, defeq, simp.sizeof]
+attribute [simp.sizeof]
 def sizeof_option_some_eq {A : Type u} [has_sizeof A] (a : A) : sizeof (some a) = 1 + sizeof a :=
 rfl
 
-instance (A : Type u) [has_sizeof A] : has_sizeof (list A) :=
-⟨λ l, list.rec_on l 1 (λ a t ih, 1 + sizeof a + ih)⟩
+protected def list.sizeof {A : Type u} [has_sizeof A] : list A → nat
+| list.nil        := 1
+| (list.cons a l) := 1 + sizeof a + list.sizeof l
 
-attribute [simp, defeq, simp.sizeof]
+instance (A : Type u) [has_sizeof A] : has_sizeof (list A) :=
+⟨list.sizeof⟩
+
+attribute [simp.sizeof]
 def sizeof_list_nil_eq (A : Type u) [has_sizeof A] : sizeof (@list.nil A) = 1 :=
 rfl
 
-attribute [simp, defeq, simp.sizeof]
+attribute [simp.sizeof]
 def sizeof_list_cons_eq {A : Type u} [has_sizeof A] (a : A) (l : list A) : sizeof (list.cons a l) = 1 + sizeof a + sizeof l :=
 rfl
 
diff --git a/tests/lean/defeq_simp_lemmas1.lean.expected.out b/tests/lean/defeq_simp_lemmas1.lean.expected.out
index bc7dde7c98..50b63d72be 100644
--- a/tests/lean/defeq_simp_lemmas1.lean.expected.out
+++ b/tests/lean/defeq_simp_lemmas1.lean.expected.out
@@ -1,21 +1,6 @@
 reflexivity lemmas:
 foo.d.def #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
 foo.f.def #3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
-sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ 1 + sizeof ?x_2 + sizeof ?x_3
-sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
-sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ 1 + sizeof ?x_2
-sizeof_option_none_eq #2, sizeof none ↦ 1
-sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
-sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
-sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
-sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
-sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
-sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ 1 + sizeof ?x_4 + sizeof ?x_5
-sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ 1 + sizeof ?x_4
-sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ 1 + sizeof ?x_4
-sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ 1 + sizeof ?x_4 + sizeof ?x_5
-sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
-default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
 id.def #2, id ?x_1 ↦ ?x_1
 foo.g.def #2, g ?x_0 ?x_1 ↦ h ?x_1
 ne.def #3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
diff --git a/tests/lean/defeq_simp_lemmas2.lean.expected.out b/tests/lean/defeq_simp_lemmas2.lean.expected.out
index a3cd439fc3..0b0f552ca8 100644
--- a/tests/lean/defeq_simp_lemmas2.lean.expected.out
+++ b/tests/lean/defeq_simp_lemmas2.lean.expected.out
@@ -3,21 +3,6 @@ foo.d.def #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3)
 foo.d.rfl #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
 foo.f.def #3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
 foo.f.rfl #3, f ?x_0 ?x_1 ?x_2 ↦ ?x_2
-sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ 1 + sizeof ?x_2 + sizeof ?x_3
-sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
-sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ 1 + sizeof ?x_2
-sizeof_option_none_eq #2, sizeof none ↦ 1
-sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
-sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
-sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
-sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
-sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
-sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ 1 + sizeof ?x_4 + sizeof ?x_5
-sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ 1 + sizeof ?x_4
-sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ 1 + sizeof ?x_4
-sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ 1 + sizeof ?x_4 + sizeof ?x_5
-sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
-default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
 id.def #2, id ?x_1 ↦ ?x_1
 foo.g.def #2, g ?x_0 ?x_1 ↦ h ?x_1
 foo.g.rfl #2, g ?x_0 ?x_1 ↦ ?x_1
@@ -29,21 +14,6 @@ foo.d.rfl #4 (prio: 1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
 foo.d.def #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
 foo.f.rfl #3 (prio: 1001), f ?x_0 ?x_1 ?x_2 ↦ ?x_2
 foo.f.def #3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
-sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ 1 + sizeof ?x_2 + sizeof ?x_3
-sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
-sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ 1 + sizeof ?x_2
-sizeof_option_none_eq #2, sizeof none ↦ 1
-sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
-sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
-sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
-sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
-sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
-sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ 1 + sizeof ?x_4 + sizeof ?x_5
-sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ 1 + sizeof ?x_4
-sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ 1 + sizeof ?x_4
-sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ 1 + sizeof ?x_4 + sizeof ?x_5
-sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
-default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
 id.def #2, id ?x_1 ↦ ?x_1
 foo.g.rfl #2 (prio: 1001), g ?x_0 ?x_1 ↦ ?x_1
 foo.g.def #2, g ?x_0 ?x_1 ↦ h ?x_1
@@ -55,21 +25,6 @@ foo.d.def #4 (prio: 1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_
 foo.d.rfl #4 (prio: 1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
 foo.f.def #3 (prio: 1001), f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
 foo.f.rfl #3 (prio: 1001), f ?x_0 ?x_1 ?x_2 ↦ ?x_2
-sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ 1 + sizeof ?x_2 + sizeof ?x_3
-sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
-sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ 1 + sizeof ?x_2
-sizeof_option_none_eq #2, sizeof none ↦ 1
-sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
-sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
-sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
-sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
-sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
-sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ 1 + sizeof ?x_4 + sizeof ?x_5
-sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ 1 + sizeof ?x_4
-sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ 1 + sizeof ?x_4
-sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ 1 + sizeof ?x_4 + sizeof ?x_5
-sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
-default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
 id.def #2, id ?x_1 ↦ ?x_1
 foo.g.def #2 (prio: 1001), g ?x_0 ?x_1 ↦ h ?x_1
 foo.g.rfl #2 (prio: 1001), g ?x_0 ?x_1 ↦ ?x_1
diff --git a/tests/lean/run/converter.lean b/tests/lean/run/converter.lean
index 107643b02d..03cbc8196d 100644
--- a/tests/lean/run/converter.lean
+++ b/tests/lean/run/converter.lean
@@ -27,6 +27,8 @@ by conversion $
 
 set_option trace.app_builder true
 
+attribute [simp, defeq] sizeof_nat_eq
+
 example (a b c : nat) : (λ x, g (f x (sizeof x))) = (λ x, 0) :=
 by conversion $
   funext $ do