Stream: MetaCoq

Topic: imported from gitter room coq/metacoq


view this post on Zulip Gregory Malecha (Sep 26 2019 at 02:47):

is there a way to generate an opaque definition from the template monad?

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 09:10):

I thought so

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 09:11):

I don't think so. I had a "implement tmOpaque command" on my todo-list for a while, but forgot about it. That would probably be the most flexible to use

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 09:18):

But Opaque is not the same as Qeded definitions

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 09:18):

Adding a boolean also to tmDefinition shouldn't be hard

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 09:18):

Yes, that should also work. Qeding things after defining them is impossible?

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 09:19):

Yes

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 09:19):

Opaque only says "expand only at last resort"

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 09:19):

It preserves subject reduction to do it this way

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 09:22):

Is there a way to tell Program not to use typeclass inference to close obligations? Even if I set Global Obligation Tactic := idtac. inferrable goals are closed

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 09:22):

If so there's a (very hacky) way to obtain opaque definitions already

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 09:23):

There's no way up-to 8.10, will be possible in 8.11

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 09:24):

Then it's probably quickest to add a boolean to tmDefinitionRed (and set it to false by default for tmDefinition)

view this post on Zulip Gregory Malecha (Sep 26 2019 at 11:11):

Thanks. I'll make an issue and can probably implement it. Just FYI, my use case is to implement sealing: http://GitHub.com/gmalecha/coq-seal

view this post on Zulip Gregory Malecha (Sep 26 2019 at 12:21):

What is the current status of the branches? E.g. 8.8 vs 8.9? It looks like 8.8 is still the main branch, but I need my feature on 8.9

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 12:23):

Copy pasting from the Slack chat from15 minutes ago: Yannick Forster [2:06 PM] What do we want to do about the 8.9 branch? I tried naively merging in 8.8, but that fails (in PCUICSafeConversion.v) Matthieu Sozeau [2:08 PM] I'll give it a try

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 12:23):

So ideally we'll have an opam relase for 8.8 and 8.9 with synced branches ready this afternoon

view this post on Zulip Gregory Malecha (Sep 26 2019 at 12:31):

Ok. Thanks. Are we using both slack and gitter?

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 12:33):

We are used to coordinating the "Coq Coq Correct" paper draft over slack, so stuff like this is discussed there occasionally as well. I think it's essentially undecided which channel we should use for public discussions :)

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 13:33):

I think gitter is simpler given that Coq is already here (and not sure slack can be used easily by others)

view this post on Zulip Théo Winterhalter (Sep 26 2019 at 13:33):

Why can't it be used easily?

view this post on Zulip Gregory Malecha (Sep 26 2019 at 13:36):

since i'm already in the code, i'm wondering if it makes sense to also expose Local

view this post on Zulip Gregory Malecha (Sep 26 2019 at 13:36):

but there are three options

type internal_flag =
  | UserAutomaticRequest
  | InternalTacticRequest
  | UserIndividualRequest

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 13:37):

Exposing all options that are avaible in interactive mode for definitions, lemmas and axioms makes probably sense

view this post on Zulip Gregory Malecha (Sep 26 2019 at 13:37):

Do you know the meaning of these three values?

view this post on Zulip Gregory Malecha (Sep 26 2019 at 13:38):

i.e. what effect they on the system?

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 13:39):

(** flag for internal message display *)
type internal_flag =
  | UserAutomaticRequest (* kernel action, a message is displayed *)
  | InternalTacticRequest  (* kernel action, no message is displayed *)
| UserIndividualRequest (* user action, a message is displayed *)```

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 13:39):

I found this more commented version

view this post on Zulip Yannick Forster (Gitter import) (Sep 26 2019 at 13:39):

But I still don't know what it means

view this post on Zulip Gregory Malecha (Sep 26 2019 at 13:40):

so maybe this isn't actually locality

view this post on Zulip Gregory Malecha (Sep 26 2019 at 13:40):

maybe this is just something about displaying messages

view this post on Zulip Gregory Malecha (Sep 26 2019 at 13:41):

oh, i think it is import_status

view this post on Zulip Gregory Malecha (Sep 26 2019 at 13:41):

type import_status = ImportDefaultBehavior | ImportNeedQualified

type locality = Discharge | Global of import_status

view this post on Zulip Gregory Malecha (Sep 26 2019 at 13:42):

not sure what Discharge is, but the other two make sense

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 14:12):

internal_flag is just about printing "foo is defined" or not indeed

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 14:12):

Not super useful

view this post on Zulip Gregory Malecha (Sep 26 2019 at 14:13):

but the locality is what we want, right?

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 14:13):

Discharge is the meaning of NOT Local in a section

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 14:13):

(I guess)

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 14:13):

The Import status could be useful as well

view this post on Zulip Gregory Malecha (Sep 26 2019 at 14:13):

should i expose all of them?

view this post on Zulip Gregory Malecha (Sep 26 2019 at 14:13):

locality contains import_status

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 14:14):

Yep

view this post on Zulip Gregory Malecha (Sep 26 2019 at 14:14):

it seems like this interface may have changed because 8.9 seems to just have Global and Local as locality

view this post on Zulip Gregory Malecha (Sep 26 2019 at 14:14):

but coq trunk has the definitions above

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 14:15):

Yep

view this post on Zulip Gregory Malecha (Sep 26 2019 at 14:15):

so in older versions, should i translate Discharge to Global?

view this post on Zulip Matthieu Sozeau (Sep 26 2019 at 14:15):

Yes, I believe so

view this post on Zulip Gregory Malecha (Sep 26 2019 at 17:23):

my co-worker running manjaro ran into an error running make in the template-coq directory

view this post on Zulip Gregory Malecha (Sep 26 2019 at 17:24):

the sed command wasn't working

view this post on Zulip Gregory Malecha (Sep 26 2019 at 17:24):

i.e. it wasn't running

view this post on Zulip Gregory Malecha (Sep 26 2019 at 17:55):

is there a story around universes yet?

view this post on Zulip Gregory Malecha (Sep 26 2019 at 17:55):

at least universes and the template-monad

view this post on Zulip Gregory Malecha (Sep 26 2019 at 17:57):

Error: Illegal application:
The term "@eq_refl" of type "forall (A : Type@{Coq.Init.Logic.8}) (x : A), x = x"
cannot be applied to the terms
 "forall T : Type@{Top.10}, T -> T" : "Type@{Top.10+1}"
 "fun (T : Type@{Top.10}) (x : T) => x" : "forall T : Type@{Top.10}, T -> T"
The 1st term has type "Type@{Top.10+1}" which should be coercible to
 "Type@{Coq.Init.Logic.8}".

view this post on Zulip Gregory Malecha (Sep 26 2019 at 17:57):

it looks like i need to add a constraint to the checker to accept this

view this post on Zulip Gregory Malecha (Sep 26 2019 at 17:58):

but i'm not certain how to do it

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 09:07):

@Gregory Malecha, did he configure.sh local at the root?

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 10:32):

Shall we just reset the counters and call the alpha release of metacoq 1.0alpha ?

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 10:32):

@/all ?

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 10:33):

Sounds good

view this post on Zulip Théo Winterhalter (Sep 27 2019 at 11:17):

Good to me. We can since it was template-coq before.

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 11:17):

Yep, no conflict really

view this post on Zulip Théo Winterhalter (Sep 27 2019 at 11:18):

After the release are we moving from coq8-8 to coq8-9 for good?
To know in which branch to start making new changes.

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 11:19):

I guess we can switch to 8.9 and backport to 8.8 instead of forward-port indeed

view this post on Zulip Théo Winterhalter (Sep 27 2019 at 11:19):

We need one last forward port then, right?

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 11:19):

Yes

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 11:56):

What's the status of the forward-port? I tried yesterday, but there was the issue with st_ in PCUICSafeChecker.v

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 12:04):

Didn't try yet. I'll give it a go before making the alpha releases in case things need to change in 8.8 somehow

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 12:05):

Looks like the dev package's CI might not finish in time because it doesn't realise it's reinstalling the same packages many times https://gitlab.com/coq/opam-coq-archive/-/jobs/305834732

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 12:24):

@Gregory Malecha if he's on macos he should install gnu sed

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 12:25):

We should be more robust though and have our own wrapper around whichever sed is available

view this post on Zulip Gregory Malecha (Sep 27 2019 at 12:29):

I can check with him. We got it working by manually running the sed script for the plug-in.

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 13:13):

@Yannick Forster I got the forward port working, release is in sight :)

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 13:16):

:fireworks:

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 13:17):

You adapted the announcement, right? Will you post it on Coq club/ discourse once the PR is merged?

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 13:22):

Yep

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 13:27):

Weird, the most recent run of the PR fails for 4.05.0

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 13:30):

You mean this https://gitlab.com/coq/opam-coq-archive/-/jobs/305834732 ?

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 13:30):

It's just out of time, because it tries to install each package individually

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 13:30):

By starting from nothing again each time

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 13:30):

Oh I see

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 13:31):

The merges seem to be working well https://travis-ci.org/MetaCoq/metacoq/branches

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 13:57):

If I load https://metacoq.github.io/metacoq/ in a browser the name of the tab still is "TemplateCoq"

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 13:57):

Ah thanks, I've seen that yesterday and forgotten

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 13:58):

I would suggest that we move up installation through opam to the top of the installation section, maybe even move installation from sources to a dedicated INSTALLATION.md file

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 13:59):

And maybe mention example_erasure and example_checker in how to use?

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 13:59):

Oh, the whole How to Use section is not adapted to MetaCoq yet

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 14:09):

Right, I'm working on it now

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 15:05):

I've been wondering whether we can implement a tWildcard feature for tmUnquote and tmUnquoteTyped. Sometimes it's annoying that you have to write out types when doing a definition in a metaprogram which could easily be inferred if you'd give the definition in Coq directly

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 15:06):

One option could be to extend the definition of terms, but that sounds wrong. An alternative might be to define an opaque constant tWildcard : term (as `tVar "_" for instance) and adapt the unquoting function in ocaml for at least the non-extractable monad to treat it like a wildcard would be treated

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 15:07):

