Use Defined for EqDec instances instead of Qed

adampetcher / fcf

Foundational Cryptography Framework for machine-checked proofs of cryptography.

Other

48 stars 23 forks source link

Use Defined for EqDec instances instead of Qed #24

Open jbaum98 opened 6 years ago

jbaum98 commented 6 years ago

As described in PrincetonUniversity/VST#290, the use of Qed when creating typeclass instances makes it so that you can't evaluate expressions using the typeclass:

Compute 1 ?= 1.
     = (let (eqb, _) := nat_EqDec in eqb) 1 1

The instances in EqDec.v that currently end in Qed and shoulde be changed to Defined are:

Vector_EqDec
unit_EqDec
bool_EqDec
nat_EqDec
option_EqDec
list_EqDec

adampetcher commented 6 years ago

This is likely a good idea, but making definitions transparent tends to cause problems when they are used. At least, it used to cause problems in older versions of Coq. Can you produce a pull request so I can see how well this works in Coq 8.8?