Decide on style for [def]rule_tac ... [and ...] in ...

[Xaphiosis]

We had some discussions on the Proofcraft mattermost (present were myself, @lsf37 , @corlewis , @michaelmcinerney ), which ended up with things not quite nailed down in the end. Let's nail it down and put it in the style guide.

General considerations:

• we need a left-operator (and) and right-operator (and) version
• does the in belong to the rule_tac, or the instantiation? (in previous discussions: to the rule_tac)
• right-alignment of the and/in to utilise space better (similar to : alignment on method args)

At the time of discussion, we settled roughly on:

(* left-operator space-utilising / pretty version 1 - preferred *)
apply (rule_tac x=longthing
            and y=longthing2
             in the_rule)

(* right-operator version - preferred when using right operator wrapping style *)
apply (rule_tac x="..." and
                y="..." and
                z=True
                in some_rule) (* this must not go on previous line for multi-line instantiations *)

(* left-operator naive version (something a tool could potentially handle) - permitted *)
apply (rule_tac x="..."
                and y="..."
                and z=True
                in some_rule)

The following were ruled out:

left-wrap pretty version 2:
apply (rule_tac x="..."
            and y="..."
            and z=True
                in some_rule)

left-wrap pretty version 3:
apply (rule_tac x="..."
            and y="..."
            and z=True
         in some_rule)

However, the above consensus caused friction in the following (one-variable long instantiation) case (pointed out by @lsf37), bringing us back to a need to go over this and pin things down:

(* one-long-instantiation version 1 *)
apply (rule_tac x="long instantiation"
             in some_rule)
vs
(* one-long-instantiation version 2 *)
apply (rule_tac x="long instantiation"
                in some_rule)

For recent proofs I've been going with version 1, because of its consistency with pretty version 1 above.
One of these days maybe we'll have a tool, but even then we'd still have to decide what the tool reformats to.

[lsf37]

I 'm fine the first two (pretty left, standard right), and can live with the naive left version as well, so those are all good.

I guess variant 1 and 2 at the end just come down to being the degenerate forms of the left and right versions, so both should be permitted, and it also explains why Raf prefers variant 1 and I prefer variant 2 :-)

So we really just have the 2 preferred versions, and the naive-left version in addition to that.

[Xaphiosis]

You are right that the degenerate form results in an ambiguous guideline, but I guess we can't win them all. Ok, then TODO for me is to schreib it in the style guide.

[corlewis]

I agree with everything said here, and can add another data point as someone who prefers the original left-operator pretty version 1 and then prefers version 1 of the one-variable case.

One additional comment on the right-operator version; I would be against the in clause going on the same line as the final variable. I think this comes back to me being one of the people who more strongly views the in as belonging to the rule_tac.

[Xaphiosis]

Thanks @corlewis !

One additional comment on the right-operator version; I would be against the in clause going on the same line as the final variable. I think this comes back to me being one of the people who more strongly views the in as belonging to the rule_tac.

Checking to confirm, since none of the above examples have the in on the same line as the last variable: do you mean line or column here? I too think of in as belonging to the rule_tac, and there are definitely examples in the proofs that shove that in onto the last line along with the final variable instantiation.

[corlewis]

Thanks @corlewis !

One additional comment on the right-operator version; I would be against the in clause going on the same line as the final variable. I think this comes back to me being one of the people who more strongly views the in as belonging to the rule_tac.

Checking to confirm, since none of the above examples have the in on the same line as the last variable: do you mean line or column here? I too think of in as belonging to the rule_tac, and there are definitely examples in the proofs that shove that in onto the last line along with the final variable instantiation.

I meant line and was referring to the comment here

(* right-operator version - preferred when using right operator wrapping style *)
apply (rule_tac x="..." and
                y="..." and
                z=True
                in some_rule) (* this could go on previous line as well *)

[lsf37]

Agreed, I would probably also not put the in line in the previous line as the comment says. The only exception would be if everything fits on one line anyway.

Let's remove the comment.

[Xaphiosis]

Right, I see it now. Agreed with both of you, have changed the comment above.