## Stream: Equations devs & users

### Topic: imported from gitter room coq/Equations

Hi there!

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

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

Great!

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

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

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

#### Matthieu Sozeau (Apr 12 2018 at 09:00):

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

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

#### Jad Hamza (Gitter import) (Apr 13 2018 at 11:49):

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

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

#### Matthieu Sozeau (Apr 19 2018 at 16:39):

The new package is being tested

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

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

#### Matthieu Sozeau (Apr 25 2018 at 12:57):

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

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

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

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

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

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

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

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

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

#### Aleksey Nogin (Gitter import) (May 03 2018 at 20:54):

@Matthieu Sozeau: Thank you!

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

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

#### Matthieu Sozeau (May 14 2018 at 18:04):

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

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

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

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

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

#### Aleksey Nogin (Gitter import) (May 14 2018 at 18:31):

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

nested recursion

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

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

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

#### Matthieu Sozeau (May 16 2018 at 16:16):

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

#### Matthieu Sozeau (May 16 2018 at 16:39):

@Aleksey Nogin the patches are on 8.8 now

Thanks!

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

#### Jad Hamza (Gitter import) (May 17 2018 at 13:17):

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

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

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

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

Argh

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

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

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

#### Jad Hamza (Gitter import) (May 17 2018 at 13:31):

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

#### Jad Hamza (Gitter import) (May 17 2018 at 13:31):

(with only two expressions to rewrite)

#### Jad Hamza (Gitter import) (May 17 2018 at 13:35):

Is there a known slowness issue here?

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

#### Matthieu Sozeau (May 17 2018 at 13:44):

Yes many tactics do not respect Opaque

#### Matthieu Sozeau (May 17 2018 at 13:45):

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

#### Matthieu Sozeau (May 17 2018 at 13:45):

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

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

#### Matthieu Sozeau (May 17 2018 at 14:39):

Probably an issue with backtracking

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

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

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

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

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

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

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

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

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

#### Matthieu Sozeau (May 23 2018 at 15:46):

Indeed, for use with simp it’s better.

#### Matthieu Sozeau (May 23 2018 at 15:46):

The tactic should handle this for you though

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

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

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

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

#### Aleksey Nogin (Gitter import) (May 23 2018 at 18:02):

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

#### Matthieu Sozeau (May 24 2018 at 12:12):

@Aleksey Nogin done, you can have a try

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

#### Matthieu Sozeau (May 29 2018 at 17:43):

Ok, still looks like legitimate bugs :)

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

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

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

#### Matthieu Sozeau (May 30 2018 at 17:20):

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

#### Matthieu Sozeau (May 30 2018 at 17:21):

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

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

#### Matthieu Sozeau (May 31 2018 at 15:05):

I'll backport to 8.8 once travis passes

Thanks!

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

#### Matthieu Sozeau (Jun 03 2018 at 18:01):

Yeah it’s strange, I’ll check tomorrow

#### Matthieu Sozeau (Jun 05 2018 at 10:32):

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

#### Matthieu Sozeau (Jun 05 2018 at 10:47):

Rather, 98 and 100

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

#### Matthieu Sozeau (Jun 05 2018 at 15:32):

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

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

#### Aleksey Nogin (Gitter import) (Jun 05 2018 at 20:05):

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

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

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

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

#### Matthieu Sozeau (Jun 07 2018 at 07:57):

That’s another instance of #85 I think

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

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

#### Matthieu Sozeau (Jun 07 2018 at 21:54):

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

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

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

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

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

Thanks

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

#### Matthieu Sozeau (Jun 11 2018 at 15:20):

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

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

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

#### Matthieu Sozeau (Jun 11 2018 at 15:25):

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

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

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

#### Matthieu Sozeau (Jun 11 2018 at 15:44):

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

#### Matthieu Sozeau (Jun 11 2018 at 15:45):

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

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

#### Jad Hamza (Gitter import) (Jun 11 2018 at 18:44):

repository: coq-released

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

#### Matthieu Sozeau (Jun 11 2018 at 19:05):

For the same code ?

#### Jad Hamza (Gitter import) (Jun 11 2018 at 19:07):

@Matthieu Sozeau yes I copied the code from issue 75

#### Matthieu Sozeau (Jun 11 2018 at 19:09):

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

#### Matthieu Sozeau (Jun 11 2018 at 19:10):

Are you sure it’s not admitted?

hmm let me check

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

#### Matthieu Sozeau (Jun 11 2018 at 19:28):

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

:)

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

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

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

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

