Monoidal structure on cartesian categories

[langston-barrett]

With certain properties of products, some of which were necessary for the proofs.

[DanGrayson]

lgtm.

Wait for #1030 and it will be an easy corollary that categories with coproducts have a monoidal structure.

[benediktahrens]

Absence of automation is one of the characteristic features of UniMath, and it would be good to keep it that way.
The use of rewrite by itself is quite bad already, since no information on where this rewrite is being done is retained in the proof script (imagine lhs of your rewrite lemma occurs more than once in the goal). Automated rewrite does not even retain the information which lemma should be rewritten with.

Please change those proofs.

[benediktahrens]

Can you please replace this automated tactic by an explicit constructon?

[DanGrayson]

The construction found by eauto here turns out to be this one:

  Proof.
    apply BinProductArrow.
    - apply BinProductArrow.
      + apply BinProductPr1.
      + exact (BinProductPr2 _ _ · BinProductPr1 _ _).
    - exact (BinProductPr2 _ _ · BinProductPr2 _ _).
  Defined.

[benediktahrens]

Can you please replace this automated tactic by an explicit constructon?

[langston-barrett]

While I certainly understand the concerns about automation in Unimath, there are certain proofs I'd rather not write out in full. Perhaps I'll put these in a separate repository. Feel free to cherry-pick the less problematic commits from the PR (e.g. uniqueness of products), or to close this.

[DanGrayson]

I don't know a definition of "automation" in proof scripts, Benedikt.

[benediktahrens]

On 29/10/2018 06:58, Daniel R. Grayson wrote: I don't know a definition of "automation" in proof scripts, Benedikt.

Surely, using a tactic called `auto` or `eauto` or `autorewrite` counts as such?

[benediktahrens]

It seems particularly worrying that the automation is being used to define a structure (Defined.), not to do a proof (Qed.).

[DanGrayson]

I've never used any of those, nor do I use eapply, but let me take a look at this pull request and see whether there is something problematic about such proofs.

We currently have no appeals to eauto, so portability would be enhanced by not admitting its use. On the other hand, we have some additions to hint databases that Vladimir installed. Did he use them?

[varkor]

We currently have no appeals to eauto, so portability would be enhanced by not admitting its use.

Is there anywhere the reasoning behind the portability arguments is set forth? I don't see how UniMath could realistically transition to another proof assistant without effectively reproving everything, as the tactic language (even without automation) seems heavily specific to Coq — but perhaps such methods have been discussed in the past?

[langston-barrett]

I'm fine rewriting the eauto proofs, that would be easy. Note that autorewrite is only used in the proofs of axioms, it could be made opaque with abstract or similar.

[DanGrayson]

We currently have no appeals to eauto, so portability would be enhanced by not admitting its use.

Is there anywhere the reasoning behind the portability arguments is set forth? I don't see how UniMath could realistically transition to another proof assistant without effectively reproving everything, as the tactic language (even without automation) seems heavily specific to Coq — but perhaps such methods have been discussed in the past?

Well, yes, it's probably a vain hope, and no, there is no "argument" set forth, especially since now we have 960274 lines of proofs.