rework Foundations

[DanGrayson]

Vladimir thought it was important for those not acquainted with UniMath to be able to learn it well by stepping through the proofs (in ProofGeneral or Coqide), working their way sequentially through the files from the first to the last, or at least until all the files in the first package, UniMath/Foundations, had been scanned. In early 2017 he told us that we should stop adding random lemmas to UniMath/Foundations, and that he should undertake the project of going through it and putting it into good shape.

We should put this project on the list of projects ultimately to do, and hence I submit this issue. I believe it should be done by a single person, as uniformity of style will enhance the pedagogical value, and I'd like to be the one to do it.

I'd adhere to the following principles:

 -  preserve the spirit of his original Foundations, as in
    https://github.com/UniMath/UniMath/tree/vv-master-for-coq8.4pl3patched
    or https://github.com/vladimirias/Foundations
 -  maintain consistency with published descriptions of Foundations, especially those
    published by Vladimir
 -  adherence to our coding style guidelines

See also the discussion at https://github.com/UniMath/UniMath/issues/77. We should probably think of this issue as subsuming that one, and try to follow the guidance there.

Items I might address first:

 -  eliminate my stuff based on DecidableProposition or move it to MoreFoundations

See also my branch where I made an attempt to start things afresh: https://github.com/DanGrayson/UniMath/tree/essential-foundations

A good place for others to submit suggestions would be as comments on this issue.

[DanGrayson]

I wonder whether we should change this, and would welcome input:

Fixpoint natgtb (n m : nat) : bool :=
  match n, m with
  | S n, S m => natgtb n m
  | O, _ => false
  | _, _ => true
  end.

Definition natgth (n m : nat) : hProp := hProppair (natgtb n m = true) (isasetbool _ _).

I would prefer defining natgth itself by induction, so it returns either hfalse or htrue, and to prune all such functions to bool from the system. I never asked Vladimir about that.

[benediktahrens]

File PartD could look much better if (unicode) notation were used throughout, e.g., instead of weq. Is there a chance we can fix this before December?

[DanGrayson]

I'll try to do it! Does that comment not apply to PartC?

[benediktahrens]

On 10/19/2017 10:06 PM, Daniel R. Grayson wrote:

I'll try to do it! Does that comment not apply to PartC?

It does, but in PartD it looks somewhat more severe, because of the construction of equivalences between types of equivalences.

[benediktahrens]

I suggest removing the use of the now tactical from Foundations.

There are several issues with now:

1. The Coq now is defined in terms of the easy tactical, which in turn is marked 'experimental'. We want to avoid experimental stuff in Foundations.
2. We redefine now in MoreFoundations, but that is completely opaque to the user. That is, at any given moment, it is difficult to find out whether a given use of the now tactical refers to the Coq one or to our now.
3. now provides some automation. We do not make use of that automation, and hence there is not really a benefit from using now. Instead, now only obscures what is going on.

Point 2. does not concern Foundations, but is still a bug, in my opinion. It deserves a separate issue.

[benediktahrens]

I suggest not using reflexivity in Foundations. The tactic has 11 chars, its counterpart apply idpath has 12. There is very little benefit to using reflexivity, and in exchange one has to learn an additional tactic.

[DanGrayson]

Removing now in Foundations is a good idea. I'm not so sure about reflexivity -- it's probably the second or third thing anyone learns when learning Coq, and it's one of those most easily remembered, because the ordinary meaning of the word conveys exactly what it does. I just attended a lecture on proof checking to a general audience, and he used it three or four times in his 4 minute demo of a Coq interaction.

[benediktahrens]

Here are my reasons to dislike reflexivity:

1. The name reflexivity is very much inspired by the idea of the identity type as a proposition.

2. I think it is easier to teach a few core tactics which take arguments (such as apply, use, etc) than to teach many different tactics that only serve one purpose. One can argue that reflexivity occurs often enough to deserve an exception to that rule, but, as I pointed out, that exception only saves minimal typing.

3. It applies to goals that don't have anything to do with paths, e.g., unit. That can be very confusing when one looks at a proof in HTML, e.g., when not having Coq installed.

Note that there is not a single use of reflexivity in Vladimir's Foundations.

[DanGrayson]

Okay, you convinced me! I'll remove reflexivity from Foundations.

[benediktahrens]

I suggest replacing unshelve refine (gradth f _ _ _). in the proof of UniqueConstruction_to_weq by use (gradth f). That is shorter and clearer. Similar with all the other occurrences of unshelve refine.

[DanGrayson]

Good idea. Also simple refine, if any.

[DanGrayson]

I'll put these last few changes in soon, for use in the workshop.

[DanGrayson]

I'll remove mkpair, too, since use tpair is a fine alternative.

[benediktahrens]

On 11/06/2017 07:34 PM, Daniel R. Grayson wrote:

I'll remove mkpair, too, since use tpair is a fine alternative.

Yes, I think that is a good idea!

[rmatthes]

I would like to remind you of missing type information in some definitions in PartA.v that were part of my previous PR #764. There are two types of suggestions: add the type of what is being defined (at least, I saw dirprodpair, weqtoempty, weqtoempty2, weqonpaths, weqpathsinv0, weqdirprodf) or add type information to an argument of the definition (I saw iscontr_move_point and iscontr_move_point_eq). In addition, in some cases, I saw superfluous information in the type, namely a name for a bound variable that does not occur in the body, and it would better be _ (underscore), seen in transportf_const, transportb_const and isweqcontrtouint (I find λ (t : T), tt particularly irritating).

[rmatthes]

@DanGrayson : if you drop mkpair, then please also remove mk_pair in UniMath/CategoryTheory/limits/pullbacks.v which can equally be replaced by use tpair at the only place where it is used.

[DanGrayson]

mk_pair -- okay, good idea.

[benediktahrens]

Should we strive to put all the Ltac definitions that are used in Foundations into Preamble? There is

Ltac contradicts a b := solve [ induction (a b) | induction (b a) ].

in PartA. I think it fits better in Preamble.

[benediktahrens]

Ltac intermediate_logeq Y' := apply (logeq_trans (Y := Y')).

defined in PartA, is only used twice in PartC, and does not really shorten the proof script. Can we do without?

[benediktahrens]

Ltac intermediate_iscontr Y' := apply (iscontrweqb (Y := Y')).

from PartA is only used once in Ktheory. It is also defined again in Ktheory/Tactics. Maybe we can remove it from PartA and leave the one in Ktheory?

[DanGrayson]

Those are good suggestions.

[benediktahrens]

We still have quite a mess in UniMath regarding Set Automatic Introduction. The plan was to restrict usage to Local (Un)Set Automatic Introduction. Could we change that before Dec 11?

[DanGrayson]

Yes, but I already fixed it. Try it out, everything works, since only Global Unset Automatic Introduction would be bad in a file that's imported by another.

[langston-barrett]

My biggest suggestion for this issue is to organize lemmas and definitions into files by topic, e.g. to group all facts about hlevels into a single file, and to have lemmas about equivalences in a separate file, etc. It can be very challenging to remember which things are where in Foundations.