The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Is that enough? Are there applications where we do need an
approximation function of type R -> Q available inside the type theory
or is it enough to be able to compute all approximations of any real
number, as long as we are in the empty context?

In my application, I *need to* approximate reals with free vars (in non-empty contexts).

Consider the function `robotPureProgam` in page 10 of the paper:

http://www.cs.cornell.edu/~aa755/ROSCoq/ROSCOQ.pdf

The variable `target` is *not* known in advance and comes from the user of the robot at runtime.

If it helps, here are the slides from a talk about the paper:

http://www.cs.cornell.edu/~aa755/ROSCoq/ITP.pdf

Please let me know if I misunderstood the question.

Below, I express some possibly misleading personal opinion:

The CoRN library[1] has reasonably convinced me that if the "Proper" instances for rewriting are declared properly, 

working with unquotiented reals can be a breeze. 

Only a few times I had some minor trouble in rewriting at the denominator of division, because the division operator also takes a proof of non-negativity of the denominator.

[1] : http://corn.cs.ru.nl/

 

> Best,
> Neel
>
>
> PS. Andrej Bauer has told me that this is essentially what people
> working in Weihrauch's Type Two Effectivity do, but you would need to
> ask him for details.
>
> [*] There are technical issues to do with needing negative digits to
> implement all the operations (such as addition and multiplications)
> using Cauchy sequences, but the solutions are known and so we can
> neglect them in this email.
>
> On 25/09/15 22:20, Abhishek Anand wrote:
>>
>> I totally agree with Arnaud's point about reals.
>> I just want to emphasize the importance of the ability to get rational
>> approximations of (constructive) reals.
>>
>> I have been using constructive reals for writing certified Coq programs
>> for robots [1] and actually running them on actual robots.
>> Unlike floating points, at most places I don't have to worry about
>> inexactness. For example, field laws hold exactly, and sin^2 x + cos^2 x
>> is /exactly/ equal to 1.
>> However, in the end when all the computation is done, and it is time to
>> send some commands to hardware, such as timers, or motor drivers, I
>> cannot send them constructive reals.
>> Instead, I /have to approximate them to a sufficiently simple rational/,
>> e.g. a timer accepts a millisecond value, and iRobot Create
>> <http://www.irobot.com/About-iRobot/STEM/Create-2.aspx> accepts an 8-bit
>> value representing the requested speed for its motors.
>>
>> [1] Abhishek Anand and Ross Knepper. “ROSCoq: Robots powered by
>> constructive reals”. In: ITP. Aug.
>> 2015. https://github.com/aa755/ROSCoq.
>>
>>
>>
>> -- Abhishek
>> http://www.cs.cornell.edu/~aa755/
>>
>> On Fri, Sep 25, 2015 at 2:19 PM, Arnaud Spiwack
>> <aspiwack AT lix.polytechnique.fr <mailto:aspiwack AT lix.polytechnique.fr>>
>>
>> wrote:
>>
>>     There is a lot to say about the type theory of setoids. I'll attempt
>>     to share some of my thought on it.
>>
>>     As Neel said already, OTT is such a theory. It does not have a very
>>     good story for universes, though, univalence can be seen as a way to
>>     address this particular issue.
>>
>>     Another difficulty is how to treat quotient types. I don't remember
>>     very well how they are handled in OTT, though I remember they were
>>     pretty convincing. Though they can be seen as a generalisation of
>>     quotients, higher inductive types are really a rather different
>>     angle on this question (though I may be wrong).
>>
>>     Setoids serve two purposes: adding some extensionality, and adding
>>     quotients to the theory of Coq. Both are rather tricky balancing
>>     games when you want to preserve the computational behaviour of Coq
>>     (if you don't care about computation, you can just posit
>>     extensionality and axiomatise quotient types, there are probably
>>     pitfalls in the case of quotient types, though, has someone looked
>>     into it?).
>>
>>     There are two things which I'd consider limits of this approach,
>>     however. First you would probably need a setoid rewriting thing in
>>     the tactics nonetheless: it handles more than setoids (like
>>     ordering) and it is useful for simplification by rewriting (just
>>     using `repeat rewrite` is terrible for your perfs). The second is
>>     that there are things which are doubtful when expressed as quotient
>>     types, like the real numbers: real numbers can be seen as a quotient
>>     of, say, function from the natural numbers to the rational
>>     (returning an approximation up to 2⁻ⁿ). But if you do so, there is
>>     no way, in the theory of setoids, to extract an approximation of a
>>     real, as it's not a function which respects the quotient equality.
>>     So there are extra complications there (maybe a type a functions
>>     which are explicitly not equality preserving, but it's not really
>>     easy to use).
>>
>>     Of course, there is much unnecessary tedium associated with proofs
>>     with setoids, and here's to hoping a solution is found some day. But
>>     as you see: it's not easy.
>>
>>
>>     On 25 September 2015 at 18:52, Gabriel Scherer
>>     <gabriel.scherer AT gmail.com <mailto:gabriel.scherer AT gmail.com>> wrote:
>>
>>         You may be interested in Marc Lasson's paramcoq plugin, which
>>         generates parametricity witnesses from Coq terms. (So it's not
>>         trying
>>         to internalize the fact that terms respect
>>         equality/parametricity, but
>>         rather make the meta-theorem available in practice as a
>>         meta-programming tool.)
>>
>>         https://github.com/mlasson/paramcoq
>>
>>         On Fri, Sep 25, 2015 at 4:37 PM, Neelakantan Krishnaswami
>>         <n.krishnaswami AT cs.bham.ac.uk
>>         <mailto:n.krishnaswami AT cs.bham.ac.uk>> wrote:
>>          > On 25/09/15 13:35, Ilmārs Cīrulis wrote:
>>          >>
>>          >> I often have to use Equivalence and Proper (while tinkering
>>         around),
>>          >> therefore a question appeared:
>>          >>
>>          >> What about Coq (or any other proof assistant / type theory)
>>         where
>>          >> setoids and morphisms are first class citizens (built in,
>>         replacing
>>          >> standard Type and function that becomes something like lower
>>         level of
>>          >> language). In such case there would be no need of special
>>         libraries for
>>          >> Equivalence, Setoid and related libraries for, e.g., lists
>>         or other data
>>          >> structures that respects equivalence.
>>          >>
>>          >> What are cons of such idea?
>>          >
>>          >
>>          > This is essentially the idea behind Observational Type
>>         Theory; you
>>          > should look at:
>>          >
>>          > * Extensional Equality in Intensional Type Theory. T.
>> Altenkirch
>>          >   LICS 1999
>>          > * Observational equality, now! T. Altenkirch, C. McBride, W.
>>         Swierstra,
>>          >   PLPV 2007
>>          >
>>          > The core idea (every type is a setoid and every definable
>>         term is a
>>          > equality-respecting morphism) is very simple, but making all
>>         the syntax
>>          > line up to make it work is tricky and intricate.
>>          >
>>          > Best,
>>          > Neel
>>          >
>>
>>
>>
>