@Gregory Malecha did you maybe encounter use cases for such a feature as well?

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:08):

A tEvar would be fine no?

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:08):

With some way to say it should be inferred

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 15:08):

I'm not sure, what happens when unquoting evars?

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:09):

Today, not much :)

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 15:10):

But yes, if unquoting would just try to infer evars instead of failing when encountering one that would solve the problem in an even nicer way

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 15:11):

Because you might be able to use the same evar twice to enforce that the same type is inferred

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:26):

Yup

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:26):

Almost there with opam packages for 8.9 :)

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:27):

What do you guys think of the latest https://metacoq.github.io/metacoq/ ?

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 15:32):

Just taking notes while reading:

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 15:33):

I can fix them myself if you tell me what you think about the ones phrased as questions

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:41):

I'm on it. The build for master always fails, that's ok.

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:44):

I'd rather leave the MetaCoq Check alone, it's fixed to 65536

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:45):

What do you mean by the partial Coq -> LC translation?

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:45):

The doc is the full .v files

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:45):

(without proof scripts)

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 15:53):

And the announcement https://gist.github.com/mattam82/765f193046320fb5acf3d4e2d641e6fd

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 16:03):

I fixed the typos and added the missing links to safechecker_test and erasure_test

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 16:07):

By the partial translation I mean the extraction to lambda calculus by me and Fabian covered in section 4.3 of the MetaCoq paper

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 16:08):

Ah right! What's the link?

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 16:08):

I like the announcement as it is, the "A good place to start" sentence just moved up into the itemize, which it probable shouldn't

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 16:09):

A static link that should not break is https://github.com/uds-psl/certifying-extraction-with-time-bounds/blob/master/Tactics/Extract.v, or https://github.com/uds-psl/certifying-extraction-with-time-bounds/blob/master/Tactics/Extract.v

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 16:12):

Where should I put this?

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 16:14):

The paper should also be linked I think

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 16:18):

I think both fit in the Papers section

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 16:18):

And I should put Fabian in the team :)

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 16:23):

Or maybe not, given he's had 0 commits in

view this post on Zulip Yannick Forster (Gitter import) (Sep 27 2019 at 16:29):

I thought about it, I would suggest that we simply add the paper to the papers section (we could split into "On MetaCoq" and "Using MetaCoq" if we want), and then use https://github.com/uds-psl/certifying-extraction-with-time-bounds as link

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 16:30):

I added a link to the paper directly and the example, people can find their way I guess :)

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 16:34):

So, 8.9 opam packages work too, only remains to push them as a PR on the Coq repo, and wait 3 hours :)

view this post on Zulip Gregory Malecha (Sep 27 2019 at 17:07):

