automatically generate merge constructors for structures

[avigad]

Suppose a structure S extends R1, R2, R3 with new axioms (x1 : X1) (x2 : X2).

The structure command should prove a "merge constructor" that builds an instance of S from (s1 : R1) (s2 : R2) (s3 : R3) (x1 : X1) (x2 : X2), with preconditions that the overlapping components of s1, s2, and s3 agree.

There is a discussion here: https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/K5I7UtwZ7nE/FuUdlG6Xr6EJ

Here is an example for group -> comm_monoid -> comm_group.

definition merge {A : Type} (g : group A) (m : comm_monoid A) : (comm_monoid.mul = group.mul) → comm_group A := group.cases_on g (λ mul₁ mul_assoc₁ one₁ lid₁ rid₁ inv₁ is_inv₁, comm_monoid.cases_on m (λ mul₂ mul_assoc₂ one₂ lid₂ rid₂ mul_comm₂, λ Heq, have Heq' : mul₂ = mul₁, from Heq, comm_group.mk mul₁ mul_assoc₁ one₁ lid₁ rid₁ inv₁ is_inv₁ (eq.rec_on Heq' mul_comm₂)))

[leodemoura]

BTW, do you care whether has_mul.mul (merge g f) is definitionally equal to has_mul.mul g? In the construction I suggested above, they aren't when g or f is opaque or a variable (in both cases the cases_on would get stuck). I assumed this is not a problem, since we will usually use merge with actual records such as int_group and int_comm_monoid. If this becomes an issue, we can use the following alternative construction:

definition merge {A : Type} (g : group A) (m : comm_monoid A) : (comm_monoid.mul = group.mul) → comm_group A :=
λ Heq,
comm_group.mk group.mul group.mul_assoc !group.one group.mul_left_id group.mul_right_id group.inv group.mul_left_inv
                (have aux : ∀f, comm_monoid.mul = f → ∀ a b, f a b = f b a, from
                   λf Heq, eq.subst Heq comm_monoid.mul_comm,
                 aux _ Heq)

In this alternative construction, has_mul.mul (merg g f) is always definitionally equal to has_mul.mul g. However, it is not definitionally equal to has_mul.mul g.

I don't think this is a big deal. Do you see any potential problems?

[avigad]

I don't think it is a problem. Even in the abstract case, the usage I described is when there a structure A that is an instance of two structures B and C, and we want to show that an instance s of A is an instance of a structure with B and C merged. In that case, "g" and "f" are the two terms that turn s into instances of B and C, respectively, and the components has_mul.mul g and has_mul.mul f will both reduce to the mul of s.

On Fri, Nov 28, 2014 at 6:36 PM, Leonardo de Moura <notifications@github.com

wrote:

BTW, do you care whether has_mul.mul (merge g f) is definitionally equal to has_mul.mul g? In the construction I suggested above, they aren't when g or f is opaque or a variable (in both cases the cases_on would get stuck). I assumed this is not a problem, since we will usually use merge with actual records such as int_group and int_comm_monoid. If this becomes an issue, we can use the following alternative construction:

definition merge {A : Type} (g : group A) (m : comm_monoid A) : (comm_monoid.mul = group.mul) → comm_group A := λ Heq,comm_group.mk group.mul group.mul_assoc !group.one group.mul_left_id group.mul_right_id group.inv group.mul_left_inv (have aux : ∀f, comm_monoid.mul = f → ∀ a b, f a b = f b a, from λf Heq, eq.subst Heq comm_monoid.mulcomm, aux Heq)

In this alternative construction, has_mul.mul (merg g f) is always definitionally equal to has_mul.mul g. However, it is not definitionally equal to has_mul.mul g.

I don't think this is a big deal. Do you see any potential problems?

— Reply to this email directly or view it on GitHub https://github.com/leanprover/lean/issues/350#issuecomment-64934705.

[fpvandoorn]

I'm not a big fan of this solution, though maybe it's better than everything suggested before. My concerns:

• The merge definitions need to be different for the standard library (using equalities) and the HoTT library (using paths).
• There are casts floating around in the definitions, although it they will likely cast/substitute over reflexivity proofs. Still, this might be computationally a little harder for the elaborator(?)
• For general structures, the merge proofs and even the theorems become quite ugly, like in the following (convoluted) example:

structure category (ob : Type) : Type :=
  (hom : ob → ob → Type)
  (compose : Π {a b c : ob}, hom b c → hom a b → hom a c)
  (id : Π {a : ob}, hom a a)
  (assoc : Π {a b c d : ob} (h : hom c d) (g : hom b c) (f : hom a b),
     compose h (compose g f) = compose (compose h g) f)
  (id_left : Π {a b : ob} (f : hom a b), compose id f = f)
  (id_right : Π {a b : ob} (f : hom a b), compose f id = f)

structure not_a_category (ob : Type) : Type :=
  (hom : ob → ob → Type)
  (compose : Π {a b c : ob}, hom b c → hom a b → hom a c)
  (foo : Π {a b c : ob} (h : hom a c) (g : hom b c) (f : hom a b),
     compose g f = h

structure merged (ob : Type) extends category ob, not_a_category ob

definition merge {ob : Type} (C : category ob) (D : not_a_category ob) 
  (H1 : category.hom = not_a_category.hom)
  (H2 : eq.rec_on H category.compose = not_a_category.compose) 
    : merged ob :=
*ugly*
--in this proof you'll need to either induct on both H1 and H2, or use something like dcongr_arg2

Not really a concern: I think we indeed need to use Leo's definition. I think we really want has_mul.mul (merge g f) definitionally equal to has_mul.mul g, also in the case that g is not of the form group.mk *something*

[fpvandoorn]

[EDIT: the following example is nonsense, see next comments]

To expand on why I think we need the multiplications definitionally equal: I think almost every proof breaks down otherwise (I might be mistaken though). For example:

  theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b :=
  calc
    a⁻¹ * (a * b) = a⁻¹ * a * b : mul_assoc
      ... = 1 * b : mul_left_inv
      ... = b : mul_left_id

In the first line of the calculation, mul_assoc refers to semigroup.mul_assoc. The statement is that a * b * c = a * (b * c) for a semigroup-multiplication, however, we need that a⁻¹ * (a * b) = a⁻¹ * a * b for a group-multiplication. If these are not definitionally equal, we get a type error.

For the same reason, we also really need that the multiplication of the merged structure is definitionally equal to the multiplication in the second structure (in a commutative group). This is true if we merged the structures with rfl, but might still require a tiny bit of computation every time we invoke a theorem.

[leodemoura]

@fpvandoorn Let me try to expand the proposal, and try to address (some of) your concerns.

1) path vs eq We can use eq even in HoTT library. eq here has an auxiliary role. It represents the idea that both muls are identical. In all examples we discussed, it will be filled with refl. Do you see examples where it is not refl? Note that the definitional package will also use eq in the HoTT library. Again, it is playing an auxiliary role (it is being used "behind the scenes").

2) The mess with casts. We can minimize it using heterogeneous equality. This is what I do in the no_confusion construction. "Casts do not scale". I mean, if we have a double/triple dependency, it becomes a super mess. By double dependency I mean: we have a_1 : A_1, a_2 : A_2[a_1], a_3 : A_3 [a_1, a_2]. The only way (I know) to control the mess is to use heterogeneous equality.

For arguments that take heterogeneous equality, we provide heq.refl instead of refl.

BTW. I'm currently finishing the inversion tactic for the definitional package. It will also be available in the front-end. It "hides" this kind of mess for us.

3) The theorems become ugly. If we provide refl and heq.refl to fill the merge "pre-conditions", then all the casts "disappear". Recall that we have K inside the kernel now. So, eq.rec_on H H2 is definitionally equal to H2. Same for heq.rec_on H H2.

Disclaimer: in theory, we should not have problems. However, in practice, we might. The eq.rec_on will be there, and the elaborator will have to get rid of it.

4) multiplications being definitionally equal. For abstract structures like semigroup, group, ... multiplication will be definitionally equal since they are not created using the merge command but extends. The merge is mainly used to produce an instance from instances for the parent structures. Example: int_comm_group from int_group and int_comm_monoid.

