Merge under tactical

[gares]

Proposal by @erikmd
Depends on #96 and and #62

[CohenCyril]

@gares @erikmd what is the status of this after the CIW?

[gares]

erikmd/coq@00cc823
Waiting for Erik to rename the bound variable. I need to refactor proofview in order to be able to focus inside a tactic.

[erikmd]

Hi @gares @CohenCyril :) thanks for the reminder!
I look forward to having a bit more time to look into this missing step for the new tactic implem.
I'll keep you informed ASAP.

[erikmd]

FYI I've just finished to implement the bound variables renaming in my branch feature/under.
(Thanks @gares for the helpful hint you had left in the code!)
I've tested the current code with (the signature of) bigop and matrices extensionality lemmas.
I now need to improve the support of the closely-related over tactic. I hope to address that very soon.
Then the last remaining part will be the focusing-related tweak mentioned by Enrico.
Cc @CohenCyril

[erikmd]

Hi @gares @CohenCyril I've just pushed a new commit with an over tactic (and lemma).

So the currently supported syntax is:

(* 1-var tactic with 1 side-condition *)
under i: eq_bigr.
  by rewrite addnC over.

under i: eq_bigr.
  tactic...; over.

(* 1-var tactic with 2 side-conditions *)
under i : {2}[in RHS]eq_big.
  over.
  move=> Pi; by rewrite addnC over.

(* 2-var tactic with 1 side-condition *)
under i j : {2}[in RHS]eq_mx.
  by rewrite addnC over.

[erikmd]

BTW I've noticed that when an evar is applied to more than one variable (e.g., for a goal expr_depending_on_i_and_j = ?x i j), sometimes the unification doesn't work out-of-the-box if the expr is not beta-expanded, cf. under.v#L47-L49

Do you think this is a bug/unwanted behavior?

Anyway, note that this fact is only reproducible in test_over_2_1 and test_over_2_2 (where I create artificially many evars) while in the more realistic test test_under_eq_mx (which not only involves over, but also under) this beta-redex-issue doesn't show up, cf. under.v#L137.

I'd be interested if someone has an explanation of that difference of behavior between test_over_2_* and test_under_eq_mx… But fortunately as I said above, it seems this small weakness of the unification won't be an issue for under/over.

[erikmd]

To sum up and complement my last-but-one comment, when we'll have the "focus-as-a-tactic" feature, the following syntax could also be implemented:

under i: lem => /andP [H1 H2]. (* the move=> acts only on the focused subgoal *)
  by rewrite addnC over.

(and it would be immediate to support a one-liner version that does not need over, if we find it useful:
under i: lem by move=> /andP [H1 H2]; rewrite addnC.)

@gares, do you think it will be possible to make the "focus-as-a-tactic" work if there are 2 or more side-conditions?
Of course this is maybe not a very frequent case, it will just occur for example if we do under i: eq_big, while the more usual use cases under i: eq_bigl and under i: eq_bigr will only yield one side-condition. Anyway, it seems to me that the possible expected behavior after under i : eq_big could be:

1. either to focus each "under goal" one after the other, e.g. like the Next Obligation facility of Program Definition (but I don't know if this is feasible),
2. or to hide all already-existing goals (by shelving them or so) and only display the 2 "under goals"… (even if a raw shelve would not make the initial goal to appear again when the "under goals" are discharged…)
3. or to display a warning in this case, saying that the specified lemma has more than one side-condition, so that the automatic focusing is disabled…

What do you think?

[gares]

I frankly tried to implement focus-as-tactic but it requires quite some refactoring, and I don't have time for that. So I suggest we try to propose under without that patch.

I won't have time to look at your code for the next 2 weeks, I'm afraid.

[erikmd]

Hi @gares!

I suggest we try to propose under without that patch.

OK for me. AFAICT the current state of the tactic is already quite useful.

I won't have time to look at your code for the next 2 weeks, I'm afraid.

OK, no worries! (I'll be quite busy in the upcoming days as well)
So I can wait for your review before we officially open a PR on Coq master for under.

BTW, note that a small PR in math-comp will also be useful to "leverage the under tactic" (basically, to add missing "extensionality lemmas" such as eq_mx). I plan to prepare one such PR in a few days.

Kind regards, Erik

[erikmd]

For the record, a newest implementation of this tactical is being prepared in PR coq/coq#9651

Feel free to close this issue #97 anytime (now or after the merge)