The Coq mailing list

[Caitlin D'Abrera <Caitlin.Dabrera AT anu.edu.au>]

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