1
$\begingroup$

Context

I am currently learning how to use the Coq proof assistant and am at the level where I know the fundamentals of dependent-type theory and have done most of the "Software Foundations" book reading / exercises. As a form of practice with the tool and to prepare to prove nontrivial results later, I have decided to as an exercise define and prove basic results about various common structures. Currently I am tackling categories.

In this endeavour I have come upon a problem (of not being able to apply destruct) in Ltac that I can't solve despite its easy mathematical content. I have made partial headway looking into solutions here / stack-overflow but am unable to fully reduce the match-statements in my goal and am looking for advice.

Below are the definitions of categories / functors I have been using for context:

Definitions Used

Definition Function_Extensionality := forall (A:Type) (B: A -> Type) (f g: (forall (a:A),B a)), (forall a: A, f a = g a) -> f = g.

Record  Category_By_Hom_Types := {
object_type                 :  Type;
morphism_type               : object_type -> object_type -> Type;
identity_morphism           : forall (A: object_type), (morphism_type A A);
morphism_composition        : forall (X Y Z: object_type) (g : (morphism_type Y Z)) (f : (morphism_type X Y)), (morphism_type X Z);
composition_associator      : forall (W X Y Z: object_type) (h : (morphism_type Y Z)) (g : (morphism_type X Y)) (f : (morphism_type W X)), morphism_composition _ _ _ h (morphism_composition _ _ _ g f) = (morphism_composition _ _ _ (morphism_composition _ _ _ h g) f);
identity_morphism_left_unitor : forall (X Y: object_type) (f: (morphism_type X Y)), morphism_composition _ _ _ (identity_morphism Y) f = f;
identity_morphism_right_unitor : forall (X Y: object_type) (f: (morphism_type X Y)), morphism_composition _ _ _ f (identity_morphism X) = f;
}.

(* Shorthands for Categories *)
Notation CHT := Category_By_Hom_Types.
Notation O := object_type.
Notation A := morphism_type.
Notation o := ( morphism_composition _ _ _ _ ).
Notation i := identity_morphism.
Notation i_left_unit := (identity_morphism_left_unitor).
Notation i_right_unit := (identity_morphism_right_unitor).
Notation o_assoc := composition_associator.

Record Functor_By_Hom_Types (C D : Category_By_Hom_Types) := {
map_of_objects : O C -> O D;
map_of_morphisms                    : forall (X Y: O C), (A C X Y) -> (A D ( map_of_objects X) (map_of_objects Y));
functor_commutes_with_composition   : forall (X Y Z: O C) (g: (A C Y Z)) (f: (A C X Y)), map_of_morphisms _ _ (o g f) = o (map_of_morphisms _ _  g) (map_of_morphisms _ _  f);
functor_commutes_with_identity      : forall (X: O C), map_of_morphisms _ _  (i C X) = (i D (map_of_objects X));
}.

(* Shorthands for Functors *)
Notation FHT := Functor_By_Hom_Types.
Notation OF := (map_of_objects _ _).
Notation AF := (fun F f => map_of_morphisms _ _ F _ _ f ).
Notation comm_F := (functor_commutes_with_composition _ _).
Notation unit_F := (functor_commutes_with_identity _ _).

Lemma Functor_Composition : forall (B C D : CHT) (G: (FHT C D)) (F: (FHT B C)) ,(FHT B D).
Proof.
intros B C D G F.
unshelve epose (OH := (fun X => (OF G (OF F X)))  : O B -> O D).
unshelve epose (MH := (fun X Y f => (AF G (AF F f)) ) : forall (X Y: O B), (A B X Y) -> (A D ( OH X) (OH Y))).
assert (Wo : forall (X Y Z: O B) (g: (A B Y Z)) (f: (A B X Y)), MH _ _ (o g f) = o (MH _ _ g) (MH _ _ f) ).
intros X Y Z g f.
unfold MH.
rewrite -> (comm_F F ).
rewrite -> (comm_F G ).
reflexivity.
assert (Wi : forall (X: O B), MH X X  (i B X) = (i D (OH X))).
intros X.
unfold MH.
unfold OH.
rewrite -> (unit_F F _).
rewrite -> (unit_F G _).
reflexivity.
exact {|map_of_objects := OH;map_of_morphisms := MH;functor_commutes_with_composition := Wo;functor_commutes_with_identity := Wi|}.
Defined.

Notation oFunctor := (Functor_Composition _ _ _).

Problem

I wish to prove inhabit a type of the form:

Lemma FE_Functor_Composition_is_Associative :  Function_Extensionality -> forall (A B C D : CHT) (H: (FHT C D)) (G: (FHT B C)) (F: (FHT A B)), oFunctor H (oFunctor G F) = oFunctor (oFunctor H G) F.

to prove this result I aim to simply compute and use function extentionality to equate the projections functor_commutes_with_composition and functor_commutes_with_identity. This leads me to begin a proof of the form:

