Library Coq.ring.LegacyArithRing




Require Import Bool.
Require Export LegacyRing.
Require Export Arith.
Require Import Eqdep_dec.

Open Local Scope nat_scope.


Lemma nateq_prop : forall n m:nat, Is_true (nateq n m) -> n = m.

Hint Resolve nateq_prop: arithring.

Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq.
Defined.

Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ].

Goal forall n:nat, S n = 1 + n.

Ltac rewrite_S_to_plus_term t :=
  match constr:t with
  | 1 => constr:1
  | (S ?X1) =>
      let t1 := rewrite_S_to_plus_term X1 in
      constr:(1 + t1)
  | (?X1 + ?X2) =>
      let t1 := rewrite_S_to_plus_term X1
      with t2 := rewrite_S_to_plus_term X2 in
      constr:(t1 + t2)
  | (?X1 * ?X2) =>
      let t1 := rewrite_S_to_plus_term X1
      with t2 := rewrite_S_to_plus_term X2 in
      constr:(t1 * t2)
  | _ => constr:t
  end.

Ltac rewrite_S_to_plus :=
  match goal with
  | |- (?X1 = ?X2) =>
      try
       let t1 :=
       
       rewrite_S_to_plus_term X1
       with t2 := rewrite_S_to_plus_term X2 in
       change (t1 = t2) in |- *
  | |- (?X1 = ?X2) =>
      try
       let t1 :=
       
       rewrite_S_to_plus_term X1
       with t2 := rewrite_S_to_plus_term X2 in
       change (t1 = t2) in |- *
  end.

Ltac ring_nat := rewrite_S_to_plus; ring.