aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/ArithRing.v
blob: 601cabe003825367021fc369a6852deb879b8f86 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
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]).