Library Coq.setoid_ring.InitialRing
Require Import Zbool.
Require Import BinInt.
Require Import BinNat.
Require Import Setoid.
Require Import Ring_theory.
Require Import Ring_polynom.
Import List.
Set Implicit Arguments.
Import RingSyntax.
Definition NotConstant := false.
Z is a ring and a setoid
Lemma Zsth : Setoid_Theory Z (@eq Z).
Proof (Eqsth Z).
Lemma Zeqe : ring_eq_ext Z.add Z.mul Z.opp (@eq Z).
Proof (Eq_ext Z.add Z.mul Z.opp).
Lemma Zth : ring_theory Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z).
Proof.
constructor. exact Z.add_0_l. exact Z.add_comm. exact Z.add_assoc.
exact Z.mul_1_l. exact Z.mul_comm. exact Z.mul_assoc.
exact Z.mul_add_distr_r. trivial. exact Z.sub_diag.
Qed.
Two generic morphisms from Z to (abrbitrary) rings, second one is more convenient for proofs but they are ext. equal
Section ZMORPHISM.
Variable R : Type.
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
Variable req : R -> R -> Prop.
Notation "0" := rO. Notation "1" := rI.
Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Variable Rsth : Setoid_Theory R req.
Add Parametric Relation : R req
reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
transitivity proved by Rsth.(@Equivalence_Transitive _ _)
as R_setoid3.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
Proof. exact (Radd_ext Reqe). Qed.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3.
Proof. exact (Rmul_ext Reqe). Qed.
Add Morphism ropp with signature (req ==> req) as ropp_ext3.
Proof. exact (Ropp_ext Reqe). Qed.
Fixpoint gen_phiPOS1 (p:positive) : R :=
match p with
| xH => 1
| xO p => (1 + 1) * (gen_phiPOS1 p)
| xI p => 1 + ((1 + 1) * (gen_phiPOS1 p))
end.
Fixpoint gen_phiPOS (p:positive) : R :=
match p with
| xH => 1
| xO xH => (1 + 1)
| xO p => (1 + 1) * (gen_phiPOS p)
| xI xH => 1 + (1 +1)
| xI p => 1 + ((1 + 1) * (gen_phiPOS p))
end.
Definition gen_phiZ1 z :=
match z with
| Zpos p => gen_phiPOS1 p
| Z0 => 0
| Zneg p => -(gen_phiPOS1 p)
end.
Definition gen_phiZ z :=
match z with
| Zpos p => gen_phiPOS p
| Z0 => 0
| Zneg p => -(gen_phiPOS p)
end.
Notation "[ x ]" := (gen_phiZ x).
Definition get_signZ z :=
match z with
| Zneg p => Some (Zpos p)
| _ => None
end.
Lemma get_signZ_th : sign_theory Z.opp Zeq_bool get_signZ.
Proof.
constructor.
destruct c;intros;try discriminate.
injection H as <-.
simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
Qed.
Section ALMOST_RING.
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext3.
Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
Proof.
induction x;simpl.
rewrite IHx;destruct x;simpl;norm.
rewrite IHx;destruct x;simpl;norm.
rrefl.
Qed.
Lemma ARgen_phiPOS_Psucc : forall x,
gen_phiPOS1 (Pos.succ x) == 1 + (gen_phiPOS1 x).
Proof.
induction x;simpl;norm.
rewrite IHx;norm.
add_push 1;rrefl.
Qed.
Lemma ARgen_phiPOS_add : forall x y,
gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
Proof.
induction x;destruct y;simpl;norm.
rewrite Pos.add_carry_spec.
rewrite ARgen_phiPOS_Psucc.
rewrite IHx;norm.
add_push (gen_phiPOS1 y);add_push 1;rrefl.
rewrite IHx;norm;add_push (gen_phiPOS1 y);rrefl.
rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl.
rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;rrefl.
rewrite IHx;norm;add_push(gen_phiPOS1 y);rrefl.
add_push 1;rrefl.
rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl.
Qed.
Lemma ARgen_phiPOS_mult :
forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.
Proof.
induction x;intros;simpl;norm.
rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm.
rewrite IHx;rrefl.
Qed.
End ALMOST_RING.
Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
Let ARth := Rth_ARth Rsth Reqe Rth.
Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext4.
Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
Proof.
destruct x;simpl; try rewrite (same_gen ARth);rrefl.
Qed.
Lemma gen_Zeqb_ok : forall x y,
Zeq_bool x y = true -> [x] == [y].
Proof.
intros x y H.
assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1.
rewrite H1;rrefl.
Qed.
Lemma gen_phiZ1_pos_sub : forall x y,
gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.
Proof.
intros x y.
rewrite Z.pos_sub_spec.
case Pos.compare_spec; intros H; simpl.
rewrite H. rewrite (Ropp_def Rth);rrefl.
rewrite <- (Pos.sub_add y x H) at 2. rewrite Pos.add_comm.
rewrite (ARgen_phiPOS_add ARth);simpl;norm.
rewrite (Ropp_def Rth);norm.
rewrite <- (Pos.sub_add x y H) at 2.
rewrite (ARgen_phiPOS_add ARth);simpl;norm.
add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); norm.
Qed.
Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
Proof.
intros x y; repeat rewrite same_genZ; generalize x y;clear x y.
destruct x, y; simpl; norm.
apply (ARgen_phiPOS_add ARth).
apply gen_phiZ1_pos_sub.
rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth).
rewrite (ARgen_phiPOS_add ARth); norm.
Qed.
Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
Proof.
intros x y;repeat rewrite same_genZ.
destruct x;destruct y;simpl;norm;
rewrite (ARgen_phiPOS_mult ARth);try (norm;fail).
rewrite (Ropp_opp Rsth Reqe Rth);rrefl.
Qed.
Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
Proof. intros;subst;rrefl. Qed.
Lemma gen_phiZ_morph :
ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH)
Z.add Z.mul Z.sub Z.opp Zeq_bool gen_phiZ.
Proof.
assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH)
Z.add Z.mul Zeq_bool gen_phiZ).
apply mkRmorph;simpl;try rrefl.
apply gen_phiZ_add. apply gen_phiZ_mul. apply gen_Zeqb_ok.
apply (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext).
Qed.
End ZMORPHISM.
Variable R : Type.
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
Variable req : R -> R -> Prop.
Notation "0" := rO. Notation "1" := rI.
Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Variable Rsth : Setoid_Theory R req.
Add Parametric Relation : R req
reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
transitivity proved by Rsth.(@Equivalence_Transitive _ _)
as R_setoid3.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
Proof. exact (Radd_ext Reqe). Qed.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3.
Proof. exact (Rmul_ext Reqe). Qed.
Add Morphism ropp with signature (req ==> req) as ropp_ext3.
Proof. exact (Ropp_ext Reqe). Qed.
Fixpoint gen_phiPOS1 (p:positive) : R :=
match p with
| xH => 1
| xO p => (1 + 1) * (gen_phiPOS1 p)
| xI p => 1 + ((1 + 1) * (gen_phiPOS1 p))
end.
Fixpoint gen_phiPOS (p:positive) : R :=
match p with
| xH => 1
| xO xH => (1 + 1)
| xO p => (1 + 1) * (gen_phiPOS p)
| xI xH => 1 + (1 +1)
| xI p => 1 + ((1 + 1) * (gen_phiPOS p))
end.
Definition gen_phiZ1 z :=
match z with
| Zpos p => gen_phiPOS1 p
| Z0 => 0
| Zneg p => -(gen_phiPOS1 p)
end.
Definition gen_phiZ z :=
match z with
| Zpos p => gen_phiPOS p
| Z0 => 0
| Zneg p => -(gen_phiPOS p)
end.
Notation "[ x ]" := (gen_phiZ x).
Definition get_signZ z :=
match z with
| Zneg p => Some (Zpos p)
| _ => None
end.
Lemma get_signZ_th : sign_theory Z.opp Zeq_bool get_signZ.
Proof.
constructor.
destruct c;intros;try discriminate.
injection H as <-.
simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
Qed.
Section ALMOST_RING.
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext3.
Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
Proof.
induction x;simpl.
rewrite IHx;destruct x;simpl;norm.
rewrite IHx;destruct x;simpl;norm.
rrefl.
Qed.
Lemma ARgen_phiPOS_Psucc : forall x,
gen_phiPOS1 (Pos.succ x) == 1 + (gen_phiPOS1 x).
Proof.
induction x;simpl;norm.
rewrite IHx;norm.
add_push 1;rrefl.
Qed.
Lemma ARgen_phiPOS_add : forall x y,
gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
Proof.
induction x;destruct y;simpl;norm.
rewrite Pos.add_carry_spec.
rewrite ARgen_phiPOS_Psucc.
rewrite IHx;norm.
add_push (gen_phiPOS1 y);add_push 1;rrefl.
rewrite IHx;norm;add_push (gen_phiPOS1 y);rrefl.
rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl.
rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;rrefl.
rewrite IHx;norm;add_push(gen_phiPOS1 y);rrefl.
add_push 1;rrefl.
rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl.
Qed.
Lemma ARgen_phiPOS_mult :
forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.
Proof.
induction x;intros;simpl;norm.
rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm.
rewrite IHx;rrefl.
Qed.
End ALMOST_RING.
Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
Let ARth := Rth_ARth Rsth Reqe Rth.
Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext4.
Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
Proof.
destruct x;simpl; try rewrite (same_gen ARth);rrefl.
Qed.
Lemma gen_Zeqb_ok : forall x y,
Zeq_bool x y = true -> [x] == [y].
Proof.
intros x y H.
assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1.
rewrite H1;rrefl.
Qed.
Lemma gen_phiZ1_pos_sub : forall x y,
gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.
Proof.
intros x y.
rewrite Z.pos_sub_spec.
case Pos.compare_spec; intros H; simpl.
rewrite H. rewrite (Ropp_def Rth);rrefl.
rewrite <- (Pos.sub_add y x H) at 2. rewrite Pos.add_comm.
rewrite (ARgen_phiPOS_add ARth);simpl;norm.
rewrite (Ropp_def Rth);norm.
rewrite <- (Pos.sub_add x y H) at 2.
rewrite (ARgen_phiPOS_add ARth);simpl;norm.
add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); norm.
Qed.
Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
Proof.
intros x y; repeat rewrite same_genZ; generalize x y;clear x y.
destruct x, y; simpl; norm.
apply (ARgen_phiPOS_add ARth).
apply gen_phiZ1_pos_sub.
rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth).
rewrite (ARgen_phiPOS_add ARth); norm.
Qed.
Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
Proof.
intros x y;repeat rewrite same_genZ.
destruct x;destruct y;simpl;norm;
rewrite (ARgen_phiPOS_mult ARth);try (norm;fail).
rewrite (Ropp_opp Rsth Reqe Rth);rrefl.
Qed.
Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
Proof. intros;subst;rrefl. Qed.
Lemma gen_phiZ_morph :
ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH)
Z.add Z.mul Z.sub Z.opp Zeq_bool gen_phiZ.
Proof.
assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH)
Z.add Z.mul Zeq_bool gen_phiZ).
apply mkRmorph;simpl;try rrefl.
apply gen_phiZ_add. apply gen_phiZ_mul. apply gen_Zeqb_ok.
apply (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext).
Qed.
End ZMORPHISM.
N is a semi-ring and a setoid
Lemma Nsth : Setoid_Theory N (@eq N).
Proof (Eqsth N).
Lemma Nseqe : sring_eq_ext N.add N.mul (@eq N).
Proof (Eq_s_ext N.add N.mul).
Lemma Nth : semi_ring_theory 0%N 1%N N.add N.mul (@eq N).
Proof.
constructor. exact N.add_0_l. exact N.add_comm. exact N.add_assoc.
exact N.mul_1_l. exact N.mul_0_l. exact N.mul_comm. exact N.mul_assoc.
exact N.mul_add_distr_r.
Qed.
Definition Nsub := SRsub N.add.
Definition Nopp := (@SRopp N).
Lemma Neqe : ring_eq_ext N.add N.mul Nopp (@eq N).
Proof (SReqe_Reqe Nseqe).
Lemma Nath :
almost_ring_theory 0%N 1%N N.add N.mul Nsub Nopp (@eq N).
Proof (SRth_ARth Nsth Nth).
Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y.
Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed.
Section NMORPHISM.
Variable R : Type.
Variable (rO rI : R) (radd rmul: R->R->R).
Variable req : R -> R -> Prop.
Notation "0" := rO. Notation "1" := rI.
Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
Variable Rsth : Setoid_Theory R req.
Add Parametric Relation : R req
reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
transitivity proved by Rsth.(@Equivalence_Transitive _ _)
as R_setoid4.
Ltac rrefl := gen_reflexivity Rsth.
Variable SReqe : sring_eq_ext radd rmul req.
Variable SRth : semi_ring_theory 0 1 radd rmul req.
Let ARth := SRth_ARth Rsth SRth.
Let Reqe := SReqe_Reqe SReqe.
Let ropp := (@SRopp R).
Let rsub := (@SRsub R radd).
Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Add Morphism radd with signature (req ==> req ==> req) as radd_ext4.
Proof. exact (Radd_ext Reqe). Qed.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext4.
Proof. exact (Rmul_ext Reqe). Qed.
Ltac norm := gen_srewrite_sr Rsth Reqe ARth.
Definition gen_phiN1 x :=
match x with
| N0 => 0
| Npos x => gen_phiPOS1 1 radd rmul x
end.
Definition gen_phiN x :=
match x with
| N0 => 0
| Npos x => gen_phiPOS 1 radd rmul x
end.
Notation "[ x ]" := (gen_phiN x).
Lemma same_genN : forall x, [x] == gen_phiN1 x.
Proof.
destruct x;simpl. reflexivity.
now rewrite (same_gen Rsth Reqe ARth).
Qed.
Lemma gen_phiN_add : forall x y, [x + y] == [x] + [y].
Proof.
intros x y;repeat rewrite same_genN.
destruct x;destruct y;simpl;norm.
apply (ARgen_phiPOS_add Rsth Reqe ARth).
Qed.
Lemma gen_phiN_mult : forall x y, [x * y] == [x] * [y].
Proof.
intros x y;repeat rewrite same_genN.
destruct x;destruct y;simpl;norm.
apply (ARgen_phiPOS_mult Rsth Reqe ARth).
Qed.
Lemma gen_phiN_sub : forall x y, [Nsub x y] == [x] - [y].
Proof. exact gen_phiN_add. Qed.
Lemma gen_phiN_morph : ring_morph 0 1 radd rmul rsub ropp req
0%N 1%N N.add N.mul Nsub Nopp N.eqb gen_phiN.
Proof.
constructor; simpl; try reflexivity.
apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult.
intros x y EQ. apply N.eqb_eq in EQ. now subst.
Qed.
End NMORPHISM.
Definition Nword := list N.
Definition NwO : Nword := nil.
Definition NwI : Nword := 1%N :: nil.
Definition Nwcons n (w : Nword) : Nword :=
match w, n with
| nil, 0%N => nil
| _, _ => n :: w
end.
Fixpoint Nwadd (w1 w2 : Nword) {struct w1} : Nword :=
match w1, w2 with
| n1::w1', n2:: w2' => (n1+n2)%N :: Nwadd w1' w2'
| nil, _ => w2
| _, nil => w1
end.
Definition Nwopp (w:Nword) : Nword := Nwcons 0%N w.
Definition Nwsub w1 w2 := Nwadd w1 (Nwopp w2).
Fixpoint Nwscal (n : N) (w : Nword) {struct w} : Nword :=
match w with
| m :: w' => (n*m)%N :: Nwscal n w'
| nil => nil
end.
Fixpoint Nwmul (w1 w2 : Nword) {struct w1} : Nword :=
match w1 with
| 0%N::w1' => Nwopp (Nwmul w1' w2)
| n1::w1' => Nwsub (Nwscal n1 w2) (Nwmul w1' w2)
| nil => nil
end.
Fixpoint Nw_is0 (w : Nword) : bool :=
match w with
| nil => true
| 0%N :: w' => Nw_is0 w'
| _ => false
end.
Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool :=
match w1, w2 with
| n1::w1', n2::w2' =>
if N.eqb n1 n2 then Nweq_bool w1' w2' else false
| nil, _ => Nw_is0 w2
| _, nil => Nw_is0 w1
end.
Section NWORDMORPHISM.
Variable R : Type.
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
Variable req : R -> R -> Prop.
Notation "0" := rO. Notation "1" := rI.
Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Variable Rsth : Setoid_Theory R req.
Add Parametric Relation : R req
reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
transitivity proved by Rsth.(@Equivalence_Transitive _ _)
as R_setoid5.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext5.
Proof. exact (Radd_ext Reqe). Qed.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext5.
Proof. exact (Rmul_ext Reqe). Qed.
Add Morphism ropp with signature (req ==> req) as ropp_ext5.
Proof. exact (Ropp_ext Reqe). Qed.
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext7.
Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Fixpoint gen_phiNword (w : Nword) : R :=
match w with
| nil => 0
| n :: nil => gen_phiN rO rI radd rmul n
| N0 :: w' => - gen_phiNword w'
| n::w' => gen_phiN rO rI radd rmul n - gen_phiNword w'
end.
Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0.
Proof.
induction w; simpl; intros; auto.
reflexivity.
destruct a.
destruct w.
reflexivity.
rewrite IHw; trivial.
apply (ARopp_zero Rsth Reqe ARth).
discriminate.
Qed.
Lemma gen_phiNword_cons : forall w n,
gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
induction w.
destruct n; simpl; norm.
intros.
destruct n; norm.
Qed.
Lemma gen_phiNword_Nwcons : forall w n,
gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
destruct w; intros.
destruct n; norm.
unfold Nwcons.
rewrite gen_phiNword_cons.
reflexivity.
Qed.
Lemma gen_phiNword_ok : forall w1 w2,
Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2.
induction w1; intros.
simpl.
rewrite (gen_phiNword0_ok _ H).
reflexivity.
rewrite gen_phiNword_cons.
destruct w2.
simpl in H.
destruct a; try discriminate.
rewrite (gen_phiNword0_ok _ H).
norm.
simpl in H.
rewrite gen_phiNword_cons.
case_eq (N.eqb a n); intros H0.
rewrite H0 in H.
apply N.eqb_eq in H0. rewrite <- H0.
rewrite (IHw1 _ H).
reflexivity.
rewrite H0 in H; discriminate H.
Qed.
Lemma Nwadd_ok : forall x y,
gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y.
induction x; intros.
simpl.
norm.
destruct y.
simpl Nwadd; norm.
simpl Nwadd.
repeat rewrite gen_phiNword_cons.
rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) by
(destruct Reqe; constructor; trivial).
rewrite IHx.
norm.
add_push (- gen_phiNword x); reflexivity.
Qed.
Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
simpl.
unfold Nwopp; simpl.
intros.
rewrite gen_phiNword_Nwcons; norm.
Qed.
Lemma Nwscal_ok : forall n x,
gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x.
induction x; intros.
norm.
simpl Nwscal.
repeat rewrite gen_phiNword_cons.
rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth))
by (destruct Reqe; constructor; trivial).
rewrite IHx.
norm.
Qed.
Lemma Nwmul_ok : forall x y,
gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y.
induction x; intros.
norm.
destruct a.
simpl Nwmul.
rewrite Nwopp_ok.
rewrite IHx.
rewrite gen_phiNword_cons.
norm.
simpl Nwmul.
unfold Nwsub.
rewrite Nwadd_ok.
rewrite Nwscal_ok.
rewrite Nwopp_ok.
rewrite IHx.
rewrite gen_phiNword_cons.
norm.
Qed.
Lemma gen_phiNword_morph :
ring_morph 0 1 radd rmul rsub ropp req
NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword.
constructor.
reflexivity.
reflexivity.
exact Nwadd_ok.
intros.
unfold Nwsub.
rewrite Nwadd_ok.
rewrite Nwopp_ok.
norm.
exact Nwmul_ok.
exact Nwopp_ok.
exact gen_phiNword_ok.
Qed.
End NWORDMORPHISM.
Section GEN_DIV.
Variables (R : Type) (rO : R) (rI : R) (radd : R -> R -> R)
(rmul : R -> R -> R) (rsub : R -> R -> R) (ropp : R -> R)
(req : R -> R -> Prop) (C : Type) (cO : C) (cI : C)
(cadd : C -> C -> C) (cmul : C -> C -> C) (csub : C -> C -> C)
(copp : C -> C) (ceqb : C -> C -> bool) (phi : C -> R).
Variable Rsth : Setoid_Theory R req.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi.
Add Parametric Relation : R req
reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
transitivity proved by Rsth.(@Equivalence_Transitive _ _)
as R_set1.
Ltac rrefl := gen_reflexivity Rsth.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
Proof. exact (Radd_ext Reqe). Qed.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
Proof. exact (Rmul_ext Reqe). Qed.
Add Morphism ropp with signature (req ==> req) as ropp_ext.
Proof. exact (Ropp_ext Reqe). Qed.
Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
Definition triv_div x y :=
if ceqb x y then (cI, cO)
else (cO, x).
Ltac Esimpl :=repeat (progress (
match goal with
| |- context [phi cO] => rewrite (morph0 morph)
| |- context [phi cI] => rewrite (morph1 morph)
| |- context [phi (cadd ?x ?y)] => rewrite ((morph_add morph) x y)
| |- context [phi (cmul ?x ?y)] => rewrite ((morph_mul morph) x y)
| |- context [phi (csub ?x ?y)] => rewrite ((morph_sub morph) x y)
| |- context [phi (copp ?x)] => rewrite ((morph_opp morph) x)
end)).
Lemma triv_div_th : Ring_theory.div_theory req cadd cmul phi triv_div.
Proof.
constructor.
intros a b;unfold triv_div.
assert (X:= morph.(morph_eq) a b);destruct (ceqb a b).
Esimpl.
rewrite X; trivial.
rsimpl.
Esimpl; rsimpl.
Qed.
Variable zphi : Z -> R.
Lemma Ztriv_div_th : div_theory req Z.add Z.mul zphi Z.quotrem.
Proof.
constructor.
intros; generalize (Z.quotrem_eq a b); case Z.quotrem; intros; subst.
rewrite Z.mul_comm; rsimpl.
Qed.
Variable nphi : N -> R.
Lemma Ntriv_div_th : div_theory req N.add N.mul nphi N.div_eucl.
constructor.
intros; generalize (N.div_eucl_spec a b); case N.div_eucl; intros; subst.
rewrite N.mul_comm; rsimpl.
Qed.
End GEN_DIV.
Ltac inv_gen_phi_pos rI add mul t :=
let rec inv_cst t :=
match t with
rI => constr:(1%positive)
| (add rI rI) => constr:(2%positive)
| (add rI (add rI rI)) => constr:(3%positive)
| (mul (add rI rI) ?p) =>
match inv_cst p with
NotConstant => constr:(NotConstant)
| 1%positive => constr:(NotConstant)
| ?p => constr:(xO p)
end
| (add rI (mul (add rI rI) ?p)) =>
match inv_cst p with
NotConstant => constr:(NotConstant)
| 1%positive => constr:(NotConstant)
| ?p => constr:(xI p)
end
| _ => constr:(NotConstant)
end in
inv_cst t.
Ltac inv_gen_phiNword rO rI add mul opp t :=
match t with
rO => constr:(NwO)
| _ =>
match inv_gen_phi_pos rI add mul t with
NotConstant => constr:(NotConstant)
| ?p => constr:(Npos p::nil)
end
end.
Ltac inv_gen_phiN rO rI add mul t :=
match t with
rO => constr:(0%N)
| _ =>
match inv_gen_phi_pos rI add mul t with
NotConstant => constr:(NotConstant)
| ?p => constr:(Npos p)
end
end.
Ltac inv_gen_phiZ rO rI add mul opp t :=
match t with
rO => constr:(0%Z)
| (opp ?p) =>
match inv_gen_phi_pos rI add mul p with
NotConstant => constr:(NotConstant)
| ?p => constr:(Zneg p)
end
| _ =>
match inv_gen_phi_pos rI add mul t with
NotConstant => constr:(NotConstant)
| ?p => constr:(Zpos p)
end
end.
Ltac inv_gen_phi rO rI cO cI t :=
match t with
| rO => cO
| rI => cI
end.
Ltac inv_morph_nothing t := constr:(NotConstant).
Ltac coerce_to_almost_ring set ext rspec :=
match type of rspec with
| ring_theory _ _ _ _ _ _ _ => constr:(Rth_ARth set ext rspec)
| semi_ring_theory _ _ _ _ _ => constr:(SRth_ARth set rspec)
| almost_ring_theory _ _ _ _ _ _ _ => rspec
| _ => fail 1 "not a valid ring theory"
end.
Ltac coerce_to_ring_ext ext :=
match type of ext with
| ring_eq_ext _ _ _ _ => ext
| sring_eq_ext _ _ _ => constr:(SReqe_Reqe ext)
| _ => fail 1 "not a valid ring_eq_ext theory"
end.
Ltac abstract_ring_morphism set ext rspec :=
match type of rspec with
| ring_theory _ _ _ _ _ _ _ => constr:(gen_phiZ_morph set ext rspec)
| semi_ring_theory _ _ _ _ _ => constr:(gen_phiN_morph set ext rspec)
| almost_ring_theory _ _ _ _ _ _ _ =>
constr:(gen_phiNword_morph set ext rspec)
| _ => fail 1 "bad ring structure"
end.
Record hypo : Type := mkhypo {
hypo_type : Type;
hypo_proof : hypo_type
}.
Ltac gen_ring_pow set arth pspec :=
match pspec with
| None =>
match type of arth with
| @almost_ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req =>
constr:(mkhypo (@pow_N_th R rI rmul req set))
| _ => fail 1 "gen_ring_pow"
end
| Some ?t => constr:(t)
end.
Ltac gen_ring_sign morph sspec :=
match sspec with
| None =>
match type of morph with
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
Z ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
constr:(@mkhypo (sign_theory copp ceqb get_signZ) get_signZ_th)
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
constr:(mkhypo (@get_sign_None_th C copp ceqb))
| _ => fail 2 "ring anomaly : default_sign_spec"
end
| Some ?t => constr:(t)
end.
Ltac default_div_spec set reqe arth morph :=
match type of morph with
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
Z ?c0 ?c1 Z.add Z.mul ?csub ?copp ?ceq_b ?phi =>
constr:(mkhypo (Ztriv_div_th set phi))
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
N ?c0 ?c1 N.add N.mul ?csub ?copp ?ceq_b ?phi =>
constr:(mkhypo (Ntriv_div_th set phi))
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
constr:(mkhypo (triv_div_th set reqe arth morph))
| _ => fail 1 "ring anomaly : default_sign_spec"
end.
Ltac gen_ring_div set reqe arth morph dspec :=
match dspec with
| None => default_div_spec set reqe arth morph
| Some ?t => constr:(t)
end.
Ltac ring_elements set ext rspec pspec sspec dspec rk :=
let arth := coerce_to_almost_ring set ext rspec in
let ext_r := coerce_to_ring_ext ext in
let morph :=
match rk with
| Abstract => abstract_ring_morphism set ext rspec
| @Computational ?reqb_ok =>
match type of arth with
| almost_ring_theory ?rO ?rI ?add ?mul ?sub ?opp _ =>
constr:(IDmorph rO rI add mul sub opp set _ reqb_ok)
| _ => fail 2 "ring anomaly"
end
| @Morphism ?m =>
match type of m with
| ring_morph _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => m
| @semi_morph _ _ _ _ _ _ _ _ _ _ _ _ _ =>
constr:(SRmorph_Rmorph set m)
| _ => fail 2 "ring anomaly"
end
| _ => fail 1 "ill-formed ring kind"
end in
let p_spec := gen_ring_pow set arth pspec in
let s_spec := gen_ring_sign morph sspec in
let d_spec := gen_ring_div set ext_r arth morph dspec in
fun f => f arth ext_r morph p_spec s_spec d_spec.
Ltac ring_lemmas set ext rspec pspec sspec dspec rk :=
let gen_lemma2 :=
match pspec with
| None => constr:(ring_rw_correct)
| Some _ => constr:(ring_rw_pow_correct)
end in
ring_elements set ext rspec pspec sspec dspec rk
ltac:(fun arth ext_r morph p_spec s_spec d_spec =>
match type of morph with
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
let gen_lemma2_0 :=
constr:(gen_lemma2 R r0 rI radd rmul rsub ropp req set ext_r arth
C c0 c1 cadd cmul csub copp ceq_b phi morph) in
match p_spec with
| @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec =>
let gen_lemma2_1 := constr:(gen_lemma2_0 _ Cp_phi rpow pp_spec) in
match d_spec with
| @mkhypo (div_theory _ _ _ _ ?cdiv) ?dd_spec =>
let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in
match s_spec with
| @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec =>
let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in
let lemma1 :=
constr:(ring_correct set ext_r arth morph pp_spec dd_spec) in
fun f => f arth ext_r morph lemma1 lemma2
| _ => fail 4 "ring: bad sign specification"
end
| _ => fail 3 "ring: bad coefficient division specification"
end
| _ => fail 2 "ring: bad power specification"
end
| _ => fail 1 "ring internal error: ring_lemmas, please report"
end).
Ltac isnatcst t :=
match t with
O => constr:(true)
| S ?p => isnatcst p
| _ => constr:(false)
end.
Ltac isPcst t :=
match t with
| xI ?p => isPcst p
| xO ?p => isPcst p
| xH => constr:(true)
| Pos.of_succ_nat ?n => isnatcst n
| _ => constr:(false)
end.
Ltac isNcst t :=
match t with
N0 => constr:(true)
| Npos ?p => isPcst p
| _ => constr:(false)
end.
Ltac isZcst t :=
match t with
Z0 => constr:(true)
| Zpos ?p => isPcst p
| Zneg ?p => isPcst p
| Z.of_nat ?n => isnatcst n
| Z.of_N ?n => isNcst n
| _ => constr:(false)
end.
Proof (Eqsth N).
Lemma Nseqe : sring_eq_ext N.add N.mul (@eq N).
Proof (Eq_s_ext N.add N.mul).
Lemma Nth : semi_ring_theory 0%N 1%N N.add N.mul (@eq N).
Proof.
constructor. exact N.add_0_l. exact N.add_comm. exact N.add_assoc.
exact N.mul_1_l. exact N.mul_0_l. exact N.mul_comm. exact N.mul_assoc.
exact N.mul_add_distr_r.
Qed.
Definition Nsub := SRsub N.add.
Definition Nopp := (@SRopp N).
Lemma Neqe : ring_eq_ext N.add N.mul Nopp (@eq N).
Proof (SReqe_Reqe Nseqe).
Lemma Nath :
almost_ring_theory 0%N 1%N N.add N.mul Nsub Nopp (@eq N).
Proof (SRth_ARth Nsth Nth).
Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y.
Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed.
Section NMORPHISM.
Variable R : Type.
Variable (rO rI : R) (radd rmul: R->R->R).
Variable req : R -> R -> Prop.
Notation "0" := rO. Notation "1" := rI.
Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
Variable Rsth : Setoid_Theory R req.
Add Parametric Relation : R req
reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
transitivity proved by Rsth.(@Equivalence_Transitive _ _)
as R_setoid4.
Ltac rrefl := gen_reflexivity Rsth.
Variable SReqe : sring_eq_ext radd rmul req.
Variable SRth : semi_ring_theory 0 1 radd rmul req.
Let ARth := SRth_ARth Rsth SRth.
Let Reqe := SReqe_Reqe SReqe.
Let ropp := (@SRopp R).
Let rsub := (@SRsub R radd).
Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Add Morphism radd with signature (req ==> req ==> req) as radd_ext4.
Proof. exact (Radd_ext Reqe). Qed.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext4.
Proof. exact (Rmul_ext Reqe). Qed.
Ltac norm := gen_srewrite_sr Rsth Reqe ARth.
Definition gen_phiN1 x :=
match x with
| N0 => 0
| Npos x => gen_phiPOS1 1 radd rmul x
end.
Definition gen_phiN x :=
match x with
| N0 => 0
| Npos x => gen_phiPOS 1 radd rmul x
end.
Notation "[ x ]" := (gen_phiN x).
Lemma same_genN : forall x, [x] == gen_phiN1 x.
Proof.
destruct x;simpl. reflexivity.
now rewrite (same_gen Rsth Reqe ARth).
Qed.
Lemma gen_phiN_add : forall x y, [x + y] == [x] + [y].
Proof.
intros x y;repeat rewrite same_genN.
destruct x;destruct y;simpl;norm.
apply (ARgen_phiPOS_add Rsth Reqe ARth).
Qed.
Lemma gen_phiN_mult : forall x y, [x * y] == [x] * [y].
Proof.
intros x y;repeat rewrite same_genN.
destruct x;destruct y;simpl;norm.
apply (ARgen_phiPOS_mult Rsth Reqe ARth).
Qed.
Lemma gen_phiN_sub : forall x y, [Nsub x y] == [x] - [y].
Proof. exact gen_phiN_add. Qed.
Lemma gen_phiN_morph : ring_morph 0 1 radd rmul rsub ropp req
0%N 1%N N.add N.mul Nsub Nopp N.eqb gen_phiN.
Proof.
constructor; simpl; try reflexivity.
apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult.
intros x y EQ. apply N.eqb_eq in EQ. now subst.
Qed.
End NMORPHISM.
Definition Nword := list N.
Definition NwO : Nword := nil.
Definition NwI : Nword := 1%N :: nil.
Definition Nwcons n (w : Nword) : Nword :=
match w, n with
| nil, 0%N => nil
| _, _ => n :: w
end.
Fixpoint Nwadd (w1 w2 : Nword) {struct w1} : Nword :=
match w1, w2 with
| n1::w1', n2:: w2' => (n1+n2)%N :: Nwadd w1' w2'
| nil, _ => w2
| _, nil => w1
end.
Definition Nwopp (w:Nword) : Nword := Nwcons 0%N w.
Definition Nwsub w1 w2 := Nwadd w1 (Nwopp w2).
Fixpoint Nwscal (n : N) (w : Nword) {struct w} : Nword :=
match w with
| m :: w' => (n*m)%N :: Nwscal n w'
| nil => nil
end.
Fixpoint Nwmul (w1 w2 : Nword) {struct w1} : Nword :=
match w1 with
| 0%N::w1' => Nwopp (Nwmul w1' w2)
| n1::w1' => Nwsub (Nwscal n1 w2) (Nwmul w1' w2)
| nil => nil
end.
Fixpoint Nw_is0 (w : Nword) : bool :=
match w with
| nil => true
| 0%N :: w' => Nw_is0 w'
| _ => false
end.
Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool :=
match w1, w2 with
| n1::w1', n2::w2' =>
if N.eqb n1 n2 then Nweq_bool w1' w2' else false
| nil, _ => Nw_is0 w2
| _, nil => Nw_is0 w1
end.
Section NWORDMORPHISM.
Variable R : Type.
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
Variable req : R -> R -> Prop.
Notation "0" := rO. Notation "1" := rI.
Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Variable Rsth : Setoid_Theory R req.
Add Parametric Relation : R req
reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
transitivity proved by Rsth.(@Equivalence_Transitive _ _)
as R_setoid5.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext5.
Proof. exact (Radd_ext Reqe). Qed.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext5.
Proof. exact (Rmul_ext Reqe). Qed.
Add Morphism ropp with signature (req ==> req) as ropp_ext5.
Proof. exact (Ropp_ext Reqe). Qed.
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext7.
Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Fixpoint gen_phiNword (w : Nword) : R :=
match w with
| nil => 0
| n :: nil => gen_phiN rO rI radd rmul n
| N0 :: w' => - gen_phiNword w'
| n::w' => gen_phiN rO rI radd rmul n - gen_phiNword w'
end.
Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0.
Proof.
induction w; simpl; intros; auto.
reflexivity.
destruct a.
destruct w.
reflexivity.
rewrite IHw; trivial.
apply (ARopp_zero Rsth Reqe ARth).
discriminate.
Qed.
Lemma gen_phiNword_cons : forall w n,
gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
induction w.
destruct n; simpl; norm.
intros.
destruct n; norm.
Qed.
Lemma gen_phiNword_Nwcons : forall w n,
gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
destruct w; intros.
destruct n; norm.
unfold Nwcons.
rewrite gen_phiNword_cons.
reflexivity.
Qed.
Lemma gen_phiNword_ok : forall w1 w2,
Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2.
induction w1; intros.
simpl.
rewrite (gen_phiNword0_ok _ H).
reflexivity.
rewrite gen_phiNword_cons.
destruct w2.
simpl in H.
destruct a; try discriminate.
rewrite (gen_phiNword0_ok _ H).
norm.
simpl in H.
rewrite gen_phiNword_cons.
case_eq (N.eqb a n); intros H0.
rewrite H0 in H.
apply N.eqb_eq in H0. rewrite <- H0.
rewrite (IHw1 _ H).
reflexivity.
rewrite H0 in H; discriminate H.
Qed.
Lemma Nwadd_ok : forall x y,
gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y.
induction x; intros.
simpl.
norm.
destruct y.
simpl Nwadd; norm.
simpl Nwadd.
repeat rewrite gen_phiNword_cons.
rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) by
(destruct Reqe; constructor; trivial).
rewrite IHx.
norm.
add_push (- gen_phiNword x); reflexivity.
Qed.
Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
simpl.
unfold Nwopp; simpl.
intros.
rewrite gen_phiNword_Nwcons; norm.
Qed.
Lemma Nwscal_ok : forall n x,
gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x.
induction x; intros.
norm.
simpl Nwscal.
repeat rewrite gen_phiNword_cons.
rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth))
by (destruct Reqe; constructor; trivial).
rewrite IHx.
norm.
Qed.
Lemma Nwmul_ok : forall x y,
gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y.
induction x; intros.
norm.
destruct a.
simpl Nwmul.
rewrite Nwopp_ok.
rewrite IHx.
rewrite gen_phiNword_cons.
norm.
simpl Nwmul.
unfold Nwsub.
rewrite Nwadd_ok.
rewrite Nwscal_ok.
rewrite Nwopp_ok.
rewrite IHx.
rewrite gen_phiNword_cons.
norm.
Qed.
Lemma gen_phiNword_morph :
ring_morph 0 1 radd rmul rsub ropp req
NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword.
constructor.
reflexivity.
reflexivity.
exact Nwadd_ok.
intros.
unfold Nwsub.
rewrite Nwadd_ok.
rewrite Nwopp_ok.
norm.
exact Nwmul_ok.
exact Nwopp_ok.
exact gen_phiNword_ok.
Qed.
End NWORDMORPHISM.
Section GEN_DIV.
Variables (R : Type) (rO : R) (rI : R) (radd : R -> R -> R)
(rmul : R -> R -> R) (rsub : R -> R -> R) (ropp : R -> R)
(req : R -> R -> Prop) (C : Type) (cO : C) (cI : C)
(cadd : C -> C -> C) (cmul : C -> C -> C) (csub : C -> C -> C)
(copp : C -> C) (ceqb : C -> C -> bool) (phi : C -> R).
Variable Rsth : Setoid_Theory R req.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi.
Add Parametric Relation : R req
reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
transitivity proved by Rsth.(@Equivalence_Transitive _ _)
as R_set1.
Ltac rrefl := gen_reflexivity Rsth.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
Proof. exact (Radd_ext Reqe). Qed.
Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
Proof. exact (Rmul_ext Reqe). Qed.
Add Morphism ropp with signature (req ==> req) as ropp_ext.
Proof. exact (Ropp_ext Reqe). Qed.
Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
Definition triv_div x y :=
if ceqb x y then (cI, cO)
else (cO, x).
Ltac Esimpl :=repeat (progress (
match goal with
| |- context [phi cO] => rewrite (morph0 morph)
| |- context [phi cI] => rewrite (morph1 morph)
| |- context [phi (cadd ?x ?y)] => rewrite ((morph_add morph) x y)
| |- context [phi (cmul ?x ?y)] => rewrite ((morph_mul morph) x y)
| |- context [phi (csub ?x ?y)] => rewrite ((morph_sub morph) x y)
| |- context [phi (copp ?x)] => rewrite ((morph_opp morph) x)
end)).
Lemma triv_div_th : Ring_theory.div_theory req cadd cmul phi triv_div.
Proof.
constructor.
intros a b;unfold triv_div.
assert (X:= morph.(morph_eq) a b);destruct (ceqb a b).
Esimpl.
rewrite X; trivial.
rsimpl.
Esimpl; rsimpl.
Qed.
Variable zphi : Z -> R.
Lemma Ztriv_div_th : div_theory req Z.add Z.mul zphi Z.quotrem.
Proof.
constructor.
intros; generalize (Z.quotrem_eq a b); case Z.quotrem; intros; subst.
rewrite Z.mul_comm; rsimpl.
Qed.
Variable nphi : N -> R.
Lemma Ntriv_div_th : div_theory req N.add N.mul nphi N.div_eucl.
constructor.
intros; generalize (N.div_eucl_spec a b); case N.div_eucl; intros; subst.
rewrite N.mul_comm; rsimpl.
Qed.
End GEN_DIV.
Ltac inv_gen_phi_pos rI add mul t :=
let rec inv_cst t :=
match t with
rI => constr:(1%positive)
| (add rI rI) => constr:(2%positive)
| (add rI (add rI rI)) => constr:(3%positive)
| (mul (add rI rI) ?p) =>
match inv_cst p with
NotConstant => constr:(NotConstant)
| 1%positive => constr:(NotConstant)
| ?p => constr:(xO p)
end
| (add rI (mul (add rI rI) ?p)) =>
match inv_cst p with
NotConstant => constr:(NotConstant)
| 1%positive => constr:(NotConstant)
| ?p => constr:(xI p)
end
| _ => constr:(NotConstant)
end in
inv_cst t.
Ltac inv_gen_phiNword rO rI add mul opp t :=
match t with
rO => constr:(NwO)
| _ =>
match inv_gen_phi_pos rI add mul t with
NotConstant => constr:(NotConstant)
| ?p => constr:(Npos p::nil)
end
end.
Ltac inv_gen_phiN rO rI add mul t :=
match t with
rO => constr:(0%N)
| _ =>
match inv_gen_phi_pos rI add mul t with
NotConstant => constr:(NotConstant)
| ?p => constr:(Npos p)
end
end.
Ltac inv_gen_phiZ rO rI add mul opp t :=
match t with
rO => constr:(0%Z)
| (opp ?p) =>
match inv_gen_phi_pos rI add mul p with
NotConstant => constr:(NotConstant)
| ?p => constr:(Zneg p)
end
| _ =>
match inv_gen_phi_pos rI add mul t with
NotConstant => constr:(NotConstant)
| ?p => constr:(Zpos p)
end
end.
Ltac inv_gen_phi rO rI cO cI t :=
match t with
| rO => cO
| rI => cI
end.
Ltac inv_morph_nothing t := constr:(NotConstant).
Ltac coerce_to_almost_ring set ext rspec :=
match type of rspec with
| ring_theory _ _ _ _ _ _ _ => constr:(Rth_ARth set ext rspec)
| semi_ring_theory _ _ _ _ _ => constr:(SRth_ARth set rspec)
| almost_ring_theory _ _ _ _ _ _ _ => rspec
| _ => fail 1 "not a valid ring theory"
end.
Ltac coerce_to_ring_ext ext :=
match type of ext with
| ring_eq_ext _ _ _ _ => ext
| sring_eq_ext _ _ _ => constr:(SReqe_Reqe ext)
| _ => fail 1 "not a valid ring_eq_ext theory"
end.
Ltac abstract_ring_morphism set ext rspec :=
match type of rspec with
| ring_theory _ _ _ _ _ _ _ => constr:(gen_phiZ_morph set ext rspec)
| semi_ring_theory _ _ _ _ _ => constr:(gen_phiN_morph set ext rspec)
| almost_ring_theory _ _ _ _ _ _ _ =>
constr:(gen_phiNword_morph set ext rspec)
| _ => fail 1 "bad ring structure"
end.
Record hypo : Type := mkhypo {
hypo_type : Type;
hypo_proof : hypo_type
}.
Ltac gen_ring_pow set arth pspec :=
match pspec with
| None =>
match type of arth with
| @almost_ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req =>
constr:(mkhypo (@pow_N_th R rI rmul req set))
| _ => fail 1 "gen_ring_pow"
end
| Some ?t => constr:(t)
end.
Ltac gen_ring_sign morph sspec :=
match sspec with
| None =>
match type of morph with
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
Z ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
constr:(@mkhypo (sign_theory copp ceqb get_signZ) get_signZ_th)
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
constr:(mkhypo (@get_sign_None_th C copp ceqb))
| _ => fail 2 "ring anomaly : default_sign_spec"
end
| Some ?t => constr:(t)
end.
Ltac default_div_spec set reqe arth morph :=
match type of morph with
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
Z ?c0 ?c1 Z.add Z.mul ?csub ?copp ?ceq_b ?phi =>
constr:(mkhypo (Ztriv_div_th set phi))
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
N ?c0 ?c1 N.add N.mul ?csub ?copp ?ceq_b ?phi =>
constr:(mkhypo (Ntriv_div_th set phi))
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
constr:(mkhypo (triv_div_th set reqe arth morph))
| _ => fail 1 "ring anomaly : default_sign_spec"
end.
Ltac gen_ring_div set reqe arth morph dspec :=
match dspec with
| None => default_div_spec set reqe arth morph
| Some ?t => constr:(t)
end.
Ltac ring_elements set ext rspec pspec sspec dspec rk :=
let arth := coerce_to_almost_ring set ext rspec in
let ext_r := coerce_to_ring_ext ext in
let morph :=
match rk with
| Abstract => abstract_ring_morphism set ext rspec
| @Computational ?reqb_ok =>
match type of arth with
| almost_ring_theory ?rO ?rI ?add ?mul ?sub ?opp _ =>
constr:(IDmorph rO rI add mul sub opp set _ reqb_ok)
| _ => fail 2 "ring anomaly"
end
| @Morphism ?m =>
match type of m with
| ring_morph _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => m
| @semi_morph _ _ _ _ _ _ _ _ _ _ _ _ _ =>
constr:(SRmorph_Rmorph set m)
| _ => fail 2 "ring anomaly"
end
| _ => fail 1 "ill-formed ring kind"
end in
let p_spec := gen_ring_pow set arth pspec in
let s_spec := gen_ring_sign morph sspec in
let d_spec := gen_ring_div set ext_r arth morph dspec in
fun f => f arth ext_r morph p_spec s_spec d_spec.
Ltac ring_lemmas set ext rspec pspec sspec dspec rk :=
let gen_lemma2 :=
match pspec with
| None => constr:(ring_rw_correct)
| Some _ => constr:(ring_rw_pow_correct)
end in
ring_elements set ext rspec pspec sspec dspec rk
ltac:(fun arth ext_r morph p_spec s_spec d_spec =>
match type of morph with
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
let gen_lemma2_0 :=
constr:(gen_lemma2 R r0 rI radd rmul rsub ropp req set ext_r arth
C c0 c1 cadd cmul csub copp ceq_b phi morph) in
match p_spec with
| @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec =>
let gen_lemma2_1 := constr:(gen_lemma2_0 _ Cp_phi rpow pp_spec) in
match d_spec with
| @mkhypo (div_theory _ _ _ _ ?cdiv) ?dd_spec =>
let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in
match s_spec with
| @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec =>
let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in
let lemma1 :=
constr:(ring_correct set ext_r arth morph pp_spec dd_spec) in
fun f => f arth ext_r morph lemma1 lemma2
| _ => fail 4 "ring: bad sign specification"
end
| _ => fail 3 "ring: bad coefficient division specification"
end
| _ => fail 2 "ring: bad power specification"
end
| _ => fail 1 "ring internal error: ring_lemmas, please report"
end).
Ltac isnatcst t :=
match t with
O => constr:(true)
| S ?p => isnatcst p
| _ => constr:(false)
end.
Ltac isPcst t :=
match t with
| xI ?p => isPcst p
| xO ?p => isPcst p
| xH => constr:(true)
| Pos.of_succ_nat ?n => isnatcst n
| _ => constr:(false)
end.
Ltac isNcst t :=
match t with
N0 => constr:(true)
| Npos ?p => isPcst p
| _ => constr:(false)
end.
Ltac isZcst t :=
match t with
Z0 => constr:(true)
| Zpos ?p => isPcst p
| Zneg ?p => isPcst p
| Z.of_nat ?n => isnatcst n
| Z.of_N ?n => isNcst n
| _ => constr:(false)
end.