Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 81 insertions, 0 deletions

diff --git a/contrib7/ring/ArithRing.v b/contrib7/ring/ArithRing.v
new file mode 100644
index 00000000..c2abc4d1
--- /dev/null
+++ b/contrib7/ring/ArithRing.v
@@ -0,0 +1,81 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: ArithRing.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *)
+
+(* Instantiation of the Ring tactic for the naturals of Arith $*)
+
+Require Export Ring.
+Require Export Arith.
+Require Eqdep_dec.
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
+
+Fixpoint nateq [n,m:nat] : bool :=
+  Cases n m of
+  | O O => true
+  | (S n') (S m') => (nateq n' m')
+  | _ _ => false
+  end.
+
+Lemma nateq_prop : (n,m:nat)(Is_true (nateq n m))->n==m.
+Proof.
+  Induction n; Induction m; Intros; Try Contradiction.
+  Trivial.
+  Unfold Is_true in H1.
+  Rewrite (H n1 H1).
+  Trivial.
+Save.
+
+Hints Resolve nateq_prop eq2eqT : arithring.
+
+Definition NatTheory : (Semi_Ring_Theory plus mult (1) (0) nateq).
+  Split; Intros; Auto with arith arithring.
+  Apply eq2eqT; Apply simpl_plus_l with n:=n.
+  Apply eqT2eq; Trivial.
+Defined.
+
+
+Add Semi Ring nat plus mult (1) (0) nateq NatTheory [O S].
+
+Goal (n:nat)(S n)=(plus (S O) n).
+Intro; Reflexivity.
+Save S_to_plus_one.
+
+(* 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.