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?

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.

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

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

Meven Lennon-Bertrand said:

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

Is it constructive or (only) classical? :)

Thanks. I was worried that there was something more to `reflect`

. More than establishing a relation between Prop and computation worlds.

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.

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.

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.

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