search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
208 stars 47 forks source link

Near message error #1320

Open mkerjean opened 2 months ago

mkerjean commented 2 months ago

While trying to solve e <= M for e : numFieldtype and M \is_near (nbhs +oo), one gets the error message no applicable tactic. A message including the necessity for e to be real (is this what's happening ?), or to try with normr e, would help a lot, would it be hard to implement?

affeldt-aist commented 1 month ago

While trying to solve e <= M for e : numFieldtype and M \is_near (nbhs +oo), one gets the error message no applicable tactic. A message including the necessity for e to be real (is this what's happening ?),

I guess so, since nbhs_pinfty_ge is registered as a Hint but requires e to verify \is Num.real for which e : R : numFieldType is not sufficient.

or to try with normr e, would help a lot, would it be hard to implement?

Do you mean by using as an intermediate step the lemma ler_norm? But the latter requires a realDomainType so numFieldType is anyway not enough. (I might be missing the point.)

mkerjean commented 1 month ago

While trying to solve e <= M for e : numFieldtype and M \is_near (nbhs +oo), one gets the error message no applicable tactic. A message including the necessity for e to be real (is this what's happening ?),

I guess so, since nbhs_pinfty_ge is registered as a Hint but requires e to verify \is Num.real for which e : R : numFieldType is not sufficient.

or to try with normr e, would help a lot, would it be hard to implement?

Do you mean by using as an intermediate step the lemma ler_norm? But the latter requires a realDomainType so numFieldType is anyway not enough. (I might be missing the point.)

I was suggesting that the error message might say "try using normr e instead of e" or something like that, but I wasn't sure how nbhs_pinfty_ge and similar lemmas were used. As this is with an Hint, can the error message be more precise ? How can we do that ?