From b24165dc7bca1066dfd1d7fba1fd3d9cb462eb74 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Nov 2014 23:06:33 -0800 Subject: [PATCH] feat(frontends/lean/structure_cmd): remove 'cases_on' for structures since it may confuse users, add 'destruct' as alternative name for 'rec_on' --- library/data/prod.lean | 2 -- library/data/sigma.lean | 3 --- src/frontends/lean/structure_cmd.cpp | 18 ++++++++++-------- tests/lean/run/record1.lean | 2 +- tests/lean/run/sigma_no_confusion.lean | 6 +++--- 5 files changed, 14 insertions(+), 17 deletions(-) diff --git a/library/data/prod.lean b/library/data/prod.lean index dd4681fb19..509b0b999a 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -20,8 +20,6 @@ namespace prod notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t variables {A B : Type} - protected theorem destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p := - rec H p notation `pr₁` := pr1 notation `pr₂` := pr2 diff --git a/library/data/sigma.lean b/library/data/sigma.lean index 55609bf624..4221dd90ea 100644 --- a/library/data/sigma.lean +++ b/library/data/sigma.lean @@ -16,9 +16,6 @@ namespace sigma theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := rfl theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := rfl - protected theorem destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p := - rec H p - theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) : dpair a₁ b₁ = dpair a₂ b₂ := dcongr_arg2 dpair H₁ H₂ diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index a96665f22e..94f111fd9c 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -28,7 +28,6 @@ Author: Leonardo de Moura #include "library/definitional/rec_on.h" #include "library/definitional/induction_on.h" #include "library/definitional/cases_on.h" -#include "library/definitional/unit.h" #include "library/definitional/eq.h" #include "library/definitional/projection.h" #include "frontends/lean/parser.h" @@ -597,7 +596,6 @@ struct structure_cmd_fn { } void declare_auxiliary() { - bool has_unit = has_unit_decls(m_env); m_env = mk_rec_on(m_env, m_name); m_env = mk_induction_on(m_env, m_name); name rec_on_name(m_name, "rec_on"); @@ -606,12 +604,16 @@ struct structure_cmd_fn { add_rec_alias(induction_on_name); save_def_info(rec_on_name); save_def_info(induction_on_name); - if (has_unit) { - m_env = mk_cases_on(m_env, m_name); - name cases_on_name(m_name, "cases_on"); - save_def_info(cases_on_name); - add_rec_alias(cases_on_name); - } + name destruct_name(m_name, "destruct"); + bool opaque = false; + declaration rec_on_decl = m_env.get(rec_on_name); + declaration destruct_decl = mk_definition(m_env, destruct_name, rec_on_decl.get_univ_params(), + rec_on_decl.get_type(), rec_on_decl.get_value(), + opaque); + m_env = module::add(m_env, check(m_env, destruct_decl)); + m_env = set_reducible(m_env, destruct_name, reducible_status::On); + save_def_info(destruct_name); + add_alias(destruct_name); } void declare_coercions() { diff --git a/tests/lean/run/record1.lean b/tests/lean/run/record1.lean index b13349dd55..d350c41070 100644 --- a/tests/lean/run/record1.lean +++ b/tests/lean/run/record1.lean @@ -11,7 +11,7 @@ check point.x check point.y check point.rec_on check point.induction_on -check point.cases_on +check point.destruct inductive color := red, green, blue diff --git a/tests/lean/run/sigma_no_confusion.lean b/tests/lean/run/sigma_no_confusion.lean index 405afb7168..e346c454ff 100644 --- a/tests/lean/run/sigma_no_confusion.lean +++ b/tests/lean/run/sigma_no_confusion.lean @@ -2,15 +2,15 @@ import data.sigma tools.tactic namespace sigma definition no_confusion_type {A : Type} {B : A → Type} (P : Type) (v₁ v₂ : sigma B) : Type := - cases_on v₁ - (λ (a₁ : A) (b₁ : B a₁), cases_on v₂ + rec_on v₁ + (λ (a₁ : A) (b₁ : B a₁), rec_on v₂ (λ (a₂ : A) (b₂ : B a₂), (Π (eq₁ : a₁ = a₂), eq.rec_on eq₁ b₁ = b₂ → P) → P)) definition no_confusion {A : Type} {B : A → Type} {P : Type} {v₁ v₂ : sigma B} : v₁ = v₂ → no_confusion_type P v₁ v₂ := assume H₁₂ : v₁ = v₂, have aux : v₁ = v₁ → no_confusion_type P v₁ v₁, from - assume H₁₁, cases_on v₁ + assume H₁₁, rec_on v₁ (λ (a₁ : A) (b₁ : B a₁) (h : Π (eq₁ : a₁ = a₁), eq.rec_on eq₁ b₁ = b₁ → P), h rfl rfl), eq.rec_on H₁₂ aux H₁₂