Hi there!

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

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!

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?

@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

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.

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

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

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

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)

The new package is being tested

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?

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.

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

@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

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

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

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

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

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.

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?

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!

@Matthieu Sozeau: Thank you!

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.

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

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

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

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.

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

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

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

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

nested recursion

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

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

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

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

@Aleksey Nogin the patches are on 8.8 now

Thanks!

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

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

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.

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

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

to `f_comp_proj`

Argh

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!

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

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

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

(with only two expressions to rewrite)

Is there a known slowness issue here?

@Matthieu Sozeau Oh, actually "constructor" also unfolds `f`

to `f_comp_proj`

when the goal is `f x y`

Yes many tactics do not respect Opaque

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

There’s the `simp f`

tactic that does the same pretty much

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

Probably an issue with backtracking

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

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?

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?

@Matthieu Sozeau Thanks! Do you mean `Print Rewrite HintDb core.`

? I just see rewrite rules about the composition of two functions.

`Print Transparent Dependencies transport.`

prints a bunch of dependencies but I guess these are the normal library dependencies?

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

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

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

When there are two files, `Opaque transport.`

solves the slowness. Maybe I should just set all Equations definitions to Opaque?

Indeed, for use with simp it’s better.

The tactic should handle this for you though

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

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

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.

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

@Aleksey Nogin done, you can have a try

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

Ok, still looks like legitimate bugs :)

Ok, still looks like legitimate bugs :)

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

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

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

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

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

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

I'll backport to 8.8 once travis passes

Thanks!

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

Yeah it’s strange, I’ll check tomorrow

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

Rather, 98 and 100

@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

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

@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

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

error

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

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

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

That’s another instance of #85 I think

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

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

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

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

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

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

@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

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

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

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

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

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

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

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

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

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

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

repository: coq-released

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

For the same code ?

@Matthieu Sozeau yes I copied the code from issue 75

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

Are you sure it’s not admitted?

hmm let me check

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

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

:)

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.

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

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

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

Yes, using the `Equations (noind) foo`

option

Awesome! Thanks

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

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

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

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

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

@Matthieu Sozeau not 1.0+8.7 but 8.7-dev

Thanks for the PR!

Ah. Makes sense

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

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

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

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

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

@Jad Hamza which definition are you referring to?

of issue 111

Equations num

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.

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

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

@Aleksey Nogin what about `num_equation_1`

?

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)

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.

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

keyword)

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.

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

@Aleksey Nogin `intro. induction f. intros. simpl in *.`

unfolds the definition of `foo_type`

(`cbn`

instead of `simpl`

works as well)

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

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.

```
```

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

@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

`Wrong argument name: f.`

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

@Aleksey Nogin your call to num_elim is equivalent

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

I suppose

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

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.

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

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

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

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

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

@Matthieu Sozeau so what's happening?

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

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

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

Hm, `Solving obligations automatically...`

seems to be getting stuck on one of my equations :( Will try to minimize/reproduce/report...

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

might help.

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.

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

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

Any news about the replacement of Function backend?

@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

Hello, are mutually recursive equations with measures supported?

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

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

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

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

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

Weirdly, if I do ```
Set Equations With UIP.
Axiom uipa : forall A, UIP A.
Existing Instance uipa.
```

before, that doesn't change anything

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

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

`dependent elimination x`

would tell you

`depelim`

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

Actually `NoConfusion for eType`

is enough here

Oh, so actually the behaviour is quite perfect :)

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

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

(The file `equations_plugin.cmxs`

does not appear at all in the folder of the `dev`

opam switch)

Strange, I'll have a look

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

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

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

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

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

Hm wait, is it still `Equations.Equations`

that I should import?

Error: Unable to locate library Equations.Equations.

From Equations Require Import Equations. Should work I think

From Equations Require Import Equations should work

Thanks, working now

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

I am getting this error

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

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

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

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

Nevermind. I think I got the idea.

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

@Mukesh Tiwari it seems `nil`

was understood as a variable

Doh, it should have been vnil not nil ?

I guess. Probably nil was not exported.

@Matthieu Sozeau Thank you.

Totally feeling stupid that how did I missed it :(

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

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

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

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

8.10.2 with equations 1.2.1+8.10

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

is that supposed to trigger the error?

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!

indeed Equations is very sensitive to Requires

Thanks @Karl Palmskog :)

Hmm. It seems `Set Implicit Arguments. `

causes this error.

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

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

It doesn't work with s implicit (I assume you mean `{s : bool}`

), whether `Set Implicit Arguments`

is set or not.

If you use `{s}`

then indeed you have to give an explicit `bmeasure (s:=true/false)`

in the clauses.

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

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

one could imagine a syntax `myeq n#(S n') := ...`

, or maybe I'm missing something

@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

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

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

Yep it would be nice, sadly `as`

is not part of the term grammar only the pattern one

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

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

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

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

:thumbsup:

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

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

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

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

But I guess you mean updating opam?

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

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

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

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

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

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

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

@Karl Palmskog Thanks!

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

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

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

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?

It might just be because `simp f`

also calls `typeclasses eauto with f`

after the `autorewrite`

But it does call `autorewrite`

so should be the same as explicit rewrites

Ah thanks, so I should write `autorewrite with f`

if I want the same effect without `eauto`

?

Yes

Thanks :)

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`

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

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

Yes you're right that might cause the difference, but `simp_red`

is often used within `repeat`

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

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

(surprising to me)

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

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

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.

Thanks! Moving there

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

I think autorewrite does not bypass opacity though

But I might be wrong :)

`rewrite_strat`

indeed worked well! (and faster than `repeat rewrite`

) after a few adjustments (importing `RelationClasses`

and defining a few missing instances)

@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

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

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

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

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?

isn’t that based on a foundation similar to `tauto`

? if so, is there any significant difference in engineering?

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

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.

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

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

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?

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

but no Coq integration available to my knowledge

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

That project doesn't seem very active

the main author is in industry these days

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

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

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

it looks like they chose to implement it quite differently

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

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

I think Jasmin and Gabriel are following Sledgehammer more closely

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

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

ah right, they target HOL instead of CIC0 it seems

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

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

Swap the imports

It messes with tactic redéfinitions

Oh… It’s that simple, thanks!

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

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 !

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

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

Last updated: Jan 29 2023 at 15:02 UTC