algorithms, Fraction in library

Stream: maths

[Sergei]

Dear Lean people,
I have the three newbie questions.

1. Generally, can Lean be used as a provable programming language?
So that to implement an efficient algorithm and also prove its correctness, and then also to run the obtained code.

2. Concretely: consider implementing fraction arithmetic over an arbitrary GCD Domain R. Find sum of fractions by doing + and * in R, by computing gcd, and cancelling by it (in various places of the method). And provide a proof for that this +' and *' on Q = (Fraction R ) make Q a field.
a) Is this possible to program in Lean and to run as a more or less efficient program?
b) Is this already in some library for Lean ?
I see "localization.lean" somewhere in mathlib, this is a generalization for Fraction field. But I do not find there using GCD, any matter of algorithms. Also I do not see there any comments.

3) The mathlib materials are difficult to understand, they just show the code. But there are needed comments in a humanly language in the first place, a reference to a textbook, to a paper (a similar problem I find in Coq).

Please, advise,

---

Sergei

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/master/src/data/rat.lean#L227

[Kenny Lau]

there are no "efficient" algorithms yet. they run kind of slowly.

[Kevin Buzzard]

I agree about comments in mathlib. Which files are you interested in in particular?

[Reid Barton]

I think we have a merge sort (of the kind that uses linear additional space)--that's about it

[Sergei]

https://github.com/leanprover-community/mathlib/blob/master/src/data/rat.lean#L227

But this is actually Rational = (Fraction Integer). And I talk about (Fraction R) for arbitrary integral domain R supplied with gcd.

[Kevin Buzzard]

Yes, this is rational numbers. We do have field of fractions of an arbitrary integral domain though: https://github.com/leanprover-community/mathlib/blob/b55e44de0cdd632c2a1c3c21ce05f814ab6f614a/src/ring_theory/localization.lean#L436

[Sergei]

I agree about comments in mathlib. Which files are you interested in in particular?

I do not see these files. They need to be about how so do + and * on Fractions with cancelling by gcd in a general case, not only for rational numbers.

[Kevin Buzzard]

The link I sent is just an abstract construction of the field of fractions of an integral domain. No gcd algorithm is needed to make this ring. There is no claim that any fraction can be put into a "canonical form" there.

[Sergei]

We do have field of fractions of an arbitrary integral domain though:
https://github.com/leanprover-community/mathlib> /blob/b55e44de0cdd632c2a1c3c21ce05f814ab6f614a/src/ring_theory/localization.lean#L436

I have seen this from the start. I understand that substituting {0} for a prime ideal in an integral ring R for localization we obtain actually the domain (Fraction R). But I do not know the Lean language. And I do not see any explanation concerning the algorithms. How are fractions summed? Is it
a/b + a'/b' = (ab' + a'b)/(b*b') ?
Is the result somehow reduced? If R has a sensible gcd, probably it can be applied, or may be one can reduce by some ideal ...
If it is not reduced, then how will this arithmetic work say for R = Z2[x] for
Z2 = Integer modulo 2 ? how will there grow the denominator degrees?
I mean different provable ways to sum fractions that aim at a bit of efficiency. Because in computer algebra not only proof matters, but also efficiency.
This file localization.lean is difficult to understand. The only thing I understood is that this is about a local ring, and that its equality is proved transitive. There needs to be somewhere a short explanation in a humanly language of what is such and such method, say, a reference to a textbook + several words about algorithms.
?
A similar strange problem is with the Coq math libraries. One needs just to read the bare code instead of observing literature references and humanly explanations.

[Reid Barton]

It's not reduced and it's not meant to be efficient. It's math, not computer algebra.
However, it would also be possible to implement what you suggest--it just hasn't been done in mathlib yet.

[Sergei]

I see now. Thank you.
Generally in these mathlib-s there is a problem of literature references and humanly explanations.

[Kevin Buzzard]

The reference is Atiyah and Macdonald's book "commutative algebra". Yes, this is maths not computer algebra. The code is written so we can reason about maths, not do computations with it.