The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>]

roconnor AT theorem.ca
 wrote:
Computing the head normal form of proof can be very costly.
Personally I prefer to use the following scheme:
     Definition semi_dec : A -> bool:= .... .
     Lemma semi_dec_correct :forall a, semi_dec a -> complex_proposition.
     Proof. .... Qed.
 Now you can trivially define your function. For proof by reflexion you 
can use the lemma
 semi_dec_correct, and what you have to compute is "semi_dec a" which 
does not contain proof terms.
    Benjamin

             
> I was working on a proof by reflection (for details see 
> <http://r6research.livejournal.com/14509.html>) by creating a function 
> that returns {True}+{complex_proposition}.  Given a result of this 
> type I wanted to extract the proof of complex_proposition (if it 
> exists).  My first attempt to do this was to write an ltac that did:
>
> let s := eval hnf in (sum_term) in
> match s with
> | left _ _ => fail
> | right _ p => assert (H:=p)
> end.
>
> But my problem was that hnf runs too slowly.
>
> I managed to get something to work by using a lemma:
>
> Lemma reflect_right :
> forall A B (x:{A}+{B}), (if x then False else True) -> B.
>
> By applying this lemma, my goal reduces to:
> -----------------------------------
> (if sum_term then False else True)
>
> Now if I try ``constructor'', it still takes a long time to solve the 
> goal, but if I instead do ``lazy beta delta iota zeta'', the the goal 
> almost instantly transforms into True, and then constructor easily 
> solves it. (Similarly if I try hnf at this point, it again takes a 
> long time to transform into True).
>
> My question is, what is hnf doing that takes so long compared to lazy 
> evalutaiton?  Also, is this a reasonable way to use reflection?