The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi Aaron,

You could simply make the instance opaque by closing the proof with
Qed instead of Defined. This will prevent the terms whose head symbol
is eq_dec from being reduced.
I realize you might be interested in keeping the instances transparent
in case you want to actually compute, and in that case you can get the
same effect by using Global Opaque eq_dec. This command basically
makes eq_dec opaque for all the conversion tactics simpl, unfold etc,
but you will still be able to compute using vm_compute. This is very
handy for making sure that some definitions are not unfolded or
reduced during the interactive proofs while still allowing computation
(e.g. I found out it is a good idea to always declare a function
defined with Function as Opaque, else some tactics tend to try and do
too much and end up looking at the underlying -big- term ; more
generally, once a function has been fully specified and its body is
not needed except for the sole purpose of computation, it can be made
opaque in this way).

Hope this helps,

Stéphane

On Thu, Apr 15, 2010 at 3:10 PM, Aaron Bohannon 
<bohannon AT cis.upenn.edu>
 wrote:
> 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
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06