Stream: Equations devs & users

Topic: imported from gitter room coq/Equations


view this post on Zulip Pierre Courtieu (Jan 24 2018 at 14:51):

Hi there!

view this post on Zulip Pierre Courtieu (Jan 24 2018 at 14:51):

It's been a while since we discussed replacing the backend of Function by Equations, did you make some advances?

view this post on Zulip Matthieu Sozeau (Jan 25 2018 at 04:46):

Not exactly, it’s clearer what is missing now: the factorization of cases and a way to interpret concrete syntax to splitting trees, Thierry Martinez is working on that.

view this post on Zulip Pierre Courtieu (Jan 25 2018 at 11:06):

Great!

view this post on Zulip Jad Hamza (Gitter import) (Apr 06 2018 at 11:34):

I don’t know how to do that in general. Because ˋf n’ˋ might still fall into the `S n’ˋ case I’m not sure this kind of reasoning can be done in a well-founded way. Currently the equations are defined after the definition itself.

On paper it would be like proving by induction on n that there exists such a function f, and that f n = match [...]. (We strengthen the induction hypothesis by adding the equality as part of the goal). Then, as long as we use that induction hypothesis on strictly smaller arguments then it seems it should be sound?

view this post on Zulip Jad Hamza (Gitter import) (Apr 06 2018 at 11:39):

@Matthieu Sozeau Since you're there :) Do you have an explanation as to why this id (x :: l) doesn't reduce to x :: id l (https://gist.github.com/jad-hamza/ff6b07794856cfdd04e1fe94d4673688) when using Program Fixpoint? With Equations it works fine thanks to the rewrite lemmas

view this post on Zulip Jad Hamza (Gitter import) (Apr 09 2018 at 11:45):

Hello, is it possible to change the tactic used by Equations? I have a tactic set with Obligation Tactic, but Equations doesn't seem to be using it. Then when I do "Next Obligation", the tactic is indeed used and the goal is solved.

view this post on Zulip Matthieu Sozeau (Apr 12 2018 at 09:00):

@Jad Hamza looks like a bug, it should be using your default tactic directly

view this post on Zulip Jad Hamza (Gitter import) (Apr 12 2018 at 11:01):

@Matthieu Sozeau Alright thanks, I'll try to make a small example to report an issue if I encounter the bug again

view this post on Zulip Jad Hamza (Gitter import) (Apr 13 2018 at 11:49):

@Matthieu Sozeau I reported it here: https://github.com/mattam82/Coq-Equations/issues/71

view this post on Zulip Jad Hamza (Gitter import) (Apr 18 2018 at 18:09):

I'm trying "opam install coq-equations" with coq.8.8.0 but it's asking me to downgrade coq to 8.7.2 (I do have the repo: https://coq.inria.fr/opam/extra-dev)

view this post on Zulip Matthieu Sozeau (Apr 19 2018 at 16:39):

The new package is being tested

view this post on Zulip Jad Hamza (Gitter import) (Apr 25 2018 at 12:48):

Hello @Matthieu Sozeau, I'm using the Equations package 8.7.dev on Coq 8.7.2, and I'm having some trouble on "Qed" or "Admitted" on obligations. It's taking very long (5 minutes and running now). Is this a known issue?

view this post on Zulip Matthieu Sozeau (Apr 25 2018 at 12:57):

It can be failing to prove induction/elimination principles in presence of obligations. One way to avoid this is to abstract them as sublemmas before the definition. Not ideal but works well.

view this post on Zulip Matthieu Sozeau (Apr 25 2018 at 12:57):

I noticed that issue recently and still have to investigate why it happens

view this post on Zulip Jad Hamza (Gitter import) (Apr 25 2018 at 13:11):

@Matthieu Sozeau I've shown the obligation in the other channel; I feel it might be related to https://github.com/mattam82/Coq-Equations/issues/71

view this post on Zulip Aleksey Nogin (Gitter import) (Apr 26 2018 at 17:50):

Is there a way to define several (>2) mutually recursive functions? If so, what is the right syntax? As far as I can tell, I can only have one "where" (when I tried adding two, weirdness happened - I posted issue mattam82/Coq-Equations#74 about it).

view this post on Zulip Aleksey Nogin (Gitter import) (Apr 27 2018 at 14:21):

@Matthieu Sozeau, thanks a lot for looking into mattam82/Coq-Equations#74 - please do not hesitate to let me know if I can be of any help with narrowing this down, or testing a potential solution (for this or any of the other issues I am reporting).

view this post on Zulip Jad Hamza (Gitter import) (May 01 2018 at 05:18):

@Matthieu Sozeau Hello, is there any quick workaround for https://github.com/mattam82/Coq-Equations/issues/75 that doesn't involve rewriting the body of the equation (nor its types)

view this post on Zulip Aleksey Nogin (Gitter import) (May 01 2018 at 18:44):

@Matthieu Sozeau, since I reported so many issues, I thought it would be worth providing an update on which one(s) I care about the most - currently out development is blocked by inability to define equations involving VST's compact_prod (https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6) - a combination of mattam82/Coq-Equations#78 and the bugs that crop up when trying to work around it (mattam82/Coq-Equations#84, mattam82/Coq-Equations#85, but not actually seeing mattam82/Coq-Equations#82 "in production").

view this post on Zulip Aleksey Nogin (Gitter import) (May 01 2018 at 20:55):

Actually, I may have spoken too soon - while the mattam82/Coq-Equations#78 is definitely and issue for us, if/when it is fixed, we might still end up struggling with mattam82/Coq-Equations#74 as well.

view this post on Zulip Aleksey Nogin (Gitter import) (May 02 2018 at 16:52):

For issues where things result in an unexpected typechecking error, is there a way to have everything generated by the plugin printed, so that we can see the context for the type error, and know where exactly it's occurring?

view this post on Zulip Matthieu Sozeau (May 03 2018 at 12:19):

Ok, I’ll try to have a look at those two in priority! Sadly my laptop broke two days ago so I’ve not been able to hack around as much as I’d like!

view this post on Zulip Aleksey Nogin (Gitter import) (May 03 2018 at 20:54):

@Matthieu Sozeau: Thank you!

view this post on Zulip Aleksey Nogin (Gitter import) (May 14 2018 at 16:49):

I came up with a potential workaround for mattam82/Coq-Equations#78 (posted it as a comment there), but when I tried to apply it in production, I got Induction principle could not be proved automatically: Anomaly "Helper not found while proving induction lemma." I do not have a good way to reproduce it yet, but will see if I can create one.

view this post on Zulip Aleksey Nogin (Gitter import) (May 14 2018 at 17:52):

So far, all my attempts to reproduce the Anomaly error above in a simplified example hit either mattam82/Coq-Equations#84 or mattam82/Coq-Equations#85 instead...

view this post on Zulip Matthieu Sozeau (May 14 2018 at 18:04):

Hmm, that must be a bug in the automated proof, I'll have to investigate.

view this post on Zulip Matthieu Sozeau (May 14 2018 at 18:05):

If I fix the issue that struct does not work on a single definition we might make progress as well, no?

view this post on Zulip Aleksey Nogin (Gitter import) (May 14 2018 at 18:09):

No, I do not have anything blocking on "Equations (struct id)" not working - the workaround was to move some of the arguments into a return type. Currently, I am stuck on needing to define >2 mutually recursive functions (mattam82/Coq-Equations#74) and the Anomaly "Helper not found while proving induction lemma." issue.

view this post on Zulip Matthieu Sozeau (May 14 2018 at 18:10):

Ok, thanks for the update. Let's see if I can get the >2 mutuals first, its pretty well localised

view this post on Zulip Aleksey Nogin (Gitter import) (May 14 2018 at 18:17):

Thanks, I'll continue trying to get a reproducible case for the Anomaly in the meantime.

view this post on Zulip Matthieu Sozeau (May 14 2018 at 18:30):

I guess in your "production" case you additionally have nesting? That would explain the "helper not found" message

view this post on Zulip Aleksey Nogin (Gitter import) (May 14 2018 at 18:31):

It has a lot of stuff :). What kinds of nesting might be causing it?

view this post on Zulip Matthieu Sozeau (May 14 2018 at 18:31):

nested recursion

view this post on Zulip Aleksey Nogin (Gitter import) (May 14 2018 at 18:33):

Right, it has stuff along the lines of my examples in mattam82/Coq-Equations#84 / mattam82/Coq-Equations#85

view this post on Zulip Aleksey Nogin (Gitter import) (May 14 2018 at 19:30):

Was finally able to reproduce the Anomaly - filed mattam82/Coq-Equations#93 (see the P.S. comment there for what makes a difference between hitting mattam82/Coq-Equations#84 and getting past it).

view this post on Zulip Aleksey Nogin (Gitter import) (May 16 2018 at 15:54):

@Matthieu Sozeau: thanks a lot for the mattam82/Coq-Equations#74 fix! Any chance it could be backported to a stable branch (e.g, 8.8)?

view this post on Zulip Matthieu Sozeau (May 16 2018 at 16:16):

I'll do that now that I've tested it more

view this post on Zulip Matthieu Sozeau (May 16 2018 at 16:39):

@Aleksey Nogin the patches are on 8.8 now

view this post on Zulip Aleksey Nogin (Gitter import) (May 16 2018 at 16:39):

Thanks!

view this post on Zulip Jad Hamza (Gitter import) (May 17 2018 at 12:54):

Hi @Matthieu Sozeau, I have a quick question: how can I prevent automatic unfolding of a function defined by Equations?

view this post on Zulip Jad Hamza (Gitter import) (May 17 2018 at 13:17):

look like the function is unfolded by cbn, but not by simpl

view this post on Zulip Jad Hamza (Gitter import) (May 17 2018 at 13:21):

I'm trying with Arguments f x y : simpl never. but cbn still unfolds it. On the other hand, cbn -[f] has the write behavior and does not unfold f.

view this post on Zulip Matthieu Sozeau (May 17 2018 at 13:24):

You can use Opaque / Transparent. The system should just be entirely parameterized with the current things one wants to unfold or not but currently only imperative state handling is available and reliable :)

view this post on Zulip Jad Hamza (Gitter import) (May 17 2018 at 13:27):

@Matthieu Sozeau I did Opaque f, but cbn still unfolds f to f_comp_proj

view this post on Zulip Matthieu Sozeau (May 17 2018 at 13:28):

Argh

view this post on Zulip Matthieu Sozeau (May 17 2018 at 13:29):

Maybe you can use a custom simplification tactic? There must be an issue on Coq’s github that adresses this, otherwise it would be good to submit one!

view this post on Zulip Jad Hamza (Gitter import) (May 17 2018 at 13:30):

@Matthieu Sozeau Yes I'll check! I'll use simpl for now. I have another quick question

view this post on Zulip Jad Hamza (Gitter import) (May 17 2018 at 13:31):

I now want to simplify the function call thanks the equations generated by Equations, so I do: repeat rewrite f_equation_1 in * || rewrite f_equation_2 in * || rewrite f_equation_3 in * || rewrite f_equation_4 in * || rewrite f_equation_5 in *.

view this post on Zulip Jad Hamza (Gitter import) (May 17 2018 at 13:31):

but for some reason, that takes 5s to finish on a very small goal

view this post on Zulip Jad Hamza (Gitter import) (May 17 2018 at 13:31):

(with only two expressions to rewrite)

view this post on Zulip Jad Hamza (Gitter import) (May 17 2018 at 13:35):

Is there a known slowness issue here?

view this post on Zulip Jad Hamza (Gitter import) (May 17 2018 at 13:37):

@Matthieu Sozeau Oh, actually "constructor" also unfolds f to f_comp_proj when the goal is f x y

view this post on Zulip Matthieu Sozeau (May 17 2018 at 13:44):

Yes many tactics do not respect Opaque

view this post on Zulip Matthieu Sozeau (May 17 2018 at 13:45):

Are you sure f is Opaque ? Rewrite does respect that I think

view this post on Zulip Matthieu Sozeau (May 17 2018 at 13:45):

There’s the simp f tactic that does the same pretty much

view this post on Zulip Jad Hamza (Gitter import) (May 17 2018 at 13:47):

wait, in fact cbn seems to respect Opaque, but not constructor. Thanks for simp. Also the slowness disappeared now after rebooting emacs, I don't know what happened, and the rewrite f_equation_i works as expected

view this post on Zulip Matthieu Sozeau (May 17 2018 at 14:39):

Probably an issue with backtracking

view this post on Zulip Matthieu Sozeau (May 18 2018 at 16:27):

@Aleksey Nogin I’m almost done fixing #93 and supporting definitions whose return type is a function type everywhere

view this post on Zulip Jad Hamza (Gitter import) (May 23 2018 at 10:21):

Hello @Matthieu Sozeau, I was able to reproduce the issue of slowness in rewrite and simp: https://github.com/coq/coq/issues/7585 https://github.com/mattam82/Coq-Equations/issues/95
any workaround?

view this post on Zulip Matthieu Sozeau (May 23 2018 at 12:57):

I’ll try to have a look today. If you inspect the rewrite hint databases and the transparency status of constants do you see anything suspect maybe?

view this post on Zulip Jad Hamza (Gitter import) (May 23 2018 at 13:39):

@Matthieu Sozeau Thanks! Do you mean Print Rewrite HintDb core.? I just see rewrite rules about the composition of two functions.

view this post on Zulip Jad Hamza (Gitter import) (May 23 2018 at 13:42):

Print Transparent Dependencies transport. prints a bunch of dependencies but I guess these are the normal library dependencies?

view this post on Zulip Matthieu Sozeau (May 23 2018 at 13:45):

I mean Print Rewrite HintDb yes, is there a difference if the definitions are in one file and multiple ones ?

view this post on Zulip Matthieu Sozeau (May 23 2018 at 13:47):

About/Print cst. Should tell you if cst is transparent or opaque, that might drastically change the time of simp if the definitions are transparent

view this post on Zulip Jad Hamza (Gitter import) (May 23 2018 at 13:55):

@Matthieu Sozeau About transport tells me that transport is transparent when there are two files. When everything is in the same file, I get: transport is basically transparent but considered opaque for reduction

view this post on Zulip Jad Hamza (Gitter import) (May 23 2018 at 14:03):

When there are two files, Opaque transport. solves the slowness. Maybe I should just set all Equations definitions to Opaque?

view this post on Zulip Matthieu Sozeau (May 23 2018 at 15:46):

Indeed, for use with simp it’s better.

view this post on Zulip Matthieu Sozeau (May 23 2018 at 15:46):

The tactic should handle this for you though

view this post on Zulip Matthieu Sozeau (May 23 2018 at 15:46):

I’ve hit the problem a few times as well, I think this deserves an issue and a fix

view this post on Zulip Matthieu Sozeau (May 23 2018 at 15:47):

The fact that the Opaque flag is not exported properly is another one. I don’t know if I can do it from the plugin side, I’ll have to try

view this post on Zulip Aleksey Nogin (Gitter import) (May 23 2018 at 17:55):

Aleksey Nogin I’m almost done fixing #93 and supporting definitions whose return type is a function type everywhere

Thanks! Looking forward to using it. (Note however that returning a function type, as opposed to just passing an argument directly, was only needed as a workaround to some of the other issues I was hitting)

view this post on Zulip Matthieu Sozeau (May 23 2018 at 18:01):

Yes I know, but it's a necessary step to treat properly definitions like [Eqns foo : a -> b -> c := foo x := ...] which were requested as well and it fixes the treatment of partial applications of recursive calls when building the graph and a few other things. My branch fix93auto works entirely now, but for spurious induction hypotheses in the graph in some dependent cases. I think I'll merge that first and try to improve cleaning later.

view this post on Zulip Aleksey Nogin (Gitter import) (May 23 2018 at 18:02):

Ah, makes sense. Will you be backporting to v8.8 as well? Thanks!

view this post on Zulip Matthieu Sozeau (May 24 2018 at 12:12):

@Aleksey Nogin done, you can have a try

view this post on Zulip Aleksey Nogin (Gitter import) (May 29 2018 at 16:56):

@Matthieu Sozeau: Thanks a lot! I just filed two new issues, but not sure whether they are are something I care about - it could be that I am hitting them in my code because I have a placeholder case where I have not yet done the proper implementation - and it's that placeholder case that's triggering the issues, not something I'd actually care about. I will let you know what I find out once I replace the placeholder with the "real" implementation.

view this post on Zulip Matthieu Sozeau (May 29 2018 at 17:43):

Ok, still looks like legitimate bugs :)

view this post on Zulip Aleksey Nogin (Gitter import) (May 29 2018 at 22:48):

Ok, still looks like legitimate bugs :)

I was not sure, but seemed like worth reporting them anyway.

view this post on Zulip Aleksey Nogin (Gitter import) (May 29 2018 at 23:34):

I just reported mattam82/Coq-Equations#100 - this one I am actually blocked on... The error message is vague enough that I am not sure whether it's my fault or Equations', but even if it's mine, I do not see it...

view this post on Zulip Aleksey Nogin (Gitter import) (May 30 2018 at 14:21):

@Matthieu Sozeau, thanks a lot for pointing out where I was going wrong with mattam82/Coq-Equations#100. With my error fixed, I am now hitting mattam82/Coq-Equations#98 in a way that stumps me. Note that while in the simple example that I posted in mattam82/Coq-Equations#98, the error message shows up by itself, in my "production" implementation, it shows up in the middle of a long sequence of messages with things being successfully defined and obligations being successfully discharged...

view this post on Zulip Matthieu Sozeau (May 30 2018 at 17:20):

There’s something wrong in the inductive graph production, but I didn’t pinpoint where yet.

view this post on Zulip Matthieu Sozeau (May 30 2018 at 17:21):

With the (noind) option it should go through I suppose.

view this post on Zulip Matthieu Sozeau (May 31 2018 at 15:05):

@Aleksey Nogin found it and fixed it, this is a really good example exercising the mutual/nested/refinement combination, thanks!

view this post on Zulip Matthieu Sozeau (May 31 2018 at 15:05):

I'll backport to 8.8 once travis passes

view this post on Zulip Aleksey Nogin (Gitter import) (May 31 2018 at 18:16):

Thanks!

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 01 2018 at 14:57):

Any luck with that backport? Thanks! (travis timed out on 2nd-last fix98 commit, but seems like it succeeded on the last one).

view this post on Zulip Matthieu Sozeau (Jun 03 2018 at 18:01):

Yeah it’s strange, I’ll check tomorrow

view this post on Zulip Matthieu Sozeau (Jun 05 2018 at 10:32):

@Aleksey Nogin Fixes for 98, 99 and 100 are in 8.8 now

view this post on Zulip Matthieu Sozeau (Jun 05 2018 at 10:47):

Rather, 98 and 100

view this post on Zulip Jad Hamza (Gitter import) (Jun 05 2018 at 13:45):

@Matthieu Sozeau Thanks for looking into issue 96! Did you get a chance to look at https://github.com/mattam82/Coq-Equations/issues/75 ?
We have some examples where the "*_unfold_eq" Equations lemma take ~1 minute to prove

view this post on Zulip Matthieu Sozeau (Jun 05 2018 at 15:32):

Hmm, that's some delicate folding issue I guess, I'll try to see

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 05 2018 at 19:20):

@Matthieu Sozeau Thanks a lot! The "production" definition now produces a Non strictly positive occurrence of "foo_ind" error - I will try to create a minimized version for a bug report

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 05 2018 at 20:05):

I filed mattam82/Coq-Equations#104 about the new Non strictly positive error

view this post on Zulip Matthieu Sozeau (Jun 05 2018 at 20:10):

Thanks! I found one such issue when I started considering recursive calls under binders and fixed it, hopefully that one will go away as well

view this post on Zulip Matthieu Sozeau (Jun 06 2018 at 16:29):

@Aleksey Nogin Now fixed in 8.8... a bit more work needed to fix 85 as well

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 06 2018 at 23:13):

Thanks! Unfortunately, still getting an error with my current attempt at a "production" definition - filed mattam82/Coq-Equations#105.

view this post on Zulip Matthieu Sozeau (Jun 07 2018 at 07:57):

That’s another instance of #85 I think

view this post on Zulip Matthieu Sozeau (Jun 07 2018 at 19:07):

@Aleksey Nogin indeed that was a duplicate, both #105 and #85 are fixed in 8.8 now

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 07 2018 at 21:31):

Thanks! I am finally back to not having any blockers (at least none I am currently aware of)

view this post on Zulip Matthieu Sozeau (Jun 07 2018 at 21:54):

Cool, that elimination principle generation under binders was not ok :)

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 08 2018 at 03:00):

I just filed mattam82/Coq-Equations#106 and mattam82/Coq-Equations#107 that have me confused even more than usual. The latter is the one I actually care about, the former is what I hit when intending to reproduce and report the latter. The difference in outcomes between the two and the error message in the latter have me particularly confused. It could be that I am once again not counting my arguments correctly, like I previously did with mattam82/Coq-Equations#100 - but I double-checked a few times (but it's also 8PM after a long day here, so who knows what I am missing)...

view this post on Zulip Matthieu Sozeau (Jun 08 2018 at 17:27):

@Aleksey Nogin Well, I fixed a bunch of things today, hopefully that lets you go further. Have a good week-end :)

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 07:58):

@Matthieu Sozeau I have another example for issue https://github.com/mattam82/Coq-Equations/issues/75 where the *_unfold_eq lemma takes 4/5 minutes to prove. Is there a way to admit those lemmas?

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 11:02):

@Jad Hamza there’s no way currently. I’ll have a look. It should be rather immediate given the technique we use, it must be reflexivity taking a very long time to check a convertibility.

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 11:37):

Thanks

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 15:18):

@Matthieu Sozeau Thanks for fixing it! What do you mean by "the following lemma proof automation fails"?

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 15:20):

After the unfolding lemma there is the functional induction proof, which currently fails

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 15:21):

It can be proven by hand (it's a proof search failure when trying to use the admitted wf obligation proof) but then Coq anomalies because of a bug with obligations and universes

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 15:24):

@Matthieu Sozeau Ok I see, so I shouldn't upgrade coq-equations before Coq is upgraded to 8.8.1

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 15:25):

Nope, you can update, it can only get better :)

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 15:33):

@Matthieu Sozeau but then the lemmas won't pass anymore :) By the way when I do "opam upgrade coq-equations" it suggests I downgrade Coq to 8.7.2, is that normal?

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 15:43):

I don't think that's normal. If you do opam info coq-equations, what does it say?

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 15:44):

You can do [Next Obligation. apply admit. Defined] for that obligation to go further

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 15:45):

The functional elimination proof already failed before, even when you proved the unfolding lemma.

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 18:44):

@Matthieu Sozeau upstream-url: https://github.com/mattam82/Coq-Equations/archive/v1.0-8.8.tar.gz

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 18:44):

repository: coq-released

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 18:46):

@Matthieu Sozeau In my current version, the functional elimination proof goes through: "FunctionalElimination_foldLeft is defined"

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 19:05):

For the same code ?

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 19:07):

@Matthieu Sozeau yes I copied the code from issue 75

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 19:09):

Hmmm that’s surprising, I couldn’t make it go though before my patch.

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 19:10):

Are you sure it’s not admitted?

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 19:10):

hmm let me check

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 19:14):

@Matthieu Sozeau So I've pasted the code that ends with "Admit Obligations.", and I got that output: https://lpaste.net/5108456774994755584

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 19:28):

Ok, I’ll try to understand that tomorrow :smile:

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 19:29):

:)

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 20:03):

Ah I checked because it bugged me. That's because the eliminator in 1.0 is weaker and actually useless. In the current branch the recursive call under the lambda is recognized and that's what makes the proof different.

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 20:05):

@Matthieu Sozeau 1.0 is the version that I'm using, which is old? Why don't I get the current branch with opam?

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 20:07):

That's because the development branches are in the extra-dev repository. Actually I'm missing an 8.8.dev package.

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 20:09):

@Matthieu Sozeau If I don't need these eliminators can I disable them? (I only need f_equation_1/2/3)

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 20:10):

Yes, using the Equations (noind) foo option

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 20:11):

Awesome! Thanks

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 20:12):

The missing package is the reason why opam asks me to downgrade to 8.7.2 then

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 20:13):

Could be. But actually if you have 1.0+88 installed then there's no reason to downgrade to 1.0+8.7

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 20:13):

I've made a PR so that you can use the extra-dev package https://github.com/coq/opam-coq-archive/pull/344

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 20:14):

To add the opam repo you can simply do opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 20:14):

Beware that it will likely eagerly select versions from this repo when you might prefer released packages in general

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 20:18):

@Matthieu Sozeau not 1.0+8.7 but 8.7-dev

view this post on Zulip Jad Hamza (Gitter import) (Jun 11 2018 at 20:24):

Thanks for the PR!

view this post on Zulip Matthieu Sozeau (Jun 11 2018 at 20:37):

Ah. Makes sense

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 11 2018 at 22:33):

Is there a documentation for all the things Equations defines and how to use them? Am I supposed to use simp to replace an instance of an equation lhs with the corresponding rhs? I am having trouble where simp works for some equation-defined constructors and not for others (basically, referring to my issue reports, it seems to work correctly for the "production" version of "simp do_foo", and not do anything for the "production" version of "simp foo_type").

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:18):

I reported the issue I am having with simp in mattam82/Coq-Equations#111. I am currently blocked by mattam82/Coq-Equations#111 and mattam82/Coq-Equations#113...

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 08:27):

Hi @Matthieu Sozeau, is your fix for slow _unfold_eq part of the new 8.8.dev package?

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 08:28):

Yes nvm I see it in the commits of the 8.8 branch

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 08:30):

@Aleksey Nogin your Equations definition doesn't go through for me on 1.0.8.8

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:30):

@Jad Hamza which definition are you referring to?

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 08:31):

of issue 111

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 08:31):

Equations num

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:33):

Yes, you would likely need to use the latest development version (I am using the latest v8.8 branch) - I reported and @Matthieu Sozeau fixed a bunch of bugs related to these kinds of definitions before I became able to get to this one.

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 08:37):

@Aleksey Nogin Ok I see. I'm not sure at all but I think simp works only on num but not on foo_type. simp num should replace num (List nil) by fun val => 0 for instance. (Similar to rewrite num_equation_1 in *, and num_equation_2, etc)

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:38):

In the specific example, it works on neither...

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 08:39):

@Aleksey Nogin what about num_equation_1?

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:42):

Ah, sorry, "simp num" works once it actually have something to work on (my example does not get there). But still having the issue of not knowing how to rewrite foo_type(List l)

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:50):

Once that is solved, I would need to figure out how to set up a proper mutual induction that would enable me to actually prove the sample lemma.

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 09:04):

@Aleksey Nogin I compiled the 8.8 branch but I still cannot compile your example (fails on the struct keyword)

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:15):

Weird. Are you using an IDE? I somewhat regularly have issues with CoqIDE getting into a weird state and complaining about random things (like the struct keyword). Clicking the "restart Coq" button and then going back solves it - at least until it happens again.

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 09:25):

@Aleksey Nogin you're right I had to restart emacs :)

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 09:27):

@Aleksey Nogin intro. induction f. intros. simpl in *. unfolds the definition of foo_type (cbn instead of simpl works as well)

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:37):

@Jad Hamza - thanks, but unfortunately it looks like that was not the real issue - still no clue how to actually prove the lemma...

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:39):

I am currently trying ```Equations (struct f) num (f:foo) (val:foo_type f) : nat := {
num (List nil) val := 0;
num (List (cons hd tl)) val := sum hd (fun val => num hd val) tl val }
where (struct fs) sum (f:foo) (numf: (foo_type f -> nat)) (fs : list foo) (val: compact_prod (map foo_type (f::fs))) : nat := {
sum f numf nil val := numf val;
sum f numf (cons hd tl) val := numf (fst val) + sum hd (fun val => num hd val) tl (snd val)}.

