The Coq mailing list

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

On Thu, Apr 15, 2010 at 9:46 AM, Matthieu Sozeau 
<mattam AT mattam.org>
 wrote:
>  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.

That's a principled way to do things, but impractical unless these
equations are generated automatically.  I forget, wasn't there some
newer facility that does generate these equations automatically?

The other suggestions are partially helpful, but let me give a
slightly more complex example.

<coq>

Inductive A: Set := A0: A | A1: nat -> A.
Inductive B: Set := B0: B | B1: A -> B -> B.

Class Summable (X: Set): Set := { sum: X -> nat }.

Instance nat_Summable: Summable nat := { sum := fun x => x }.

Instance A_Summable: Summable A :=
  { sum := fun a =>
      match a with
      | A0 => 0
      | A1 n => sum n
      end
  }.

Fixpoint sum_B (b: B): nat :=
  match b with
  | B0 => 0
  | B1 a b1 => sum a + sum_B b1
  end.

Instance B_Summable: Summable B := { sum := sum_B }.

Lemma foo:
  forall (a1 a2: A) (b: B),
  sum a1 = sum a2 -> sum (B1 a1 b) = sum (B1 a2 b).
Proof.
  intros ? ? ? H.

</coq>

At this point, I would hope that "simpl" would leave me with --

  sum a1 + sum_B b = sum a2 + sum_B b

-- or even better:

  sum a1 + sum b = sum a2 + sum b

Instead, "sum a1" and "sum a2" get fully expanded into their primitive
definitioins.  (Obviously, I can't make "sum" opaque here before I use
"simpl".)  Other than being difficult to read (imagine a much larger
program), I cannot use "rewrite H" after "simpl".  Of course, in this
case, I can just use "simpl; simpl in H; rewrite H", but, more
generally, I may have a lemma that looks like H rather than a
hypothesis in the context -- and perhaps more importantly, the fully
expanded terms make it difficult to discover which lemma I want to
use.

It seems the situation can be partly alleviated by using an auxiliary
definition for "sum_A" as I did with "sum_B", in order to block the
reduction performed by "simpl".  (I didn't really understand this
principal before I wrote my last email.)  Maybe that's not too
troublesome, but it does make type classes a little more cumbersome
than they would be with better conversion tactics.

 - Aaron