Equality of constructors with dependent types coq

Question

I have the following setup (sorry if it's a bit long for an MCVE) and am trying to prove the last theorem, but I'm getting stuck because it can't unify the types of the morphisms as they rely on theoretically different object types, even though the object types are identical.

Is there a general strategy for decomposing constructors with dependent types in them? injection and inversion produce what seem to be useless results having to do with ob_fn (which I can prove the equivalent theorem for easily) rather than morph_fn.

Inductive Cat := cons_cat (O : Type) (M : O -> O -> Type).

Definition ob (c : Cat) :=
    match c with cons_cat o _ => o end.

Definition morph (c : Cat) : ob c -> ob c -> Type :=
    match c with cons_cat _ m => m end.

Inductive Functor
    (A B : Cat)
        : Type :=
    cons_functor
        (ob_fn : ob A -> ob B)
        (morph_fn : forall {c d : ob A}, morph A c d -> morph B (ob_fn c) (ob_fn d)).

Definition ob_fn {A B : Cat} (f : Functor A B) : ob A -> ob B :=
    match f with cons_functor f' _ => f' end.

Definition morph_fn {A B : Cat} {c d : ob A} (f : Functor A B)
        : morph A c d -> morph B (ob_fn f c) (ob_fn f d) :=
    match f with cons_functor _ f' => f' c d end.

Theorem functor_decompose {A B : Cat} {o fm gm} : cons_functor A B o fm = cons_functor A B o gm -> fm = gm.
    intros H.
    assert (forall c d, @morph_fn A B c d (cons_functor A B o fm) = @morph_fn A B c d (cons_functor A B o gm)).
        intros.
        rewrite H.

You are facing the typical problem with dependent types, your goal can't be rewritten as it won't be well typed when it is generalized over the first parameter. If you want to introduce axioms you can use eq_dec or JM_eq to avoid this problem, (or alternatively you could make some of your base types decidable) If not, you will have little other option than proving injectivity with a complex pattern matching. — ejgallego
If I assume that my base types are decidable (I assume you mean O in this example), is there a straightforward path to a solution? — k_g
Yes, there is. See Dependent Case Analysis in Coq without Axioms by James Wilcox. An excerpt from the linked post: "if the indices have a type with decidable equality, you don't need JMeq to get dependent case analysis". Alternatively, you can Require Import Coq.Program.Equality. and do dependent destruction on the constructor equality. The resulting proof in this case will use some additional axioms. Use Print Assumptions <name>. to get them. — Anton Trunov

Jason Gross Jason Gross · Accepted Answer · 2017-07-28T04:57:08

The standard pattern is to convert your records into sigma types and talk about either equality of sigma types, or transported equality of the fields. See, e.g., this version of functor_decompose used in the HoTT library. You might also be interested in the inversion_sigma tactic of Coq 8.7 and the corresponding sigma equality classifications.

Equality of constructors with dependent types coq

1 Answers