The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Aaron,
  
Le 15 avr. 2010 à 09:10, Aaron Bohannon a écrit :

<snip/>

> -- without taking so many character to write out.  Under normal
> circumstances, this is exactly what "simpl in H" would do.
> However, in this case "simpl in H" gives me:
> 
> H: (if eq_nat_dec m n then true else is_lt m n) = true
> 
> It has left me with "eq_nat_dec" instead of "eq_dec" in this case.  In
> general, "simpl" seems to have the side-effect of unfolding all nested
> occurrences of any type-class-defined functions and then perform beta
> reduction on them (regardless of whether iota reductions are possible
> after unfolding these type-class-defined functions).  If you can
> imagine a more complex example than this one, you may realize why this
> could be very problematic.  At first, I thought the undesired
> unfolding could be patched up after the fact with --
> 
> fold (eq_dec m n) in H.
> 
> -- but this tactic has no effect, which was rather surprising and dismaying.

This one's probably a bug.

> This lack of control over conversion is really a deal-breaker for
> programming with type classes.  I've been trying to think of a
> practical Ltac incantation to do the reduction I want but haven't
> really come up with one yet.

  There are many workarounds for that situation. One is to prove the equations
of [is_lt] and rewrite with them to simplify expressions, ensuring the best
control over the form of terms. You could also make [eq_dec] or [eq_dec_nat]
temporarily opaque using [Opaque eq_dec] to avoid the reduction. Also, with
singleton classes like this you can declare instead:

Class eq_dec_class (A: Set): Set :=
 eq_dec: forall (a a': A), {a = a'} + {a <> a'}.

Instances of this singleton class are not records but simply objects of
type [forall (a a':A), {a = a'} + {a <> a'}], and [simpl] won't unfold 
applications of the trivial [eq_dec] projection in that case.

  Lastly, you could use a special reduction function like:

  let x := type of H in
  let y := eval cbv beta iota zeta delta -[eq_dec] in x in
    change x with y in H.

However, only [simpl] is able to fold back recursive prototypes 
automatically, 
so you'd always get an unfolded [is_lt] in the reduced term in that case.

Hope this helps,
-- Matthieu