The Coq mailing list

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

Hi!

I'd be interested in an answer to this question too.

I am not sure if this is related but I've also had a problem where unwanted axioms started showing up when using tactics from Psatz. I was using lra to prove some inequalities over real numbers, so I was expecting the axioms of the reals, but I additionally got the epsilon axiom. I never actually pined down where it came from, because I didn't know how, but lra was my main suspect. I don't really mind the axiom but I'd rather not use it if I don't need to.

Btw, @Caitlin: I believe the axioms of the reals have some classical consequences that leak to types different from the reals through the inclusion mappings and the rounding function. Proving the axioms for the naturals is not enough to remove them. It shouldn't make a difference in your setting, though. Anyway, what I want to say is I think you are right in wanting to avoid them.

Best,

Florian

On 25/01/2019 07:14, Caitlin D'Abrera wrote:

Hi all, 

I have noticed some peculiar behaviour with tactics like firstorder and was hoping for an explanation.

I had been using firstorder with expressions that involve standard library nat as well as my own definitions. I noticed the following:
  1) When I had "Require Import Psatz", sometimes firstorder would use a bunch of axioms (as displayed with "Print Assumptions my_lem.") As far as I can see, all the axioms are easily provable with e.g. nat and lt, gt, plus, etc.
  2) If I don't import Psatz, firstorder either doesn't alter the goal or it does without using the aforementioned axioms.

MWE: https://gist.github.com/caitlindabrera/0a9c43c919352101718dadc08f32609a.

I don't want to be relying on these axioms, particularly because I don't need them. I've found a workaround for my current context: use "Require Import Lia" instead of Psatz, which allows firstorder to work with similar strength as before but without having access to Raxioms. 

I am still puzzled though; why would Psatz use the axioms in Raxioms when they're so obviously provable (and I think all proven elsewhere for nat)? R seems to be modelling reals (not nat) so why is it being called upon in my context, which doesn't use reals, at all?

Best regards,

Caitlin