The Coq mailing list

[Florian Steinberg <florian.steinberg AT inria.fr>]

Hi!

I've meanwhile figured out where my problem came from: I use the Rstruct.v file which proves two lemmas RlebP and RleP, where RleP gets the R_numDomainType involved whose definition uses the epsilon axiom and functional extensionality. I meant to use RlebP and misstyped...

So... this problem was easy to fix but super hard to locate. In particular, if I print the assumptions of RleP it does not show anything suspicious, just the regular operations on the Reals. Even if you go look through its proof of RleP everything looks fine... But if I use it in combination with lra additional axioms get involved. Am I missing a good way to troubleshoot for something like this?

Best,

Florian

On 25/01/2019 13:44, Tej Chajed wrote:

Another source of problems is that firstorder by default calls [auto with *] on all goals, using all hint databases, which is far too aggressive (here's a bug report proposing to fix this). In the meantime you can use [Set Firstorder Solver auto] or manually pass firstorder a tactic.

Note that it doesn't matter what hint database the INR_eq theorem is in if you're using firstorder auto with *.

On Fri, Jan 25, 2019 at 7:15 AM Laurent Thery <Laurent.Thery AT inria.fr> wrote:

Hi

it is just that the theorem INR_eq : INR m = INR n -> m = n has wrongly
been put in the hint resolve database of reals.
When you load Psatz you lod this database.

So firstorder automatically lifts your equality to the reals applying
this theorem and then unlift it by f_equal to finally prove it with
omega ;-)

Could you file a bug report at

https://github.com/coq/coq/issues

so we remember to fix this issue.


On 1/25/19 7:14 AM, Caitlin D'Abrera wrote:
> Hi all, 
>
> I have noticed some peculiar behaviour with tactics like firstorder and
> was hoping for an explanation.
>