@Yannick Forster regarding wildcards. They would be awesome to support! But I think that care about be taken. I would personally prefer a new type to an opaque constant, and I would expose a monadic operation `tmElaborate : pre_term -> term. This also makes it possible to implement some forms of elaboration in the monad.

view this post on Zulip Gregory Malecha (Sep 27 2019 at 17:09):

The connection with tEvar is interesting, it seems like they should be the same...so maybe there is something slightly off about the current setup? Maybe term represents pre_term and there is a subset type that represents real terms.

view this post on Zulip Gregory Malecha (Sep 27 2019 at 17:10):

That said, I don't think enough information is persisted in terms to reconstruct everything about evars.

view this post on Zulip Théo Winterhalter (Sep 27 2019 at 17:15):

@Matthieu Sozeau The new webpage is pretty good. :)

view this post on Zulip Gregory Malecha (Sep 27 2019 at 17:18):

After looking, it looks like tEVar has enough information, we might not need to add anything.

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 17:19):

Damn I used curl http:?/ | sha256sum which sums the http request stuff, have to copy the fixed hash again everywhere :/ Hopefully we can use opam-publish in the future

view this post on Zulip Gregory Malecha (Sep 27 2019 at 17:22):

The webpage looks great!

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 17:50):

Ok, finally done with this :) Let's hope these two go and I can have a good week-end! https://github.com/coq/opam-coq-archive/pulls

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 17:53):

Regarding tEvar we could associate arbitrary things to them, so I think they could be the right interface. Indeed right now we represent pre-terms (in the sense of econstr), but without the support of an evar-map (that will come though)

view this post on Zulip Matthieu Sozeau (Sep 27 2019 at 17:54):

At some point we might even have fun writting an elaborator purely in MetaCoq

view this post on Zulip Gregory Malecha (Sep 28 2019 at 01:50):

I think tEvar is the right interface. Do you have thoughts on how to handle the evar map though? In particular, i assume that every time that you run tmQuote you will get a fresh evar map

view this post on Zulip Gregory Malecha (Sep 30 2019 at 01:04):

could it be possible to use metacoq to construct a module inside a section (assuming that it is pre-"cooked", i.e. none of the definitions mention any section variables)

view this post on Zulip Théo Winterhalter (Sep 30 2019 at 07:24):

Well, as metacoq doesn’t handle modules or sections, I’m not sure. For each definition, putting it inside a section is just the identity if it doesn’t mentions tVars no?

view this post on Zulip Gregory Malecha (Sep 30 2019 at 11:32):

That's right. The top-level prevents you from opening a module at all within a section, but I was thinking that if we could simply generate the kernel object directly, we wouldn't need to worry about that. The reason that I'm wondering about this is because there is a more efficient representation of sealed functions using modules.

view this post on Zulip Matthieu Sozeau (Sep 30 2019 at 12:32):

With sections in the kernel it might become possible to implement test

view this post on Zulip Gregory Malecha (Sep 30 2019 at 13:39):

@Matthieu Sozeau is that comment to me?

view this post on Zulip Matthieu Sozeau (Sep 30 2019 at 14:36):

Yes, and the last word should have been « that »

view this post on Zulip Gregory Malecha (Sep 30 2019 at 16:58):

Ah, that makes sense.

view this post on Zulip Gregory Malecha (Sep 30 2019 at 16:59):

Maybe I should say "that" makes sense :grinning:

view this post on Zulip Matthieu Sozeau (Sep 30 2019 at 17:42):

Haha :)

view this post on Zulip Yannick Forster (Gitter import) (Oct 07 2019 at 15:33):

I just found myself writing "The command is implemented in MetaCoq (which explains the Run TemplateProgram prefix)" and took this as a hint to rethink wether "Run TemplateProgram" is the most telling vernacular name possible. In line with MetaCoq Check, we might want to call it MetaCoq Run? (and rename Quote into MetaCoq Quote?) That way outsiders who find it in code have an idea where its coming from

view this post on Zulip Théo Winterhalter (Oct 07 2019 at 15:33):

I would not be against the idea.

view this post on Zulip Théo Winterhalter (Oct 07 2019 at 15:34):

And maybe rename Make.

view this post on Zulip Matthieu Sozeau (Oct 07 2019 at 15:34):

Indeed, that'd be more uniform

view this post on Zulip Yannick Forster (Gitter import) (Oct 07 2019 at 15:44):

I have to touch ML code tomorrow anyways, I'll file a pull request in case nobody objects until then

view this post on Zulip Jason Gross (Oct 08 2019 at 20:27):

I want to automate the following sequence of steps into a single command:

  1. given a list of names (say, of the form of a list (Prop -> Prop) whose elements are all fun name : Prop => name where I want to extract name) and the type of the eliminator/church encoding, emit an inductive declaration whose constructors have the given names and whose eliminator matches the given principle
  2. emit a definition of a given type by running an Ltac tactic (must not be via tactics-in-terms, because I need the names emitted by abstract to persist/not be inlined)
  3. emit a Strategy command, whose identifier list will be taken from the previously emitted definition (basically, the tactic constructs a record, each of the fields are constants hidden via transparent_abstract, and I need to emit Strategy -1000 for two of these)

Is this something I can automate with MetaCoq?

view this post on Zulip Théo Winterhalter (Oct 08 2019 at 20:58):

Hi, when you say names you mean identifiers? I don’t really understand what you’re trying to do. Since you have a list of identity functions I assume you want the name of the binder each time?
So as input you would take for instance [ fun O => O ; fun S => S ] and forall N, N -> (N -> N) -> N?
Why not just take forall (N : Type) (O : N) (S : N -> N), N?

Anyway, if the three can be done separately, then can probably be composed into one thing.
You cannot create vernacular commands from metacoq though, you’ll have to do some Run TemplateProgram.

view this post on Zulip Jason Gross (Oct 08 2019 at 20:59):

Sure, I could compose them and take the names just from the eliminator, that's a fine starting point. And having to do Run TemplateProgram seems fine.

view this post on Zulip Jason Gross (Oct 08 2019 at 21:00):

The question is if I can make a template program that emits an inductive, then calls an Ltac tactic to emit a definition, and then issues a Strategy command

view this post on Zulip Théo Winterhalter (Oct 08 2019 at 21:05):

Ok, so the first part I would say yes. I’m not sure about the Ltac tactic though. I mean, we can open an obligation and let the user input the tactic then. Or even set the tactic obligation to the one you want, but that’s not very nice if you use other things that generate obligations.
If the ltac tactic is simple enough, it can be written in metacoq instead maybe.

As for Strategy, as far as I know it’s not reified as of now. I suppose it could be added without too much effort.

view this post on Zulip Jason Gross (Oct 08 2019 at 21:09):

I don't suppose a template program can set the obligation tactic and then revert the setting after? (The tactic takes arguments, though, which include the names of the inductives just emitted... I'm not super-enthusiastic about porting the tactic code from Ltac to MetaCoq at the moment; it's currently 2200 loc and does a number of hacks with evars and partial instantiation across multiple goals to transmit information between them, and also relies on emitting constants at particular times for good performance, and running particular reduction strategies on terms in various places. It also calls an Ltac reification procedure in the middle of things.)

view this post on Zulip Matthieu Sozeau (Oct 08 2019 at 22:26):

Shouldn't be too hard to call an ltac, passing arguments to them is a headache though

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 06:40):

Yes I see, on what is the tactic run? Maybe it can be embedded in a different goal with extra information (with let bidings for instance that would just go away with simpl) so that the tactic can be called without arguments.

view this post on Zulip Théo Winterhalter (Oct 09 2019 at 06:40):

But otherwise, metacoq doesn’t allow you to change the obligation tactic either.

view this post on Zulip Jason Gross (Oct 09 2019 at 16:04):

Yes, I suppose I could embed the arguments in the goal structure as arguments to a definition that the tactic will then just unfold or something. So I could do it with a tactic that takes no arguments

view this post on Zulip Jason Gross (Oct 11 2019 at 06:21):

Would I be correct in assuming that Not_found anomalies in program definition (https://github.com/coq/coq/issues/10879) would also show up in trying to embed Ltac in MetaCoq?

view this post on Zulip Yannick Forster (Gitter import) (Oct 11 2019 at 07:31):

I think running Ltac is also possible by a combination of InferInstance and Hint Extern, ignoring obligations altogether. Passing arguments is also no issue I think. You could imagine a typeclass Class RunLtac (tactic_name : string) {argument_type : Type} (args : argument_type) (return_type : Type) := mk_RunLtac : return_type. together with hints of the form Hint Extern 0 (RunLtac "tac" ?a ?R) => tac a.

view this post on Zulip Yannick Forster (Gitter import) (Oct 11 2019 at 07:33):

We don't support Strategy right now, but there's also no reason why we shouldn't implement tmStrategy as a monadic operation, it should be essentially a copy-paste of the implementation of the Strategy vernacular

view this post on Zulip Matthieu Sozeau (Oct 11 2019 at 09:01):

Ha didn’t think of going though classes, nice hack!

view this post on Zulip Jason Gross (Oct 11 2019 at 15:42):

Unfortunately, typeclasses are subject to the same issues with Not_found, see https://github.com/coq/coq/issues/10879#issuecomment-541114794. Though if you add tmStrategy to a version of MetaCoq that works with 8.9/8.10, I will strongly consider switching from OCaml to MetaCoq for my automation here.

view this post on Zulip matrixbot (Gitter import) (Oct 11 2019 at 18:28):

pedroabreu What are the benefits to implement app with a list of arguments instead of only one argument and currying the result?

view this post on Zulip Matthieu Sozeau (Oct 12 2019 at 08:54):

It’s an implementation choice, to make heads of applications accessible in constant time and have a compact representation of argument lists. The PCUIC version of the language has standard binary apps

view this post on Zulip Matthieu Sozeau (Oct 12 2019 at 08:54):

(In OCaml, app takes an array rather than a list)

view this post on Zulip Yannick Forster (Gitter import) (Oct 23 2019 at 13:11):

I encountered a nice way of passing Coq-identifiers to commands instead of strings. I'm using it to implement lots of commands in a paper Kathrin Stark and I on a suggestion how to use modular syntax in Coq (http://www.ps.uni-saarland.de/Publications/documents/ForsterStark_2019_CoqALaCarte.pdf). Here's the trick:

view this post on Zulip Yannick Forster (Gitter import) (Oct 23 2019 at 13:12):

Require Import String.
From MetaCoq Require Import Template.All.
Export MonadNotation.

Definition getName (x : nat -> nat) :=
  x <- tmEval cbv x;;
  t <- tmQuote x ;; match t with tLambda (nNamed na) _ _ => ret na | _ => ret "" end.


Notation name_of n := (ltac:(let k x := exact x in run_template_program (getName (fun n : nat => 0)) k)).

Compute (name_of n).
     (* = "n" *)
     (* : string *)

view this post on Zulip Matthieu Sozeau (Oct 23 2019 at 13:22):

Cute, you might make Pierre-Marie cry if he sees this :smile:

view this post on Zulip Jason Gross (Oct 23 2019 at 18:28):

This seems like the same trick I use to pass identifiers from Ltac to OCaml in the plugin I wrote recently. Why do you need the cbv here?

view this post on Zulip Jason Gross (Oct 23 2019 at 18:42):

I'm also curious where you encountered it (and am trying to recall where I got it from ... I feel like after spending many hours struggling with bugs in fresh trying to write name-preserving reification to PHOAS, storing names in binders of dummy functions seemed like the obvious way to pass names between Ltac and Gallina?)

view this post on Zulip Jason Gross (Oct 23 2019 at 18:44):

Also, if you are interested in a confusing gotcha, I think if you replace cbv with vm_compute, your code will produce the wrong name in many cases.

view this post on Zulip Théo Winterhalter (Oct 23 2019 at 19:44):

This is just because vm_compute isn’t working directly with the coq ast and so the names aren’t preserved right?

view this post on Zulip Jason Gross (Oct 23 2019 at 19:45):

Yeah, the round-trip through vm_compute's representation doesn't preserve names

view this post on Zulip matrixbot (Gitter import) (Oct 24 2019 at 18:20):

pedroabreu I'm trying to quote and unquote a datatype in the same style of test-suite/case.v but apparently it does not work for datatypes? Am I missing something? https://gist.github.com/pedrotst/103b9c76302431508b01d624f99414d2

view this post on Zulip Matthieu Sozeau (Oct 24 2019 at 20:16):

You need to use a translation from inductive bodies to inductive entries I guess

view this post on Zulip Matthieu Sozeau (Oct 24 2019 at 20:17):

And use Make Inductive I guess

view this post on Zulip Danil Annenkov (Oct 25 2019 at 11:33):

Hi @pedrotst , Quote Recursively returns a list of global definitions and a term. So, you should project the term first:

Make Definition list_from_syntax :=
  ltac:(let t := eval cbv in (snd list_syntax) in exact t).

view this post on Zulip Danil Annenkov (Oct 25 2019 at 11:34):

This does not give you a new inductive though. The result is a definition list_from_syntax = list : Type -> Type

view this post on Zulip Yannick Forster (Gitter import) (Oct 25 2019 at 12:26):

@Jason Gross I don't think I saw it somewhere explicitly. I was discussing notations using names as arguments in functions in relation to Coq issue #10894, and then it felt natural to do it this way

view this post on Zulip Jason Gross (Oct 31 2019 at 00:12):

Does metacoq have an implementation of autorewrite / rewrite_strat (or even just rewrite, but one that goes under binders)?

view this post on Zulip Gregory Malecha (Oct 31 2019 at 08:20):

@Jason Gross no

view this post on Zulip Gregory Malecha (Oct 31 2019 at 08:21):

you could implement it, but it would require implementing some aggressive unification

view this post on Zulip Jason Gross (Oct 31 2019 at 20:31):

What if I'm only interested in subterm selection modulo beta-iota?

view this post on Zulip Gregory Malecha (Oct 31 2019 at 20:33):

it probably wouldn't be difficult to implement a very simple thing for what you want to do

view this post on Zulip Gregory Malecha (Oct 31 2019 at 20:33):

i'm not certain though

view this post on Zulip Gregory Malecha (Oct 31 2019 at 20:33):

it kind of depends

view this post on Zulip Gregory Malecha (Oct 31 2019 at 20:34):

most of the pieces are probably there, but you would have to put them together. that said, it would probably be very useful to the project overall

view this post on Zulip Jason Gross (Oct 31 2019 at 20:35):

I have a definition Let_In {A B} (f : A -> B) (x : A) := f x which is Opaque, and then I have a term like Let_In (x + x + 0) (fun y => Let_In (y + y +0) (fun z => Let_In (z + z + 0) (fun w => ...))), and I have the appropriate Proper lemma for Let_In, and I want to rewrite with the lemma that forall x, x + 0 = x in all the places. (I have other slightly more complicated examples, which involve interleaving cbn [nat_rect] with rewriting like this, but this is basically the extent of what I'm looking at.) How complicated would this be to have?

view this post on Zulip Gregory Malecha (Oct 31 2019 at 20:35):

ah, these are not dependent lets..

view this post on Zulip Jason Gross (Oct 31 2019 at 20:36):

No, not dependent. No dependent types.

view this post on Zulip Gregory Malecha (Oct 31 2019 at 20:36):

i can revise the answer from my email then, mirror core could handle this

view this post on Zulip Jason Gross (Oct 31 2019 at 20:36):

Neat!

view this post on Zulip Jason Gross (Oct 31 2019 at 20:37):

Could you help me get this example working in MirrorCore (or MetaCoq) or whatever?

view this post on Zulip Gregory Malecha (Oct 31 2019 at 20:37):

as far as metacoq goes, i think you could make it work, what is the timeline that you have for this?

view this post on Zulip Gregory Malecha (Oct 31 2019 at 20:37):

i'm on vacation next week and won't have much time before that

view this post on Zulip Jason Gross (Oct 31 2019 at 20:38):

(Actual code for this is at https://github.com/mit-plv/rewriter/blob/master/src/Rewriter/Rewriter/Examples/UnderLetsPlus0.v#L14-L20). Ideally by the end of next week; I'm aiming to evaluate a bunch of ways of doing this for the PLDI paper I'm working on

view this post on Zulip Jason Gross (Oct 31 2019 at 20:38):

(Going to be AFK for a bit; I'll be back soon)

view this post on Zulip Suzanne Dupéron (Gitter import) (Feb 15 2020 at 23:31):

Hi :wave:. Just wondering, is there a way in MetaCoq to quote a term with holes ? I'd like to quote a term like @cons _ true _ and later programmatically fill in both _.

view this post on Zulip Kenji Maillard (Feb 16 2020 at 00:05):

@Suzanne Dupéron looking at this message I think it's not (yet) possible

view this post on Zulip Théo Winterhalter (Feb 16 2020 at 13:46):

@Kenji Maillard I think it’s a bit different because the question here is to quote terms with holes. In the case of @cons _ true _ I think, it will be hard to bypass unification, I don’t see how it won’t become bool.
For the other one, if you manage to quote it, it should come with a tEvar that you could replace with a function. The question is also at what level you want to do this @Suzanne Dupéron: inside a goal? or outside?

view this post on Zulip Théo Winterhalter (Feb 16 2020 at 13:47):

But yeah since we don’t really deal with evars I’m not sure it would work well.

view this post on Zulip Matthieu Sozeau (Mar 01 2020 at 23:14):

FYI, the 8.10 and 8.11 branches work now

view this post on Zulip Kenji Maillard (Mar 02 2020 at 01:16):

FYI, the 8.10 and 8.11 branches work now

\o/

view this post on Zulip Suzanne Dupéron (Gitter import) (Mar 02 2020 at 17:31):

@Théo Winterhalter I'm trying to use this to do metaprogramming, so that Definition foo := macro(some_gallina_here). can have macro rewrite and/or infer some _ as it wants. Using a Notation + ltac:(…) + uconstr(…) it's possible to do this to some extent with LTac, but ironically LTac's representation of terms is not very nice to manipulate. Good to know metacoq doesn't really deal with evars, this is knid of a showstopper :) ! Thanks!

view this post on Zulip Théo Winterhalter (Mar 02 2020 at 18:17):

I mean you can still inspect a term with evars and try to fill them, but I don’t think you will have access to the constraints set on the hole, I might be wrong though, I’m not an expert on evars.
In principle what you want to do should be possible, but it’s always a bit painful to fordib Coq to infer stuff.

view this post on Zulip Matthieu Sozeau (Mar 02 2020 at 18:20):

@Suzanne Dupéron indeed you can still quote "open" terms but you'll be on your own solving the evars if you want to send the term back to Coq.

view this post on Zulip Suzanne Dupéron (Gitter import) (Mar 02 2020 at 18:40):

Hm, interesting. I would hope to fill make some transformations and/or fill in in some relevant parts, then let the usual unification do its job. How would you quote an open term, though?

view this post on Zulip Matthieu Sozeau (Mar 02 2020 at 18:45):

All the quotation mechanisms allow "open_constr", e.g. you can call tmQuote from the template monad on an open term. If you tmPrint it you'll see tEvar constructors for the holes

view this post on Zulip Danil Annenkov (Mar 04 2020 at 14:55):

Hi guys, do you know where I can look at examples of how to use the certified erasure in the template monad (not as an extracted plugin)? It seems that erasure/tests-suite/Test.v is outdated.

view this post on Zulip Danil Annenkov (Mar 04 2020 at 15:56):

Examples from https://github.com/MetaCoq/metacoq/blob/coq-8.9/test-suite/erasure_live_test.v do not produce fully evaluated terms (which supposed to be strings). For example,

view this post on Zulip Danil Annenkov (Mar 04 2020 at 15:56):

Quote Recursively Definition zero := 0.
Time Eval lazy in test zero.

view this post on Zulip Danil Annenkov (Mar 04 2020 at 15:57):

Takes 1 min to compute and as a result I see some huge term with nested "match" and stuff :)

view this post on Zulip Yannick Forster (Gitter import) (Mar 04 2020 at 16:00):

That looks like a bug, if I recall correctly those examples used to work

view this post on Zulip Danil Annenkov (Mar 04 2020 at 16:12):

It seems I'm using an old version of MetaCoq distribution: 1.0~alpha+8.9. I'll try the 2.0-beta.

view this post on Zulip Yannick Forster (Gitter import) (Mar 04 2020 at 17:27):

I'm afraid for an actually working live erasure you'll either have to wait for the new alpha to be released in the next couple of days (then for 8.9, 8.10 and 8.11) or use the code from github

view this post on Zulip Danil Annenkov (Mar 04 2020 at 19:47):

That's fine, I can wait.

view this post on Zulip Danil Annenkov (Mar 04 2020 at 19:47):

I have another question: I want to implement a pretty printer to something OCaml-like form the erased AST. But terms contain redundant abstractions and application of boxes. Currently, I am interested only in prenex-polymorphic fragment, so, I guess it should not be too hard to strip away these redundant abstractions and box applications. One issue is that lambdas are not annotated with types anymore and I don't know where they type abstractions or "regular" lambdas.

view this post on Zulip Danil Annenkov (Mar 04 2020 at 19:47):

Maybe this has been done somewhere already?

view this post on Zulip Matthieu Sozeau (Mar 05 2020 at 08:48):

It has not been done yet, but type abstraction lambdas bind variables that are not used in the body. I guess a better setup would be to mark binders for erasable types though during erasure

view this post on Zulip Danil Annenkov (Mar 05 2020 at 08:50):

Yes, marking of binders would be very helpful. Then it would be clear which abstractions to remove.

view this post on Zulip Danil Annenkov (Mar 05 2020 at 09:44):

It seems this is exactly what happens in the OCaml extraction: https://github.com/coq/coq/blob/6a6a2575c10d05cd0151a83c133825d43bd3cb28/plugins/extraction/extraction.ml#L633

view this post on Zulip Danil Annenkov (Mar 05 2020 at 09:45):

If the domain type it not extractable it is replaced with Dummy

view this post on Zulip Matthieu Sozeau (Mar 13 2020 at 12:24):

@/all The 8.10 and 8.11 packages are available on opam

view this post on Zulip Danil Annenkov (Mar 14 2020 at 18:56):

I am experimenting with annotating binders during extraction to determine later if we can omit type abstractions: https://github.com/annenkov/template-coq/commit/1c7bf36c3ec9b41226d8d87200527026293c6185

Basically, I annotate binders for lambda abstractions (lets can be annotated in the same way) with a boolean flag. The flag is true if the type of the binder reduces to arity (I use the same is_arity as in is_erasable). Is this right?

I adjusted the pretty-printing by adding print_term_deboxed function, which is almost the same as print_term but ignores abstractions marked as "dummy" and removes applications of boxes. It is easy to do it at the pretty-printing phase, but seems a bit hacky. Do you think it's worth implementing a "debox" function taking a term and removing dummy abstractions and boxes? It would be a bit more annoyng, because we have to adjust de Bruijn indices when removing abstractions. Especially annoing if the abstractions are mixed, e.g. something like this (fun (X : Set) (x : X -> unit) (Y : Set) (x0 : X) (Z : Type) => x x0).

There are some examples in https://github.com/annenkov/template-coq/blob/erase-annotated/test-suite/erasure_test.v

view this post on Zulip Matthieu Sozeau (Mar 14 2020 at 19:23):

Cool. The is_arity test sounds right. I think doing deboxing/simplification should be done after erasure but will require some thinking. Eg removing boxes in constructor applications should involve a change in the corresponding inductive declaration

view this post on Zulip Yannick Forster (Gitter import) (Mar 14 2020 at 19:28):

I think there are thoughts on that in Pierre Letouzey's thesis. Removing type abstractions should be fine. Removing binders for proofs is fine in many cases, but there are examples (definitely in Pierre's thesis) where that introduces problems

view this post on Zulip Yannick Forster (Gitter import) (Mar 14 2020 at 19:28):

Deboxing also sounds interesting, I never thought of that (and I think neither did Pierre)

view this post on Zulip Danil Annenkov (Mar 14 2020 at 19:31):

Eg removing boxes in constructor applications should involve a change in the corresponding inductive declaration

view this post on Zulip Danil Annenkov (Mar 14 2020 at 19:32):

If we just remove parameters of parameterised inductives, wouldn't it be fine?

view this post on Zulip Matthieu Sozeau (Mar 15 2020 at 10:09):

That part is done in certicoq

view this post on Zulip Matthieu Sozeau (Mar 15 2020 at 10:10):

It is non-trivial as you must first eta expand all constructor applications

view this post on Zulip Danil Annenkov (Mar 15 2020 at 10:14):

Ah, I see. Could you point me at which intermidiate representation in CertiCoq this is done?

view this post on Zulip Danil Annenkov (Mar 15 2020 at 10:46):

In the OCaml extraction https://github.com/coq/coq/blob/6a6a2575c10d05cd0151a83c133825d43bd3cb28/plugins/extraction/extraction.ml#L797
the comment says "We also suppressed all Coq parameters to the inductives, since
they are fixed, and thus are not used for the computation."
Does that mean that the boxes are removed without eta-expansion?

view this post on Zulip Danil Annenkov (Mar 15 2020 at 21:01):

It seems the OCaml extraction does eta-expansion, at least eta_args_sign is used there.
What if all the constructors are applied to all type arguments? Would eta-expansion be still required? Just trying to understand why eta-expansion is necessary.

view this post on Zulip Danil Annenkov (Mar 17 2020 at 17:07):

I want to use the erasure plugin in my own plugin. How can I do that? I've tried to just extract the erasure function with all the dependencies and import it. But this requires basically to do the same steps as in the erasure building script (and even more, because it depends on pcuic and template-coq). Is there a better way?

view this post on Zulip Danil Annenkov (Mar 17 2020 at 17:09):

@Matthieu Sozeau @Yannick Forster ?

view this post on Zulip Matthieu Sozeau (Mar 17 2020 at 19:11):

This is done in the L2 phase of certicoq

view this post on Zulip Matthieu Sozeau (Mar 17 2020 at 19:12):

There’s no better way than doing your whole copy of eveything, extraction messes up name clash management which renders separate compilation very brittle

view this post on Zulip Matthieu Sozeau (Mar 17 2020 at 19:12):

So we abandoned it now

view this post on Zulip Matthieu Sozeau (Mar 17 2020 at 19:13):

You can just reuse what the erasure plugin does I guess

view this post on Zulip Matthieu Sozeau (Mar 17 2020 at 19:16):

I’m not so familiar with the phases of coq’s extraction, but for partial applications I don’t think you can just remove all parameters blindly

view this post on Zulip Danil Annenkov (Mar 17 2020 at 19:38):

Thanks for your answers! I'll try to reuse the setup for erasure to rebuild in in the folder with my development.

view this post on Zulip Danil Annenkov (Mar 17 2020 at 19:40):

I’m not so familiar with the phases of coq’s extraction, but for partial applications I don’t think you can just remove all parameters blindly

Ok, that sounds reasonable. I'll do the naive version for now with a check that the constructors are fully applied.

view this post on Zulip Bas Spitters (Mar 18 2020 at 09:14):

@Danil Annenkov Information on extraction should be here:
http://www.pps.jussieu.fr/~letouzey/download/these_letouzey_English.ps.gz

view this post on Zulip Bas Spitters (Mar 18 2020 at 09:16):

BTW Does anyone know more about this?
https://github.com/letouzey/extraction-compute
I hadn't seen it before. Perhaps it's just a wrapper.

view this post on Zulip Danil Annenkov (Mar 20 2020 at 17:57):

Thanks @Bas Spitters I'll have a look.

view this post on Zulip Danil Annenkov (Mar 20 2020 at 18:02):

I think I need to distinguish between different reasons for boxing terms. Something like kill_reason in the OCaml extraction. I want to remove only boxed coming from types and not for props, because I don't remove abstractions corresponding to proofs, since this might be bad. Would such a more informative box would be useful in general? I mean, I can add this stuff and make a pull request if it makes sense.

view this post on Zulip Matthieu Sozeau (Mar 20 2020 at 19:17):

I guess that could be useful in any case

view this post on Zulip Danil Annenkov (Mar 20 2020 at 19:20):

Great, I'll try to do that and then you guys can review the pull requiest.

view this post on Zulip Bohdan Liesnikov (Mar 27 2020 at 15:55):

Hi everyone!
I'm currently looking for a lemma that would assert existence of a type of type, something along the lines of Sigma ;;; Gamma |- t : T -> exists s, Sigma ;;; Gamma |- T : tSort s.
But Sigma above can't stay the same since in some cases we have to declare a new universe.

I looked for it in the repo, but couldn't find anything resembling this. Did I miss it or is it indeed currently not there?
And if not, what do you think would be the best way to state it/prove it?

view this post on Zulip Théo Winterhalter (Mar 27 2020 at 15:56):

This lemma does not hold. However in metacoq we call it validity.

view this post on Zulip Théo Winterhalter (Mar 27 2020 at 15:56):

Instead we show that T : tSort s for some s _or_ that T is a valid arity.

view this post on Zulip Théo Winterhalter (Mar 27 2020 at 15:57):

Here is the theorem
https://github.com/MetaCoq/metacoq/blob/coq-8.11/pcuic/theories/PCUICValidity.v#L311
(It’s not completely proven yet I think.)

view this post on Zulip Théo Winterhalter (Mar 27 2020 at 15:58):

It’s in PCUIC and not in TemplateCoq where there isn’t much of the meta-theory done.

view this post on Zulip Théo Winterhalter (Mar 27 2020 at 15:59):

But in principle Σ should stay the same.

view this post on Zulip Bohdan Liesnikov (Mar 27 2020 at 16:09):

Thanks! I talked with Yannick about this before and he aslo pointed me in direction of that lemma.
However, what I don't quite get is if arities are iterated products\letins, wouldn't it be possible to assign a type (sort) to a valid arity?

view this post on Zulip Théo Winterhalter (Mar 27 2020 at 16:10):

Unfortunately no, there are so-called algebraic universes (like max(i,j), i+1) that can only appear on the right-hand side of the colon.

view this post on Zulip Bohdan Liesnikov (Mar 27 2020 at 16:18):

Yep, but then couldn't you declare a new universe with a constraint that it's strictly bigger than whatever algebraic universe appears on the right-hand side?
A side question would be where can I read up on that? I saw "Type checking with universes" by Harper and Pollack, but maybe there is more recent work?

view this post on Zulip Théo Winterhalter (Mar 27 2020 at 16:18):

I mean, by design, algebraic universes should _not_ be typed.

view this post on Zulip Théo Winterhalter (Mar 27 2020 at 16:19):

I don’t know, @Matthieu Sozeau do you know if it’s written anywhere?

view this post on Zulip Bohdan Liesnikov (Mar 27 2020 at 16:20):

I mean, by design, algebraic universes should _not_ be typed.

I guess, this is something that I was missing, thanks :)

view this post on Zulip Théo Winterhalter (Mar 27 2020 at 16:21):

I’m sorry I can’t really explain this point because I’m not an expert, I’d rather have @Matthieu Sozeau do it.

view this post on Zulip Karl Palmskog (Mar 28 2020 at 15:14):

so one thing I'd have liked at various point in verified program development using sigma-types is the ability to remove Props automatically inside Coq from various functions

view this post on Zulip Karl Palmskog (Mar 28 2020 at 15:15):

... so they can actually be executed inside Coq in reasonable time

view this post on Zulip Karl Palmskog (Mar 28 2020 at 15:15):

is there a way to accomplish something like this using MetaCoq, or what needs to be done first?

view this post on Zulip Théo Winterhalter (Mar 28 2020 at 15:38):

What would you replace the propositions with (or the proof of those)?

view this post on Zulip Théo Winterhalter (Mar 28 2020 at 15:39):

It sound a bit like erasure that we have, but this does not preserve typing.

view this post on Zulip Théo Winterhalter (Mar 28 2020 at 15:39):

Would you like to replace all proofs of propositions with opaque constants, like abstract would do?

view this post on Zulip Karl Palmskog (Mar 28 2020 at 15:40):

basically, I want to go from a function: nat -> { a : A | P a } to a function nat -> A

view this post on Zulip Karl Palmskog (Mar 28 2020 at 15:40):

such that the latter preserves the computational behavior of the former

view this post on Zulip Théo Winterhalter (Mar 28 2020 at 15:41):

I mean you would have to work out the translation but I expect it could be done with metacoq.

view this post on Zulip Karl Palmskog (Mar 28 2020 at 15:41):

and it could be done recursively, like extraction does?

view this post on Zulip Karl Palmskog (Mar 28 2020 at 15:42):

so there is no Prop generation slowing down execution anywhere

view this post on Zulip Karl Palmskog (Mar 28 2020 at 15:43):

if this is possible, could one reuse something from the existing erasure?

view this post on Zulip Matthieu Sozeau (Mar 28 2020 at 15:43):

@B. L. The problem is we don't know how to do type inference efficiently if we allow arbitrary max(i, j) <= max(k, l) constraints, hence we restrict the type system so that only max(i,j) <= k constraints can be generated. In practice it means Type@{max(i,j)} does not have a type, but indeed a different version of the system where the typing rule of Type becomes : i < j |- Type@{i} < Type@{j} would allow to get rid of the special case for arities.

view this post on Zulip Matthieu Sozeau (Mar 28 2020 at 15:43):

Hugo Herbelin has a not about algebraic universes where this is explained (it appeared at TYPES IIRC)

view this post on Zulip Matthieu Sozeau (Mar 28 2020 at 15:46):

@Karl Palmskog If what you want is to allow during a proof script execution to solve a conversion [A = B] using (erase(A) = erase(B)) for A, B : nat then MetaCoq + CertiCoq ought to provide that.

view this post on Zulip Matthieu Sozeau (Mar 28 2020 at 15:47):

nat or any other first-order inductive type with Props in it should be fine

view this post on Zulip Matthieu Sozeau (Mar 28 2020 at 15:49):

@B. L. about such a lemma, indeed I think it is provable, with an extended Sigma, using validity. What you want to prove is that isWfArity_or_Type Sigma Gamma T -> exists s, Sigma + s and a constraint ;;; Gamma |- T : tSort s basically.

view this post on Zulip Karl Palmskog (Mar 28 2020 at 15:50):

@Matthieu Sozeau you mean they (metacoq + certicoq) provide this right now? yeah basically I want to develop using sigma types, but then get "regular" functions with some companion lemma

view this post on Zulip Matthieu Sozeau (Mar 30 2020 at 10:41):

Not yet, we’ll need a way to extend the conversion algorithms in the kernel so we can call the certicoq based evaluator first, or find a way around that

view this post on Zulip Bohdan Liesnikov (Mar 30 2020 at 12:14):

@Matthieu Sozeau Thanks a lot!

view this post on Zulip Bohdan Liesnikov (Mar 30 2020 at 12:22):

For the sources - I see “Type inference with algebraic universes in the Calculus of Inductive Constructions” from 2005 (http://pauillac.inria.fr/~herbelin/articles/univalgcci.pdf), but not much else
Is this what you meant?

view this post on Zulip Matthieu Sozeau (Apr 01 2020 at 13:06):

Yes

view this post on Zulip Danil Annenkov (Apr 07 2020 at 13:29):

I am reading Pierre Letouzey's thesis. He discusses simplifications such as removing abstractions and boxes in Chapter 4.3. It's safe to remove boxes for fully applied constants and constructors. The tricky part comes when constants and constructors are partially applied (but for global definitions all dummy abstractions are removed and only the application sides are adjusted). Interestingly, boxes coming from propositions and type schemes are treated in the same way. I understand why removing all abstractions for propositions might be a problem (seems like False_rect and Acc, mainly), but why it is not safe to remove all abstractions corresponding to type schemes, I don't understand. Maybe you have some ideas @Yannick Forster ?

view this post on Zulip Matthieu Sozeau (Apr 09 2020 at 14:36):

@Danil Annenkov It is curious if we cannot remove all type abstractions. It would seem to go against parametricity

view this post on Zulip Danil Annenkov (Apr 09 2020 at 14:41):

Yes, it should be possible. I'm wondering why this is not mentioned as a possibility for optimisation. I found the following footnote in Pierre's thesis "In fact, these residues can also come from type schemes and not only from logical parts, but we will merge here these two situations by simply speaking of "residues"."

view this post on Zulip Danil Annenkov (Apr 09 2020 at 14:43):

For example, extraction for the following example:

Definition p_ex1 (A : Type) (a : A) (B : Type) (C : Type):= a.

Definition p_ex2 :=
  let f := p_ex1 nat 0 in
  (fun _ : unit => f nat bool).

Extraction p_ex2.

view this post on Zulip Danil Annenkov (Apr 09 2020 at 14:43):

gives

let p_ex2 =
  let f = fun _ _ -> p_ex1 O in (fun _ -> f __ __)

view this post on Zulip Danil Annenkov (Apr 09 2020 at 14:45):

Clearly, the boxes for the dummy arguments are not removed.

view this post on Zulip Matthieu Sozeau (Apr 09 2020 at 15:22):

Indeed, it doesn't do it for local definitions

view this post on Zulip Danil Annenkov (Apr 09 2020 at 15:24):

I think it's for partial applications, because for fully applied p_ext1 it extracts to let p_ex2 = let f = p_ex1 O in (fun _ -> f)

view this post on Zulip Danil Annenkov (Apr 09 2020 at 15:25):

It behaves the same way for partial application of types as for partial applications of logical arguments.

view this post on Zulip Cyril Cohen (Apr 15 2020 at 14:08):

Hi, I am in the process of exporting gitter channels (public) data to zulip, (it can be done only once, during the creation of the zulip chatroom), do you wish that I export the data of this channel too?

view this post on Zulip Matthieu Sozeau (Apr 15 2020 at 14:08):

Yes

view this post on Zulip matrixbot (Gitter import) (Apr 16 2020 at 15:34):

pedroabreu What is the best way to debug when Make Definition fails?

view this post on Zulip Danil Annenkov (Apr 16 2020 at 15:39):

@pedrotst I think, it depends why it fails. I don't know the best way, but first, I look at the template Coq AST, if it's not too big.

view this post on Zulip Danil Annenkov (Apr 16 2020 at 15:40):

What kind of error do you get?

view this post on Zulip matrixbot (Gitter import) (Apr 16 2020 at 15:42):

pedroabreu inspect_term: cannot recognize (huge term) (maybe you forgot to reduce it?)

view this post on Zulip matrixbot (Gitter import) (Apr 16 2020 at 15:43):

pedroabreu basically what I'm trying to do is quote and unquote the lemma and_cancel_l, It seems to me that it is not quoting quite correctly

view this post on Zulip matrixbot (Gitter import) (Apr 16 2020 at 15:43):

pedroabreu in particular a lambda variable that should be named is not

view this post on Zulip matrixbot (Gitter import) (Apr 16 2020 at 15:43):

pedroabreu hence I was trying to unquote to see it

view this post on Zulip matrixbot (Gitter import) (Apr 16 2020 at 15:45):

pedroabreu * basically what I'm trying to do is quote and unquote the lemma and_cancel_l, basically it is not being quoted as I expected

view this post on Zulip Danil Annenkov (Apr 16 2020 at 18:31):

Could you please tell me how you quote and_cancel_l? Using Quote Definition?

I've tried the following:

Quote Definition z := (and_cancel_l).
Make Definition zzz := z.
Print zzz.
(* zzz =
and_cancel_l
     : forall A B C : Prop,
       (B -> A) -> (C -> A) -> (A /\ B <-> A /\ C) <-> (B <-> C)
*)

view this post on Zulip Danil Annenkov (Apr 16 2020 at 18:33):

This seems to work fine, but Quote Definition z := (and_cancel_l). just quotes it as a constant.
It's hard to do better, I guess, because and_cancel_l is opaque.

view this post on Zulip Danil Annenkov (Apr 16 2020 at 18:35):

If you use Quote Recursively Definition z := (and_cancel_l). Then you need to take a second projection to unquote. Because the first component is global environment with all the definitions that and_cancel_l depends on.

view this post on Zulip Danil Annenkov (Apr 16 2020 at 19:27):

The body of the and_cancel_l is accessible in the global environment (when you do Quote Recursively).
You can print it like this:

Compute lookup_env z.1 "Coq.Init.Logic.and_cancel_l".

view this post on Zulip matrixbot (Gitter import) (Apr 17 2020 at 03:38):

pedroabreu Yeah, I was getting the term with Quote Recursively I didn't know about the lookup_env function, so I was walking through the list until the position I wanted.

view this post on Zulip matrixbot (Gitter import) (Apr 17 2020 at 03:40):

pedroabreu But anyways, I upgraded the version of Metacoq to see if I see the same behaviour and apparently I cannot get Unquote to work. The demo files says I should do Metacoq Unquote Definition bar := foo, but I get Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

view this post on Zulip matrixbot (Gitter import) (Apr 17 2020 at 03:40):

pedroabreu same happens with Unquote Definition bar := foo

view this post on Zulip matrixbot (Gitter import) (Apr 17 2020 at 03:41):

pedroabreu * But anyways, I upgraded the version of Metacoq to see if I see the same behaviour and apparently I cannot get Unquote to work. The demo.v files says I should do Metacoq Unquote Definition bar := foo, but I get Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

view this post on Zulip matrixbot (Gitter import) (Apr 17 2020 at 03:41):

pedroabreu * But anyways, I upgraded the version of Metacoq to 8.11 to see if I see the same behaviour and apparently I cannot get Unquote to work. The demo.v files says I should do Metacoq Unquote Definition bar := foo, but I get Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

view this post on Zulip matrixbot (Gitter import) (Apr 17 2020 at 03:41):

pedroabreu * But anyways, I upgraded the version of Metacoq to 8.11 to see if I get the same behaviour and apparently I cannot get Unquote to work. The demo.v files says I should do Metacoq Unquote Definition bar := foo, but I get Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

view this post on Zulip Danil Annenkov (Apr 17 2020 at 08:07):

I use MetaCoq for Coq 8.11 from opam before the last update of the vernacular syntax. Maybe the problem is not in the MetaCoq version, but what you are trying to unquote? The global environment contains global declarations, not terms. You need to unwrap them before you unquote. The following code works in my installation (for Coq 8.11):

Definition lookup_const (g : global_env) (cst : ident) :=
  match (lookup_env g "Coq.Init.Logic.and_cancel_l") with
  | Some (ConstantDecl d) =>
    match d.(cst_body) with
    | Some b => b
    | None => tVar "decl without a body"
    end
  | Some _ => tVar "not a constant"
  | None => tVar "decl not found"
  end.

Quote Recursively Definition z := (and_cancel_l).
Make Definition zzz := (lookup_const z.1 "Coq.Init.Logic.and_cancel_l").

view this post on Zulip Danil Annenkov (Apr 17 2020 at 08:09):

lookup_const uses lookup_env and unwraps global_decl into a term, if possible. Otherwise returns a dummy tVar.

view this post on Zulip Danil Annenkov (Apr 17 2020 at 08:11):

Does the old syntax Make Definition still works for you?

view this post on Zulip Danil Annenkov (Apr 17 2020 at 12:35):

If you use TemplateMonad then you can use tmQuoteConstant to quote a constant directly. Passing true as a second argument would allow to get bodies for opaque definitions.

view this post on Zulip matrixbot (Gitter import) (Apr 17 2020 at 13:08):

pedroabreu awesome, Make Definition was the syntax I was missing, thanks! Everything is working as expected now thanks for you time Danil Annenkov (Gitter)

view this post on Zulip Danil Annenkov (Apr 17 2020 at 13:09):

@pedrotst no problem :)

view this post on Zulip matrixbot (Gitter import) (Apr 17 2020 at 14:04):

pedroabreu I see what my problem was now

view this post on Zulip matrixbot (Gitter import) (Apr 17 2020 at 14:05):

pedroabreu I was assuming that we shouldn't reference unnamed variables (which in hindsight is not a fair assumption). Which means the following should work
```Definition nat_id_syntax :=
tLambda nAnon
(tInd
{|
inductive_mind := "Coq.Init.Datatypes.nat";
inductive_ind := 0 |} []) (tRel 0).
Make Definition unquote_nat_id := nat_id_syntax.

