[Agda] decidable equality in algebra

[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



On Thu, 2017-10-05 at 21:58 +0300, Sergei Meshveliani wrote:
> 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
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda