From 8e9c794b42f00ff4dbcd0e1961a95335e5b88c85 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 18 Jul 2007 22:38:06 +0000 Subject: A generic preprocessing tactic zify for (r)omega ------------------------------------------------ See file PreOmega for more details and/or test-suite/succes/*Omega*.v The zify tactic performs a Z-ification of your current goal, transforming parts of type nat, N, positive, taking advantage of many equivalences of operations, and of the positivity implied by these types. Integration with omega and romega: (r)omega : the earlier tactics, 100% compatible (r)omega with * : full zify applied before the (r)omega run (r)omega with , where is a sub-list of {nat,N,positive,Z}, applies only specific parts of zify (btw "with Z" means take advantage of Zmax, Zmin, Zabs and Zsgn). As a particular consequence, "romega with nat" should now be a close-to-perfect replacement for omega. Slightly more powerful, since (forall x:nat, x*x>=0) is provable and also slightly less powerful: if False is somewhere in the hypothesis, it doesn't use it. For the moment zify is done in a direct way in Ltac, using rewrite when necessary, but crucial chains of rewrite may be made reflexive some day. Even though zify is designed to help (r)omega, I think it might be of interest for other tactics (micromega ?). Feel free to complete zify if your favorite operation / type isn't handled yet. Side-effects: - additional results for ZArith, NArith, etc... - definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope - romega now start by doing "intros". Since the conclusion will be negated, and this operation will be justified by means of decidability, it helps to have as little as possible in the conclusion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10028 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/FSets/FMapAVL.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/FSets/FMapAVL.v') diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index cc2d04e58..6e4c4b26f 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -416,7 +416,7 @@ Ltac bal_tac := Ltac bal_tac_imp := match goal with | |- context [ assert_false ] => - inv avl; avl_nns; simpl in *; false_omega + inv avl; avl_nns; simpl in *; omega_max | _ => idtac end. @@ -703,7 +703,7 @@ Proof. rewrite e3; simpl;destruct 1. split. apply bal_avl; auto. - simpl; omega_max. + omega_max. omega_bal. Qed. -- cgit v1.2.3