From 22e47430b5356421a3b922d31829d23375f2d80c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 27 Sep 2014 21:47:37 -0700 Subject: [PATCH] feat(library/unifier): add 'on-demand' choice constraints, they are processed as soon as their type does not contain meta-variables anymore --- src/frontends/lean/placeholder_elaborator.cpp | 14 +- src/kernel/constraint.cpp | 47 +++- src/kernel/constraint.h | 20 +- src/library/unifier.cpp | 87 +++++- tests/lean/empty.lean.expected.out | 13 +- tests/lean/run/group3.lean | 258 ++++++++++++++++++ 6 files changed, 403 insertions(+), 36 deletions(-) create mode 100644 tests/lean/run/group3.lean diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index e03732cc7..7dfdc3669 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -263,14 +263,18 @@ static bool has_expr_metavar_relaxed(expr const & e) { } constraint mk_placeholder_root_cnstr(std::shared_ptr const & C, expr const & m, bool is_strict, - unifier_config const & cfg, unsigned delay_factor) { + unifier_config const & cfg, delay_factor const & factor) { environment const & env = C->env(); justification j = mk_failed_to_synthesize_jst(env, m); auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, name_generator const & ngen) { if (has_expr_metavar_relaxed(meta_type)) { - if (delay_factor < to_delay_factor(cnstr_group::ClassInstance)) { - constraint delayed_c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, delay_factor+1); + // TODO(Leo): remove + if (factor.on_demand()) { + constraint delayed_c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, to_delay_factor(cnstr_group::Basic)); + return lazy_list(constraints(delayed_c)); + } else if (factor.explict_value() < to_delay_factor(cnstr_group::ClassInstance)) { + constraint delayed_c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, factor.explict_value()+1); return lazy_list(constraints(delayed_c)); } } @@ -315,7 +319,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr const }; bool owner = false; bool relax = C->m_relax; - return mk_choice_cnstr(m, choice_fn, delay_factor, owner, j, relax); + return mk_choice_cnstr(m, choice_fn, factor, owner, j, relax); } /** \brief Create a metavariable, and attach choice constraint for generating @@ -327,7 +331,7 @@ pair mk_placeholder_elaborator( bool is_strict, optional const & type, tag g, unifier_config const & cfg) { auto C = std::make_shared(env, ios, ctx, prefix, relax, use_local_instances); expr m = C->m_ctx.mk_meta(C->m_ngen, type, g); - constraint c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, to_delay_factor(cnstr_group::Basic)); + constraint c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, delay_factor()); return mk_pair(m, c); } } diff --git a/src/kernel/constraint.cpp b/src/kernel/constraint.cpp index 2aba36bd6..9d1ffe1de 100644 --- a/src/kernel/constraint.cpp +++ b/src/kernel/constraint.cpp @@ -17,7 +17,8 @@ struct constraint_cell { constraint_kind m_kind; justification m_jst; bool m_relax_main_opaque; - constraint_cell(constraint_kind k, justification const & j, bool relax):m_rc(1), m_kind(k), m_jst(j), m_relax_main_opaque(relax) {} + constraint_cell(constraint_kind k, justification const & j, bool relax): + m_rc(1), m_kind(k), m_jst(j), m_relax_main_opaque(relax) {} }; struct eq_constraint_cell : public constraint_cell { expr m_lhs; @@ -34,13 +35,14 @@ struct level_constraint_cell : public constraint_cell { m_lhs(lhs), m_rhs(rhs) {} }; struct choice_constraint_cell : public constraint_cell { - expr m_expr; - choice_fn m_fn; - unsigned m_delay_factor; - bool m_owner; - choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, bool owner, justification const & j, bool relax): + expr m_expr; + choice_fn m_fn; + delay_factor m_delay_factor; + bool m_owner; + choice_constraint_cell(expr const & e, choice_fn const & fn, delay_factor const & f, + bool owner, justification const & j, bool relax): constraint_cell(constraint_kind::Choice, j, relax), - m_expr(e), m_fn(fn), m_delay_factor(delay_factor), m_owner(owner) {} + m_expr(e), m_fn(fn), m_delay_factor(f), m_owner(owner) {} }; void constraint_cell::dealloc() { @@ -69,13 +71,20 @@ constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j) { return constraint(new level_constraint_cell(lhs, rhs, j)); } -constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, bool owner, justification const & j, bool relax_main_opaque) { +constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, delay_factor const & f, + bool owner, justification const & j, bool relax_main_opaque) { lean_assert(is_meta(m)); - return constraint(new choice_constraint_cell(m, fn, delay_factor, owner, j, relax_main_opaque)); + return constraint(new choice_constraint_cell(m, fn, f, owner, j, relax_main_opaque)); } -expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast(c.raw())->m_lhs; } -expr const & cnstr_rhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast(c.raw())->m_rhs; } +expr const & cnstr_lhs_expr(constraint const & c) { + lean_assert(is_eq_cnstr(c)); + return static_cast(c.raw())->m_lhs; +} +expr const & cnstr_rhs_expr(constraint const & c) { + lean_assert(is_eq_cnstr(c)); + return static_cast(c.raw())->m_rhs; +} bool relax_main_opaque(constraint const & c) { return c.raw()->m_relax_main_opaque; } level const & cnstr_lhs_level(constraint const & c) { lean_assert(is_level_eq_cnstr(c)); @@ -85,12 +94,20 @@ level const & cnstr_rhs_level(constraint const & c) { lean_assert(is_level_eq_cnstr(c)); return static_cast(c.raw())->m_rhs; } -expr const & cnstr_expr(constraint const & c) { lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_expr; } +expr const & cnstr_expr(constraint const & c) { + lean_assert(is_choice_cnstr(c)); + return static_cast(c.raw())->m_expr; +} choice_fn const & cnstr_choice_fn(constraint const & c) { lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_fn; } +bool cnstr_on_demand(constraint const & c) { + lean_assert(is_choice_cnstr(c)); + return static_cast(c.raw())->m_delay_factor.on_demand(); +} unsigned cnstr_delay_factor(constraint const & c) { - lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_delay_factor; + lean_assert(is_choice_cnstr(c)); + return static_cast(c.raw())->m_delay_factor.explict_value(); } bool cnstr_is_owner(constraint const & c) { lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_owner; @@ -103,7 +120,9 @@ constraint update_justification(constraint const & c, justification const & j) { case constraint_kind::LevelEq: return mk_level_eq_cnstr(cnstr_lhs_level(c), cnstr_rhs_level(c), j); case constraint_kind::Choice: - return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), cnstr_is_owner(c), j, relax_main_opaque(c)); + return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), + static_cast(c.raw())->m_delay_factor, + cnstr_is_owner(c), j, relax_main_opaque(c)); } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h index 4af0d564d..6a3fc30d3 100644 --- a/src/kernel/constraint.h +++ b/src/kernel/constraint.h @@ -16,6 +16,16 @@ namespace lean { class expr; class justification; class substitution; + +class delay_factor { + optional m_value; +public: + delay_factor() {} + delay_factor(unsigned v):m_value(v) {} + bool on_demand() const { return !m_value; } + unsigned explict_value() const { lean_assert(!on_demand()); return *m_value; } +}; + /** \brief The lean kernel type checker produces two kinds of constraints: @@ -69,7 +79,7 @@ public: friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque); friend constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j); - friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, bool owner, + friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, delay_factor const & f, bool owner, justification const & j, bool relax_main_opaque); constraint_cell * raw() const { return m_ptr; } @@ -83,6 +93,7 @@ inline bool operator!=(constraint const & c1, constraint const & c2) { return !( */ constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque); constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j); + /** \brief Create a "choice" constraint m in fn(...), where fn produces a stream of possible solutions. \c delay_factor allows to control when the constraint is processed by the elaborator, bigger == later. If \c owner is true, then the elaborator should not assign the metavariable get_app_fn(m). @@ -92,7 +103,8 @@ constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification If \c relax_main_opaque is true, then it signs that constraint was created in a context where opaque constants of the main module can be treated as transparent. */ -constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, bool owner, justification const & j, bool relax_main_opaque); +constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, delay_factor const & f, + bool owner, justification const & j, bool relax_main_opaque); inline bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; } inline bool is_level_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::LevelEq; } @@ -110,10 +122,12 @@ bool relax_main_opaque(constraint const & c); level const & cnstr_lhs_level(constraint const & c); /** \brief Return the rhs of an level constraint. */ level const & cnstr_rhs_level(constraint const & c); -/** \brief Return the expression associated with a choice constraint */ +/** \brief Return the expression associated with the given choice constraint */ expr const & cnstr_expr(constraint const & c); /** \brief Return the choice_fn associated with a choice constraint. */ choice_fn const & cnstr_choice_fn(constraint const & c); +/** \brief Return true iff the choice constraint should be solved as soon the type does not contains type variables */ +bool cnstr_on_demand(constraint const & c); /** \brief Return the choice constraint delay factor */ unsigned cnstr_delay_factor(constraint const & c); /** \brief Return true iff the given choice constraints owns the right to assign the metavariable in \c c. */ diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index e0506902e..4de1d0b7a 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -29,6 +29,7 @@ Author: Leonardo de Moura #include "library/unifier_plugin.h" #include "library/kernel_bindings.h" #include "library/print.h" +#include "library/expr_lt.h" #ifndef LEAN_DEFAULT_UNIFIER_MAX_STEPS #define LEAN_DEFAULT_UNIFIER_MAX_STEPS 20000 @@ -283,18 +284,22 @@ cnstr_group get_choice_cnstr_group(constraint const & c) { struct unifier_fn { typedef pair cnstr; // constraint + idx struct cnstr_cmp { - int operator()(cnstr const & c1, cnstr const & c2) const { return c1.second < c2.second ? -1 : (c1.second == c2.second ? 0 : 1); } + int operator()(cnstr const & c1, cnstr const & c2) const { + return c1.second < c2.second ? -1 : (c1.second == c2.second ? 0 : 1); + } }; typedef rb_tree cnstr_set; typedef rb_tree cnstr_idx_set; typedef rb_map name_to_cnstrs; typedef rb_map owned_map; + typedef rb_map, expr_quick_cmp> expr_map; typedef std::unique_ptr type_checker_ptr; environment m_env; name_generator m_ngen; substitution m_subst; constraints m_postponed; // constraints that will not be solved owned_map m_owned_map; // mapping from metavariable name m to delay factor of the choice constraint that owns m + expr_map m_type_map; // auxiliary map for storing the type of the expr in choice constraints unifier_plugin m_plugin; type_checker_ptr m_tc[2]; type_checker_ptr m_flex_rigid_tc[2]; // type checker used when solving flex rigid constraints. By default, @@ -343,6 +348,7 @@ struct unifier_fn { substitution m_subst; constraints m_postponed; cnstr_set m_cnstrs; + expr_map m_type_map; name_to_cnstrs m_mvar_occs; owned_map m_owned_map; bool m_pattern; @@ -350,7 +356,7 @@ struct unifier_fn { /** \brief Save unifier's state */ case_split(unifier_fn & u, justification const & j): m_assumption_idx(u.m_next_assumption_idx), m_jst(j), m_subst(u.m_subst), - m_postponed(u.m_postponed), m_cnstrs(u.m_cnstrs), + m_postponed(u.m_postponed), m_cnstrs(u.m_cnstrs), m_type_map(u.m_type_map), m_mvar_occs(u.m_mvar_occs), m_owned_map(u.m_owned_map), m_pattern(u.m_pattern) { u.m_next_assumption_idx++; } @@ -364,6 +370,7 @@ struct unifier_fn { u.m_mvar_occs = m_mvar_occs; u.m_owned_map = m_owned_map; u.m_pattern = m_pattern; + u.m_type_map = m_type_map; m_assumption_idx = u.m_next_assumption_idx; m_failed_justifications = mk_composite1(m_failed_justifications, *u.m_conflict); u.m_next_assumption_idx++; @@ -468,11 +475,16 @@ struct unifier_fn { add_mvar_occ(mlocal_name(get_app_fn(m)), cidx); } - void add_meta_occs(expr const & e, unsigned cidx) { + /** \brief For each metavariable m in e add an entry m -> cidx at m_mvar_occs. + Return true if at least one entry was added. + */ + bool add_meta_occs(expr const & e, unsigned cidx) { + bool added = false; if (has_expr_metavar(e)) { for_each(e, [&](expr const & e, unsigned) { if (is_meta(e)) { add_meta_occ(e, cidx); + added = true; return false; } if (is_local(e)) @@ -480,6 +492,7 @@ struct unifier_fn { return has_expr_metavar(e); }); } + return added; } /** \brief Add constraint to the constraint queue */ @@ -661,7 +674,8 @@ struct unifier_fn { return true; } - justification mk_invalid_local_ctx_justification(expr const & lhs, expr const & rhs, justification const & j, expr const & bad_local) { + justification mk_invalid_local_ctx_justification(expr const & lhs, expr const & rhs, justification const & j, + expr const & bad_local) { justification new_j = mk_justification(get_app_fn(lhs), [=](formatter const & fmt, substitution const & subst) { format r = format("invalid local context when tried to assign"); r += pp_indent_expr(fmt, rhs); @@ -979,15 +993,64 @@ struct unifier_fn { return true; } - bool preprocess_choice_constraint(constraint const & c) { - if (cnstr_is_owner(c)) { - expr m = get_app_fn(cnstr_expr(c)); - lean_assert(is_metavar(m)); - m_owned_map.insert(mlocal_name(m), cnstr_delay_factor(c)); + bool preprocess_choice_constraint(constraint c) { + if (!cnstr_on_demand(c)) { + if (cnstr_is_owner(c)) { + expr m = get_app_fn(cnstr_expr(c)); + lean_assert(is_metavar(m)); + m_owned_map.insert(mlocal_name(m), cnstr_delay_factor(c)); + } + add_cnstr(c, get_choice_cnstr_group(c)); + return true; + } else { + expr m = cnstr_expr(c); + // choice constraints that are marked as "on demand" + // are only processed when all metavariables in the + // type of m have been instantiated. + expr type; + justification jst; + if (auto it = m_type_map.find(m)) { + // Type of m is already cached in m_type_map + type = it->first; + jst = it->second; + } else { + // Type of m is not cached yet, we + // should infer it, process generated + // constraints and save the result in + // m_type_map. + bool relax = relax_main_opaque(c); + constraint_seq cs; + optional t = infer(m, relax, cs); + if (!t) { + set_conflict(c.get_justification()); + return false; + } + if (!process_constraints(cs)) + return false; + type = *t; + m_type_map.insert(m, mk_pair(type, justification())); + } + // Try to instantiate metavariables in type + pair type_jst = m_subst.instantiate_metavars(type); + if (type_jst.first != type) { + // Type was modified by instantiation, + // we update the constraint justification, + // and store the new type in m_type_map + jst = mk_composite1(jst, type_jst.second); + type = type_jst.first; + c = update_justification(c, jst); + m_type_map.insert(m, mk_pair(type, jst)); + } + unsigned cidx = add_cnstr(c, cnstr_group::ClassInstance); + if (!add_meta_occs(type, cidx)) { + // type does not contain metavariables... + // so this "on demand" constraint is ready to be solved + m_cnstrs.erase(cnstr(c, cidx)); + add_cnstr(c, cnstr_group::Basic); + m_type_map.erase(m); + } + return true; } - // Choice constraints are never considered easy. - add_cnstr(c, get_choice_cnstr_group(c)); - return true; } /** diff --git a/tests/lean/empty.lean.expected.out b/tests/lean/empty.lean.expected.out index 83750af98..64e1db665 100644 --- a/tests/lean/empty.lean.expected.out +++ b/tests/lean/empty.lean.expected.out @@ -1,2 +1,11 @@ -empty.lean:6:25: error: failed to synthesize placeholder - ⊢ nonempty Empty +empty.lean:6:25: error: type error in placeholder assigned to + Empty +placeholder has type + Type.{1} +but is expected to have type + Type.{?M_1} +the assignment was attempted when trying to solve + type mismatch at definition 'v2', has type + Empty + but is expected to have type + Empty diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean new file mode 100644 index 000000000..04ba739f9 --- /dev/null +++ b/tests/lean/run/group3.lean @@ -0,0 +1,258 @@ +-- Copyright (c) 2014 Jeremy Avigad. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Authors: Jeremy Avigad, Leonardo de Moura + +-- algebra.group +-- ============= + +-- Various structures with 1, *, inv, including groups. + +import logic.core.eq logic.core.connectives +import data.unit data.sigma data.prod +import algebra.function algebra.binary + +open eq + +namespace algebra + +-- classes for notation +-- -------------------- + +inductive has_mul [class] (A : Type) : Type := mk : (A → A → A) → has_mul A +inductive has_one [class] (A : Type) : Type := mk : A → has_one A +inductive has_inv [class] (A : Type) : Type := mk : (A → A) → has_inv A + +definition mul {A : Type} {s : has_mul A} (a b : A) : A := has_mul.rec (fun f, f) s a b +definition one {A : Type} {s : has_one A} : A := has_one.rec (fun o, o) s +definition inv {A : Type} {s : has_inv A} (a : A) : A := has_inv.rec (fun i, i) s a + +infix `*` := mul +postfix `⁻¹` := inv +notation 1 := one + +-- semigroup +-- --------- + +inductive semigroup [class] (A : Type) : Type := +mk : Π mul: A → A → A, + (∀a b c : A, (mul (mul a b) c = mul a (mul b c))) → + semigroup A + +namespace semigroup + section + parameters {A : Type} {s : semigroup A} + definition mul (a b : A) : A := semigroup.rec (λmul assoc, mul) s a b + definition assoc {a b c : A} : mul (mul a b) c = mul a (mul b c) := + semigroup.rec (λmul assoc, assoc) s a b c + end +end semigroup + +section + parameters {A : Type} {s : semigroup A} + definition semigroup_has_mul [instance] : including A s, has_mul A := has_mul.mk (semigroup.mul) + + theorem mul_assoc [instance] {a b c : A} : including A s, a * b * c = a * (b * c) := + semigroup.assoc +end + + +-- comm_semigroup +-- -------------- + +inductive comm_semigroup [class] (A : Type) : Type := +mk : Π mul: A → A → A, + (∀a b c : A, (mul (mul a b) c = mul a (mul b c))) → + (∀a b : A, mul a b = mul b a) → + comm_semigroup A + +namespace comm_semigroup + section + parameters {A : Type} {s : comm_semigroup A} + definition mul (a b : A) : A := comm_semigroup.rec (λmul assoc comm, mul) s a b + definition assoc {a b c : A} : mul (mul a b) c = mul a (mul b c) := + comm_semigroup.rec (λmul assoc comm, assoc) s a b c + definition comm {a b : A} : mul a b = mul b a := + comm_semigroup.rec (λmul assoc comm, comm) s a b + end +end comm_semigroup + +section + parameters {A : Type} {s : comm_semigroup A} + definition comm_semigroup_semigroup [instance] : including A s, semigroup A := + semigroup.mk (comm_semigroup.mul) (@comm_semigroup.assoc _ _) + + theorem mul_comm {a b : A} : including A s, a * b = b * a := comm_semigroup.comm + + theorem mul_left_comm {a b c : A} : including A s, a * (b * c) = b * (a * c) := + binary.left_comm (@mul_comm) (@mul_assoc _ _) a b c +end + + +-- monoid +-- ------ + +inductive monoid [class] (A : Type) : Type := +mk : Π mul: A → A → A, + Π one : A, + (∀a b c : A, (mul (mul a b) c = mul a (mul b c))) → + (∀a : A, mul a one = a) → + (∀a : A, mul one a = a) → + monoid A + +namespace monoid + section + parameters {A : Type} {s : monoid A} + definition mul (a b : A) : A := monoid.rec (λmul one assoc right_id left_id, mul) s a b + definition one : A := monoid.rec (λmul one assoc right_id left_id, one) s + definition assoc {a b c : A} : mul (mul a b) c = mul a (mul b c) := + monoid.rec (λmul one assoc right_id left_id, assoc) s a b c + definition right_id {a : A} : mul a one = a := + monoid.rec (λmul one assoc right_id left_id, right_id) s a + definition left_id {a : A} : mul one a = a := + monoid.rec (λmul one assoc right_id left_id, left_id) s a + end +end monoid + +section + parameters {A : Type} {s : monoid A} + definition monoid_has_one [instance] : including A s, has_one A := has_one.mk (monoid.one) + definition monoid_semigroup [instance] : including A s, semigroup A := + semigroup.mk (monoid.mul) (@monoid.assoc _ _) + + theorem mul_right_id {a : A} : including s, a * one = a := monoid.right_id + theorem mul_left_id {a : A} : including s, one * a = a := monoid.left_id +end + + +-- comm_monoid +-- ----------- + +inductive comm_monoid [class] (A : Type) : Type := +mk : Π mul: A → A → A, + Π one : A, + (∀a b c : A, (mul (mul a b) c = mul a (mul b c))) → + (∀a : A, mul a one = a) → + (∀a : A, mul one a = a) → + (∀a b : A, mul a b = mul b a) → + comm_monoid A + +namespace comm_monoid + section + parameters {A : Type} {s : comm_monoid A} + definition mul (a b : A) : A := comm_monoid.rec (λmul one assoc right_id left_id comm, mul) s a b + definition one : A := comm_monoid.rec (λmul one assoc right_id left_id comm, one) s + definition assoc {a b c : A} : mul (mul a b) c = mul a (mul b c) := + comm_monoid.rec (λmul one assoc right_id left_id comm, assoc) s a b c + definition right_id {a : A} : mul a one = a := + comm_monoid.rec (λmul one assoc right_id left_id comm, right_id) s a + definition left_id {a : A} : mul one a = a := + comm_monoid.rec (λmul one assoc right_id left_id comm, left_id) s a + definition comm {a b : A} : mul a b = mul b a := + comm_monoid.rec (λmul one assoc right_id left_id comm, comm) s a b + end +end comm_monoid + +section + parameters {A : Type} {s : comm_monoid A} + definition comm_monoid_monoid [instance] : including A s, monoid A := + monoid.mk (comm_monoid.mul) (comm_monoid.one) (@comm_monoid.assoc _ _) + (@comm_monoid.right_id _ _) (@comm_monoid.left_id _ _) + definition comm_monoid_comm_semigroup [instance] : including A s, comm_semigroup A := + comm_semigroup.mk (comm_monoid.mul) (@comm_monoid.assoc _ _) (@comm_monoid.comm _ _) +end + + +-- bundled structures +-- ------------------ + +inductive Semigroup [class] : Type := mk : Π carrier : Type, semigroup carrier → Semigroup +namespace Semigroup + section + parameter (S : Semigroup) + definition carrier : Type := Semigroup.rec (λc s, c) S + definition struc : semigroup carrier := Semigroup.rec (λc s, s) S + end +end Semigroup +coercion Semigroup.carrier +instance Semigroup.struc + +inductive CommSemigroup [class] : Type := + mk : Π carrier : Type, comm_semigroup carrier → CommSemigroup +namespace CommSemigroup + section + parameter (S : CommSemigroup) + definition carrier : Type := CommSemigroup.rec (λc s, c) S + definition struc : comm_semigroup carrier := CommSemigroup.rec (λc s, s) S + end +end CommSemigroup +coercion CommSemigroup.carrier +instance CommSemigroup.struc + +inductive Monoid [class] : Type := mk : Π carrier : Type, monoid carrier → Monoid +namespace Monoid + section + parameter (S : Monoid) + definition carrier : Type := Monoid.rec (λc s, c) S + definition struc : monoid carrier := Monoid.rec (λc s, s) S + end +end Monoid +coercion Monoid.carrier +instance Monoid.struc + +inductive CommMonoid : Type := mk : Π carrier : Type, comm_monoid carrier → CommMonoid +namespace CommMonoid + section + parameter (S : CommMonoid) + definition carrier : Type := CommMonoid.rec (λc s, c) S + definition struc : comm_monoid carrier := CommMonoid.rec (λc s, s) S + end +end CommMonoid +coercion CommMonoid.carrier +instance CommMonoid.struc + +end algebra + + +open algebra + +section examples + +theorem test1 {S : Semigroup} (a b c d : S) : a * (b * c) * d = a * b * (c * d) := +calc + a * (b * c) * d = a * b * c * d : {symm mul_assoc} + ... = a * b * (c * d) : mul_assoc + +theorem test2 {M : CommSemigroup} (a b : M) : a * b = a * b := rfl + +theorem test3 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) := +calc + a * (b * c) * d = a * b * c * d : {symm mul_assoc} + ... = a * b * (c * d) : mul_assoc + +-- for test4b to work, we need instances at the level of the bundled structures as well +definition Monoid_Semigroup [instance] (M : Monoid) : Semigroup := +Semigroup.mk (Monoid.carrier M) _ + +theorem test4 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) := +test1 a b c d + +theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) := +calc + a * 1 * b * c = a * b * c : {mul_right_id} + ... = a * (b * c) : mul_assoc + +theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) := +calc + a * 1 * b * c = a * b * c : {mul_right_id} + ... = a * (b * c) : mul_assoc + +theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) := +calc + a * 1 * b * c = a * b * c : {mul_right_id} + ... = a * (b * c) : mul_assoc + +theorem test6 {M : CommMonoid} (a b c : M) : a * 1 * b * c = a * (b * c) := +calc + a * 1 * b * c = a * b * c : {mul_right_id} + ... = a * (b * c) : mul_assoc +end examples