Print unquote_nat_id.
(*
unquote_nat_id = fun H : nat => H
: nat -> nat
*)


view this post on Zulip matrixbot (Gitter import) (Apr 17 2020 at 14:06):

pedroabreu So I guess my question is how does coq/metacoq deal with naming unnamed variables like this?

view this post on Zulip Théo Winterhalter (Apr 17 2020 at 14:07):

You should see names as printing hints, nothing more.
It’s true that we often write _ in a binder (on paper) to mean that the variable isn’t used, but here it just means that it’s up to Coq to figure out how to name it.

view this post on Zulip Danil Annenkov (Apr 24 2020 at 12:52):

Hej guys, is there any way for quoting recursively but not fetching bodies of opaque definitions? Otherwise, any definition involving a proof from the standard library will quote half of the standard library :) Some times I it just takes forever, so I had to terminate the process. We hit this problem before when working on the forcing translation. Loïc had to reimplement proof about natural numbers, otherwise, it took too long to quote dependencies.

view this post on Zulip Matthieu Sozeau (Apr 25 2020 at 10:45):

You could try to program it using the non-recursive quoting I guess, turning opaque proofs into axioms in the reified environment ?

view this post on Zulip Danil Annenkov (Apr 25 2020 at 10:48):

tmQuoteConstant actually takes a flag whether it should bypass opacity or not. I'll try to use this one. But then the problem is that I'll have to manage dependencies manually.

