# RpRing.v: Ring and Field tactics for Rplus

Contributed by David Baelde, 2011

Require Import Uprop.
Require Import Rplus.
Open Scope Rp_scope.

Require Export Ring.

Lemma RplusSRth : semi_ring_theory R0 R1 Rpplus Rpmult (Oeq (A:=Rp)).

## Power theory and how to recognize constant in powers

Require Import NArith.

Lemma RplusSRpowertheory :
power_theory R1 Rpmult (@Oeq Rp Rpord)
nat_of_N Rpexp.

## Morphism for coefficients in nat

Lemma RplusSRmorph :
semi_morph R0 R1 Rpplus Rpmult (@Oeq Rp Rpord)
0%nat 1%nat plus mult beq_nat
N2Rp.

Ltac is_nat_cst n :=
match n with
| minus ?x ?y =>
match (is_nat_cst x) with
| true =>
match (is_nat_cst y) with
| true => constr:true
| false => constr:false
end
| false => constr:false
end
| S ?p => is_nat_cst p
| O => constr:true
| _ => constr:false
end.

Ltac nat_cst t :=
match is_nat_cst t with
| true => constr:(N_of_nat t)
| false => constr:NotConstant
end.

Ltac coeff_nat t :=
match t with
| N2Rp ?n =>
match is_nat_cst n with
| true => n | _ => constr:NotConstant
end
| _ => constr:NotConstant
end.

Add Ring Rp_ring : RplusSRth (morphism RplusSRmorph,
constants [coeff_nat],
power_tac RplusSRpowertheory [nat_cst]).

## Tests

Goal forall x y, x * 2 * x + y * x == x * y + 2 * x * x.

Goal forall x y, x * y * x == y * x^2.

## Field

Require Export Field.

Lemma RplusSFth :
semi_field_theory R0 R1 Rpplus Rpmult Rpdiv Rp1div (Oeq (A:=Rp)).

Ltac remove_Sx x := match goal with
| |- context[(S x)] => change (S x) with (1+x)%nat
end.

Ltac remove_S := match goal with
| x:nat |- _ => remove_Sx x
end.

Ltac field_pre :=
try apply Ole_refl_eq;
repeat remove_S;
repeat first [
rewrite U2Rp_Unth

| rewrite <- plus_Sn_m
| rewrite <- N2Rp_plus
| rewrite N2Rp_mult ].

Add Field Rp_field : RplusSFth (morphism RplusSRmorph,
constants [coeff_nat],
power_tac RplusSRpowertheory [nat_cst],
preprocess [field_pre],
postprocess [auto]).
Trick to kill subgoals of fields
Lemma post_field_notz : forall x, notz (N2Rp x) -> ~ (mkRp x 0 == R0).
Hint Resolve post_field_notz.

Section Test.

Variable x y z : Rp.
Variable n : nat.

Goal (1 / 2 * x + 1 / 2 * x == x).

Goal (x / 2 + x) * x == x^2 * 3 / 2.

Goal 3 * x == 6 * x * [1/2].

Goal ([1/2] * x + x) * x <= x^2 * 3 / 2.

Goal N2Rp (2-1)%nat == R1.

Goal x^(2-1) == x^1.

Goal (S (S n)) * x == (S n) * x + x.

End Test.