5) computation We currently need some computation when using theorems from structure A in a structure B. This is already an issue. To use a theorem from semigroup in a ring, we need to perform a lot of folding/unfolding. If this becomes an issue, we have some a backup plan: automatically generate definitions that shortcut the folding/unfolding in commonly used paths.

We will need a similar trick for the simplifier. Otherwise, we will need to perform a lot of unfolding whenever we want to rewrite using abstract theorems.

[fpvandoorn]

(1) Good point: all proofs will be rfl anyway, so we can just use strict equality. (2) Yes, heq will give cleaner theorems and more systematic proofs. (3) Yeah, hopefully we will never notice the eq.rec_on rfl floating around in the proofs for performance. (4) You're right, my example didn't work at all. I also had another misconception about the algebra library. If I have elements a, b in ring A, and I write a * b, then I thought this meant ring.mul a b, but it means @has_mul.mul A (*composition of a bunch of instances*) a b, right? (5) Ok, that makes sense.

Ok, I'm now convinced that his is indeed the way to go. Thanks.

[leodemoura]

I thought this meant ring.mul a b, but it means (bunch of coercions) (has_mul.mul a b), right?

Yes. This may become a problem. I don't know if this is a performance problem or not.

Right now, I know that the calc expression shortcuts produce a lot of overhead in ring.lean. Suppose we write mul_assoc in a calc expression, but it is supposed to be {!mul_assoc \sy}. Then, calc will try first {!mul_assoc}, and it will spend a lot of time to figure out that there is no way to solve the unification problems generated by this attempt. I plan to address this issue by one of the following alternatives: 1) having a new flag that uses higher-order-pattern-matching + computation. We need to perform computation during unification because of all unfolding/folding that has to happen. 2) use the simplifier (when we have one) instead of subst. 3) implement a custom subst tactic for the calc command.

I think Jeremy did not notice the performance problem because of the cache, It takes almost 2 secs on my machine to process some of his new files.

[avigad]

My sense is that the only situations where we will be inclined to use merge is where the components are definitionally equal. Building structures out of components is common. The issue is that we want to recognize s : A as instances of B and C where certain components of B and C are identified because of the history of how A, B, and C were constructed (which is not reflected in the flat record). We are not merging arbitrary structures; we are merging (A_to_B s) and (A_to_C s), and the common components will be definitionally equal, by construction. I think the net effect of Leo's solution is that the merge will reduce exactly to the structure we would otherwise have to write out by hand.

This reminds me of a conversation I had with Bob Harper last summer in Paris, when I asked him general questions about Lean. Somehow the conversation got to modules. Bob said that it often comes up that you want to have two modules share a parameter, and (at least from the point of programming languages), there are two way to handle it, a "right" way and a "wrong" way.

The wrong way is to have each module depend on the common parameter, e.g. B (mul) and C (mul). The reason that is wrong is because you have the extra information, mul, threaded through the system. The right way is to have a "where" construct, i.e. you say "A = B + C where B.mul = C.mul".

We are using records rather than modules, but this is exactly what the structure command does with "extends". The problem is that we do not have built-in syntax for "merge (f g, where f.mul == g.mul)", but Leo's solution is a nice approximation. We might be able to hide the extra generality by providing a macro that fills in all the preconditions with refl (and fails if that doesn't work), but I don't know whether that would really help anything.

BTW, I have noticed the slowdown. The file ring.lean, which isn't huge, takes about 3 seconds on my laptop. Flycheck is getting sluggish; when I make changes, I often have to wait a couple of seconds to see the effect. There are probably things I can do to make things easier on Lean, like giving parameters explicitly instead of using !mul_assoc in a substitution. (I feel guilty every time I do that, knowing that I am torturing the elaborator with a higher-order unification.)

But so far everything is still workable, and we can look for optimizations later. I think it is remarkable that the algebraic calculations work as well as they do, given that the system has to find all the relevant information. I will let you know if things get markedly worse when I do ordered rings.

On Fri, Nov 28, 2014 at 10:51 PM, Leonardo de Moura < notifications@github.com> wrote:

I thought this meant ring.mul a b, but it means (bunch of coercions) (has_mul.mul a b), right?

Yes. This may become a problem. I don't know if this is a performance problem or not.

