Ignat Insarov (Jun 21 2021 at 13:55): 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 ℕ).
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):Glad you asked, because that brings me to the other thing I had in mind. See:
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})".
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?
Théo Winterhalter (Jun 21 2021 at 19:51):Have you read what the reference manual has to say about it? https://coq.inria.fr/refman/addendum/program.html
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: Apr 20 2024 at 06:02 UTC