Lemma num_zero: forall (f:foo) (val:foo_type f), num f val = 0. Check num_elim.
Proof. refine (proj1 (num_elim (fun f n v => v = 0) (fun f nf fs val s => s = 0) _ _ _ _)); intros; auto.


view this post on Zulip Matthieu Sozeau (Jun 12 2018 at 09:39):

@Aleksey Nogin for mutual induction you should probably call the eliminator using apply funelim (f:=num f) rather than doing an induction on f which doesn’t give you the right induction hypotheses for the List case.

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 09:41):

@Matthieu Sozeau I've tried your fix on the example for the issue and it works well, thanks! Unfortunately I have another example which is still very slow

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:41):

Wrong argument name: f.

view this post on Zulip Matthieu Sozeau (Jun 12 2018 at 09:41):

Probably in the second predicate you need to have (forall v, numf v = 0)

view this post on Zulip Matthieu Sozeau (Jun 12 2018 at 09:43):

@Aleksey Nogin your call to num_elim is equivalent

view this post on Zulip Matthieu Sozeau (Jun 12 2018 at 09:47):

Or rather, (forall v, nf v = 0) -> s = 0 I suppose

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:49):

For funelim, this was the first thing I tried, but I have not figured out how I am supposed to call it. E.g.

Equations (struct f) num (f:foo) (val:foo_type f) : nat := {
  num (List nil) val := 0;
  num (List (cons hd tl)) val := sum hd (fun val => num hd val) tl val }
where (struct fs) sum (f:foo) (numf: (foo_type f -> nat)) (fs : list foo) (val: compact_prod (map foo_type (f::fs))) : nat := {
  sum f numf nil val := numf val;
  sum f numf (cons hd tl) val := numf (fst val) + sum hd (fun val => num hd val) tl (snd val)}.

Lemma num_zero (f:foo) (val:foo_type f): num f val = 0.
Proof. funelim (num f val).

Gives me

In nested Ltac calls to "funelim" and "funelim_JMeq_tac", last call failed.

view this post on Zulip Matthieu Sozeau (Jun 12 2018 at 09:50):

Right. I didn't figure out yet how to make the tactic take additional predicates for mutual/nested definitions. So you have to call the eliminator directly like you did.

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:54):

Ah, OK, the following works indeed:

Equations (struct f) num (f:foo) (val:foo_type f) : nat := {
  num (List nil) val := 0;
  num (List (cons hd tl)) val := sum hd (fun val => num hd val) tl val }
where (struct fs) sum (f:foo) (numf: (foo_type f -> nat)) (fs : list foo) (val: compact_prod (map foo_type (f::fs))) : nat := {
  sum f numf nil val := numf val;
  sum f numf (cons hd tl) val := numf (fst val) + sum hd (fun val => num hd val) tl (snd val)}.

