The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

I know, it is not satisfactory, but you can do:

Lemma foo: forall m n, is_lt m n = true -> m < n.
Proof.
 induction n; intros H.
   inversion H.
 cbv delta [is_lt] iota beta in H.
 fold is_lt in H.
 destruct (eq_dec m n).
  case e; left.
 right; now apply IHn.
Qed.

As far as I know simpl does something similar, but it guesses more than
just is_lt to use (~cbv delta iota beta zeta. fold {all unfolded
fixpoints}).

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


-- 
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay