The Coq mailing list

[roconnor AT theorem.ca]

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?

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''