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, 16 insertions, 0 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 5cb4bcd5a..8f739e0da 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -692,6 +692,22 @@ Proof.
   destruct b; intuition.
 Qed.
 
+(* Rewrite rules about andb, orb and if (used in romega) *)
+
+Lemma andb_if : forall (A:Set)(a a':A)(b b' : bool), 
+  (if b && b' then a else a') = 
+  (if b then if b' then a else a' else a').
+Proof.
+ destruct b; destruct b'; auto.
+Qed.
+
+Lemma negb_if : forall (A:Set)(a a':A)(b:bool), 
+ (if negb b then a else a') = 
+ (if b then a' else a).
+Proof.
+ destruct b; auto.
+Qed.
+
 (* Compatibility *)
 
 Notation andb := Datatypes.andb (only parsing).