leanprover/lean — pull request #379 by avigad (2014-12-17 18:47:11+00:00)
Title: refactor(library/data/int/basic): make the integers an instance of ring

I made the integers and instance of the class comm_ring, and then "ported" facts about rings to the integers.

Some notes:

As proof of concept, it went pretty well. It is nice that basic facts about the integers are now instances of the generic algebraic theorems, with the same names.

There is still a lot more to do. I still need to do the same for the ordering on int, and also make int an integral domain with dvd and abs, and ordered_ring, etc. And I have to do the similar thing for nat.

As predicted, porting the list of theorems by hand is tedious, but workable. It will be nice to have automation for this later.

One of the theorems uncovered a possible bug. At least, I can't understand why one theorem (and only one from the list I ported!) fails to type check. Lean reports a Type mismatch, but evaluating both sides yields exactly the same term. Search on "TODO" in int/basic.lean.

Question: when porting theorems, I used "open algebra". Is there any way to "limit" the open to a section, or "close" it afterwards? It would be nice if the "open" were limited to the scope of a section. In general, I have noticed that overloading can be a real pain -- error messages, for example, become less helpful. When working with ints, it would be helpful to open nat notation very selectively.

@javra : I am afraid I renamed some theorems in group.lean:

eq_of_neg_eq_neg -> neg.inj
neg_zero_eq -> neg_zero
neg_neg_eq_ -> neg_neg
eq_of_inv_eq_inv -> inv.inj
inv_one_eq -> inv_one
inv_inv_eq -> inv_inv

I am afraid there will be a lot more renaming and housecleaning to come. In particular, I have to revise nat to match our naming conventions.

By the way: the naming conventions are working really well. Autocompletion is great.