From 78a52468777ab14cb88a9acd5b26f549177762fa Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 10 Jul 2007 23:54:53 +0000 Subject: 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 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 --- theories/Bool/Bool.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'theories/Bool') 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). -- cgit v1.2.3