Open aleloi opened 2 years ago
CoqHammer was designed to work well with "standard Coq", i.e., standard-library-like developments. Poor performance on mathcomp is a known issue and an open research problem (which I personally won't work on in any near future).
One way to improve the success rate on mathcomp problems could be to preprocess mathcomp goals into a form which CoqHammer can handle better. This wouldn't actually require much modification of CoqHammer itself.
Following up: the breflect
tactic (https://coqhammer.github.io/#boolean-reflection) that comes with CoqHammer is a very basic version of such a preprocessing tactic. It converts boolean statements (arguments of is_true
) into propositions in Prop
. You can try it. I don't expect that much success (it doesn't convert any lemmas in the mathcomp library), but it's a start.
I have tried the hammer on mathcomp lemmas and it has mostly failed. Here is a simple example: addition of algebraic complex numbers commutes. I want hammer to construct the proof term
(@GRing.Theory.addrC Algebraics.Implementation.zmodType a b)
. Thepredict
tool finds the correct lemmaGRing.Theory.addrC
, but then all external provers either time out after 10 minutes or crash after using up a few 10s of GB RAM. I think what happens is that the TPTP output fails to encode the conversion betweenAlgebraics.Implementation.zmodType
andalgC =Algebraics.Implementation.Type
. The TPTP output (with a small value for the number of predictions) is uploaded here. I have tested with both few (10) predictions and many (1000). I have also tested with all the supported external provers.Mathcomp heavily uses canonical structures. IIUC (my understanding is taken from section 6.3 of the math comp book), whenever the the unification algorithm experts a zmodType, and the term is not zmodType, it looks in a 'canonical solutions table'. If it finds that there is a canonical construction of zmodType from the type of the current term, it applies the conversion. Here is the conversion that I think predict fails to include in the TPTP output. Can it be that canonical handling is not fully handled in Coq? Or is it
predict
that doesn't include the right conversion?