aac_congruence about aac-tactics HOT 20 OPEN

Release with aac_normalise changes is done and submitted as opam package: coq/opam#3040

I think we keep this issue open to track any progress on aac_congruence that might happen, so I will remove "aac_normalise in" from the title.

from aac-tactics.

@aa755 I just maintain this project, and unfortunately have no plans to extend it with new tactics (but a PR implementing aac_congruence would be welcome).

Someone who may be able to give a quick answer is @damien-pous, one of the original developers of the plugin/library. See also his website with contact info outside GitHub.

from aac-tactics.

Hi @aa755,
aac_congruence has been on my todo list since the beginning, but it requires a non-trivial effort (coding and certifying an algorithm for... computing congruence closure modulo AAC).
I may do it at some point, but not in the near future, unfortunately.
All the best,
Damien

from aac-tactics.

Indeed, the ordering of uninterpreted subterms (here variables) is unspecified.
It is fixed in each call to aac_normalise, but not persistent across various calls.

A patch should be feasible, but not straightforward. I'll try to have a look.

from aac-tactics.

I've pushed a patch proposal in branch canonical-ordering (based on v8.19)
@aa755 can you try it out? Does it fit your needs?

@palmskog what would be the best way to provide a new version? (git/community/opam-wise...)

I would be happy to test it against more users - my own libs using aac-tactics do not require any change.
I would also integrate the trick for [aac_normalise in H].

from aac-tactics.

Then it seems we all agree on a new release.

@aa755 can I include your gcd example and instances into the tutorial?

@damien-pous I assume I can take it from there and merge canonical-ordering into v8.19, do the release, and then merge canonical-ordering-master into master.

from aac-tactics.

Thanks Damien, I will leave this issue open since there is still the possibility of aac_congruence happening.

Just to double check also @aa755, you know about the aac_normalise tactic, right?

from aac-tactics.

I didnt know about aac_normalize. Thanks for pointing that out. But it seems it only works on the conclusion, not the hypotheses. I thought maybe reverting would solve that but it seems it doesn't like implications in the conclusion either:

from aac-tactics.

if we had an aac_normalise in hyp, or aac_normalise in *, aac_normalise in *; lia may work better in many usecases than aac_congruence because the latter would probably know less about arithmetic than lia

from aac-tactics.

