## Stream: Coq users

### Topic: `reflect` Type of ssreflect

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

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

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

#### Meven Lennon-Bertrand (Jan 04 2024 at 11:14):

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

#### 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? :)

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

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

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

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

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