5

I am currently trying to generate Haskell code from my program verification lemma, which looks like this:

Lemma the_thing_is_ok : forall (e:Something),  Matches e (calculate_value e).

Right after ending my Section, I do:

Extraction Language Haskell.
Recursive Extraction the_thing_is_ok

And it does not seem to be really happy about something, since it returns the following error:

__ = Prelude.error "Logical or arity value used"

I have another Lemma which does seem to export just fine but I could not figure out what the problem was exactly. Any clues on how to work around that error?

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
wtf8_decode
  • 452
  • 6
  • 19
  • Is your Lemma in Prop, as usually is the case? I believe Coq discards all the Prop information during extraction. E.g. if you extract `{ n:nat | somePredicate n }` you will get a natural, but without the proof of the predicate. – chi Nov 27 '14 at 18:29

1 Answers1

7

Coq erases values of type Prop during extraction—they're considered to have no computational meaning. If you have a computation which requires computing with a Prop then extraction will fail.

J. Abrahamson
  • 72,246
  • 9
  • 135
  • 180
  • Just write your Props in Set. Everything ought to work there essentially the same—the only functional differences are exactly what makes Prop extraction break. – J. Abrahamson Nov 28 '14 at 00:02