Big reorganization of romega/ReflOmegaCore.v: towards a modular

and generic romega tactic...

For the moment, nothing is visible yet from the user's point of view 
(hopefully). But internally, we prepare a romega that can works on 
any integer types. ReflOmegaCore is now separated in several modules: 

* First, an interface Int that specifies the minimal amount of things 
  needed on our integer type for romega to work: 
  - int should be a ring (re-use of ring_theory definition ;-)
  - it should come with an total order, compatible with + * -
  - we should have a decidable ternary comparison function
  - moreover, we ask one (and only one!) critical property specific to
    integers:    a<b <-> a<=b-1

* Then a functor IntProperties derives from this interface all the 
  various lemmas on integers that are used in the romega part, 
  in particular the famous OMEGA?? lemmas. 
  
* The romega reflexive part is now in another functor IntOmega, 
  that rely on some Int: no more Z inside. The main changes is
  that Z0 was a constructor whereas our abstract zero isn't. So
  matching Z0 is transformed into (if beq ... 0 then ...). With
  extensive use of && and if then else, it's almost clearer this way.

* Finally, for the moment Z_as_Int show that Z fulfills our interface, 
  and ZOmega = IntOmega(Z_as_Int) is used by the tactic. 


Remains to be done: 
 - revision of the refl_omega to use any Int instead of just Z, 
   and creating a user interface. 
 - Int has no particular reason to use the leibniz equality (only 
   rely on the beq boolean test). Setoids someday ?
 - a version with "semi-ring" for nat ? or rather a generic way to plug 
   additional equations on the fly, e.g. n>=0 for every nat subpart ?




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9966 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions