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

1 files changed, 10 insertions, 0 deletions

diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 2a5e7f3c4..7cfad89e4 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -89,3 +89,13 @@ Proof.
     intros n H1 H2. discriminate H2.
     intros n H1 z H2 H3. case (H2 _ H3). reflexivity.
 Defined.
+
+Lemma beq_nat_true : forall x y, beq_nat x y = true -> x=y.
+Proof.
+ induction x; destruct y; simpl; auto; intros; discriminate.
+Qed.
+
+Lemma beq_nat_false : forall x y, beq_nat x y = false -> x<>y.
+Proof.
+ induction x; destruct y; simpl; auto; intros; discriminate.
+Qed.