The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Hi John,

"John Wiegley" 
<johnw AT newartisans.com>
 writes:

> Is this the best way of solving the problem? For larger categories there is 
> a
> lot of boilerplate in providing all these reduction rules, but it's worth it
> to avoid axioms. Though I thought perhaps, someone knows of a better way?

You could try using `eq_dep`, with can be usually made axiom-free as
long as you can prove you indexes are decidable. In this case you need
to elaborate a bit more:

8<----------------------------------------------------------------------8<
Arguments eq_dep [U] P p x q y.

Lemma RoofObj_dec (o1 o2 : RoofObj * RoofObj) : { o1 = o2 } + { o1 <> o2 }.
Proof. repeat decide equality. Qed.

Definition R_abs x := RoofHom x.1 x.2.

Lemma RNeg_RNeg_id_gen o1 o2 (h1 : o1 = RNeg) (h2 : o2 = RNeg) (f : RoofHom 
o1 o2) :
  eq_dep R_abs (o1, o2) f (RNeg, RNeg) IdNeg.
Proof. by case: f h1 h2. Qed.

Lemma RNeg_RNeg_id (f : RoofHom RNeg RNeg) : f = IdNeg.
Proof.
exact/(@eq_dep_eq_dec _ RoofObj_dec R_abs (RNeg, RNeg))/RNeg_RNeg_id_gen.
Qed.
8<----------------------------------------------------------------------8<

[I'm sure you can easily make the code better]

IMO this is not a big improvement over your approach, however it is a
bit more systematic and easier to write than the elaborate matches.

Best,
E.