[Agda] decidable equality in algebra

[Sergei Meshveliani]

People,

My DoCon-A library currently requires DecSetoid as a base for all the
computer algebra.
But I think about making _≟_ optional.
Because I think, for example, that a Real number can be reasonably
represented as a certain sequence of embedded seqments, so that it will
be possible to prove in Agda that Real has the instances of
CommutativeRing and Field. But equality will not be solvable there.

(only I mean a real Real, do not confuse with floating point).

However I expect that most known algorithms will require various
complicated additional witness arguments to be correct for the case of
real numbers.
For example, for univariate polynomials over Rational coefficients it is
easy to resolve the divisibility relation.
And for Real coefficients, resolving the relation

(x + c) divides (x^2 + a*x + b) (1)

is equivalent to resolving
b - (a-c)*c ≈ 0 (2)

-- a witness for (1) is reduced to a witness for (2).
For arbitrary polynomials over Real, the corresponding condition will be
complicated.

Anyone here dealt with constructive methods for arbitrary real numbers?
(the Coq users mentioned some library).

I wonder of how many nice algorithms are known for real numbers, whether
they are interesting so that it could be worthy to lift the ≟
requirement.

Thanks,

------
Sergei

[Sergei Meshveliani]

Still I am not sure about Field for Real, because the instance for _≈_
occurs rather complicated. I do not know the subject, but I suspect that
thif Field for Real is possible.

------
Sergei

Post by Sergei Meshveliani
People,
My DoCon-A library currently requires DecSetoid as a base for all the
computer algebra.
But I think about making _≟_ optional.
Because I think, for example, that a Real number can be reasonably
represented as a certain sequence of embedded seqments, so that it will
be possible to prove in Agda that Real has the instances of
CommutativeRing and Field. But equality will not be solvable there.
(only I mean a real Real, do not confuse with floating point).
However I expect that most known algorithms will require various
complicated additional witness arguments to be correct for the case of
real numbers.
For example, for univariate polynomials over Rational coefficients it is
easy to resolve the divisibility relation.
And for Real coefficients, resolving the relation
(x + c) divides (x^2 + a*x + b) (1)
is equivalent to resolving
b - (a-c)*c ≈ 0 (2)
-- a witness for (1) is reduced to a witness for (2).
For arbitrary polynomials over Real, the corresponding condition will be
complicated.
Anyone here dealt with constructive methods for arbitrary real numbers?
(the Coq users mentioned some library).
I wonder of how many nice algorithms are known for real numbers, whether
they are interesting so that it could be worthy to lift the ≟
requirement.
Thanks,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Martin Escardo]

Post by Sergei Meshveliani
I wonder of how many nice algorithms are known for real numbers, whether
they are interesting so that it could be worthy to lift the ≟
requirement.

There is a huge literature on constructive analysis. You may with to
start with Bishop's Founctions of Constructive Analysis, and Bishop and
Bridges' Constructive Analysis.

Bishop works with setoids, and in particular with a setoid of real
numbers along the lines you describe in your message.


Fred Richman has many interesting papers on constructive analysis, most
of them available on his web page. But he doesn't work with setoids. If
I were to try to formalize his work, I would use univalent type theory
rather than setoids.

As I said, many authors have worked on this vast subject.

Best,
Martin

[Martin Escardo]

Too many typos, sorry. Here we go again more carefully.


There is a huge literature on constructive analysis. You may wish to
start with Bishop's Foundations of Constructive Analysis, and Bishop and
Bridges' Constructive Analysis.

Bishop works with setoids, and in particular with a setoid of real
numbers along the lines you describe in your message.

Fred Richman has many interesting papers on constructive analysis, most
of them available on his web page. But he doesn't work with setoids. If
I were to try to formalize his work, I would use univalent type theory
rather than setoids.

As I said, many authors have worked on this vast subject.

Best,
Martin

Post by Martin Escardo

Post by Sergei Meshveliani
I wonder of how many nice algorithms are known for real numbers, whether
they are interesting so that it could be worthy to lift the ≟
requirement.

There is a huge literature on constructive analysis. You may with to
start with Bishop's Founctions of Constructive Analysis, and Bishop and
Bridges' Constructive Analysis.
Bishop works with setoids, and in particular with a setoid of real
numbers along the lines you describe in your message.
Fred Richman has many interesting papers on constructive analysis, most
of them available on his web page. But he doesn't work with setoids. If
I were to try to formalize his work, I would use univalent type theory
rather than setoids.
As I said, many authors have worked on this vast subject.
Best,
Martin

[Bas Spitters]

We've developed a substantial library for constructive analysis in Coq.
Here's an list of related publications:
http://corn.cs.ru.nl/pub.html

Please let me know it you have any questions.

I agree with Martin, I would also like to UF for this. Perhaps cubical
agda will make this possible!
https://hott-uf.github.io/2017/abstracts/cubicalagda.pdf

Best,

Bas

Post by Sergei Meshveliani
I wonder of how many nice algorithms are known for real numbers, whether
they are interesting so that it could be worthy to lift the ≟
requirement.

There is a huge literature on constructive analysis. You may with to start
with Bishop's Founctions of Constructive Analysis, and Bishop and Bridges'
Constructive Analysis.
Bishop works with setoids, and in particular with a setoid of real numbers
along the lines you describe in your message.
Fred Richman has many interesting papers on constructive analysis, most of
them available on his web page. But he doesn't work with setoids. If I were
to try to formalize his work, I would use univalent type theory rather than
setoids.
As I said, many authors have worked on this vast subject.
Best,
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda