diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/setoid_ring/ArithRing.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/setoid_ring/ArithRing.v')
-rw-r--r-- | contrib/setoid_ring/ArithRing.v | 60 |
1 files changed, 0 insertions, 60 deletions
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v deleted file mode 100644 index 601cabe0..00000000 --- a/contrib/setoid_ring/ArithRing.v +++ /dev/null @@ -1,60 +0,0 @@ -(************************************************************************) -(* 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]). - |