view this post on Zulip Danil Annenkov (Apr 30 2020 at 15:16):

@Matthieu Sozeau there are two versions of the erasure function: one in SafeErasureFunction.v and one in ErasureFunction.v. As far as I understand, the difference is that the first one takes a well-typed term. How this typing information is used during erasure? The extracted plugin is based on the safe version, if I understand correctly. What would be the downsides of using the version from ErasureFunction.v for the plugin?

view this post on Zulip Théo Winterhalter (Apr 30 2020 at 16:45):

The difference is that the safe one doesn’t need fuel I think.

view this post on Zulip Théo Winterhalter (Apr 30 2020 at 16:46):

(At least that’s the difference between SafeChecker and Checker.)

view this post on Zulip Théo Winterhalter (Apr 30 2020 at 16:46):

The Safe one is the proven correct modulo normalisation. But it should extract more or less to the desired implementation.

view this post on Zulip Danil Annenkov (Apr 30 2020 at 18:50):

Hi @Théo Winterhalter, thank for you answer!
I've checked erase from ErasureFunction.v:

erase :
forall Σ : global_env_ext,
∥ wf_ext Σ ∥ ->
forall Γ : context, ∥ wf_local Σ Γ ∥ -> term -> typing_result E.term

view this post on Zulip Danil Annenkov (Apr 30 2020 at 18:50):

