From 3215af39263ca0d5764297c732bcfbf3bb10792e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Jun 2015 12:36:43 -0700 Subject: [PATCH] feat(frontends/lean): add '[trans-instance]' attribute see issue #666 --- library/algebra/field.lean | 2 +- library/algebra/group.lean | 8 ++++---- library/algebra/group_bigops.lean | 6 +++--- library/algebra/order.lean | 20 ++++++++++---------- library/algebra/ordered_field.lean | 6 +++--- library/algebra/ordered_group.lean | 4 ++-- library/algebra/ordered_ring.lean | 6 +++--- library/algebra/ring.lean | 4 ++-- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/decl_attributes.cpp | 22 ++++++++++++++++++++-- src/frontends/lean/decl_attributes.h | 1 + src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 4 ++++ src/frontends/lean/tokens.h | 1 + src/frontends/lean/tokens.txt | 1 + 15 files changed, 57 insertions(+), 32 deletions(-) diff --git a/library/algebra/field.lean b/library/algebra/field.lean index 18a9c8b24e..5bb640df2a 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -326,7 +326,7 @@ section discrete_field (assume H1 : x ≠ 0, or.inr (by rewrite [-one_mul, -(inv_mul_cancel H1), mul.assoc, H, mul_zero])) - definition discrete_field.to_integral_domain [instance] [reducible] [coercion] : + definition discrete_field.to_integral_domain [trans-instance] [reducible] [coercion] : integral_domain A := ⦃ integral_domain, s, eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄ diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 6054ecf9b4..169339f985 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -278,12 +278,12 @@ section group theorem mul_eq_one_iff_mul_eq_one (a b : A) : a * b = 1 ↔ b * a = 1 := iff.intro !mul_eq_one_of_mul_eq_one !mul_eq_one_of_mul_eq_one - definition group.to_left_cancel_semigroup [instance] [coercion] [reducible] : + definition group.to_left_cancel_semigroup [trans-instance] [coercion] [reducible] : left_cancel_semigroup A := ⦃ left_cancel_semigroup, s, mul_left_cancel := @mul_left_cancel A s ⦄ - definition group.to_right_cancel_semigroup [instance] [coercion] [reducible] : + definition group.to_right_cancel_semigroup [trans-instance] [coercion] [reducible] : right_cancel_semigroup A := ⦃ right_cancel_semigroup, s, mul_right_cancel := @mul_right_cancel A s ⦄ @@ -395,12 +395,12 @@ section add_group ... = (c + b) + -b : H ... = c : add_neg_cancel_right - definition add_group.to_left_cancel_semigroup [instance] [coercion] [reducible] : + definition add_group.to_left_cancel_semigroup [trans-instance] [coercion] [reducible] : add_left_cancel_semigroup A := ⦃ add_left_cancel_semigroup, s, add_left_cancel := @add_left_cancel A s ⦄ - definition add_group.to_add_right_cancel_semigroup [instance] [coercion] [reducible] : + definition add_group.to_add_right_cancel_semigroup [trans-instance] [coercion] [reducible] : add_right_cancel_semigroup A := ⦃ add_right_cancel_semigroup, s, add_right_cancel := @add_right_cancel A s ⦄ diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean index 9c6f3b53db..280526d019 100644 --- a/library/algebra/group_bigops.lean +++ b/library/algebra/group_bigops.lean @@ -146,7 +146,7 @@ end comm_monoid section add_monoid variable [amB : add_monoid B] include amB - local attribute add_monoid.to_monoid [instance] + local attribute add_monoid.to_monoid [trans-instance] definition Suml (l : list A) (f : A → B) : B := Prodl l f @@ -175,7 +175,7 @@ end add_monoid section add_comm_monoid variable [acmB : add_comm_monoid B] include acmB - local attribute add_comm_monoid.to_comm_monoid [instance] + local attribute add_comm_monoid.to_comm_monoid [trans-instance] theorem Suml_add (l : list A) (f g : A → B) : Suml l (λx, f x + g x) = Suml l f + Suml l g := Prodl_mul l f g @@ -186,7 +186,7 @@ end add_comm_monoid section add_comm_monoid variable [acmB : add_comm_monoid B] include acmB - local attribute add_comm_monoid.to_comm_monoid [instance] + local attribute add_comm_monoid.to_comm_monoid [trans-instance] definition Sum (s : finset A) (f : A → B) : B := Prod s f diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 14d45adee8..86b3c1ed26 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -138,7 +138,7 @@ section private theorem lt_trans (s' : order_pair A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c := lt_of_lt_of_le lt_ab (le_of_lt lt_bc) - definition order_pair.to_strict_order [instance] [coercion] [reducible] : strict_order A := + definition order_pair.to_strict_order [trans-instance] [coercion] [reducible] : strict_order A := ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄ @@ -168,13 +168,13 @@ iff.mp le_iff_lt_or_eq le_ab theorem le_of_lt_or_eq [s : strong_order_pair A] {a b : A} (lt_or_eq : a < b ∨ a = b) : a ≤ b := iff.mp' le_iff_lt_or_eq lt_or_eq -private theorem lt_irrefl' [s : strong_order_pair A] (a : A) : ¬ a < a := +private theorem lt_irrefl' [s : strong_order_pair A] (a : A) : ¬ a < a := !strong_order_pair.lt_irrefl -private theorem le_of_lt' [s : strong_order_pair A] (a b : A) : a < b → a ≤ b := +private theorem le_of_lt' [s : strong_order_pair A] (a b : A) : a < b → a ≤ b := take Hlt, le_of_lt_or_eq (or.inl Hlt) -private theorem lt_iff_le_and_ne [s : strong_order_pair A] {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) := +private theorem lt_iff_le_and_ne [s : strong_order_pair A] {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) := iff.intro (take Hlt, and.intro (le_of_lt_or_eq (or.inl Hlt)) (take Hab, absurd (Hab ▸ Hlt) !lt_irrefl')) (take Hand, @@ -210,8 +210,8 @@ private theorem lt_of_lt_of_le' [s : strong_order_pair A] (a b c : A) : a < b show a < c, from iff.mp' (lt_iff_le_and_ne) (and.intro le_ac ne_ac) -definition strong_order_pair.to_order_pair [instance] [coercion] [reducible] [s : strong_order_pair A] - : order_pair A := +definition strong_order_pair.to_order_pair [trans-instance] [coercion] [reducible] [s : strong_order_pair A] + : order_pair A := ⦃ order_pair, s, lt_irrefl := lt_irrefl', le_of_lt := le_of_lt', @@ -258,7 +258,7 @@ iff.intro iff.mp !strict_order_with_le.le_iff_lt_or_eq (and.elim_left H), show a < b, from or_resolve_left H1 (and.elim_right H)) -private theorem le_of_lt' (s : strict_order_with_le A) (a b : A) : a < b → a ≤ b := +private theorem le_of_lt' (s : strict_order_with_le A) (a b : A) : a < b → a ≤ b := take Hlt, and.left (iff.mp (lt_iff_le_ne s _ _) Hlt) private theorem lt_trans (s : strict_order_with_le A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c := @@ -296,7 +296,7 @@ private theorem lt_trans (s : strict_order_with_le A) (a b c: A) (lt_ab : a < b) show a < c, from iff.mp' (lt_iff_le_ne s _ _) (and.intro le_ac ne_ac) -definition strict_order_with_le.to_order_pair [instance] [coercion] [reducible] [s : strict_order_with_le A] : +definition strict_order_with_le.to_order_pair [trans-instance] [coercion] [reducible] [s : strict_order_with_le A] : strong_order_pair A := ⦃ strong_order_pair, s, le_refl := le_refl s, @@ -315,7 +315,7 @@ structure linear_order_pair [class] (A : Type) extends order_pair A, linear_weak structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A, linear_weak_order A -definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion] [reducible] +definition linear_strong_order_pair.to_linear_order_pair [trans-instance] [coercion] [reducible] [s : linear_strong_order_pair A] : linear_order_pair A := ⦃ linear_order_pair, s, strong_order_pair.to_order_pair⦄ @@ -437,7 +437,7 @@ section or.elim H' (take H'' : b = a, or.inl (symm H'')) (take H'' : b < a, or.inr H'') - + theorem max.right (a b : A) : b ≤ max a b := decidable.by_cases (λ h : a < b, eq.rec_on (max.eq_right h) !le.refl) diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index cbe88de1b3..c1b24d3224 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -323,9 +323,9 @@ section discrete_linear_ordered_field (assume H' : ¬ y < x, decidable.inl (le.antisymm (le_of_not_gt H') (le_of_not_gt H)))) - definition discrete_linear_ordered_field.to_discrete_field [instance] [reducible] [coercion] - [s : discrete_linear_ordered_field A] : discrete_field A := - ⦃ discrete_field, s, has_decidable_eq := dec_eq_of_dec_lt⦄ + definition discrete_linear_ordered_field.to_discrete_field [trans-instance] [reducible] [coercion] + : discrete_field A := + ⦃ discrete_field, s, has_decidable_eq := dec_eq_of_dec_lt⦄ theorem pos_of_div_pos (H : 0 < 1 / a) : 0 < a := have H1 : 0 < 1 / (1 / a), from div_pos_of_pos H, diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 4499969746..aea8f39ab5 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -229,7 +229,7 @@ theorem ordered_comm_group.lt_of_add_lt_add_left [s : ordered_comm_group A] {a b assert H' : -a + (a + b) < -a + (a + c), from ordered_comm_group.add_lt_add_left _ _ H _, by rewrite *neg_add_cancel_left at H'; exact H' -definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [reducible] +definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans-instance] [coercion] [reducible] [s : ordered_comm_group A] : ordered_cancel_comm_monoid A := ⦃ ordered_cancel_comm_monoid, s, add_left_cancel := @add.left_cancel A s, @@ -450,7 +450,7 @@ private theorem add_le_add_left' (A : Type) (s : decidable_linear_ordered_comm_g a ≤ b → (∀ c : A, c + a ≤ c + b) := decidable_linear_ordered_comm_group.add_le_add_left a b -definition decidable_linear_ordered_comm_group.to_ordered_comm_group [instance] [reducible] [coercion] +definition decidable_linear_ordered_comm_group.to_ordered_comm_group [trans-instance] [reducible] [coercion] (A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A := ⦃ordered_comm_group, s, le_of_lt := @le_of_lt A s, diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 60fe11d89b..e4f7502121 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -226,7 +226,7 @@ begin exact (iff.mp !sub_pos_iff_lt H2) end -definition ordered_ring.to_ordered_semiring [instance] [coercion] [reducible] [s : ordered_ring A] : +definition ordered_ring.to_ordered_semiring [trans-instance] [coercion] [reducible] [s : ordered_ring A] : ordered_semiring A := ⦃ ordered_semiring, s, mul_zero := mul_zero, @@ -308,7 +308,7 @@ structure linear_ordered_ring [class] (A : Type) extends ordered_ring A, linear_ -- print fields linear_ordered_semiring -definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion] [reducible] +definition linear_ordered_ring.to_linear_ordered_semiring [trans-instance] [coercion] [reducible] [s : linear_ordered_ring A] : linear_ordered_semiring A := ⦃ linear_ordered_semiring, s, @@ -362,7 +362,7 @@ lt.by_cases end)) -- Linearity implies no zero divisors. Doesn't need commutativity. -definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion] [reducible] +definition linear_ordered_comm_ring.to_integral_domain [trans-instance] [coercion] [reducible] [s: linear_ordered_comm_ring A] : integral_domain A := ⦃ integral_domain, s, eq_zero_or_eq_zero_of_mul_eq_zero := diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 678227ee66..56497c583b 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -165,7 +165,7 @@ have H : 0 * a + 0 = 0 * a + 0 * a, from calc ... = 0 * a + 0 * a : by rewrite {_*a}ring.right_distrib, show 0 * a = 0, from (add.left_cancel H)⁻¹ -definition ring.to_semiring [instance] [coercion] [reducible] [s : ring A] : semiring A := +definition ring.to_semiring [trans-instance] [coercion] [reducible] [s : ring A] : semiring A := ⦃ semiring, s, mul_zero := ring.mul_zero, zero_mul := ring.zero_mul ⦄ @@ -244,7 +244,7 @@ end structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A -definition comm_ring.to_comm_semiring [instance] [coercion] [reducible] [s : comm_ring A] : comm_semiring A := +definition comm_ring.to_comm_semiring [trans-instance] [coercion] [reducible] [s : comm_ring A] : comm_semiring A := ⦃ comm_semiring, s, mul_zero := mul_zero, zero_mul := zero_mul ⦄ diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index c19115905f..67e55da1ab 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -118,7 +118,7 @@ ;; place holder (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face) ;; modifiers - (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]" + (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[trans-instance\]" "\[class\]" "\[parsing-only\]" "\[coercion\]" "\[unfold-f\]" "\[constructor\]" "\[reducible\]" "\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]" "\[none\]" diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 0ac0cbc043..06d7e2d942 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -25,6 +25,7 @@ decl_attributes::decl_attributes(bool is_abbrev, bool persistent): m_is_abbrev = is_abbrev; m_persistent = persistent; m_is_instance = false; + m_is_trans_instance = false; m_is_coercion = false; m_is_reducible = is_abbrev; m_is_irreducible = false; @@ -88,6 +89,13 @@ void decl_attributes::parse(buffer const & ns, parser & p) { auto pos = p.pos(); if (p.curr_is_token(get_instance_tk())) { m_is_instance = true; + if (m_is_trans_instance) + throw parser_error("invalid '[instance]' attribute, '[trans-instance]' was already provided", pos); + p.next(); + } else if (p.curr_is_token(get_trans_inst_tk())) { + m_is_trans_instance = true; + if (m_is_instance) + throw parser_error("invalid '[trans-instance]' attribute, '[instance]' was already provided", pos); p.next(); } else if (p.curr_is_token(get_coercion_tk())) { p.next(); @@ -204,6 +212,16 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c env = add_instance(env, d, m_persistent); } } + if (m_is_trans_instance) { + if (m_priority) { + #if defined(__GNUC__) && !defined(__CLANG__) + #pragma GCC diagnostic ignored "-Wmaybe-uninitialized" + #endif + env = add_trans_instance(env, d, *m_priority, m_persistent); + } else { + env = add_trans_instance(env, d, m_persistent); + } + } if (m_is_coercion) env = add_coercion(env, d, ios, m_persistent); auto decl = env.find(d); @@ -243,7 +261,7 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c } void decl_attributes::write(serializer & s) const { - s << m_is_abbrev << m_persistent << m_is_instance << m_is_coercion + s << m_is_abbrev << m_persistent << m_is_instance << m_is_trans_instance << m_is_coercion << m_is_reducible << m_is_irreducible << m_is_semireducible << m_is_quasireducible << m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_f_hint << m_constructor_hint << m_symm << m_trans << m_refl << m_subst << m_recursor @@ -251,7 +269,7 @@ void decl_attributes::write(serializer & s) const { } void decl_attributes::read(deserializer & d) { - d >> m_is_abbrev >> m_persistent >> m_is_instance >> m_is_coercion + d >> m_is_abbrev >> m_persistent >> m_is_instance >> m_is_trans_instance >> m_is_coercion >> m_is_reducible >> m_is_irreducible >> m_is_semireducible >> m_is_quasireducible >> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_f_hint >> m_constructor_hint >> m_symm >> m_trans >> m_refl >> m_subst >> m_recursor diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h index 1a21640206..522c8f90ea 100644 --- a/src/frontends/lean/decl_attributes.h +++ b/src/frontends/lean/decl_attributes.h @@ -13,6 +13,7 @@ class decl_attributes { bool m_is_abbrev; // if true only abbreviation attributes are allowed bool m_persistent; bool m_is_instance; + bool m_is_trans_instance; bool m_is_coercion; bool m_is_reducible; bool m_is_irreducible; diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index e92cb1fb52..b303561e0c 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -106,7 +106,7 @@ void init_token_table(token_table & t) { char const * commands[] = {"theorem", "axiom", "axioms", "variable", "protected", "private", "reveal", "definition", "example", "coercion", "abbreviation", - "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", + "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[trans-instance]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]", "[rewrite]", "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor", "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-f]", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 037f42ee2a..7efa4f580e 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -97,6 +97,7 @@ static name const * g_constants_tk = nullptr; static name const * g_variable_tk = nullptr; static name const * g_variables_tk = nullptr; static name const * g_instance_tk = nullptr; +static name const * g_trans_inst_tk = nullptr; static name const * g_priority_tk = nullptr; static name const * g_unfold_c_tk = nullptr; static name const * g_unfold_f_tk = nullptr; @@ -233,6 +234,7 @@ void initialize_tokens() { g_variable_tk = new name{"variable"}; g_variables_tk = new name{"variables"}; g_instance_tk = new name{"[instance]"}; + g_trans_inst_tk = new name{"[trans-instance]"}; g_priority_tk = new name{"[priority"}; g_unfold_c_tk = new name{"[unfold-c"}; g_unfold_f_tk = new name{"[unfold-f]"}; @@ -370,6 +372,7 @@ void finalize_tokens() { delete g_variable_tk; delete g_variables_tk; delete g_instance_tk; + delete g_trans_inst_tk; delete g_priority_tk; delete g_unfold_c_tk; delete g_unfold_f_tk; @@ -506,6 +509,7 @@ name const & get_constants_tk() { return *g_constants_tk; } name const & get_variable_tk() { return *g_variable_tk; } name const & get_variables_tk() { return *g_variables_tk; } name const & get_instance_tk() { return *g_instance_tk; } +name const & get_trans_inst_tk() { return *g_trans_inst_tk; } name const & get_priority_tk() { return *g_priority_tk; } name const & get_unfold_c_tk() { return *g_unfold_c_tk; } name const & get_unfold_f_tk() { return *g_unfold_f_tk; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index c2247d3fb7..c0197211b5 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -99,6 +99,7 @@ name const & get_constants_tk(); name const & get_variable_tk(); name const & get_variables_tk(); name const & get_instance_tk(); +name const & get_trans_inst_tk(); name const & get_priority_tk(); name const & get_unfold_c_tk(); name const & get_unfold_f_tk(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index 1d108b77cd..050ceb7ff2 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -92,6 +92,7 @@ constants constants variable variable variables variables instance [instance] +trans_inst [trans-instance] priority [priority unfold_c [unfold-c unfold_f [unfold-f]