The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Hi,

I am trying to do some programming with type classes and write proofs
about the programs.  However, the conversion tactics do not seem to be
working as expected.  Here is the smallest example I could come up
with:

<coq>

(* We declare a class for types with decidable equality. *)

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

(* We show that "nat" is an instance of this class. *)

Instance eq_dec_nat: eq_dec_class nat.
Proof. split. exact eq_nat_dec. Defined.

(* We define "is_lt" in terms of "eq_dec". *)

Fixpoint is_lt (m n: nat): bool :=
 match n with
 | 0 => false
 | S (n1) => if eq_dec m n1 then true else is_lt m n1
 end.

(* Now we want to prove a simple lemma. *)

Lemma foo: forall m n, is_lt m n = true -> m < n.
Proof.
 induction n; intros H.
   inversion H.

</coq>

Now at this point, we have one goal left, which has this in its context:

 H: is_lt m (S n) = true

Now what I want is a tactic that does exactly this --

 change (is_lt m (S n))
   with (if eq_dec m n then true else is_lt m n)
   in H.

-- 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 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.

 - Aaron