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

@@ -263,14 +263,18 @@ static bool has_expr_metavar_relaxed(expr const & e) {
 }
 
 constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> 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)) {
+            // TODO(Leo): remove
-                constraint delayed_c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, delay_factor+1);
+            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>(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>(constraints(delayed_c));
             }
         }
@@ -315,7 +319,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> 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<expr, constraint> mk_placeholder_elaborator(
     bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg) {
     auto C       = std::make_shared<placeholder_context>(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);
 }
 }

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;
+    expr         m_expr;
-    choice_fn m_fn;
+    choice_fn    m_fn;
-    unsigned  m_delay_factor;
+    delay_factor m_delay_factor;
-    bool      m_owner;
+    bool         m_owner;
-    choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, bool owner, justification const & j, bool relax):
+    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<eq_constraint_cell*>(c.raw())->m_lhs; }
+expr const & cnstr_lhs_expr(constraint const & c) {
-expr const & cnstr_rhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast<eq_constraint_cell*>(c.raw())->m_rhs; }
+    lean_assert(is_eq_cnstr(c));
+    return static_cast<eq_constraint_cell*>(c.raw())->m_lhs;
+}
+expr const & cnstr_rhs_expr(constraint const & c) {
+    lean_assert(is_eq_cnstr(c));
+    return static_cast<eq_constraint_cell*>(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<level_constraint_cell*>(c.raw())->m_rhs;
 }
-expr const & cnstr_expr(constraint const & c) { lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_expr; }
+expr const & cnstr_expr(constraint const & c) {
+    lean_assert(is_choice_cnstr(c));
+    return static_cast<choice_constraint_cell*>(c.raw())->m_expr;
+}
 choice_fn const & cnstr_choice_fn(constraint const & c) {
     lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_fn;
 }
+bool cnstr_on_demand(constraint const & c) {
+    lean_assert(is_choice_cnstr(c));
+    return static_cast<choice_constraint_cell*>(c.raw())->m_delay_factor.on_demand();
+}
 unsigned cnstr_delay_factor(constraint const & c) {
-    lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_delay_factor;
+    lean_assert(is_choice_cnstr(c));
+    return static_cast<choice_constraint_cell*>(c.raw())->m_delay_factor.explict_value();
 }
 bool cnstr_is_owner(constraint const & c) {
     lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(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<choice_constraint_cell*>(c.raw())->m_delay_factor,
+                               cnstr_is_owner(c), j, relax_main_opaque(c));
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }

src/kernel/constraint.h

@@ -16,6 +16,16 @@ namespace lean {
 class expr;
 class justification;
 class substitution;
+
+class delay_factor {
+    optional<unsigned> 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. */

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<constraint, unsigned> 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, cnstr_cmp> cnstr_set;
     typedef rb_tree<unsigned, unsigned_cmp> cnstr_idx_set;
     typedef rb_map<name, cnstr_idx_set, name_quick_cmp> name_to_cnstrs;
     typedef rb_map<name, unsigned, name_quick_cmp> owned_map;
+    typedef rb_map<expr, pair<expr, justification>, expr_quick_cmp> expr_map;
     typedef std::unique_ptr<type_checker> 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) {
+    bool preprocess_choice_constraint(constraint c) {
-        if (cnstr_is_owner(c)) {
+        if (!cnstr_on_demand(c)) {
-            expr m = get_app_fn(cnstr_expr(c));
+            if (cnstr_is_owner(c)) {
-            lean_assert(is_metavar(m));
+                expr m = get_app_fn(cnstr_expr(c));
-            m_owned_map.insert(mlocal_name(m), cnstr_delay_factor(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<expr> 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<expr, justification> 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;
     }
 
     /**

tests/lean/empty.lean.expected.out

@@ -1,2 +1,11 @@
-empty.lean:6:25: error: failed to synthesize placeholder
+empty.lean:6:25: error: type error in placeholder assigned to
- ⊢ nonempty Empty
+  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

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