It looks like there is no fuel here.

view this post on Zulip Danil Annenkov (Apr 30 2020 at 18:51):

In seems that the difference is in is_erasable

view this post on Zulip Danil Annenkov (Apr 30 2020 at 18:55):

In the "safe" version is_erasable calls type_of and in the other one it calls make_graph_and_infer

view this post on Zulip Danil Annenkov (Apr 30 2020 at 18:57):

And is_erasable from ErasureFunction.v returns also welltyped Sigma Gamma t if the term is not erasable (and the call to is_erasable succeeds).

view this post on Zulip Théo Winterhalter (Apr 30 2020 at 19:16):

I see. I mean, it would be better for @Yannick Forster or @Matthieu Sozeau to answer here because I didn’t work on erasure at all.

view this post on Zulip Gregory Malecha (May 01 2020 at 01:25):

I was toying with some performance tuning today and built a simple bytestring library. would people be interested in using that instead of ascii for storing strings?

view this post on Zulip Danil Annenkov (May 04 2020 at 15:56):

@Gregory Malecha we use strings in Coq for pretty-printing a lot. So far they were not the bottleneck, but it would be interesting to try bytestrings instead.

view this post on Zulip Gregory Malecha (May 04 2020 at 15:57):

i recall there being something a bit annoying when you tried to quote a quoted term @Jason Gross brought this up a long time ago, not sure if he's still interested in it