intros Q A B C D H G F.
destruct (F) as [of af wof wif].
destruct (G) as [og ag wog wig].
destruct (H) as [oh ah woh wiH].
unfold oFunctor.
f_equal.
repeat (apply (Q _ _ _);intros).
compute.

At this stage in the proof I am left with two truly awful looking subgoals asking to prove equality between to equality types (=). However, they are of the form of repeated match statements where all cases lead to the element eq_refl. In all proofs and exercises I have done in the past in this state, I have simply needed only copy-paste the term t inside the match-clause to apply a tactic of the form destruct (t). to massage the goal / computation as required. Yet trying to doso results in an error of the form

Abstracting over the terms "m" and "e" leads to a term  ... <Super long term> ... ill-formed elimination predicate.

Clearly there is some miss-understanding with my attempt. However looking around I can attempt repeat match goal with |- context[match ?S with _ => _ end] => destruct S end. This seems to reduce the problem somewhat in size but I still end up with match statements that are to me intractable. For reference here is the first subgoal (rather long).

match
  match
    match
      match wog (of a) (of a0) (of a1) (af a0 a1 a2) (af a a0 a3) in (_ = a4) return (a4 = ag (of a) (of a1) (morphism_composition3 (of a) (of a0) (of a1) (af a0 a1 a2) (af a a0 a3))) with
      | eq_refl => eq_refl
      end in (_ = a4) return (a4 = morphism_composition2 (og (of a)) (og (of a0)) (og (of a1)) (ag (of a0) (of a1) (af a0 a1 a2)) (ag (of a) (of a0) (af a a0 a3)))
    with
    | eq_refl => eq_refl
    end in (_ = a4) return (a4 = ag (of a) (of a1) (o (af a0 a1 a2) (af a a0 a3)))
  with
  | eq_refl => eq_refl
  end in (_ = a4)
  return
    (ah (og (of a)) (og (of a1)) a4 =
     morphism_composition0 (oh (og (of a))) (oh (og (of a0))) (oh (og (of a1))) (ah (og (of a0)) (og (of a1)) (ag (of a0) (of a1) (af a0 a1 a2))) (ah (og (of a)) (og (of a0)) (ag (of a) (of a0) (af a a0 a3))))
with
| eq_refl =>
    match
      match
        woh (og (of a)) (og (of a0)) (og (of a1)) (ag (of a0) (of a1) (af a0 a1 a2)) (ag (of a) (of a0) (af a a0 a3)) in (_ = a4)
        return (a4 = ah (og (of a)) (og (of a1)) (morphism_composition2 (og (of a)) (og (of a0)) (og (of a1)) (ag (of a0) (of a1) (af a0 a1 a2)) (ag (of a) (of a0) (af a a0 a3))))
      with
      | eq_refl => eq_refl
      end in (_ = a4)
      return
        (a4 =
         morphism_composition0 (oh (og (of a))) (oh (og (of a0))) (oh (og (of a1))) (ah (og (of a0)) (og (of a1)) (ag (of a0) (of a1) (af a0 a1 a2)))
           (ah (og (of a)) (og (of a0)) (ag (of a) (of a0) (af a a0 a3))))
    with
    | eq_refl => eq_refl
    end
end =
match
  match
    match
      match wog (of a) (of a0) (of a1) (af a0 a1 a2) (af a a0 a3) in (_ = a4) return (a4 = ag (of a) (of a1) (morphism_composition3 (of a) (of a0) (of a1) (af a0 a1 a2) (af a a0 a3))) with
      | eq_refl => eq_refl
      end in (_ = a4)
      return
        (ah (og (of a)) (og (of a1)) a4 =
         morphism_composition0 (oh (og (of a))) (oh (og (of a0))) (oh (og (of a1))) (ah (og (of a0)) (og (of a1)) (ag (of a0) (of a1) (af a0 a1 a2)))
           (ah (og (of a)) (og (of a0)) (ag (of a) (of a0) (af a a0 a3))))
    with
    | eq_refl =>
        match
          match
            woh (og (of a)) (og (of a0)) (og (of a1)) (ag (of a0) (of a1) (af a0 a1 a2)) (ag (of a) (of a0) (af a a0 a3)) in (_ = a4)
            return (a4 = ah (og (of a)) (og (of a1)) (morphism_composition2 (og (of a)) (og (of a0)) (og (of a1)) (ag (of a0) (of a1) (af a0 a1 a2)) (ag (of a) (of a0) (af a a0 a3))))
          with
          | eq_refl => eq_refl
          end in (_ = a4)
          return
            (a4 =
             morphism_composition0 (oh (og (of a))) (oh (og (of a0))) (oh (og (of a1))) (ah (og (of a0)) (og (of a1)) (ag (of a0) (of a1) (af a0 a1 a2)))
               (ah (og (of a)) (og (of a0)) (ag (of a) (of a0) (af a a0 a3))))
        with
        | eq_refl => eq_refl
        end
    end in (_ = a4) return (a4 = ah (og (of a)) (og (of a1)) (ag (of a) (of a1) (morphism_composition3 (of a) (of a0) (of a1) (af a0 a1 a2) (af a a0 a3))))
  with
  | eq_refl => eq_refl
  end in (_ = a4)
  return
    (a4 =
     morphism_composition0 (oh (og (of a))) (oh (og (of a0))) (oh (og (of a1))) (ah (og (of a0)) (og (of a1)) (ag (of a0) (of a1) (af a0 a1 a2))) (ah (og (of a)) (og (of a0)) (ag (of a) (of a0) (af a a0 a3))))
