From a524c2dab3b6eb2c42c2789489f3dec4e8136ed4 Mon Sep 17 00:00:00 2001 From: bertot Date: Wed, 21 Nov 2001 08:27:54 +0000 Subject: Make sure that NatRing won't loop forever. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2226 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/ring/ArithRing.v | 32 +++++++++++++++++++++++++++++++- 1 file changed, 31 insertions(+), 1 deletion(-) diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v index 0dfb1f4e3..b9883d5cd 100644 --- a/contrib/ring/ArithRing.v +++ b/contrib/ring/ArithRing.v @@ -45,4 +45,34 @@ Goal (n:nat)(S n)=(plus (S O) n). Intro; Reflexivity. Save S_to_plus_one. -Tactic Definition NatRing := (Repeat Rewrite S_to_plus_one); Ring. +(* Replace all occurrences of (S exp) by (plus (S O) exp), except when + exp is already O and only for those occurrences than can be reached by going + down plus and mult operations *) +Recursive Meta Definition S_to_plus t := + Match t With + | [(S O)] -> '(S O) + | [(S ?1)] -> Let t1 = (S_to_plus ?1) In + '(plus (S O) t1) + | [(plus ?1 ?2)] -> Let t1 = (S_to_plus ?1) + And t2 = (S_to_plus ?2) In + '(plus t1 t2) + | [(mult ?1 ?2)] -> Let t1 = (S_to_plus ?1) + And t2 = (S_to_plus ?2) In + '(mult t1 t2) + | [?] -> 't. + +(* Apply S_to_plus on both sides of an equality *) +Tactic Definition S_to_plus_eq := + Match Context With + | [ |- ?1 = ?2 ] -> + (**) Try (**) + Let t1 = (S_to_plus ?1) + And t2 = (S_to_plus ?2) In + Change t1=t2 + | [ |- ?1 == ?2 ] -> + (**) Try (**) + Let t1 = (S_to_plus ?1) + And t2 = (S_to_plus ?2) In + Change (t1==t2). + +Tactic Definition NatRing := S_to_plus_eq;Ring. -- cgit v1.2.3