I hear Adam talking.  I tend to disagree, not least with the assumption
that Coq proofs should be regarded as "fully automated".  (-:

(I have however used bare "repeat match goal" in a proof script myself,
when I wanted to apply a given lemma three or four times in "obvious"
locations, so it's not such constructs themselves that I object to.)

On Mon, Oct 21, 2013 at 11:47 PM, Jason Gross <notifications@github.com>wrote:

> In theories/types/Universe.v:
>
> > +        generalize (equiv_fun _ _ f) (equiv_fun _ _ g)
> > +  end.
> > +  let f' := fresh in
> > +  let g' := fresh in
> > +  intros f' g' ? ?;
> > +    assert (f' = g'); [ | path_induction; apply ap; apply allpath_hprop ].
> > +  apply path_forall; intro.
> > +  apply allpath_hprop.
> > +Qed.
> > +
> > +Instance trunc_hProp `{Funext} : IsHSet hProp.
> > +Proof.
> > +  eapply trunc_equiv'; [ apply issig_hProp | ].
> > +  (intros ? [? ?]).
> > +  apply hprop_allpath.
> > +  repeat match goal with
>
> @mikeshulman <https://github.com/mikeshulman> That's a failure of my
> tactic, I think, not a failure of this approach. I've updated this pull
> request to factor out this part of the tactic into a separate lemma, which
> I've called path_path_sigma. (This was at 64da19f<https://github.com/HoTT/HoTT/commit/64da19f14db7bf0abd15a3563ccd0a1f67caa854>.
> I subsequently realized that each step only got applied once, and removed
> the repeat match goal all together. But I do think it's useful in other
> places, where lemmas will be applied multiple times.) I think that any
> reasoning sufficiently complicated to be more enlightening as a
> step-by-step proof than as a tactic deserves its own lemma. The idea behind
> fully automated proofs, I think, is that the automation should be mostly
> trivial and mostly brute force (I make exceptions for the "trivial" part
> when I need to do fancy things to get Co q to infer arguments correctly). I
> do think that you should be able to understand a proof, at a high level,
> without stepping through it (though you might need to get the type of all
> the lemmas that it uses); any non-trivial bits of reasoning should be in
> their own lemmas. (Trivial bits of reasoning include things like "remove
> all of the compositions with identity morphisms" and "uniformize
> associativity", which I think is where some of the tedium in simple diagram
> chasing proofs comes from.)
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/226/files#r7117589>
> .
>