with
| eq_refl => eq_refl
end

Note that all possible cases will lead to needing to witness a type of the form eq_refl = eq_refl, in essence all roads lead to reflexivity. I * Should * be able to just brute-force destruct and be done but it seems I am unable to do so and are thus stuck. please advise!

Note, I have used this strategy to prove a lemma of the form FE_OPOP: Function_Extensionality -> (forall (C :CHT), (Opposite_Category (Opposite_Category C)) = C). for the standard notion of opposite category internalized w.r.t. my definition of category by applying the same strategy as above, the difference is that in the opposite category case the element that needed destructing went trough without complaint.

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ For me your code dies on Notation O with The reference Category_By_Hom_Types.object_type. Are you secretly setting some options we don't know about? $\endgroup$
    – Andrej Bauer
    Commented Mar 21 at 12:50
  • $\begingroup$ yes I removed this from a larger body of Coq. I will quickly fix $\endgroup$
    – user2628206
    Commented Mar 21 at 15:39
  • $\begingroup$ fixed the error! $\endgroup$
    – user2628206
    Commented Mar 21 at 15:42

1 Answer 1

Reset to default
2
$\begingroup$

Solution 1. Use UIP (Uniqueness of Identity Proofs).

From Coq Require Import ProofIrrelevance.

About UIP.
(*
   UIP : forall (U : Type) (x y : U) (p1 p2 : x = y), p1 = p2
 *)

UIP is not provable in Coq. That's arguably why you were having trouble. But it's fine to admit, at least as a starting point.

Life without UIP is harder. You have to be careful about the syntax of equality proofs. "Simplify and destruct" has no power here. You might like to read Formalizing Category Theory in Agda to see what it's like.

Solution 2. Think in higher category theory

If you want to avoid UIP, you must then reason about the structure of the equality type: stop thinking of equality as an equivalence relation, but as a category instead.

Once proofs of equality are accepted as non-trivial constructions, the definition of a category, naively written out in dependent type theory, actually defines a wild category---which is a kind of 2-category.

Concretely, to prove an equality between morphisms f = g is to construct a morphism in a discrete category. You can do a lot with just the following combinators (using the names from the Coq standard library):

  • eq_refl : x = x
  • eq_trans : x = y -> y = z -> x = z
  • eq_sym : x = y -> y = x
  • f_equal f : x = y -> f x = f y

and they satisfy the usual categorical equations, which enables equational reasoning about proofs of equality.

(Here's an example using this approach: https://gist.github.com/Lysxia/c33a3757f4184e993610d73cff757265)

Improve this answer
$\endgroup$
10
  • $\begingroup$ Is what I wish to prove dependent on UIP? I am aware of Proof irrelevance as a concept and was trying to avoid it where possible. $\endgroup$
    – user2628206
    Commented Mar 21 at 15:44
  • 1
    $\begingroup$ You can probably do this particular proof without UIP, but then that goes beyond the goal of "define and prove basic results about various common structures". If you want to take the computational content of equality proofs into account, then what you will have formalized is a richer structure than the pen-and-paper definitions of categories and functors. $\endgroup$
    – Li-yao Xia
    Commented Mar 21 at 16:27
  • $\begingroup$ Noted. Thanks for the info. I will accept your answer in this case. Other than what you have already provided (am looking into it rn), do you have any other resources of note that would help me tackle this problem without UIP (either ltac tactics or research papers or names of richer structures)? $\endgroup$
    – user2628206
    Commented Mar 21 at 16:52
  • 2
    $\begingroup$ @user2628206 The "richer structure" you get is a 2-category. Instead of "proving an equality", think of it as "constructing a morphism (in the discrete category)". Instead of rewrite, use the combinators f_equal and eq_trans, which can then be reasoned about categorically. Here's a commented proof of associativity using your definitions: gist.github.com/Lysxia/c33a3757f4184e993610d73cff757265 $\endgroup$
    – Li-yao Xia
    Commented Mar 22 at 10:09
  • 1
    $\begingroup$ Given your gist, would it not make more sense for this answer to not mention UIP at all and just explain how to do it using the technology of gist? Also, I don't think you've got a 2-category, but rather a wild category. It's just that 2-categorical thinking suffices for finding the proof, but the higher-categorical structure is still there. $\endgroup$
    – Andrej Bauer
    Commented Mar 22 at 12:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.