#### Matthieu Sozeau (Jun 11 2018 at 20:10):

Yes, using the `Equations (noind) foo` option

Awesome! Thanks

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

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

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

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

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

#### Jad Hamza (Gitter import) (Jun 11 2018 at 20:18):

@Matthieu Sozeau not 1.0+8.7 but 8.7-dev

#### Jad Hamza (Gitter import) (Jun 11 2018 at 20:24):

Thanks for the PR!

Ah. Makes sense

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

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

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

#### Jad Hamza (Gitter import) (Jun 12 2018 at 08:28):

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

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

#### Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:30):

@Jad Hamza which definition are you referring to?

of issue 111

Equations num

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

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

#### Aleksey Nogin (Gitter import) (Jun 12 2018 at 08:38):

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

#### Jad Hamza (Gitter import) (Jun 12 2018 at 08:39):

@Aleksey Nogin what about `num_equation_1`?

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

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

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

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

#### Jad Hamza (Gitter import) (Jun 12 2018 at 09:25):

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

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

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

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

``````
``````

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

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

#### Aleksey Nogin (Gitter import) (Jun 12 2018 at 09:41):

`Wrong argument name: f.`

#### Matthieu Sozeau (Jun 12 2018 at 09:41):

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

#### Matthieu Sozeau (Jun 12 2018 at 09:43):

@Aleksey Nogin your call to num_elim is equivalent

#### Matthieu Sozeau (Jun 12 2018 at 09:47):

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

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

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

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

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

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

#### Matthieu Sozeau (Jun 12 2018 at 10:13):

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

#### Jad Hamza (Gitter import) (Jun 12 2018 at 10:20):

@Matthieu Sozeau so what's happening?

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

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

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

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

#### Matthieu Sozeau (Jun 12 2018 at 18:47):

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

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

#### Aleksey Nogin (Gitter import) (Jun 13 2018 at 21:35):

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

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

Hi there!

#### Pierre Courtieu (Dec 07 2018 at 09:16):

Any news about the replacement of Function backend?

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

great

#### Jad Hamza (Gitter import) (Dec 21 2018 at 09:22):

Hello, are mutually recursive equations with measures supported?

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

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

I see thanks

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

If I do

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

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

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

#### Yannick Forster (Gitter import) (Apr 03 2019 at 13:44):

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

#### Matthieu Sozeau (Apr 03 2019 at 13:46):

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

#### Matthieu Sozeau (Apr 03 2019 at 13:48):

`dependent elimination x` would tell you

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

#### Matthieu Sozeau (Apr 03 2019 at 13:49):

Actually `NoConfusion for eType` is enough here

#### Yannick Forster (Gitter import) (Apr 03 2019 at 13:52):

Oh, so actually the behaviour is quite perfect :)

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

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

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

#### Matthieu Sozeau (Dec 06 2019 at 14:38):

Strange, I'll have a look

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

#### Matthieu Sozeau (Dec 08 2019 at 11:19):

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

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

#### Matthieu Sozeau (Dec 08 2019 at 11:42):

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

#### Jad Hamza (Gitter import) (Dec 08 2019 at 14:27):

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

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

#### Matthieu Sozeau (Dec 08 2019 at 14:42):

From Equations Require Import Equations. Should work I think

#### Matthieu Sozeau (Dec 08 2019 at 14:42):

From Equations Require Import Equations should work

#### Jad Hamza (Gitter import) (Dec 08 2019 at 14:52):

Thanks, working now

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

#### Mukesh Tiwari (Gitter import) (Dec 16 2019 at 01:40):

I am getting this error

#### 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)".
``````

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

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

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

#### Mukesh Tiwari (Gitter import) (Dec 16 2019 at 05:52):

Nevermind. I think I got the idea.

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

#### Matthieu Sozeau (Dec 16 2019 at 09:19):

@Mukesh Tiwari it seems `nil` was understood as a variable

#### Paolo Giarrusso (Dec 16 2019 at 11:00):

Doh, it should have been vnil not nil ?

#### Matthieu Sozeau (Dec 16 2019 at 11:15):

I guess. Probably nil was not exported.

#### Mukesh Tiwari (Gitter import) (Dec 16 2019 at 11:32):

@Matthieu Sozeau Thank you.

#### Mukesh Tiwari (Gitter import) (Dec 16 2019 at 11:33):

