Library ALEA.RpRing
Add Rec LoadPath "." as ALEA.
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)).
Require Import NArith.
Lemma RplusSRpowertheory :
power_theory R1 Rpmult (@Oeq Rp Rpord)
nat_of_N Rpexp.
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]).
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.
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.