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.