Lemma num_zero: forall (f:foo) (val:foo_type f), num f val = 0. Check num_elim.
Proof. refine (proj1 (num_elim (fun f n v => v = 0) (fun f nf fs val s => (forall v, nf v = 0) -> s = 0) _ _ _ _)); intros; auto.
simpl in val. destruct val. simpl. rewrite H1. simpl in H0. rewrite H0; auto.

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:55):

Thanks a lot - I guess I will be able to figure it out from here - that is, once I know how to deal with mattam82/Coq-Equations#113...

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 09:58):

@Matthieu Sozeau https://lpaste.net/1238354859460132864 I didn't reduce much to make sure I don't oversimplify

view this post on Zulip Matthieu Sozeau (Jun 12 2018 at 10:13):

Hmm, #113 is again about what is recursive and what is not it seems.

view this post on Zulip Matthieu Sozeau (Jun 12 2018 at 10:15):

@Jad Hamza https://lpaste.net/7506427794780323840

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 10:20):

@Matthieu Sozeau so what's happening?

view this post on Zulip Matthieu Sozeau (Jun 12 2018 at 10:22):

I would rather avoid doing pattern-matching in the right-hand side like here, although that's possible of course. About the slowness it seems that there is retypechecking taking a different conversion path which explodes again

view this post on Zulip Jad Hamza (Gitter import) (Jun 12 2018 at 10:26):