Right now, I know that the calc expression shortcuts produce a lot of overhead in ring.lean. Suppose we write mul_assoc in a calc expression, but it is supposed to be {!mul_assoc \sy}. Then, calc will try first {!mul_assoc}, and it will spend a lot of time to figure out that there is no way to solve the unification problems generated by this attempt. I plan to address this issue by one of the following alternatives: 1) having a new flag that uses higher-order-pattern-matching + computation. We need to perform computation during unification because of all unfolding/folding that has to happen. 2) use the simplifier (when we have one) instead of subst. 3) implement a custom subst tactic for the calc command.

I think Jeremy did not notice the performance problem because of the cache, It takes almost 2 secs on my machine to process some of his new files.

— Reply to this email directly or view it on GitHub https://github.com/leanprover/lean/issues/350#issuecomment-64940478.

[leodemoura]

@avigad When I analyzed ring.lean, the performance bottlenecks were places where you wrote P, but the elaborator has to generate {!P\sy}.

In calc expressions, the elaborator can easily find out if it needs ! or not. It just checks whether the proof is a Pi type or not. So, the conversion P -> !P is "free", and there is no case analysis going on. After deciding whether a ! is needed or not, let P' be the resultant proof term. Then, the elaborator tries the following sequence:

• P', P'\sy, {P'} and {P'\sy}.

The first two are usually cheap. If the second is the right choice, the first will probably fail quickly. If the third is also ok, usually the first two will fail quickly. The problem is the fourth one because the third one may take a long time to fail.

[avigad]

This is helpful. I will changes these instances. Thanks!

On Sat, Nov 29, 2014 at 11:12 AM, Leonardo de Moura < notifications@github.com> wrote:

@avigad https://github.com/avigad When I analyzed ring.lean, the performance bottlenecks were places where you wrote P, but the elaborator has to generate {!P\sy}.

In calc expressions, the elaborator can easily find out if it needs ! or not. It just checks whether the proof is a Pi type or not. So, the conversion P -> !P is "free", and there is no case analysis going on. After deciding whether a ! is needed or not, let P' be the resultant proof term. Then, the elaborator tries the following sequence:

• P', P'\sy, {P'} and {P'\sy}.

The first two are usually cheap. If the second is the right choice, the first will probably fail quickly. If the third is also ok, usually the first two will fail quickly. The problem is the fourth one because the third one may take a long time to fail.

— Reply to this email directly or view it on GitHub https://github.com/leanprover/lean/issues/350#issuecomment-64956484.

[avigad]

Making some arguments explicit in calc helped a little.

I think this made a bigger difference: in two of the big "merge" instance declarations, I had used the generic lemmas to fill in the holes, rather than the explicit constructors for the structure. Changing to the latter (e.g. below) helped. In other words, instead of "mul.assoc" I now use "comm_ring_dvd.assoc". Now compilation time is down from about 3 seconds on my laptop to about 1.5 seconds.

---

definition comm_ring_dvd.to_comm_semiring_dvd [instance] [s : comm_ring_dvd A] : comm_semiring_dvd A := comm_semiring_dvd.mk comm_ring_dvd.add comm_ring_dvd.add_assoc (@comm_ring_dvd.zero A s) comm_ring_dvd.add_left_id comm_ring_dvd.add_right_id comm_ring_dvd.add_comm comm_ring_dvd.mul comm_ring_dvd.mul_assoc (@comm_ring_dvd.one A s) comm_ring_dvd.mul_left_id comm_ring_dvd.mul_right_id comm_ring_dvd.distrib_left comm_ring_dvd.distrib_right mul_zero_left mul_zero_right (@comm_ring_dvd.zero_ne_one A s) comm_ring_dvd.mul_comm comm_ring_dvd.dvd (@comm_ring_dvd.dvd_intro A s) (@comm_ring_dvd.dvd_imp_exists A s)

On Sat, Nov 29, 2014 at 11:56 AM, Jeremy Avigad avigad@cmu.edu wrote:

This is helpful. I will changes these instances. Thanks!

On Sat, Nov 29, 2014 at 11:12 AM, Leonardo de Moura < notifications@github.com> wrote:

@avigad https://github.com/avigad When I analyzed ring.lean, the performance bottlenecks were places where you wrote P, but the elaborator has to generate {!P\sy}.

In calc expressions, the elaborator can easily find out if it needs ! or not. It just checks whether the proof is a Pi type or not. So, the conversion P -> !P is "free", and there is no case analysis going on. After deciding whether a ! is needed or not, let P' be the resultant proof term. Then, the elaborator tries the following sequence:

• P', P'\sy, {P'} and {P'\sy}.

The first two are usually cheap. If the second is the right choice, the first will probably fail quickly. If the third is also ok, usually the first two will fail quickly. The problem is the fourth one because the third one may take a long time to fail.

— Reply to this email directly or view it on GitHub https://github.com/leanprover/lean/issues/350#issuecomment-64956484.

[leodemoura]

I implemented syntax sugar for creating structures. It addresses this issue. Here are some examples:

   {| point, x := 10, y := 20 |}   -- create a point setting s.t. field x contains 10, and field y 20
   {| point, x := 10, using p |}  -- similar to previous one, but gets unspecified fields from p

More examples: https://github.com/leanprover/lean/blob/f9d7480f5ce5986cff0708f4add3620082c900ba/tests/lean/run/struct_inst_exprs.lean

I used the new construct to cleanup many definitions in algebra. Example: https://github.com/leanprover/lean/blob/master/library/algebra/ordered_ring.lean#L262

[avigad]

This was a great idea. It depends on the fields having the same name, but it covers all the examples I can think of. It will also make it easier to declare concrete instances too, e.g. in nat and int. I will do these and make sure you got all the others when I am back in Pittsburgh.

The structure mechanism is getting close to optimal. The only remaining desiderata that I can think of are these:

(1) performance issues (short-circuiting paths) (2) having a convenient way to instantiate all the theorems for a structure in a concrete instance.

Thanks again for making Lean so great.

On Fri, Jan 16, 2015 at 9:14 PM, Leonardo de Moura <notifications@github.com

wrote:

Closed #350 https://github.com/leanprover/lean/issues/350.

— Reply to this email directly or view it on GitHub https://github.com/leanprover/lean/issues/350#event-220446143.

[avigad]

Can we use more than one structure, as in "using s1, s2"?

Jeremy

P.S. We have notation "dec_trivial" for "of_is_true trivial"

On Sat, Jan 17, 2015 at 8:19 PM, Jeremy Avigad avigad@cmu.edu wrote:

This was a great idea. It depends on the fields having the same name, but it covers all the examples I can think of. It will also make it easier to declare concrete instances too, e.g. in nat and int. I will do these and make sure you got all the others when I am back in Pittsburgh.

The structure mechanism is getting close to optimal. The only remaining desiderata that I can think of are these:

(1) performance issues (short-circuiting paths) (2) having a convenient way to instantiate all the theorems for a structure in a concrete instance.

Thanks again for making Lean so great.

On Fri, Jan 16, 2015 at 9:14 PM, Leonardo de Moura < notifications@github.com> wrote:

Closed #350 https://github.com/leanprover/lean/issues/350.

— Reply to this email directly or view it on GitHub https://github.com/leanprover/lean/issues/350#event-220446143.

[leodemoura]

Yes, we can more than one. Here is an example: https://github.com/leanprover/lean/blob/edcc92d9c79a9f8f7b2d04fe3a724e370d2249f1/tests/lean/run/struct_inst_exprs2.lean

BTW, I removed the using.

I also described the new notation in the tutorial. http://leanprover.github.io/tutorial/10_Structures_Records.html

[avigad]

Beautiful.

On Sat, Jan 17, 2015 at 9:58 PM, Leonardo de Moura <notifications@github.com

wrote:

Yes, we can more than one. Here is an example:

https://github.com/leanprover/lean/blob/edcc92d9c79a9f8f7b2d04fe3a724e370d2249f1/tests/lean/run/struct_inst_exprs2.lean

BTW, I removed the using.

I also described the new notation in the tutorial. http://leanprover.github.io/tutorial/10_Structures_Records.html

— Reply to this email directly or view it on GitHub https://github.com/leanprover/lean/issues/350#issuecomment-70394526.