The Coq mailing list

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

Timers also don't accept constructive reals.

After extraction (compilation) to Haskell, `robotPureProgram` is used in another Haskell program (a.k.a. shim) that passes the `delay` value to something like threadDelay.

So, it needs to be not just a rational, but a microsecond value, i.e. a rational of the form $\frac{...}{1000000}$

Again, that `delay` value depends on user input at runtime; it is not known at statically.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Sep 30, 2015 at 3:52 AM, Guillaume Brunerie <guillaume.brunerie AT gmail.com> wrote:

On 2015-09-29 23:39 GMT+02:00 Abhishek Anand
<abhishek.anand.iitg AT gmail.com> wrote:
>>
>> 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.

Thanks!
But is there a reason for doing the approximation in this function
instead of even later?
Could you instead have robotPureProgram return something of type  list
(R × Polar2D Q), have the `delay' field in `Message` be a real number
instead of a rational number, and then do the approximation only when
sending an actual command to the robot? I guess you can’t send to the
robot a real with free variables,

Best,
Guillaume

> 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
>> >>          >
>> >>
>> >>
>> >>
>> >
>
>