## Stream: Coq users

### Topic: How does the `Program` stuff work?

#### Ignat Insarov (Jun 21 2021 at 13:55):

Example:

``````Program Example example₁: {n: ℕ | n < 3} := (2: ℕ).
Next Obligation. simpl. auto. Defined.

Program Example example₂: gset ℕ := singleton 1.

Program Example example₃: gset {n: ℕ | n < 3} := (singleton 1: gset ℕ).
``````
• The first definition shows that the types on the left and on the right do not have to coincide.
• The second definition shows that I can use `singleton` to define a set.

But now I want to combine these two features and I receive an unsurprizing error: `cannot unify "ℕ" and "{n : ℕ | n < 3}"`.

How is it supposed to work? How can I make it work?

My first theory was that the type on the right should be like the type on the left but with some propositions omitted. Unfortunately the last example tells me that it is not that simple.

#### Ignat Insarov (Jun 21 2021 at 13:59):

_(What I would like to happen is for an obligation to show `1 < 3` to appear, as in example 1.)_

#### Ignat Insarov (Jun 21 2021 at 14:06):

The value that I want to construct can be constructed like this:

``````Program Example example₃: gset {n: ℕ | n < 3}.
refine (singleton ?[Σ]). refine (2 ↾ ?[proof]). auto. Defined.
``````

— So it type checks, it is not broken.

#### Li-yao (Jun 21 2021 at 17:34):

Does removing the `gset nat` signature in the RHS help? The type signature requires `gset nat` to unify with `gset {n | n < 3}`; inserting a conversion `gset nat -> gset {n | n < 3}` would require knowledge that `gset` is a functor, which is way beyond what `Program` is made for. What's more reasonable is to expect the unification to happen at the argument, because `nat` can be converted to `{n | n < 3}` by just inserting a pair constructor `exist 1 _` and generating an obligation.

#### Ignat Insarov (Jun 21 2021 at 19:36):

``````Program Example example₃: gset {n: ℕ | n < 3} := singleton 1.
``````
``````Error: Cannot infer the implicit parameter Singleton of singleton whose type
is "Singleton ℕ (gset {n : ℕ | n < 3})" (no type class instance found).
``````

And then this of course does not work either, because type mismatch:

``````Program Example example₃: gset {n: ℕ | n < 3} := @singleton ℕ (gset {n: ℕ | n < 3}) (gset_singleton 1).
``````
``````The term "gset_singleton 1" has type "gset ℕ"
while it is expected to have type "Singleton ℕ (gset {n : ℕ | n < 3})".
``````

#### Ignat Insarov (Jun 21 2021 at 19:40):

So, either I need to figure out how to help this instance resolve, or it actually cannot get resolved because `Program` does not do anything.

#### Ignat Insarov (Jun 21 2021 at 19:40):

And if `Program` does not do anything then how is it supposed to work?

#### Ignat Insarov (Jun 21 2021 at 19:51):

I tried… it does not make much sense to me yet.

#### Ignat Insarov (Jun 21 2021 at 19:52):

Seeing that it is a reference, it is not supposed to explain anything, and truly it hardly ever does.

#### Ignat Insarov (Jun 21 2021 at 19:53):

Is there any particular subsection I should pay special attention to?

#### Théo Winterhalter (Jun 21 2021 at 19:57):

To be honest, I wasn't even aware `Program` had special support for subset types, I mainly see `Program` as a way to generate obligations out of holes in a definition, with some handy automation.
It is also my understanding that `Equations` (http://mattam82.github.io/Coq-Equations/) should eventually replace it, and I now only ever use it rahter than `Program`.

#### Ignat Insarov (Jun 21 2021 at 19:58):

So Théo, can you help me understand how to make holes in definitions, on the example above?

#### Ignat Insarov (Jun 21 2021 at 19:58):

I tried this and that but I cannot put it together yet.

#### Théo Winterhalter (Jun 21 2021 at 20:00):

Basically I would use the constructor for the type singleton using `_` where the proof would need to go, it will then be asked as an obligation.

#### Ignat Insarov (Jun 21 2021 at 20:03):

Oh, nice!

This does not work:

``````Example example₃: gset {n: ℕ | n < 3} := singleton ( 1 ↾ _ ).
``````

But this does:

``````Program Example example₃: gset {n: ℕ | n < 3} := singleton ( 1 ↾ _ ).
``````

I can live with that!

#### Ignat Insarov (Jun 21 2021 at 20:05):

I am looking at `Equations` too, but I understand it is not yet officially a part of Coq… Should I wield it nevertheless?

#### Ignat Insarov (Jun 21 2021 at 20:05):

I mean, should I treat it as a standard library?

#### Théo Winterhalter (Jun 21 2021 at 20:06):

No it's not standard library, but it's also maintained by Matthieu Sozeau (who also did `Program`) and he works actively on it.

#### Ignat Insarov (Jun 21 2021 at 22:31):

Why did no one tell me about these underscores before… This is exactly what I wanted all this time! Works great!

Last updated: Jun 20 2024 at 13:02 UTC