alright, thanks! It's anyways much faster than before your fix :) the style is indeed terrible but it's hard for us to do it differently since this is translated from another language. Or we would have to include some special cases than translate the pattern matching to a case analysis on the left hand side

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 17:39):

@Matthieu Sozeau Thanks so much for all the fixes - will hopefully be able to get my "production" code going again :smile: ! Just hoping I still have enough time to finish my "production" work in time for a big demo I have next Tuesday :worried: .

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 17:45):

Hm, Solving obligations automatically... seems to be getting stuck on one of my equations :( Will try to minimize/reproduce/report...

view this post on Zulip Matthieu Sozeau (Jun 12 2018 at 18:47):

@Anogin probably looping, that was reported already. Obligation Tactic := program_simplify might help.

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 12 2018 at 23:30):

I reported mattam82/Coq-Equations#116 on nontermination and a potentially related mattam82/Coq-Equations#117 where a very similar code results in another Illegal Application. Obligation Tactic := program_simplify. does not seem to make any difference for the non-terminating example.

view this post on Zulip Aleksey Nogin (Gitter import) (Jun 13 2018 at 21:35):

@Matthieu Sozeau - my "production" version compiles again - thanks!

view this post on Zulip Aleksey Nogin (Gitter import) (Jul 13 2018 at 03:38):

@Matthieu Sozeau: with all your fixes, I was able to finish all the proofs I wanted to do for an initial set of definitions I wanted to define - thanks so much!!! But now hit another issue with a new definition :( I filed mattam82/Coq-Equations#130.

view this post on Zulip Pierre Courtieu (Dec 07 2018 at 09:16):

Hi there!

view this post on Zulip Pierre Courtieu (Dec 07 2018 at 09:16):

Any news about the replacement of Function backend?

view this post on Zulip Matthieu Sozeau (Dec 07 2018 at 12:15):

@Pierre Courtieu that's still on my list. I'm finishing a rewriting and cleanup of the Equations' handling of fixpoints (including nested well-founded ones) that should make the translation from a constrexpr/glob_constr to an input of Equations easier.

view this post on Zulip Pierre Courtieu (Dec 19 2018 at 16:40):

great

view this post on Zulip Jad Hamza (Gitter import) (Dec 21 2018 at 09:22):

Hello, are mutually recursive equations with measures supported?

view this post on Zulip Jad Hamza (Gitter import) (Dec 21 2018 at 09:44):

Require Import Equations.Equations.

Equations even (n: nat): Prop :=
  even n by rec n lt :=

  even 0 := True;
  even (S n) := odd n

where odd (n: nat): Prop :=
  odd n by rec n lt :=

  odd 0 := False;
  odd (S n) := even n
.

Here of course we don't need to use the custom by measures but in general is that supported?

view this post on Zulip Matthieu Sozeau (Dec 21 2018 at 10:39):

Nesting is supported but not mutual well-founded. For that you’d need an n-ary FixWf combinator. Using dependent pattern-matching you can encode it by defining even_odd (b : bool) (n : nat) : Prop though.

view this post on Zulip Jad Hamza (Gitter import) (Dec 21 2018 at 14:29):

I see thanks

view this post on Zulip Yannick Forster (Gitter import) (Apr 03 2019 at 13:42):

There was a question on Coq club where I wanted to jump in and say "Equations does exactly what you want!"... except it doesn't, at least not for me

view this post on Zulip Yannick Forster (Gitter import) (Apr 03 2019 at 13:42):

If I do

view this post on Zulip Yannick Forster (Gitter import) (Apr 03 2019 at 13:42):

From Equations Require Import Equations.

Inductive eType : Set := Integer | Boolean.

Inductive unop : eType -> Type :=
  Neg : unop Integer
| Not : unop Boolean.

Lemma a : forall x : unop Integer, x = Neg.
Proof.
  intros. depelim x.

view this post on Zulip Yannick Forster (Gitter import) (Apr 03 2019 at 13:43):

I get H : {| pr1 := Integer; pr2 := x0 |} = {| pr1 := Integer; pr2 := Neg |} as assumption. That can be manually eliminated using EqDec.inj_right_pair, but that's somewhat unsatisfying

view this post on Zulip Yannick Forster (Gitter import) (Apr 03 2019 at 13:44):

Weirdly, if I do Set Equations With UIP. Axiom uipa : forall A, UIP A. Existing Instance uipa. before, that doesn't change anything

view this post on Zulip Yannick Forster (Gitter import) (Apr 03 2019 at 13:44):

Am I doing something wrong or should I file a bug?

view this post on Zulip Matthieu Sozeau (Apr 03 2019 at 13:46):

You don't need UIP, but Derive NoConfusion for eType unop

view this post on Zulip Matthieu Sozeau (Apr 03 2019 at 13:48):

dependent elimination x would tell you

view this post on Zulip Matthieu Sozeau (Apr 03 2019 at 13:48):

depelim is an Ltac wrapper that does things a bit differently, trying to be closer to Program's depelim

view this post on Zulip Matthieu Sozeau (Apr 03 2019 at 13:49):

Actually NoConfusion for eType is enough here

view this post on Zulip Yannick Forster (Gitter import) (Apr 03 2019 at 13:52):

Oh, so actually the behaviour is quite perfect :)

view this post on Zulip Yannick Forster (Gitter import) (Apr 03 2019 at 13:53):

And (contrarily to what Gaëtan stated on the list) there's no axiom needed

view this post on Zulip Jad Hamza (Gitter import) (Dec 05 2019 at 21:29):

Hello, is anyone able to use coq-equations master with coq master? I'm getting an error File not found on loadpath : equations_plugin.cmxs when trying to use coq master + coq-equations master (either compiled from source using make, or installed through opam with the dev versions) on files with equations

view this post on Zulip Jad Hamza (Gitter import) (Dec 06 2019 at 06:53):

