Flattening lemma for colimits

[ThomatoTomato]

We reprove the flattening lemma for colimits using descent. This particular method has the perk of being the same method as used for graph quotients, coequalizers, and pushouts. A lot of the proofs involved in the flattening lemma simplifies a lot, and become completely analogous to the other three cases. The only major difference appears first after we're done with proving all the necessary lemmata, and we're proving the flattening lemma.

This approach suffers from some of the same slowness problems as the first proof. The functions are in general a lot faster, but more parts are acting slowly.

With this approach we also get a characterization of path spaces of colimits basicly for free, using Kraus-von Raumer.

There are still a couple of cleanups that can be done. I think there are some overlap with the Descent section and some files in the Diagrams subdirectory.

(This work is done on an old version of some of the files found here. Consider only the parts after descent, as that are the only relevant parts.)

[jdchristensen]

Nice!

[jdchristensen]

The comments all need updating.

[jdchristensen]

Suggested change

	{ nrapply Colimit_ind_beta_colimp. }
	1: nrapply Colimit_ind_beta_colimp.

I prefer 1: tactic. to { tactic } when it is a single tactic.

[jdchristensen]

Here I think bullets would be better. In general, I'd only use braces when you need to avoid the bullets getting too deep, which is rare.

[jdchristensen]

The + bullet isn't needed, since there is only one goal.

[jdchristensen]

These should use bullets. (I've just given some examples, and you can apply the same ideas elsewhere.)

[jdchristensen]

I think this is a good use of braces. A temporary hole was produced that takes two tactics to fill. If you used bullets each time you had a step like this, the indentation would keep growing. And if you use 1:, then you need to chain the tactics with ; which makes it harder to step through.

Note: one set of parentheses can be removed on the last line.

[jdchristensen]

Include the word "slow" at each of these spots to make them easy to search for.

[jdchristensen]

This is great. The slow lines aren't too bad, but here are some ideas that might (or might not) help if you want to speed them up:

I think there's not much you can do about slow closing of Sections, except to remove the Section. In one case, the section is long and provides enough benefit that I don't think it's worth removing it. But in one other case, there are only a couple of results in the section, so the context could be repeated. If you do this, time the build of the whole file to see if things improve. Sometimes the slowness can just move somewhere else.

Slow Defined lines are also tricky. Almost always it comes down to definitional equalities needing to be computed in order for type checking to go through. Some ideas:

• Try making some things Opaque, if the details of their definitions aren't needed for the proof to type check. E.g. maybe things related to Colimit can be Opaque.
• If some parts of a proof are causing the slow down, and their details aren't needed, you can wrap those parts in abstract to make them opaque. (Or, combine this with the next item.) You can sometimes identify the part that is causing trouble by replacing some parts with admit. (see below) and seeing if the Defined line gets faster.
• A long proof can be split into separate results. E.g. equiv_adjointify has four goals, so the proof could be split into 4 smaller definitions (or 3, with the two composites being combined). In principle, this alone shouldn't speed anything up, but it might. And even if it doesn't, when the parts are split, some can be made Opaque (or ended with Qed instead of Defined), which might speed things up.
• Sometimes using rewrite is faster than proofs that don't use it.
• Sometimes it helps to insert a lemma whose proof is reflexivity, so that Coq doesn't need to compute that the two terms are definitionally equal.
• Before all of the above, you should see if any of the proofs can be simplified. E.g. if you need to associate one way, then the other way, sometimes you can save steps by doing things in a different order. Or sometimes you can apply a lemma from PathGroupoids to save some steps.

Here's a replacement for admit that still lets you end a proof with Defined.

    Axiom proof_admitted : False.
    Tactic Notation "admit" := abstract case proof_admitted.

[jdchristensen]

Can you rebase the last two commits on the latest master, now that the functor colimit material is merged? (Rebasing avoids merge commits giving a cleaner history.)

[jdchristensen]

@ThomatoTomato What's the status of this? (We can discuss at our next meeting if that's easier.)

[ThomatoTomato]

I have been ignoring this for sometime, let us talk about it at our next meeting. I will have a look at your comments and try to find subresults to generalize before that. I don't know how possible that is, since the proof of flattening is very streamlined from the recipe that you gave me. Anyways, the most important thing to do before considering a serious commit is to remove duplicate code.

[jdchristensen]

@ThomatoTomato Is this still something you are planning to finish?

[ThomatoTomato]

I have not been thinking about this for a while, but I think it is good to finish this once I've dealt with the other PR in my backlog.