The Coq mailing list

[Ben Sherman <sherman AT csail.mit.edu>]

The issue is not so much that [adj_left] is being unfolded in the statement of [adj_left_nat], but rather that it has not yet even been defined at this point. Remember that [adj_left] must take an [Adjunction] as an argument, yet [adj_left_nat] must be present in the *definition* of an [Adjunction], so it cannot possibly refer to [adj_left]. The best one could do is think of the [adj_left] as defining a [let], but this still wouldn't help in unifying in the situation you're running into.

I have run into this issue before, and one approach that I took was to split up such a type class into two parts, one with the "data" and the other with the "proofs". The "proof" part would depend on the "data" part and live in [Prop] rather than [Type], or at least definitions of the "proof" class instances could be closed off opaquely, which can also be beneficial for performance reasons. Then your [adj_left] definition can come *after* the "data" part but before the "proof" part. You could still later choose to package up the data and proof part into a single object.

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

Subject: [Coq-Club] Question about definitions inside type classes

Date: April 25, 2017 at 4:59:11 AM EDT

To: coq-club AT inria.fr

Reply-To: coq-club AT inria.fr

I have a type class with some defined members:

Class Adjunction := {
 adj_iso  {a b} : F a ~{C}~> b ≊ a ~{D}~> U b;
 adj_left  {X Y} := to (@adj_iso X Y);
 adj_left_nat_l {a b c} (f : F b ~> c) (g : a ~> b) :
   adj_left _ _ (f ∘ fmap[F] g) ≈ adj_left _ _ f ∘ g
}.

As you can see, adj_left is defined directly in terms of adj_iso.

My problem is that I cannot rewrite suing adj_left_nat_l when I see a use of
"adj_left" in my goal, because adj_left_nat_l has already unfolded the
definition of adj_left and is actually now in terms of adj_iso. I have to
simplify my goal to unfold adj_left to a use of adj_iso, and then the rewrite
works.

Is there any way to make the member adj_left so that it does not unfold on
simplification, and is not unfolded in the type of adj_left_nat_l?

-- 
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2