From 60eac0195d294ffe7283697918e2fd146dd60028 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Nov 2014 09:10:25 -0800 Subject: [PATCH] feat(frontends/lean/structure_cmd): generate projection over constructor theorems for structures --- library/data/int/basic.lean | 8 +++--- library/data/nat/div.lean | 2 +- library/data/prod.lean | 6 ----- library/data/quotient/util.lean | 18 ++++++------- library/data/sigma.lean | 3 --- src/frontends/lean/structure_cmd.cpp | 39 +++++++++++++++++++++++++--- 6 files changed, 49 insertions(+), 27 deletions(-) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index c0606ee878..de9c96ad2b 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -84,22 +84,22 @@ or.elim le_or_gt theorem proj_ge_pr1 {a : ℕ × ℕ} (H : pr1 a ≥ pr2 a) : pr1 (proj a) = pr1 a - pr2 a := calc pr1 (proj a) = pr1 (pair (pr1 a - pr2 a) 0) : {proj_ge H} - ... = pr1 a - pr2 a : pr1.pair (pr1 a - pr2 a) 0 + ... = pr1 a - pr2 a : pr1.mk (pr1 a - pr2 a) 0 theorem proj_ge_pr2 {a : ℕ × ℕ} (H : pr1 a ≥ pr2 a) : pr2 (proj a) = 0 := calc pr2 (proj a) = pr2 (pair (pr1 a - pr2 a) 0) : {proj_ge H} - ... = 0 : pr2.pair (pr1 a - pr2 a) 0 + ... = 0 : pr2.mk (pr1 a - pr2 a) 0 theorem proj_le_pr1 {a : ℕ × ℕ} (H : pr1 a ≤ pr2 a) : pr1 (proj a) = 0 := calc pr1 (proj a) = pr1 (pair 0 (pr2 a - pr1 a)) : {proj_le H} - ... = 0 : pr1.pair 0 (pr2 a - pr1 a) + ... = 0 : pr1.mk 0 (pr2 a - pr1 a) theorem proj_le_pr2 {a : ℕ × ℕ} (H : pr1 a ≤ pr2 a) : pr2 (proj a) = pr2 a - pr1 a := calc pr2 (proj a) = pr2 (pair 0 (pr2 a - pr1 a)) : {proj_le H} - ... = pr2 a - pr1 a : pr2.pair 0 (pr2 a - pr1 a) + ... = pr2 a - pr1 a : pr2.mk 0 (pr2 a - pr1 a) theorem proj_flip (a : ℕ × ℕ) : proj (flip a) = flip (proj a) := have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 34bf4dd49f..0c58520c64 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -610,7 +610,7 @@ show lhs = rhs, from ... = rhs : (if_pos H1)⁻¹) (assume H1 : y ≠ 0, have ypos : y > 0, from ne_zero_imp_pos H1, - have H2 : gcd_aux_measure p' = x mod y, from pr2.pair _ _, + have H2 : gcd_aux_measure p' = x mod y, from pr2.mk _ _, have H3 : gcd_aux_measure p' < gcd_aux_measure p, from H2⁻¹ ▸ mod_lt ypos, calc lhs = g1 p' : if_neg H1 diff --git a/library/data/prod.lean b/library/data/prod.lean index 509b0b999a..247246960d 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -26,12 +26,6 @@ namespace prod variables (a : A) (b : B) - theorem pr1.pair : pr₁ (a, b) = a := - rfl - - theorem pr2.pair : pr₂ (a, b) = b := - rfl - variables {a₁ a₂ : A} {b₁ b₂ : B} theorem pair_eq : a₁ = a₂ → b₁ = b₂ → (a₁, b₁) = (a₂, b₂) := diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean index 8c7b5c96cf..a8e60816c6 100644 --- a/library/data/quotient/util.lean +++ b/library/data/quotient/util.lean @@ -47,13 +47,13 @@ rfl theorem map_pair_pair {A B : Type} (f : A → B) (a a' : A) : map_pair f (pair a a') = pair (f a) (f a') := -(pr1.pair a a') ▸ (pr2.pair a a') ▸ rfl +(pr1.mk a a') ▸ (pr2.mk a a') ▸ rfl theorem map_pair_pr1 {A B : Type} (f : A → B) (a : A × A) : pr1 (map_pair f a) = f (pr1 a) := -!pr1.pair +!pr1.mk theorem map_pair_pr2 {A B : Type} (f : A → B) (a : A × A) : pr2 (map_pair f a) = f (pr2 a) := -!pr2.pair +!pr2.mk -- ### coordinatewise binary maps @@ -68,16 +68,16 @@ theorem map_pair2_pair {A B C : Type} (f : A → B → C) (a a' : A) (b b' : B) calc map_pair2 f (pair a a') (pair b b') = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) (pr2 (pair b b'))) - : {pr1.pair b b'} - ... = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) b') : {pr2.pair b b'} - ... = pair (f (pr1 (pair a a')) b) (f a' b') : {pr2.pair a a'} - ... = pair (f a b) (f a' b') : {pr1.pair a a'} + : {pr1.mk b b'} + ... = pair (f (pr1 (pair a a')) b) (f (pr2 (pair a a')) b') : {pr2.mk b b'} + ... = pair (f (pr1 (pair a a')) b) (f a' b') : {pr2.mk a a'} + ... = pair (f a b) (f a' b') : {pr1.mk a a'} theorem map_pair2_pr1 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : -pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := !pr1.pair +pr1 (map_pair2 f a b) = f (pr1 a) (pr1 b) := !pr1.mk theorem map_pair2_pr2 {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : -pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := !pr2.pair +pr2 (map_pair2 f a b) = f (pr2 a) (pr2 b) := !pr2.mk theorem map_pair2_flip {A B C : Type} (f : A → B → C) (a : A × A) (b : B × B) : flip (map_pair2 f a b) = map_pair2 f (flip a) (flip b) := diff --git a/library/data/sigma.lean b/library/data/sigma.lean index 4221dd90ea..4f79d2dff5 100644 --- a/library/data/sigma.lean +++ b/library/data/sigma.lean @@ -13,9 +13,6 @@ namespace sigma universe variables u v variables {A A' : Type.{u}} {B : A → Type.{v}} {B' : A' → Type.{v}} - 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 - 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 5e929cf00f..639b6674b8 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -74,6 +74,7 @@ struct structure_cmd_fn { buffer m_parents; buffer m_private_parents; name m_mk; + name m_mk_short; pos_info m_mk_pos; implicit_infer_kind m_mk_infer; buffer m_fields; @@ -703,26 +704,55 @@ struct structure_cmd_fn { add_alias(eta_name); } + void declare_proj_over_mk() { + if (!has_eq_decls(m_env)) + return; + level_param_names lnames = to_list(m_level_names.begin(), m_level_names.end()); + levels st_ls = param_names_to_levels(lnames); + expr st_type = mk_app(mk_constant(m_name, st_ls), m_params); + expr mk_fields = mk_app(mk_app(mk_constant(m_mk, st_ls), m_params), m_fields); + for (unsigned i = 0; i < m_fields.size(); i++) { + expr const & field = m_fields[i]; + name const & field_name = mlocal_name(field); + expr const & field_type = mlocal_type(field); + level field_level = sort_level(m_tc->ensure_type(field_type).first); + name proj_name = m_name + field_name; + expr lhs = mk_app(mk_app(mk_constant(proj_name, st_ls), m_params), mk_fields); + expr rhs = field; + expr eq = mk_app(mk_constant("eq", to_list(field_level)), field_type, lhs, rhs); + expr refl = mk_app(mk_constant(name{"eq", "refl"}, to_list(field_level)), field_type, lhs); + name proj_over_name = m_name + field_name + m_mk_short; + expr proj_over_type = infer_implicit(Pi(m_params, Pi(m_fields, eq)), m_params.size(), true); + expr proj_over_value = Fun(m_params, Fun(m_fields, refl)); + + declaration proj_over_decl = mk_theorem(proj_over_name, lnames, proj_over_type, proj_over_value); + m_env = module::add(m_env, check(m_env, proj_over_decl)); + save_thm_info(proj_over_name); + add_alias(proj_over_name); + } + } + environment operator()() { process_header(); if (m_p.curr_is_token(get_assign_tk())) { m_p.check_token_next(get_assign_tk(), "invalid 'structure', ':=' expected"); m_mk_pos = m_p.pos(); if (m_p.curr_is_token(get_lparen_tk()) || m_p.curr_is_token(get_lcurly_tk()) || m_p.curr_is_token(get_lbracket_tk())) { - m_mk = m_name + LEAN_DEFAULT_STRUCTURE_INTRO; + m_mk_short = LEAN_DEFAULT_STRUCTURE_INTRO; m_mk_infer = implicit_infer_kind::Implicit; } else { - m_mk = m_p.check_atomic_id_next("invalid 'structure', identifier expected"); - m_mk = m_name + m_mk; + m_mk_short = m_p.check_atomic_id_next("invalid 'structure', identifier expected"); m_mk_infer = parse_implicit_infer_modifier(m_p); if (!m_p.curr_is_command_like()) m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected"); } + m_mk = m_name + m_mk_short; process_new_fields(); } else { m_mk_pos = m_name_pos; - m_mk = m_name + LEAN_DEFAULT_STRUCTURE_INTRO; + m_mk_short = LEAN_DEFAULT_STRUCTURE_INTRO; m_mk_infer = implicit_infer_kind::Implicit; + m_mk = m_name + m_mk_short; process_empty_new_fields(); } infer_resultant_universe(); @@ -735,6 +765,7 @@ struct structure_cmd_fn { declare_auxiliary(); declare_coercions(); declare_eta(); + declare_proj_over_mk(); return m_env; } };