fix(library/elaborator): add hack for experimenting with algebraic hierarchy

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

examples/lean/test_algebra.lean

@@ -0,0 +1,108 @@
+import macros
+
+---
+--- Classes of structures, and axiomatic classes of structures
+---
+
+--- A "structure" consists of a carrier, and some data (whose type depends on the carrier)
+
+definition StructClass : (Type 1) := Type → Type   -- the type of the data
+
+definition structure (S : StructClass) : (Type 1)
+:= sig T : Type, S T
+
+definition carrier {S : StructClass} (M : structure S) : Type
+:= proj1 M
+
+definition data {S : StructClass} (M : structure S) : S (carrier M)
+:= proj2 M
+
+--- An "axiomatic class" is a class of structures satisfying some predicate (the "axioms")
+
+definition AxClass : (Type 1)
+:= sig S : StructClass, structure S → Bool
+
+-- Coercion from AxClass to StructClass
+definition struct_class (C : AxClass) : StructClass
+:= proj1 C
+
+definition axioms {C : AxClass} (M : structure (struct_class C))
+:= proj2 C M
+
+definition instance (C : AxClass) : (Type 1)
+:= sig M : structure (struct_class C), axioms M
+
+definition struct {C : AxClass} (M : instance C)
+:= proj1 M
+
+definition hyps {C : AxClass} (M : instance C) : axioms (struct M)
+:= proj2 M
+
+---
+--- Examples
+---
+
+--- multiplication (for overloading *)
+
+definition MulStruct : StructClass
+:= λ T, T → T → T
+
+definition mul {M : structure MulStruct} (x y : carrier M) : carrier M
+:= data M x y
+
+infixl 70 * : mul
+
+definition mul_is_assoc (M : structure MulStruct) : Bool
+:= ∀ x y z : carrier M, (x * y) * z = x * (y * z)
+
+definition mul_is_comm (M : structure MulStruct) : Bool
+:= ∀ x y z : carrier M, x * y = y * x
+
+--- semigroups
+
+definition Semigroup : AxClass
+:= pair MulStruct mul_is_assoc
+
+--- to fill the hole above automatically
+theorem semigroup_mul_is_assoc (M : instance Semigroup) : mul_is_assoc (struct M)
+:= hyps M
+
+definition OneStruct : StructClass
+:= λ T, T
+
+definition one {M : structure OneStruct} : carrier M
+:= data M
+
+-- structures with mult and one
+
+definition MonoidStruct : StructClass
+:= λ T, OneStruct T # MulStruct T
+
+definition MonoidStruct_to_OneStruct (M : structure MonoidStruct) : (structure OneStruct)
+:= pair (carrier M) (proj1 (data M))
+
+definition MonoidStruct_to_MulStruct (M : structure MonoidStruct) : (structure MulStruct)
+:= pair (carrier M) (proj2 (data M))
+
+variable M : structure MonoidStruct
+check carrier M = carrier (MonoidStruct_to_OneStruct M)
+
+theorem test1 (M : structure MonoidStruct) : carrier M = carrier (MonoidStruct_to_OneStruct M)
+:= refl (carrier M)
+
+definition is_mul_right_id (M : structure MonoidStruct) : Bool
+:= let m : carrier M → carrier M → carrier M := @mul (MonoidStruct_to_MulStruct M),
+       o : carrier M                            := @one (MonoidStruct_to_OneStruct M)
+   in ∀ x : carrier M, m x o = x
+
+definition is_monoid (M : structure MonoidStruct) : Bool
+:= mul_is_assoc (MonoidStruct_to_MulStruct M) ∧ is_mul_right_id M
+
+definition Monoid : AxClass
+:= pair MonoidStruct is_monoid
+
+theorem monoid_is_mul_right_id (M : instance Monoid) : is_mul_right_id (struct M)
+:= and_elimr (proj2 M)
+
+theorem monoid_mul_is_assoc (M : instance Monoid) : mul_is_assoc (MonoidStruct_to_MulStruct (struct M))
+:= and_eliml (proj2 M)

src/library/elaborator/elaborator.cpp

@@ -1641,7 +1641,9 @@ class elaborator::imp {
         if (process_assigned_metavar(c, a, true) || process_assigned_metavar(c, b, false))
             return true;
 
-        if (m_assume_injectivity && is_app(a) && is_app(b) && num_args(a) == num_args(b) && arg(a, 0) == arg(b, 0) && !is_metavar(arg(a, 0))) {
+        if (m_assume_injectivity && is_app(a) && is_app(b) && num_args(a) == num_args(b) && arg(a, 0) == arg(b, 0) && !is_metavar(arg(a, 0))
+            // BIG (temporary) HACK
+            && !(is_constant(arg(a, 0)) && const_name(arg(a, 0)) == "carrier")) {
             // If m_assume_injectivity is true, we apply the following rule
             // ctx |- (f a1 a2) ≈ (f b1 b2)
             // ==>