(The file equations_plugin.cmxs does not appear at all in the folder of the dev opam switch)

view this post on Zulip Matthieu Sozeau (Dec 06 2019 at 14:38):

Strange, I'll have a look

view this post on Zulip Jad Hamza (Gitter import) (Dec 07 2019 at 08:51):

Thanks! Aren't there continuous integration tests that make sure coq-equations master is always working with coq master?

view this post on Zulip Matthieu Sozeau (Dec 08 2019 at 11:19):

There are, but I don't think they test the installation

view this post on Zulip Matthieu Sozeau (Dec 08 2019 at 11:41):

@Jad Hamza indeed the install target was broken and only the vo's were installed, fixed now

view this post on Zulip Matthieu Sozeau (Dec 08 2019 at 11:42):

That was fixed in 8.10 already but not ported in master, sorry

view this post on Zulip Jad Hamza (Gitter import) (Dec 08 2019 at 14:27):

@Matthieu Sozeau Thanks! I think it's working now in opam

view this post on Zulip Jad Hamza (Gitter import) (Dec 08 2019 at 14:36):

Hm wait, is it still Equations.Equations that I should import?

Error: Unable to locate library Equations.Equations.

view this post on Zulip Matthieu Sozeau (Dec 08 2019 at 14:42):

From Equations Require Import Equations. Should work I think

view this post on Zulip Matthieu Sozeau (Dec 08 2019 at 14:42):

From Equations Require Import Equations should work

view this post on Zulip Jad Hamza (Gitter import) (Dec 08 2019 at 14:52):

Thanks, working now

view this post on Zulip Mukesh Tiwari (Gitter import) (Dec 16 2019 at 01:39):

Require Import Equations.Equations.
Require Vectors.Vector.
Arguments Vector.nil {A}.
Arguments Vector.cons {A} _ {n}.
Notation vnil := Vector.nil.
Notation vcons := Vector.cons.

Equations prod {F G n}  (f : G -> F -> G) (g : G -> G -> G)
  (v : Vector.t G (S n)) (w : Vector.t F (S n)) :  G :=
  prod f g (vcons h nil) (vcons m nil) := f h m;
  prod f g (vcons h hs)  (vcons m ms)  :=
        g (f h m) (prod f g hs ms).

view this post on Zulip Mukesh Tiwari (Gitter import) (Dec 16 2019 at 01:40):

I am getting this error

view this post on Zulip Mukesh Tiwari (Gitter import) (Dec 16 2019 at 01:41):

Error:
In environment
prod :
let H := fixproto in
forall (F G : Type) (n : nat),
(G -> F -> G) -> (G -> G -> G) -> Vector.t G (S n) -> Vector.t F (S n) -> G
F : Type
G : Type
f : G -> F -> G
g : G -> G -> G
h : G
m : F
ms : Vector.t F 0
hs := vnil : Vector.t G 0
The term "hs" has type "Vector.t G 0" while it is expected to have type "Vector.t G (S ?n)".

view this post on Zulip Paolo Giarrusso (Dec 16 2019 at 03:40):

Maybe a bug, but as a workaround I’d try to spell out the match against n and/or hs (and/or ms)

view this post on Zulip Paolo Giarrusso (Dec 16 2019 at 03:41):

the first line should match n against 0, the second against S n; it seems Equations fails to infer that

view this post on Zulip Mukesh Tiwari (Gitter import) (Dec 16 2019 at 04:05):

@Paolo G. Giarrusso Thanks. I manged to rewrite it.

Equations prod {F G}  (f : G -> F -> G) (g : G -> G -> G)
          (n : nat) (v : Vector.t G (S n)) (w : Vector.t F (S n)) :  G :=
  prod f g 0 _ _ := _;
  prod f g (S n) (vcons h hs)  (vcons m ms)  :=
        g (f h m) (prod f g n hs ms).
Next Obligation.
  inversion_clear v;
    inversion_clear w.
  exact (f h h0).
Defined.

view this post on Zulip Mukesh Tiwari (Gitter import) (Dec 16 2019 at 05:52):

Nevermind. I think I got the idea.

view this post on Zulip Mukesh Tiwari (Gitter import) (Dec 16 2019 at 05:53):

Equations prod {F G n}  (f : G -> F -> G) (g : G -> G -> G)
          (v : Vector.t G (S n)) (w : Vector.t F (S n)) : G :=
  prod (n := 0) f g (vcons m _) (vcons h _) := f m h;
  prod (n := (S n)) f g (vcons h hs) (vcons m ms)  :=
     g (f h m) (prod f g hs ms).

view this post on Zulip Matthieu Sozeau (Dec 16 2019 at 09:19):

@Mukesh Tiwari it seems nil was understood as a variable

view this post on Zulip Paolo Giarrusso (Dec 16 2019 at 11:00):

Doh, it should have been vnil not nil ?

view this post on Zulip Matthieu Sozeau (Dec 16 2019 at 11:15):

I guess. Probably nil was not exported.

view this post on Zulip Mukesh Tiwari (Gitter import) (Dec 16 2019 at 11:32):

@Matthieu Sozeau Thank you.

view this post on Zulip Mukesh Tiwari (Gitter import) (Dec 16 2019 at 11:33):

Totally feeling stupid that how did I missed it :(

view this post on Zulip Paolo Giarrusso (Dec 16 2019 at 12:19):

yeah, but you're in good company, so no worries :-)

view this post on Zulip Matthieu Sozeau (Dec 16 2019 at 13:18):

I was bitten by it before, that’s why I thought of it :)

view this post on Zulip Daniel Patterson (Gitter import) (Jan 02 2020 at 16:03):

Hi there -- I'm trying to use the mutual well-founded encoding described here: http://mattam82.github.io/Coq-Equations/examples/Examples.mutualwfrec.html -- but I'm running into issues with an error message "Too many patterns in clauses for this type" that I don't understand. I changed the provided example (the second encoding) relatively minimally to get the following reproduction:

Equations bmeasure (s : bool) (e : if s then nat else Z) : nat := {
bmeasure true e := e;
bmeasure false e := Z.to_nat e
}.

view this post on Zulip Karl Palmskog (Jan 02 2020 at 16:42):

what's your Coq version? that code works fine for me on Coq 8.10.2

view this post on Zulip Daniel Patterson (Gitter import) (Jan 02 2020 at 16:42):

8.10.2 with equations 1.2.1+8.10

view this post on Zulip Karl Palmskog (Jan 02 2020 at 16:43):

same here, and I can't see any error there

view this post on Zulip Karl Palmskog (Jan 02 2020 at 16:44):

is that supposed to trigger the error?

view this post on Zulip Daniel Patterson (Gitter import) (Jan 02 2020 at 16:44):

Oh, shoot. Must be some other library interfering again -- I _was_ being careful about running these in isolation from the rest of the development but forgot in this case. Sorry!

view this post on Zulip Karl Palmskog (Jan 02 2020 at 16:44):

indeed Equations is very sensitive to Requires

view this post on Zulip Daniel Patterson (Gitter import) (Jan 02 2020 at 16:48):

Thanks @Karl Palmskog :)

view this post on Zulip Daniel Patterson (Gitter import) (Jan 02 2020 at 16:52):

Hmm. It seems Set Implicit Arguments. causes this error.

view this post on Zulip Paolo Giarrusso (Jan 02 2020 at 18:12):

If that’s the bug, does it disappear if you make s implicit manually?

view this post on Zulip Paolo Giarrusso (Jan 02 2020 at 18:14):

(On phone, but set implicit arguments might be marking that implicit automatically, causing confusion)

view this post on Zulip Daniel Patterson (Gitter import) (Jan 02 2020 at 20:30):

It doesn't work with s implicit (I assume you mean {s : bool}), whether Set Implicit Arguments is set or not.

view this post on Zulip Matthieu Sozeau (Jan 03 2020 at 10:10):

If you use {s} then indeed you have to give an explicit bmeasure (s:=true/false) in the clauses.

view this post on Zulip Karl Palmskog (Jan 03 2020 at 10:43):

is there a way to refer to (or specify the name of) the whole "superterm" of a pattern-matched parameter? E.g., I want to refer to S n' as only n in myeq (S n') := ...;

view this post on Zulip Karl Palmskog (Jan 03 2020 at 10:44):

the intuition is that in manual matches, I always have the name of the variable I match on

view this post on Zulip Karl Palmskog (Jan 03 2020 at 10:45):

one could imagine a syntax myeq n#(S n') := ..., or maybe I'm missing something

view this post on Zulip Paolo Giarrusso (Jan 03 2020 at 13:49):

@Karl Palmskog have you tried the Gallina syntax (S n') as n ? Equations should ideally use the same, IMO (and maybe it does already?) Reference at https://coq.inria.fr/refman/addendum/extended-pattern-matching.html#aliasing-subpatterns if needed

view this post on Zulip Karl Palmskog (Jan 03 2020 at 14:12):

@Paolo G. Giarrusso indeed I tried this syntax, it doesn't work as far as I can tell

view this post on Zulip Karl Palmskog (Jan 03 2020 at 14:13):

unless @Matthieu Sozeau thinks otherwise I can write an issue with the feature request

view this post on Zulip Matthieu Sozeau (Jan 05 2020 at 03:50):

Yep it would be nice, sadly as is not part of the term grammar only the pattern one

view this post on Zulip Jakob Botsch Nielsen (Feb 12 2020 at 12:15):

Equations? egcd_aux (r0 a0 b0 r1 a1 b1 : bigZ) : Z * Z
  by wf (BigZ.log2 (BigZ.abs r0) + BigZ.log2 (BigZ.abs r1))
        (fun n m => 0 <= n < m) :=
egcd_aux r0 a0 b0 r1 a1 b1 with BigZ.div_eucl r0 r1 :=
  | (q, r) with dec (r =? 0) := {
    | left _ := ([a1], [b1]);
    | right _ := egcd_aux r1 a1 b1 r (a0 - q*a1) (b0 - q*b1)
  }.

How can I keep the equality BigZ.div_eucl r0 r1 = (q, r) around when proving that the measure is decreasing?

view this post on Zulip Matthieu Sozeau (Feb 12 2020 at 13:05):

You can use the "inspect" pattern by first defining a function inspect : forall {A} (a : A), { x : A | x = a } and pattern-matching on inspect (BigZ.div_eucld r0 r1)

view this post on Zulip Jakob Botsch Nielsen (Feb 13 2020 at 23:20):

Thanks

view this post on Zulip Karl Palmskog (Feb 28 2020 at 12:36):

@Matthieu Sozeau any chance of a release of Equations for 8.11 in the near future?

view this post on Zulip Matthieu Sozeau (Feb 28 2020 at 12:53):

I'm actually working on it right now. There's an issue in the HoTT version

view this post on Zulip Karl Palmskog (Feb 28 2020 at 12:54):

:thumbsup:

view this post on Zulip Karl Palmskog (Feb 28 2020 at 13:00):

are there plans to do actual releases of coq-hott? It's not great to have a "stable" package have a depopt on an experimental package, this could potentially break at any time...

view this post on Zulip Karl Palmskog (Feb 28 2020 at 13:00):

right now, we are not even testing that in Guillaume Claret's coq-bench

view this post on Zulip Karl Palmskog (Feb 28 2020 at 13:19):

(for the record, the HoTT repo also takes a long, long time to clone, releases would elide this)

view this post on Zulip Bas Spitters (Feb 28 2020 at 20:32):

@Karl Palmskog https://github.com/HoTT/HoTT/releases

view this post on Zulip Bas Spitters (Feb 28 2020 at 20:32):

But I guess you mean updating opam?

view this post on Zulip Karl Palmskog (Feb 28 2020 at 20:32):

@Bas Spitters right, yes, so coq-equations can depend on it

view this post on Zulip Karl Palmskog (Feb 28 2020 at 20:33):

does V8.10 release work with stock Coq 8.10.2, etc.?

view this post on Zulip Bas Spitters (Feb 28 2020 at 20:34):

Yep, that issue is still open. Hope we can get to it next week. https://github.com/HoTT/HoTT/issues/1132

view this post on Zulip Bas Spitters (Feb 28 2020 at 20:35):

Yes, I don't think anything was broken since then.

view this post on Zulip Karl Palmskog (Feb 28 2020 at 20:35):

OK, we are happy to help out with refining OPAM stuff once someone opens a PR

view this post on Zulip Karl Palmskog (Feb 28 2020 at 20:36):

they even allow multi-line code suggestions these days in PRs...

view this post on Zulip Bas Spitters (Feb 28 2020 at 20:36):

@Matthieu Sozeau, @alizter has been looking at hott equations. I believe his experiments were mostly positive.

view this post on Zulip Bas Spitters (Feb 28 2020 at 20:37):

@Karl Palmskog Thanks!

view this post on Zulip Matthieu Sozeau (Mar 01 2020 at 12:45):

@Bas Spitters Cool, I just been fixing a bug on master for hott-equations. I should have a release for 8.11 upcoming as well. I'd love to have a stable hott package to depend on too :)

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

Well, I can't release hott-equations until we have a coq-hott-8.11 package in fact

view this post on Zulip Bas Spitters (Mar 01 2020 at 13:08):

@Matthieu Sozeau I've asked @alizter to look into it. He's interning in Aarhus at the moment.

view this post on Zulip Jad Hamza (Gitter import) (Mar 07 2020 at 08:01):

Thanks for the Equations opam release for 8.11 :)
I noticed that simp f in * is in general slow compared to rewrite f_equation_1 in * || ... || rewrite f_equation_n in * (at least when f is marked Opaque), could it be that simp doesn't respect opacity?

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

It might just be because simp f also calls typeclasses eauto with f after the autorewrite

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

But it does call autorewrite so should be the same as explicit rewrites

view this post on Zulip Jad Hamza (Gitter import) (Mar 10 2020 at 13:16):

Ah thanks, so I should write autorewrite with f if I want the same effect without eauto?

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

Yes

view this post on Zulip Jad Hamza (Gitter import) (Mar 10 2020 at 13:18):

Thanks :)

view this post on Zulip Jad Hamza (Gitter import) (Mar 10 2020 at 13:59):

I tried this change https://github.com/epfl-lara/SystemFR/commit/8fe17d0925cafdf73be50d6606cec00111a641bf but this slows down the proofs by a large factor. But that doesn't seem to be coq equations issue, rather a difference of behavior between rewrite and autorewrite

view this post on Zulip Paolo Giarrusso (Mar 10 2020 at 14:11):

@Jad Hamza Hi! Assuming the lia change is not involved, autorewrite will iterate rewrites, like repeat rewrite; while your earlier code only rewrites once.

view this post on Zulip Jad Hamza (Gitter import) (Mar 10 2020 at 14:12):

Yes the lia change is not related (only local to proving obligations)

view this post on Zulip Jad Hamza (Gitter import) (Mar 10 2020 at 14:12):

Yes you're right that might cause the difference, but simp_red is often used within repeat

view this post on Zulip Jad Hamza (Gitter import) (Mar 10 2020 at 14:40):

