Stream: Coq users

Topic: `reflect` Type of ssreflect


view this post on Zulip Julin Shaji (Jan 04 2024 at 06:43):

Hi.

I was trying to understand views of ssreflect.

The reflect P b is a type saying that a proposition P and a boolean b are 'equivalent', right?

Is the reason for having such a relation that we can use the two of the interchangeably?
For proofs, Props are easier so we can rewrite bool with equivalent prop or something like that?

view this post on Zulip Meven Lennon-Bertrand (Jan 04 2024 at 09:32):

Yes, this is more or less the idea. In general, booleans are nice because they compute, for instance true || p simplifies to p by computation, while it is easier to manipulate the structure of propositions, for instance if you have a hypothesis P /\ Q you can destruct it into a proof of P and a proof of Q.

The whole idea of ssreflect is to use the reflect predicate and views to navigate easily between the two equivalent formulations of the same predicate, so that you can use both advantages at the same time. The name ssreflect (for small scale reflection) comes from this. Reflection is the idea to use Coq's computation to decide certain propositions, by turning them into booleans which we can compute to true or false, telling us whether the propositions holds or not. The small scale aspect is the idea that even if we do not compute all the way to true or false, boolean computation can still give some nice little simplification steps.

view this post on Zulip Julio Di Egidio (Jan 04 2024 at 09:37):

To complement what @Meven Lennon-Bertrand has just said, here are a couple of places where reflection is explained in Software Foundations / Logical Foundations:

A first quick encounter:
https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html#lab215

Here the notion is expanded and then applied:
https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html#lab262

view this post on Zulip Meven Lennon-Bertrand (Jan 04 2024 at 11:14):

You might also be interested in having a look at the Mathematical Components book.

view this post on Zulip Julio Di Egidio (Jan 04 2024 at 11:16):

Meven Lennon-Bertrand said:

You might also be interested in having a look at the Mathematical Components book.

Is it constructive or (only) classical? :)

view this post on Zulip Julin Shaji (Jan 04 2024 at 11:34):

Thanks. I was worried that there was something more to reflect. More than establishing a relation between Prop and computation worlds.

view this post on Zulip Julin Shaji (Jan 04 2024 at 11:36):

Are structures in mathcomp more aligned towards Prop-world kind of things?
I once tried extracting a \matrix and it was too big. Full of ordinal and stuff.

view this post on Zulip Julin Shaji (Jan 04 2024 at 11:38):

I was aiming at having a matrix multiplication (computable) operation verified and extracted out to ocaml.
Saw a suggestion to look into coqEAL, but I didn't figure how that was done finally.

I had tried going from \matrix to list (list A) at the time. I guess it should've been the other way around. Refining from abstract to more concrete.

view this post on Zulip Meven Lennon-Bertrand (Jan 04 2024 at 12:45):

Julio Di Egidio said:

Is it constructive or (only) classical? :)

The whole Mathematical Components library (and the proof of the odd-order theorem!) is completely axiom-free. Only the matcomp-analysis extension heavily uses excluded middle.

view this post on Zulip Meven Lennon-Bertrand (Jan 04 2024 at 12:49):

Julin Shaji said:

Are structures in mathcomp more aligned towards Prop-world kind of things?
I once tried extracting a \matrix and it was too big. Full of ordinal and stuff.

Maybe more expert people can comment, but afaik structures are oriented towards small-scale computation, in Coq. That is, there are primarily adapted for proofs and propositions, rather than yielding "reasonable" extracted code, yet they should in general support the "simplification-through-computation" pattern. Note that this is different from "large scale" reflection, ie full-blown execution. The whole goal of CoqEAL is to relate such representations to ones adapted to extraction to efficient implementation, for instance relating unary to binary natural numbers.


Last updated: Jun 23 2024 at 04:03 UTC