Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 60 insertions, 0 deletions

diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
new file mode 100644
index 00000000..e5a4c8d1
--- /dev/null
+++ b/plugins/setoid_ring/ArithRing.v
@@ -0,0 +1,60 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Import Mult.
+Require Import BinNat.
+Require Import Nnat.
+Require Export Ring.
+Set Implicit Arguments.
+
+Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat).
+ Proof.
+  constructor. exact plus_0_l. exact plus_comm. exact plus_assoc.
+  exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc.
+  exact mult_plus_distr_r.
+ Qed.
+
+Lemma nat_morph_N :
+   semi_morph 0 1 plus mult (eq (A:=nat))
+          0%N 1%N Nplus Nmult Neq_bool nat_of_N.
+Proof.
+  constructor;trivial.
+  exact nat_of_Nplus.
+  exact nat_of_Nmult.
+  intros x y H;rewrite (Neq_bool_ok _ _ H);trivial.
+Qed.
+
+Ltac natcst t :=
+  match isnatcst t with
+    true => constr:(N_of_nat t)
+  | _ => constr:InitialRing.NotConstant
+  end.
+
+Ltac Ss_to_add f acc :=
+  match f with
+  | S ?f1 => Ss_to_add f1 (S acc)
+  | _ => constr:(acc + f)%nat
+  end.
+
+Ltac natprering :=
+  match goal with
+    |- context C [S ?p] =>
+    match p with
+      O => fail 1 (* avoid replacing 1 with 1+0 ! *)
+    | p => match isnatcst p with
+           | true => fail 1
+           | false => let v := Ss_to_add p (S 0) in
+                         fold v; natprering
+           end
+    end
+  | _ => idtac
+  end.
+
+Add Ring natr : natSRth
+  (morphism nat_morph_N, constants [natcst], preprocess [natprering]).
+