The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT csl.sri.com>]

In his message of Wed April 26, 2000, Pablo Argon writes: 
> 
>       I'm building a "toy" example using the Refine tactic.
> [...]
> But  "I loose" the equality l=(cons a l') deriving from the
> case analysis.
> I don't see any "simple" way (without modifying the function
> given in the Refine) to reintroduce this equality in the hypothesis.

Indeed, you need to make that information available inside the
branches. Here is one way of doing it:

======================================================================
Theorem Quick : (l:(list nat))(Acc (list nat) (LgthOrder nat) l)->(list
nat).
Proof.
Fix Quick 2; Intros l H.
Refine
  (<[x]l=x->(list nat)>Cases l of
       nil        => [_](nil nat)
   |  (cons a l') => [h](Quick (Filter (before a) l') ?) ^ 
                        (cons a (Quick (Filter (after a) l' ) ?))
   end 
   (refl_equal (list nat) l)).
======================================================================

and h is your expecting hypothesis (l=(cons a l'))

This is the way both Program and Correctness tactics manage to avoid
that caveat. Notice that it is no big deal: in the general case, you
just transform

     <P>Cases e of p1 => e1 | ... | pn => en end

into
        
    (<[x]e=x->P>Cases e of p1 => [h1]e1 | ... | pn => [hn]en end 
     (refl_equal T e))

where T is the type of e.       

Hope this helps,
-- 
Jean-Christophe Filliatre    
  Computer Science Laboratory   Phone (650) 859-5173
  SRI International             FAX   (650) 859-2844
  333 Ravenswood Ave.           email  
filliatr AT csl.sri.com
  Menlo Park, CA 94025, USA     web    http://www.csl.sri.com/~filliatr