(I tried with this change https://github.com/epfl-lara/SystemFR/pull/11/files, still faster than the autorewrite version)

view this post on Zulip Paolo Giarrusso (Mar 10 2020 at 14:43):

(any chance you need repeat also on the other variants of those tactics?) But Robbert Krebbers has complained about autorewrite performance a lot, but it being slower than repeat rewrite is surprising.

view this post on Zulip Paolo Giarrusso (Mar 10 2020 at 14:44):

(surprising to me)

view this post on Zulip Paolo Giarrusso (Mar 10 2020 at 14:45):

(maybe performance of autorewrite is best discussed in coq/coq? For instance, Jason Gross has been working on rewriting tactics and comparing with rewrite_strat)

view this post on Zulip Paolo Giarrusso (Mar 10 2020 at 14:49):

maybe unrelated: IIRC, Equations uses Opaque which is ignored by some tactics, and by conversion checking. I wonder if something like stdpp’s sealing https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/base.v#L42 would be better (see https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/namespaces.v#L11 for the use pattern).

view this post on Zulip Paolo Giarrusso (Mar 10 2020 at 14:51):

that relies on Qed, which is actually Opaque, and it allows you to give a definition which is actually equal to its body only propositionally and not definitionally.

view this post on Zulip Jad Hamza (Gitter import) (Mar 10 2020 at 18:58):

Thanks! Moving there

view this post on Zulip Matthieu Sozeau (Mar 11 2020 at 12:45):

You might indeed want a more refined rewrite strategy (using rewrite_strat)

view this post on Zulip Matthieu Sozeau (Mar 11 2020 at 12:46):

I think autorewrite does not bypass opacity though

view this post on Zulip Matthieu Sozeau (Mar 11 2020 at 12:46):

But I might be wrong :)

view this post on Zulip Jad Hamza (Gitter import) (Mar 11 2020 at 12:52):

rewrite_strat indeed worked well! (and faster than repeat rewrite) after a few adjustments (importing RelationClasses and defining a few missing instances)

view this post on Zulip Paolo Giarrusso (Mar 11 2020 at 18:06):

@Jad Hamza oh, is rewrite_strat just faster or do you need to do optimizations yourself? I use Autosubst which uses autorewrite, and its performance is annoying

view this post on Zulip Jad Hamza (Gitter import) (Mar 11 2020 at 18:28):

I think it was faster out of the box (using this: https://github.com/epfl-lara/SystemFR/blob/7eff4ae12a8441001f49c58f3dea93758e78090f/ReducibilityDefinition.v#L213-L225), but I cannot tell for sure because some proofs didn't go through automatically and I had to do adjustments. There seems to be a difference with rewrite in *, which doesn't rewrite under binders while rewrite_strat maybe does? So I ended up using variants in these places such as simp_red_top_level_hyp, which will only rewrite top level occurrences. After all these changes (in commit https://github.com/epfl-lara/SystemFR/commit/7eff4ae12a8441001f49c58f3dea93758e78090f), the build using make -j10 went from around ~12min45 to ~11min20 (I didn't run these many times so these times may be off). Also, I didn't try other strategies (topdown or bottomup or innermost). Tell me your results if you try something :)

view this post on Zulip Paolo Giarrusso (Mar 11 2020 at 18:36):

ah, there's https://github.com/coq/coq/issues/6105 on this

view this post on Zulip Matthieu Sozeau (Mar 12 2020 at 09:44):

rewrite_strat uses congruence lemmas and produces smaller proof terms a priori, but indeed it's not 100% the same as autorewrite's strategy which is just repeat rewrite

view this post on Zulip Bas Spitters (Mar 15 2020 at 13:44):

Idris2 has some cool technology to generate programs from a type. Apparently, it originated here:
https://hackage.haskell.org/package/djinn
has anyone looked at porting it to Coq?

view this post on Zulip Paolo Giarrusso (Mar 15 2020 at 14:02):

isn’t that based on a foundation similar to tauto? if so, is there any significant difference in engineering?

view this post on Zulip Paolo Giarrusso (Mar 15 2020 at 14:06):

in particular, they're both based on decision procedures for LJT by Roy Dyckhoff (as Augustsson describes e.g. in http://lambda-the-ultimate.org/node/1178; https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.tauto); but I could easily miss some subtlety...

view this post on Zulip Bas Spitters (Mar 15 2020 at 14:43):

Yes, I think the basic algorithms are there, and one could hope that it can be put together cheaply, but I haven't looked into it deeply, as I would expect someone has done so already.

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

applications seem to be quite limited, basically a special case of synthesis

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

something like Isabelle's Nitpick would be more valuable, and solves a similar problem

view this post on Zulip Bas Spitters (Mar 15 2020 at 16:51):

Edwin referred to it as a "magic trick". Jasmin has been promising nitpick for DTT for some time, but I could find much progress. Do you happen to know more?

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

@Bas Spitters Nunchaku is still being worked on by Jasmin's collaborator: https://github.com/nunchaku-inria/nunchaku

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

but no Coq integration available to my knowledge

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

it wouldn't surprise me if they do Lean integration first, since that's what Jasmin's current project targets

view this post on Zulip Bas Spitters (Mar 15 2020 at 20:29):

That project doesn't seem very active

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

the main author is in industry these days

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

to be honest, I don't think any focused efforts will happen (w.r.t. counter-example generation and synthesis etc.) for Coq unless someone gets specific funds for it, I would say postdoc level for 1+ year or something like that

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

Jasmin has one postdoc working on tools part-time (Gabriel Ebner), but my understanding is he mostly works on the hammer for Lean

view this post on Zulip Bas Spitters (Mar 15 2020 at 21:14):

Would a hammer for lean be fundamentally different from a hammer for Coq?

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

it looks like they chose to implement it quite differently

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

I think the most design choices are in how to map the type theory to TPTP format and how to do reconstruction

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

for CoqHammer, they (Kalizcyk and Csajka) chose to implicitly use an intermediate calculus "CIC0" and write custom reconstruction tactics

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

I think Jasmin and Gabriel are following Sledgehammer more closely

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

they also implement it in C++ to hook into Lean's implementation: https://leanprover-community.github.io/archive/113488general/28743Hammertalk.html

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

https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_ebner.pdf

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

ah right, they target HOL instead of CIC0 it seems

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

I’m trying to port an old project from coq 8.8 and I seem to have problems with Equations.
For instance

Derive NoConfusion for nat.

gives off the warning

Solve Obligations tactic returned error: Tactic failure: Equations.Init.solve_noconf has not been bound yet.
This will become an error in the future [solve_obligation_error,tactics]

twice.
And it leaves me to prove no confusion myself.

I import Equations with

From Equations Require Import Equations.
Require Import Equations.Prop.DepElim.

and use 1.2.1+8.11

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

I guess I’m missing something but I can’t figure it out. If someone knows, thanks. :)

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

Swap the imports

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

It messes with tactic redéfinitions

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

Oh… It’s that simple, thanks!

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

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 15:12):

Yes

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

@Cyril Cohen

view this post on Zulip PLBegay (Gitter import) (Apr 23 2020 at 14:08):

Hi everyone, when trying to install coq-equations 1.2+8.9 or 1.2.1+8.9 via opam on two different computers, I get an error (the sources couldn't be obtained, curl error code 500). I did add the https://coq.inria.fr/opam/released repo and I'm pretty sure it was working yesterday. Thanks in advance !

view this post on Zulip Paolo Giarrusso (Apr 23 2020 at 16:37):

@PLBegay releases are hosted on GitHub and GitHub was down. Please try again now that GitHub is up.

view this post on Zulip PLBegay (Gitter import) (Apr 23 2020 at 16:41):

@Paolo G. Giarrusso It indeeds works like a charm now, thanks!


Last updated: Mar 28 2024 at 21:01 UTC