view this post on Zulip Matthieu Sozeau (May 05 2020 at 11:12):

@Danil Annenkov the main difference is in the use of retyping which is less costly than typing IIRC.

view this post on Zulip Matthieu Sozeau (May 05 2020 at 11:13):

@Gregory Malecha you build bytestring out of native ints?

view this post on Zulip Danil Annenkov (May 05 2020 at 12:46):

@Matthieu Sozeau by retyping you mean type_of? What is the difference with make_graph_and_infer?

view this post on Zulip Jason Gross (May 06 2020 at 01:52):

I'm not actively working on anything around it currently, but I am still at least vaguely interested. It came up when trying to formalize Lob's theorem in Coq using Template Coq / MetaCoq, because there are a bunch of places where you need a doubly-quoted thing. (For example, one of the things needed is a Gallina function from AST -> (quote AST), and then I also need a quoted version of this function, I believe.)

view this post on Zulip Jason Gross (May 06 2020 at 01:54):

And regarding bytestrings, I'm assuming you mean using https://github.com/coq/coq/blob/master/theories/Init/Byte.v and making a list of them. Note that if you make a custom inductive type that is a list of these, much like string is a specialized list of ascii, you can have them pretty-printed as strings automatically. (Allowing this with list byte and list ascii is still a work in progress on string notations, but should hopefully be coming in the next couple of Coq versions)

view this post on Zulip Gregory Malecha (May 06 2020 at 01:56):

it is a very simple implementation: https://github.com/bedrocksystems/cpp2v/blob/master/theories/bytestring.v

view this post on Zulip Gregory Malecha (May 06 2020 at 01:57):

i think that i might implement C-style escapes for it though so that "\n" parses to (String x13 EmptyString)

view this post on Zulip Gregory Malecha (May 06 2020 at 01:59):

specializing the inductive achieves two things: 1/ it is a drop-in replacement for string in more cases; 2/ it avoids the extra Byte.byte parameter to every cons


Last updated: Aug 11 2022 at 02:03 UTC