Indeed aac_normalise does not work in hypotheses so far (and revert cannot help due to the way it's implemented).
Still, this feature should not be too difficult to implement.

Meanwhile, here is a workaround:

  Lemma trans4 `{Equivalence} a b a' b': R a a' -> R b b' -> R a b -> R a' b'.
  Proof. now intros -> ->. Qed.
  Tactic Notation "aac_normalise" "in" hyp(H) :=
    eapply trans4 in H; [| aac_normalise; reflexivity | aac_normalise; reflexivity].

  Import ZArith.
  Import Instances.Z.
  
  Goal forall n m p: Z, n * (m * 1 + 0) = p * 1 -> True.
  Proof.
    intros n m p H.
    aac_normalise in H.
    trivial.
  Qed.

We may also imagine variations, such as

  Lemma trans `{Equivalence} {P: A -> Prop} {HP: Proper (R ==> Basics.impl) P} a b: R a b -> P a -> P b.
  Proof. apply HP. Qed.

  Goal forall P: Z -> Prop, forall n m: Z, P (n * (m*1 + 0)) -> P (m * n).
  Proof.
    intros P n m H.
    eapply trans in H; [| aac_normalise; reflexivity].
    assumption. 
  Qed.

from aac-tactics.

The workaround is good enough for me. But aac_normalize isn't what I thought it was, or there seems to be a bug:
the ordering of arguments chosen by aac_normalize doesnt seem to be unique:

From AAC_tactics Require Import AAC.
From AAC_tactics Require Instances.
Import Instances.Z.
Require Import ZArith.
Require Import Psatz.
#[export] Instance aac_Z_gcd_Comm : Commutative eq Z.gcd := Z.gcd_comm.
#[export] Instance aac_Z_gcd_assoc : Associative eq Z.gcd := Z.gcd_assoc.

  Lemma test1 a b : 0=Z.gcd a b.
    Fail progress aac_normalise.
  Abort.
  Lemma test1 a b : Z.gcd a b =0.
    Fail progress aac_normalise.
  Abort.

  Lemma test3 a b a' b':
    Z.gcd a' b' = Z.gcd a b.
    aac_normalise.
    match goal with
    | |-  Z.gcd b' a' = Z.gcd b a => idtac
    end.

from aac-tactics.

The concrete problem I have now is that aac_normalize in H choses a different order than aac_normalize thus confusing lia, congruence, etc.
It would be great if the whole goal (including hyps) could be normalized with the same ordering.
Even better would be some ordering that is chosen independent of the goal (e.g. lexicographic ordering) so that the normalization can be done incrementally (only normalize new hyps or goal subterms): great for performance.

from aac-tactics.

@damien-pous I think if the changes in the branch canonical-ordering fits the needs of @aa755, we should do two things:

• merge those changes into the v8.19 branch and make a new GitHub release/tag v8.19.1 which is then packaged on the Coq opam repository (and included in the next Coq Platform)
• port the changes to the master branch, so the feature is preserved in the upcoming release of AAC Tactics for Coq 8.20.0 (and is maintained beyond this)

I can take care of the merging to v8.19 and releasing/packaging, but I might need help to port to master. And the prerequisite would be that we all agree these changes are "worthy" of a new release.

from aac-tactics.

Thanks @palmskog ; would be great indeed if you could do the releasing/packaging ; I'll take care of porting to master.
(I'll start now in a side branch of master)

I would say the changes are worth a release (I was unhappy of the old behaviour quite a few times).
The main prerequisite for me is to check that it works correctly, both for @aa755 and for other potential users.
(The code dates back from 2010 and was not so pleasant to update... I hope I did not introduce bugs)

from aac-tactics.

Thanks for the fix. Indeed, the order now seems independent of the goal in my experiments. Also, the following proof which previously didn't work, does work now:

From AAC_tactics Require Import AAC.
From AAC_tactics Require Instances.
Import Instances.Z.
Require Import ZArith.
Require Import Psatz.
#[export] Instance aac_Z_gcd_Comm : Commutative eq Z.gcd := Z.gcd_comm.
#[export] Instance aac_Z_gcd_assoc : Associative eq Z.gcd := Z.gcd_assoc.

  Lemma trans4 `{Equivalence} a b a' b': R a a' -> R b b' -> R a b -> R a' b'.
  Proof. now intros -> ->. Qed.

  Tactic Notation "aac_normalise" "in" hyp(H) :=
    eapply trans4 in H; [| aac_normalise; reflexivity | aac_normalise; reflexivity].

  Ltac aac_normalise_all :=
    aac_normalise;
    repeat match goal with
      | H: _ |- _ => aac_normalise in H
      end.

(* this goal comes from a proof of a C++ gcd function *)
Lemma gcd:  forall a b a' b' : Z,  0< b' -> Z.gcd a' b' = Z.gcd a b -> Z.gcd b' (a' mod b') = Z.gcd a b.
Proof.
  intros.
  aac_rewrite Z.gcd_mod; try lia.
  aac_normalise_all.
  lia.
Qed.

I am using your tactic notation (aac_normalize in) to normalize in hypothesis. You may want to add that as well to the new release.

from aac-tactics.

Thanks @aa755 !
@palmskog : I've added the [aac_normalise in H] tactic (still in branch canonical-ordering), and I've ported to master in branch canonical-ordering-master.

from aac-tactics.

@aa755 can I include your gcd example and instances into the tutorial?

Sure.

from aac-tactics.

@palmskog, if you were not too fast, I've pushed the gcd instances in canonical-ordering, and I'm about to do it in canonical-ordering-master ;)

from aac-tactics.

@damien-pous thanks, I will likely do the release by tomorrow, so no chance of duplicated effort yet.

from aac-tactics.

ok, then I'll add lcm... (and stop there)

from aac-tactics.