The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Thank you all for the answers!

On Sat, Sep 26, 2015 at 12:20 AM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> 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 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> 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> 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> 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
>