Totally feeling stupid that how did I missed it :(

#### Paolo Giarrusso (Dec 16 2019 at 12:19):

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

#### Matthieu Sozeau (Dec 16 2019 at 13:18):

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

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

#### Karl Palmskog (Jan 02 2020 at 16:42):

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

#### Daniel Patterson (Gitter import) (Jan 02 2020 at 16:42):

8.10.2 with equations 1.2.1+8.10

#### Karl Palmskog (Jan 02 2020 at 16:43):

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

#### Karl Palmskog (Jan 02 2020 at 16:44):

is that supposed to trigger the error?

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

#### Karl Palmskog (Jan 02 2020 at 16:44):

indeed Equations is very sensitive to Requires

#### Daniel Patterson (Gitter import) (Jan 02 2020 at 16:48):

Thanks @Karl Palmskog :)

#### Daniel Patterson (Gitter import) (Jan 02 2020 at 16:52):

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

#### Paolo Giarrusso (Jan 02 2020 at 18:12):

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

#### Paolo Giarrusso (Jan 02 2020 at 18:14):

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

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

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

#### 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') := ...;`

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

#### Karl Palmskog (Jan 03 2020 at 10:45):

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

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

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

#### Karl Palmskog (Jan 03 2020 at 14:13):

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

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

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

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

Thanks

#### Karl Palmskog (Feb 28 2020 at 12:36):

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

#### Matthieu Sozeau (Feb 28 2020 at 12:53):

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

:thumbsup:

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

#### Karl Palmskog (Feb 28 2020 at 13:00):

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

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

#### Bas Spitters (Feb 28 2020 at 20:32):

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

#### Bas Spitters (Feb 28 2020 at 20:32):

But I guess you mean updating opam?

#### Karl Palmskog (Feb 28 2020 at 20:32):

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

#### Karl Palmskog (Feb 28 2020 at 20:33):

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

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

#### Bas Spitters (Feb 28 2020 at 20:35):

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

#### Karl Palmskog (Feb 28 2020 at 20:35):

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

#### Karl Palmskog (Feb 28 2020 at 20:36):

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

#### Bas Spitters (Feb 28 2020 at 20:36):

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

#### Bas Spitters (Feb 28 2020 at 20:37):

@Karl Palmskog Thanks!

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

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

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

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

#### Matthieu Sozeau (Mar 10 2020 at 13:14):

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

#### Matthieu Sozeau (Mar 10 2020 at 13:15):

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

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

Yes

Thanks :)

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

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

#### Jad Hamza (Gitter import) (Mar 10 2020 at 14:12):

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

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

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

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

#### Paolo Giarrusso (Mar 10 2020 at 14:44):

(surprising to me)

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

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

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

#### Jad Hamza (Gitter import) (Mar 10 2020 at 18:58):

Thanks! Moving there

#### Matthieu Sozeau (Mar 11 2020 at 12:45):

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

#### Matthieu Sozeau (Mar 11 2020 at 12:46):

I think autorewrite does not bypass opacity though

#### Matthieu Sozeau (Mar 11 2020 at 12:46):

But I might be wrong :)

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

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

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

#### Paolo Giarrusso (Mar 11 2020 at 18:36):

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

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

#### Bas Spitters (Mar 15 2020 at 13:44):

Idris2 has some cool technology to generate programs from a type. Apparently, it originated here:
has anyone looked at porting it to Coq?

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

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

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

#### Karl Palmskog (Mar 15 2020 at 16:01):

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

#### Karl Palmskog (Mar 15 2020 at 16:02):

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

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

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

#### Karl Palmskog (Mar 15 2020 at 18:59):

but no Coq integration available to my knowledge

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

#### Bas Spitters (Mar 15 2020 at 20:29):

That project doesn't seem very active

#### Karl Palmskog (Mar 15 2020 at 20:35):

the main author is in industry these days

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

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

#### Bas Spitters (Mar 15 2020 at 21:14):

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

#### Karl Palmskog (Mar 15 2020 at 21:21):

it looks like they chose to implement it quite differently

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

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

#### Karl Palmskog (Mar 15 2020 at 21:23):

I think Jasmin and Gabriel are following Sledgehammer more closely

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

#### Karl Palmskog (Mar 15 2020 at 21:28):

ah right, they target HOL instead of CIC0 it seems

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

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

Swap the imports

#### Matthieu Sozeau (Mar 16 2020 at 15:38):

It messes with tactic redéfinitions

#### Théo Winterhalter (Mar 16 2020 at 15:39):

Oh… It’s that simple, thanks!

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

Yes

@Cyril Cohen

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

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

#### PLBegay (Gitter import) (Apr 23 2020 at 16:41):

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

Last updated: Jan 29 2023 at 15:02 UTC