Create coding style

[stop-cran]

Current code is somewhat hard to read. I'd suggest to create a coding style guide and amend all existing proofs to follow that style.

Below are my ideas about coding style to be discussed:

• Use bullets in all proofs. For nested bullets of 5th order and deeper, consider extracting separate lemmas.
• For goals generated by assert tactic use curly braces to logically separate from other goals. Possibly with other bullets inside the assertion goal if needed. E.g.:

    ...
    assert (forall a b:R, -b <= a -> a <= b -> Rabs a <= b).
  { intros.
    unfold Rabs.
    destruct Rcase_abs; lra. }
    intros.
    apply H.
    ...

• Explicitly declare all terms, that are explicitly referenced later in proofs - current proofs are fragile because auto-generated names like H0, H1, H2, etc. tend to change all together in case of even minor proof amendments. E.g.:

...
destruct H.
apply H1. (* Fragile *)
...
destruct H as [? H1].
apply H1. (* Okay *)
...

• Any other ideas?

[Columbus240]

I also think a style guide would be good. This way we can define how certain issues should be solved.

On Zulip, Karl Palmskog listed some already existing style guides:

• https://gitlab.mpi-sws.org/iris/iris/blob/iris-3.2.0/StyleGuide.md
• https://github.com/math-comp/math-comp/blob/mathcomp-1.9.0/CONTRIBUTING.md
• https://github.com/uwplse/verdi-raft/blob/master/STYLE.md
• https://www.ssi.gouv.fr/uploads/2014/11/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.0-en.pdf
• https://github.com/HoTT/HoTT/blob/master/STYLE.md (this link is from me)

Other useful stuff he listed:

• https://github.com/Karmaki/coq-dpdgraph
• https://github.com/coq-community/awesome-coq.

I think using Set Bullet Behavior Strict Subproofs would be useful.

And your points above agree (more or less) with what I had in mind. Always explicitly declaring hypotheses if they are used later might be a bit hard to enforce... I have not a lot of experience using that approach. (I think Chlipala wrote something about that in CPDT...) Something I found useful to make my proofs less fragile is the following:

match goal with
| H0 : ?a = true,
  H1 : ?a = false |- _ =>
  rewrite H0 in H1; discriminate H1
end.

How about

    ...
    assert (forall a b:R, -b <= a -> a <= b -> Rabs a <= b).
    { intros.
      unfold Rabs.
      destruct Rcase_abs; lra.
    }
    intros.
    apply H.
    ...

or

    ...
    assert (forall a b:R, -b <= a -> a <= b -> Rabs a <= b). {
      intros.
      unfold Rabs.
      destruct Rcase_abs; lra.
    }
    intros.
    apply H.
    ...

I like these more, because I’m used to having each subproof indented another layer. I use the first variant more often.
Sometimes I also do the following, if the proof of the subgoal is especially short (one to two tactics maybe).

  ...
  destruct some_boolean.
  2: { assumption. }
  intros.
  ...

Let’s start bikeshedding! :D On another day, I’ll write more concrete ideas and respond more to your above ideas.

P.S. We might consider not defining every possible thing in the style guide, like every possible placement of braces and every possible ambiguity and corner case.

[Zimmi48]

I think using Set Bullet Behavior Strict Subproofs would be useful.

It's Set Bullet Behavior "Strict Subproofs" and it is already the default. Were you actually looking for something like Set Default Goal Selector "!" (see https://coq.inria.fr/refman/proof-engine/proof-handling.html#mandatory-bullets)?

Explicitly declare all terms, that are explicitly referenced later in proofs - current proofs are fragile because auto-generated names like H0, H1, H2, etc. tend to change all together in case of even minor proof amendments

You can check for this with Set Mangle Names (see https://coq.inria.fr/refman/proof-engine/tactics.html#proof-maintenance) or -mangle-name (see https://coq.inria.fr/refman/practical-tools/coq-commands.html#by-command-line-options).

[stop-cran]

At least I'm going to put bullets in all existing proofs.

[Columbus240]

Thanks for the clarification @Zimmi48.

I agree with you (@stop-cran), about using bullets & braces where applicable.

[Columbus240]

Other stuff that is sometimes inconsistent:

• Capitalisation in the names in ZornsLemma. The stdlib uses capitalised function names (Complement, Intersection, Full_set, ...) and uses capitalised names in lemmas that use these functions (Complement_Complement, Intersection_inv, Union_commutative, ...).
  ZornsLemma follows this convention very often in function names (FamilyUnion, IndexedFamilyIntersection, ...) with some exceptions (inverse_image). But it often doesn’t follow this convention in the names of lemmas (empty_family_union, inj_countable, ...).
  I just wanted to note this, but am not very inclined to do something about it.
• Where the parameters of a lemma go, isn’t always done the same way. There are examples of Lemma foo (X : Type) : bar X. and Lemma foo : forall (X : Type), bar X..
• Indentation level of proofs. Most times the following is done:

Lemma foo : bar.
Proof.
intros; reflexivity.
Qed.

But there are also examples of this:

Lemma foo : baz.
Proof.
  intros; reflexivity.
Qed.

The latter is the "default" setting of ProofGeneral. Instances of the latter style can be detected (very crudely) using grep -rozP "Proof.\n " (executed in /theories/). The command is somehow rendered wrongly, there should be two spaces after the '\n'.

[Columbus240]

I added a hint to automatically prove In Full_set x. This makes some proofs a little shorter.

I think functions from/to topological spaces could be declared more concisely if we declare point_set : TopologicalSpace -> Type to be a coercion. But note: in forall f : RTop -> RTop, continuous f coq will be able to insert the necessary point_set around RTop, but in forall f : R -> R, continuous f it can’t, because we haven’t specified the topology on R.
@stop-cran what do you think about declaring the coercion?

[stop-cran]

@Columbus240 yes, why not. I thought more about Hint Constructors for Full_set and using auto, but these ways are not mutually exclusive.

[Columbus240]

More in the direction of automatic proofs: We could declare topological properties as "typeclasses" and then write implications between the properties as instances.

[Columbus240]

We could harmonize the naming of definitions/lemmas. A consistent (& hopefully) short naming style. Currently, because styles from the stdlib and the style of the library mix, we have Complement_FamilyUnion and image_family_union next to eachother. Powerset_facts or the stdlib theorems about Included, Union and Intersection are also all over the place. With very wordy names.
More automatization would also be nice. A lot of the apply Extensionality_Ensembles; ... could be simplified to a single tactic. extensionality_ensembles and extensionality_ensembles_inv already exist for this. More hints, maybe a "simplification" tactic for things related to sets. Make open not unfold on simpl when dealing with topological spaces constructed by some other notion.

[Columbus240]

I created a note on formatting. Mostly I wrote down how I (and for example the Coq stdlib) format and indent braces, bullets and proofs.