The Coq mailing list

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

More generally, in "type theory" (at least in Coq), to be able to reason about something, it must be well typed (AFAIK).

So, if one insists that there be no well-typed approximation function, I don't see how one will be  able to reason about a large class of useful functions which need to perform such approximations.

I have to not only run the robotic programs, but also to reason about them, e.g. prove safety or liveness properties.

The robot application is just one among several ones. 

I think we should have a Matlab/Mathematica based on constructive reals, and proved correct at least to some extent.

I think the authors of the article below would love it:

http://www.ams.org/notices/201410/rnoti-p1249.pdf (the section preceeding "Conclusions" has examples involving real numbers.)

Neel's solution seems very plausible. But I think that entering a monad can complicate the reasoning, and can potentially more than offset the advantages (if any) of quotiented reals.

-- Abhishek

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

On Thu, Oct 1, 2015 at 5:38 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

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