Extend app_inj_tail and other list lemmas

[edwardcwang]

The lemma is true in the other direction and can be useful in proofs.

Kind: feature.

Fixes / closes #12093

• Added / updated test-suite

• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[olaure01]

This raises two questions for me:

• A general one: is it better in this kind of situation to have one lemma based on <-> or two lemmas (one for each implication)?
  The first possibility is more compact and more readable, while the second is AFAIK sometimes more easy to apply.
• Concerning these injectivity properties, they seem to be a direct consequence of substitution or a particular case of f_equal. Are there situations where it is better to have an explicit lemma?

Lemma app_inj_tail_inv :
  forall (x y:list A) (a b:A), x = y /\ a = b -> x ++ [a] = y ++ [b].
Proof. intros ? ? ? ? [-> ->]; reflexivity. Qed.
(* alternative proofs
Proof. intros ? ? ? ? [? ?]; subst; reflexivity. Qed.
Proof. now intros; repeat f_equal. Qed.
*)

[anton-trunov]

It looks like this change is not backwards compatible. And as already mentioned by @olaure01 the reverse directions are simple congruence lemmas, so I personally am not sure if it's worth it.

[edwardcwang]

That is a good point. I stumbled upon this issue as a Coq user from using Search and trying to apply what I saw to be relevant List lemmas only to find out that they were unidirectional, and in my project I ended up creating a copy of the lemma with both directions and then applying it. It's a good point that the converse could just be proven with injectivity.

If you think this is not worthwhile, I can close this and the accompanying issue, though it might be interesting to consider this from a user perspective.

[anton-trunov]

Do you have a concrete example where the other direction is needed? Because in simple cases it can be solved with something as trivial as intros [-> ->].

Also, to really merge this PR in its current form you would need to fix the failing dependencies. It might be easier to introduce new names for the equivalences.

[edwardcwang]

That's a fair point. I had a goal of the form x ++ [a] = y ++ [b], though now I see that it can also be proven with f_equal.

[herbelin]

A general one: is it better in this kind of situation to have one lemma based on <-> or two lemmas (one for each implication)?
The first possibility is more compact and more readable, while the second is AFAIK sometimes more easy to apply.

Some people like the <-> style (see for instance in Structures or ZArith). It is in general ok with apply because when given a disjunctive statement, apply tries to apply each conjunct taking the first that works.

In the failures, here, color is failing because it does a destruct on app_inj_tail which thus works differently. fiat-crypto is failing because an apply on app_inv_head is done (presumably) is the wrong direction.

Concerning these injectivity properties, they seem to be a direct consequence of substitution or a particular case of f_equal. Are there situations where it is better to have an explicit lemma?

Here again, the opinions diverge. Some people like to state common lemma even if is is only to save a few tactics and/or because they consider that it makes sense as an algebraic property.

Also, to really merge this PR in its current form you would need to fix the failing dependencies. It might be easier to introduce new names for the equivalences.

A common name used for equivalences is to add the suffix _iff.

[herbelin]

@edwardcwang: it seems that you rally to the arguments of @olaure01 and @anton-trunov. Maybe shall we close the PR then?

[edwardcwang]

Apologies for the delay in responding; I've been a bit busier lately. I also agree with your point @herbelin on using _iff to solve the test failures in this case; I just haven't had the time to fix up the PR yet, and intend to do so as soon as I get some more spare time.

[herbelin]

OK

[edwardcwang]

@herbelin I resolved the previous issues using the _iff suggestion. The CI failure might appear to be unrelated to the additional list lemmas though?

Error: /builds/coq/coq/_install_ci/lib/coq/kernel/nativevalues.cmi
is not a compiled interface for this version of OCaml.
It seems to be for a newer version of OCaml.
Finished failing transaction in 1.37 secs (0.014u,0.009s) (failure)
File "./src/UnsaturatedSolinasHeuristics/Tests.v", line 138, characters 0-459:
Error: Native compiler exited with status 2

Command exited with non-zero status 1
src/UnsaturatedSolinasHeuristics/Tests.vo (real: 17.93, user: 1.82, sys: 0.43, mem: 606904 ko)
Makefile.coq:719: recipe for target 'src/UnsaturatedSolinasHeuristics/Tests.vo' failed

[SkySkimmer]

I don't understand the point of the new direction, isn't it just f_equal?

@herbelin I resolved the previous issues using the _iff suggestion. The CI failure might appear to be unrelated to the additional list lemmas though?

These CI failures are indeed spurious, rebase to rerun.

[edwardcwang]

Here I refer to Hugo's commentary on April 22 with regards to the desirability of <->.

[herbelin]

I don't understand the point of the new direction, isn't it just f_equal`?

This was somehow the discussion above.

As I said, I know that some people like <-> lemmas, and other people find that lemmas which have a clear intuitive algebraic or logical "meaning" are stated, even if their proof is trivial. So, my point of view is that it does not hurt and fills a need to state here the <->. But, of course, this is questionable...

Anyway, my proposal, unless there is a strong objection, would be to validate the PR as it is, by a couple of days.

I'm also assigning.

[edwardcwang]

@herbelin Hi Hugo, any updates on this? Thank you for your help!

[herbelin]

@olaure01, @anton-trunov: would you like some changes? If not, I would merge within a couple of days.

[anton-trunov]

@herbelin I left a comment inplace. Also, this PR needs a changelog entry. How to add it is described here: https://github.com/coq/coq/tree/master/doc/changelog

[anton-trunov]

@edwardcwang Thank you!

@herbelin LGTM

[herbelin]

Looks indeed very good. If no other comments by then, I'll merge tomorrow.