diff options
Diffstat (limited to 'plugins/setoid_ring')
26 files changed, 2940 insertions, 1534 deletions
diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v new file mode 100644 index 00000000..e896554e --- /dev/null +++ b/plugins/setoid_ring/Algebra_syntax.v @@ -0,0 +1,25 @@ + +Class Zero (A : Type) := zero : A. +Notation "0" := zero. +Class One (A : Type) := one : A. +Notation "1" := one. +Class Addition (A : Type) := addition : A -> A -> A. +Notation "_+_" := addition. +Notation "x + y" := (addition x y). +Class Multiplication {A B : Type} := multiplication : A -> B -> B. +Notation "_*_" := multiplication. +Notation "x * y" := (multiplication x y). +Class Subtraction (A : Type) := subtraction : A -> A -> A. +Notation "_-_" := subtraction. +Notation "x - y" := (subtraction x y). +Class Opposite (A : Type) := opposite : A -> A. +Notation "-_" := opposite. +Notation "- x" := (opposite(x)). +Class Equality {A : Type}:= equality : A -> A -> Prop. +Notation "_==_" := equality. +Notation "x == y" := (equality x y) (at level 70, no associativity). +Class Bracket (A B: Type):= bracket : A -> B. +Notation "[ x ]" := (bracket(x)). +Class Power {A B: Type} := power : A -> B -> A. +Notation "x ^ y" := (power x y). + diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v index 6998b656..ed35bb46 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/plugins/setoid_ring/ArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -21,17 +21,17 @@ Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat). Lemma nat_morph_N : semi_morph 0 1 plus mult (eq (A:=nat)) - 0%N 1%N Nplus Nmult Neq_bool nat_of_N. + 0%N 1%N N.add N.mul N.eqb N.to_nat. Proof. constructor;trivial. - exact nat_of_Nplus. - exact nat_of_Nmult. - intros x y H;rewrite (Neq_bool_ok _ _ H);trivial. + exact N2Nat.inj_add. + exact N2Nat.inj_mul. + intros x y H. apply N.eqb_eq in H. now subst. Qed. Ltac natcst t := match isnatcst t with - true => constr:(N_of_nat t) + true => constr:(N.of_nat t) | _ => constr:InitialRing.NotConstant end. diff --git a/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v index 905625cc..b3c59457 100644 --- a/plugins/setoid_ring/BinList.v +++ b/plugins/setoid_ring/BinList.v @@ -1,16 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Set Implicit Arguments. Require Import BinPos. Require Export List. -Require Export ListTactics. -Open Local Scope positive_scope. +Set Implicit Arguments. +Local Open Scope positive_scope. Section MakeBinList. Variable A : Type. @@ -18,76 +17,64 @@ Section MakeBinList. Fixpoint jump (p:positive) (l:list A) {struct p} : list A := match p with - | xH => tail l + | xH => tl l | xO p => jump p (jump p l) - | xI p => jump p (jump p (tail l)) + | xI p => jump p (jump p (tl l)) end. Fixpoint nth (p:positive) (l:list A) {struct p} : A:= match p with | xH => hd default l | xO p => nth p (jump p l) - | xI p => nth p (jump p (tail l)) + | xI p => nth p (jump p (tl l)) end. - Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l). + Lemma jump_tl : forall j l, tl (jump j l) = jump j (tl l). Proof. - induction j;simpl;intros. - repeat rewrite IHj;trivial. - repeat rewrite IHj;trivial. - trivial. + induction j;simpl;intros; now rewrite ?IHj. Qed. - Lemma jump_Psucc : forall j l, - (jump (Psucc j) l) = (jump 1 (jump j l)). + Lemma jump_succ : forall j l, + jump (Pos.succ j) l = jump 1 (jump j l). Proof. induction j;simpl;intros. - repeat rewrite IHj;simpl;repeat rewrite jump_tl;trivial. - repeat rewrite jump_tl;trivial. - trivial. + - rewrite !IHj; simpl; now rewrite !jump_tl. + - now rewrite !jump_tl. + - trivial. Qed. - Lemma jump_Pplus : forall i j l, - (jump (i + j) l) = (jump i (jump j l)). + Lemma jump_add : forall i j l, + jump (i + j) l = jump i (jump j l). Proof. - induction i;intros. - rewrite xI_succ_xO;rewrite Pplus_one_succ_r. - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat rewrite IHi. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite jump_Psucc;trivial. - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat rewrite IHi;trivial. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite jump_Psucc;trivial. + induction i using Pos.peano_ind; intros. + - now rewrite Pos.add_1_l, jump_succ. + - now rewrite Pos.add_succ_l, !jump_succ, IHi. Qed. - Lemma jump_Pdouble_minus_one : forall i l, - (jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)). + Lemma jump_pred_double : forall i l, + jump (Pos.pred_double i) (tl l) = jump i (jump i l). Proof. induction i;intros;simpl. - repeat rewrite jump_tl;trivial. - rewrite IHi. do 2 rewrite <- jump_tl;rewrite IHi;trivial. - trivial. + - now rewrite !jump_tl. + - now rewrite IHi, <- 2 jump_tl, IHi. + - trivial. Qed. - - Lemma nth_jump : forall p l, nth p (tail l) = hd default (jump p l). + Lemma nth_jump : forall p l, nth p (tl l) = hd default (jump p l). Proof. induction p;simpl;intros. - rewrite <-jump_tl;rewrite IHp;trivial. - rewrite <-jump_tl;rewrite IHp;trivial. - trivial. + - now rewrite <-jump_tl, IHp. + - now rewrite <-jump_tl, IHp. + - trivial. Qed. - Lemma nth_Pdouble_minus_one : - forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l). + Lemma nth_pred_double : + forall p l, nth (Pos.pred_double p) (tl l) = nth p (jump p l). Proof. induction p;simpl;intros. - repeat rewrite jump_tl;trivial. - rewrite jump_Pdouble_minus_one. - repeat rewrite <- jump_tl;rewrite IHp;trivial. - trivial. + - now rewrite !jump_tl. + - now rewrite jump_pred_double, <- !jump_tl, IHp. + - trivial. Qed. End MakeBinList. - - diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v new file mode 100644 index 00000000..02194d4f --- /dev/null +++ b/plugins/setoid_ring/Cring.v @@ -0,0 +1,271 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Export List. +Require Import Setoid. +Require Import BinPos. +Require Import BinList. +Require Import Znumtheory. +Require Export Morphisms Setoid Bool. +Require Import ZArith_base. +Require Export Algebra_syntax. +Require Export Ncring. +Require Export Ncring_initial. +Require Export Ncring_tac. + +Class Cring {R:Type}`{Rr:Ring R} := + cring_mul_comm: forall x y:R, x * y == y * x. + +Ltac reify_goal lvar lexpr lterm:= + (*idtac lvar; idtac lexpr; idtac lterm;*) + match lexpr with + nil => idtac + | ?e1::?e2::_ => + match goal with + |- (?op ?u1 ?u2) => + change (op + (@Ring_polynom.PEeval + _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) + (@Ring_theory.pow_N _ 1 multiplication) lvar e1) + (@Ring_polynom.PEeval + _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) + (@Ring_theory.pow_N _ 1 multiplication) lvar e2)) + end + end. + +Section cring. +Context {R:Type}`{Rr:Cring R}. + +Lemma cring_eq_ext: ring_eq_ext _+_ _*_ -_ _==_. +Proof. +intros. apply mk_reqe; solve_proper. +Defined. + +Lemma cring_almost_ring_theory: + almost_ring_theory (R:=R) zero one _+_ _*_ _-_ -_ _==_. +intros. apply mk_art ;intros. +rewrite ring_add_0_l; reflexivity. +rewrite ring_add_comm; reflexivity. +rewrite ring_add_assoc; reflexivity. +rewrite ring_mul_1_l; reflexivity. +apply ring_mul_0_l. +rewrite cring_mul_comm; reflexivity. +rewrite ring_mul_assoc; reflexivity. +rewrite ring_distr_l; reflexivity. +rewrite ring_opp_mul_l; reflexivity. +apply ring_opp_add. +rewrite ring_sub_def ; reflexivity. Defined. + +Lemma cring_morph: + ring_morph zero one _+_ _*_ _-_ -_ _==_ + 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool + Ncring_initial.gen_phiZ. +intros. apply mkmorph ; intros; simpl; try reflexivity. +rewrite Ncring_initial.gen_phiZ_add; reflexivity. +rewrite ring_sub_def. unfold Z.sub. rewrite Ncring_initial.gen_phiZ_add. +rewrite Ncring_initial.gen_phiZ_opp; reflexivity. +rewrite Ncring_initial.gen_phiZ_mul; reflexivity. +rewrite Ncring_initial.gen_phiZ_opp; reflexivity. +rewrite (Zeqb_ok x y H). reflexivity. Defined. + +Lemma cring_power_theory : + @Ring_theory.power_theory R one _*_ _==_ N (fun n:N => n) + (@Ring_theory.pow_N _ 1 multiplication). +intros; apply Ring_theory.mkpow_th. reflexivity. Defined. + +Lemma cring_div_theory: + div_theory _==_ Z.add Z.mul Ncring_initial.gen_phiZ Z.quotrem. +intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory. +simpl. apply ring_setoid. Defined. + +End cring. + +Ltac cring_gen := + match goal with + |- ?g => let lterm := lterm_goal g in + match eval red in (list_reifyl (lterm:=lterm)) with + | (?fv, ?lexpr) => + (*idtac "variables:";idtac fv; + idtac "terms:"; idtac lterm; + idtac "reifications:"; idtac lexpr; *) + reify_goal fv lexpr lterm; + match goal with + |- ?g => + generalize + (@Ring_polynom.ring_correct _ 0 1 _+_ _*_ _-_ -_ _==_ + ring_setoid + cring_eq_ext + cring_almost_ring_theory + Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool + Ncring_initial.gen_phiZ + cring_morph + N + (fun n:N => n) + (@Ring_theory.pow_N _ 1 multiplication) + cring_power_theory + Z.quotrem + cring_div_theory + O fv nil); + let rc := fresh "rc"in + intro rc; apply rc + end + end + end. + +Ltac cring_compute:= vm_compute; reflexivity. + +Ltac cring:= + intros; + cring_gen; + cring_compute. + +Instance Zcri: (Cring (Rr:=Zr)). +red. exact Z.mul_comm. Defined. + +(* Cring_simplify *) + +Ltac cring_simplify_aux lterm fv lexpr hyp := + match lterm with + | ?t0::?lterm => + match lexpr with + | ?e::?le => + let t := constr:(@Ring_polynom.norm_subst + Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool Z.quotrem O nil e) in + let te := + constr:(@Ring_polynom.Pphi_dev + _ 0 1 _+_ _*_ _-_ -_ + + Z 0%Z 1%Z Zeq_bool + Ncring_initial.gen_phiZ + get_signZ fv t) in + let eq1 := fresh "ring" in + let nft := eval vm_compute in t in + let t':= fresh "t" in + pose (t' := nft); + assert (eq1 : t = t'); + [vm_cast_no_check (eq_refl t')| + let eq2 := fresh "ring" in + assert (eq2:(@Ring_polynom.PEeval + _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) + (@Ring_theory.pow_N _ 1 multiplication) fv e) == te); + [let eq3 := fresh "ring" in + generalize (@ring_rw_correct _ 0 1 _+_ _*_ _-_ -_ _==_ + ring_setoid + cring_eq_ext + cring_almost_ring_theory + Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool + Ncring_initial.gen_phiZ + cring_morph + N + (fun n:N => n) + (@Ring_theory.pow_N _ 1 multiplication) + cring_power_theory + Z.quotrem + cring_div_theory + get_signZ get_signZ_th + O nil fv I nil (eq_refl nil) ); + intro eq3; apply eq3; reflexivity| + match hyp with + | 1%nat => rewrite eq2 + | ?H => try rewrite eq2 in H + end]; + let P:= fresh "P" in + match hyp with + | 1%nat => + rewrite eq1; + pattern (@Ring_polynom.Pphi_dev + _ 0 1 _+_ _*_ _-_ -_ + + Z 0%Z 1%Z Zeq_bool + Ncring_initial.gen_phiZ + get_signZ fv t'); + match goal with + |- (?p ?t) => set (P:=p) + end; + unfold t' in *; clear t' eq1 eq2; + unfold Pphi_dev, Pphi_avoid; simpl; + repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c, + mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult, + mkpow;simpl) + | ?H => + rewrite eq1 in H; + pattern (@Ring_polynom.Pphi_dev + _ 0 1 _+_ _*_ _-_ -_ + + Z 0%Z 1%Z Zeq_bool + Ncring_initial.gen_phiZ + get_signZ fv t') in H; + match type of H with + | (?p ?t) => set (P:=p) in H + end; + unfold t' in *; clear t' eq1 eq2; + unfold Pphi_dev, Pphi_avoid in H; simpl in H; + repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c, + mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult, + mkpow in H;simpl in H) + end; unfold P in *; clear P + ]; cring_simplify_aux lterm fv le hyp + | nil => idtac + end + | nil => idtac + end. + +Ltac set_variables fv := + match fv with + | nil => idtac + | ?t::?fv => + let v := fresh "X" in + set (v:=t) in *; set_variables fv + end. + +Ltac deset n:= + match n with + | 0%nat => idtac + | S ?n1 => + match goal with + | h:= ?v : ?t |- ?g => unfold h in *; clear h; deset n1 + end + end. + +(* a est soit un terme de l'anneau, soit une liste de termes. +J'ai pas réussi à un décomposer les Vlists obtenues avec ne_constr_list + dans Tactic Notation *) + +Ltac cring_simplify_gen a hyp := + let lterm := + match a with + | _::_ => a + | _ => constr:(a::nil) + end in + match eval red in (list_reifyl (lterm:=lterm)) with + | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr; + let n := eval compute in (length fv) in + idtac n; + let lt:=fresh "lt" in + set (lt:= lterm); + let lv:=fresh "fv" in + set (lv:= fv); + (* les termes de fv sont remplacés par des variables + pour pouvoir utiliser simpl ensuite sans risquer + des simplifications indésirables *) + set_variables fv; + let lterm1 := eval unfold lt in lt in + let lv1 := eval unfold lv in lv in + idtac lterm1; idtac lv1; + cring_simplify_aux lterm1 lv1 lexpr hyp; + clear lt lv; + (* on remet les termes de fv *) + deset n + end. + +Tactic Notation "cring_simplify" constr(lterm):= + cring_simplify_gen lterm 1%nat. + +Tactic Notation "cring_simplify" constr(lterm) "in" ident(H):= + cring_simplify_gen lterm H. + diff --git a/plugins/setoid_ring/Field.v b/plugins/setoid_ring/Field.v index 6a755af2..6d454ba8 100644 --- a/plugins/setoid_ring/Field.v +++ b/plugins/setoid_ring/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index eee89e61..8ac952c0 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -447,7 +447,7 @@ Ltac prove_field_eqn ope FLD fv expr := pose (res' := res); let lemma := get_L1 FLD in let lemma := - constr:(lemma O fv List.nil expr' res' I List.nil (refl_equal _)) in + constr:(lemma O fv List.nil expr' res' I List.nil (eq_refl _)) in let ty := type of lemma in let lhs := match ty with forall _, ?lhs=_ -> _ => lhs @@ -487,7 +487,7 @@ Ltac reduce_field_expr ope kont FLD fv expr := kont c. (* Hack to let a Ltac return a term in the context of a primitive tactic *) -Ltac return_term x := generalize (refl_equal x). +Ltac return_term x := generalize (eq_refl x). Ltac get_term := match goal with | |- ?x = _ -> _ => x diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index ccdec656..bc05c252 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1,13 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) Require Ring. -Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List. +Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List Morphisms. Require Import ZArith_base. (*Require Import Omega.*) Set Implicit Arguments. @@ -27,7 +27,7 @@ Section MakeFieldPol. Notation "x == y" := (req x y) (at level 70, no associativity). (* Equality properties *) - Variable Rsth : Setoid_Theory R req. + Variable Rsth : Equivalence req. Variable Reqe : ring_eq_ext radd rmul ropp req. Variable SRinv_ext : forall p q, p == q -> / p == / q. @@ -75,7 +75,6 @@ Qed. (* Useful tactics *) - Add Setoid R req Rsth as R_set1. Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. @@ -96,7 +95,7 @@ Hint Resolve (ARadd_0_l ARth) (ARadd_comm ARth) (ARadd_assoc ARth) (ARsub_def ARth) . (* Power coefficients *) - Variable Cpow : Set. + Variable Cpow : Type. Variable Cp_phi : N -> Cpow. Variable rpow : R -> Cpow -> R. Variable pow_th : power_theory rI rmul req Cp_phi rpow. @@ -116,16 +115,17 @@ Notation NPphi_pow := (Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi (* add abstract semi-ring to help with some proofs *) Add Ring Rring : (ARth_SRth ARth). +Local Hint Extern 2 (_ == _) => f_equiv. (* additional ring properties *) Lemma rsub_0_l : forall r, 0 - r == - r. -intros; rewrite (ARsub_def ARth) in |- *;ring. +intros; rewrite (ARsub_def ARth);ring. Qed. Lemma rsub_0_r : forall r, r - 0 == r. -intros; rewrite (ARsub_def ARth) in |- *. -rewrite (ARopp_zero Rsth Reqe ARth) in |- *; ring. +intros; rewrite (ARsub_def ARth). +rewrite (ARopp_zero Rsth Reqe ARth); ring. Qed. (*************************************************************************** @@ -135,42 +135,40 @@ Qed. ***************************************************************************) Theorem rdiv_simpl: forall p q, ~ q == 0 -> q * (p / q) == p. +Proof. intros p q H. -rewrite rdiv_def in |- *. +rewrite rdiv_def. transitivity (/ q * q * p); [ ring | idtac ]. -rewrite rinv_l in |- *; auto. +rewrite rinv_l; auto. Qed. Hint Resolve rdiv_simpl . -Theorem SRdiv_ext: - forall p1 p2, p1 == p2 -> forall q1 q2, q1 == q2 -> p1 / q1 == p2 / q2. -intros p1 p2 H q1 q2 H0. +Instance SRdiv_ext: Proper (req ==> req ==> req) rdiv. +Proof. +intros p1 p2 Ep q1 q2 Eq. transitivity (p1 * / q1); auto. transitivity (p2 * / q2); auto. Qed. -Hint Resolve SRdiv_ext . - - Add Morphism rdiv : rdiv_ext. exact SRdiv_ext. Qed. +Hint Resolve SRdiv_ext. Lemma rmul_reg_l : forall p q1 q2, ~ p == 0 -> p * q1 == p * q2 -> q1 == q2. -intros. -rewrite <- (@rdiv_simpl q1 p) in |- *; trivial. -rewrite <- (@rdiv_simpl q2 p) in |- *; trivial. -repeat rewrite rdiv_def in |- *. -repeat rewrite (ARmul_assoc ARth) in |- *. -auto. +Proof. +intros p q1 q2 H EQ. +rewrite <- (@rdiv_simpl q1 p) by trivial. +rewrite <- (@rdiv_simpl q2 p) by trivial. +rewrite !rdiv_def, !(ARmul_assoc ARth). +now rewrite EQ. Qed. Theorem field_is_integral_domain : forall r1 r2, ~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0. Proof. -red in |- *; intros. -apply H0. +intros r1 r2 H1 H2. contradict H2. transitivity (1 * r2); auto. transitivity (/ r1 * r1 * r2); auto. -rewrite <- (ARmul_assoc ARth) in |- *. -rewrite H1 in |- *. +rewrite <- (ARmul_assoc ARth). +rewrite H2. apply ARmul_0_r with (1 := Rsth) (2 := ARth). Qed. @@ -179,15 +177,15 @@ Theorem ropp_neq_0 : forall r, intros. setoid_replace (- r) with (- (1) * r). apply field_is_integral_domain; trivial. - rewrite <- (ARopp_mul_l ARth) in |- *. - rewrite (ARmul_1_l ARth) in |- *. + rewrite <- (ARopp_mul_l ARth). + rewrite (ARmul_1_l ARth). reflexivity. Qed. Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1. intros. -rewrite (AFdiv_def AFth) in |- *. -rewrite (ARmul_comm ARth) in |- *. +rewrite (AFdiv_def AFth). +rewrite (ARmul_comm ARth). apply (AFinv_l AFth). trivial. Qed. @@ -203,14 +201,14 @@ Theorem rdiv2: r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4). Proof. intros r1 r2 r3 r4 H H0. -assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). +assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * r4); trivial. -rewrite rdiv_simpl in |- *; trivial. -rewrite (ARdistr_r Rsth Reqe ARth) in |- *. +rewrite rdiv_simpl; trivial. +rewrite (ARdistr_r Rsth Reqe ARth). apply (Radd_ext Reqe). - transitivity (r2 * (r1 / r2) * r4); [ ring | auto ]. - transitivity (r2 * (r4 * (r3 / r4))); auto. - transitivity (r2 * r3); auto. +- transitivity (r2 * (r1 / r2) * r4); [ ring | auto ]. +- transitivity (r2 * (r4 * (r3 / r4))); auto. + transitivity (r2 * r3); auto. Qed. @@ -225,35 +223,36 @@ assert (HH1: ~ r2 == 0) by (intros HH; case H; rewrite HH; ring). assert (HH2: ~ r5 == 0) by (intros HH; case H; rewrite HH; ring). assert (HH3: ~ r4 == 0) by (intros HH; case H0; rewrite HH; ring). assert (HH4: ~ r2 * (r4 * r5) == 0) - by complete (repeat apply field_is_integral_domain; trivial). + by (repeat apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * (r4 * r5)); trivial. -rewrite rdiv_simpl in |- *; trivial. -rewrite (ARdistr_r Rsth Reqe ARth) in |- *. +rewrite rdiv_simpl; trivial. +rewrite (ARdistr_r Rsth Reqe ARth). apply (Radd_ext Reqe). transitivity ((r2 * r5) * (r1 / (r2 * r5)) * r4); [ ring | auto ]. transitivity ((r4 * r5) * (r3 / (r4 * r5)) * r2); [ ring | auto ]. Qed. Theorem rdiv5: forall r1 r2, - (r1 / r2) == - r1 / r2. +Proof. intros r1 r2. transitivity (- (r1 * / r2)); auto. transitivity (- r1 * / r2); auto. Qed. Hint Resolve rdiv5 . -Theorem rdiv3: - forall r1 r2 r3 r4, +Theorem rdiv3 r1 r2 r3 r4 : ~ r2 == 0 -> ~ r4 == 0 -> r1 / r2 - r3 / r4 == (r1 * r4 - r3 * r2) / (r2 * r4). -intros r1 r2 r3 r4 H H0. +Proof. +intros H2 H4. assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). transitivity (r1 / r2 + - (r3 / r4)); auto. transitivity (r1 / r2 + - r3 / r4); auto. -transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)); auto. +transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)). apply rdiv2; auto. -apply SRdiv_ext; auto. -transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto. +f_equiv. +transitivity (r1 * r4 + - (r3 * r2)); auto. Qed. @@ -279,13 +278,13 @@ intros r1 r2 H H0. assert (~ r1 / r2 == 0) as Hk. intros H1; case H. transitivity (r2 * (r1 / r2)); auto. - rewrite H1 in |- *; ring. + rewrite H1; ring. apply rmul_reg_l with (r1 / r2); auto. transitivity (/ (r1 / r2) * (r1 / r2)); auto. transitivity 1; auto. - repeat rewrite rdiv_def in |- *. + repeat rewrite rdiv_def. transitivity (/ r1 * r1 * (/ r2 * r2)); [ idtac | ring ]. - repeat rewrite rinv_l in |- *; auto. + repeat rewrite rinv_l; auto. Qed. Hint Resolve rdiv6 . @@ -296,11 +295,11 @@ Hint Resolve rdiv6 . (r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4). Proof. intros r1 r2 r3 r4 H H0. -assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). +assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * r4); trivial. -rewrite rdiv_simpl in |- *; trivial. +rewrite rdiv_simpl; trivial. transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ]. -repeat rewrite rdiv_simpl in |- *; trivial. +repeat rewrite rdiv_simpl; trivial. Qed. Theorem rdiv4b: @@ -334,8 +333,8 @@ Theorem rdiv7: (r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3). Proof. intros. -rewrite (rdiv_def (r1 / r2)) in |- *. -rewrite rdiv6 in |- *; trivial. +rewrite (rdiv_def (r1 / r2)). +rewrite rdiv6; trivial. apply rdiv4; trivial. Qed. @@ -373,14 +372,14 @@ Theorem cross_product_eq : forall r1 r2 r3 r4, ~ r2 == 0 -> ~ r4 == 0 -> r1 * r4 == r3 * r2 -> r1 / r2 == r3 / r4. intros. transitivity (r1 / r2 * (r4 / r4)). - rewrite rdiv_r_r in |- *; trivial. - symmetry in |- *. + rewrite rdiv_r_r; trivial. + symmetry . apply (ARmul_1_r Rsth ARth). - rewrite rdiv4 in |- *; trivial. - rewrite H1 in |- *. - rewrite (ARmul_comm ARth r2 r4) in |- *. - rewrite <- rdiv4 in |- *; trivial. - rewrite rdiv_r_r in |- * by trivial. + rewrite rdiv4; trivial. + rewrite H1. + rewrite (ARmul_comm ARth r2 r4). + rewrite <- rdiv4; trivial. + rewrite rdiv_r_r by trivial. apply (ARmul_1_r Rsth ARth). Qed. @@ -390,52 +389,16 @@ Qed. ***************************************************************************) -Fixpoint positive_eq (p1 p2 : positive) {struct p1} : bool := - match p1, p2 with - xH, xH => true - | xO p3, xO p4 => positive_eq p3 p4 - | xI p3, xI p4 => positive_eq p3 p4 - | _, _ => false - end. - -Theorem positive_eq_correct: - forall p1 p2, if positive_eq p1 p2 then p1 = p2 else p1 <> p2. -intros p1; elim p1; - (try (intros p2; case p2; simpl; auto; intros; discriminate)). -intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4. -generalize (rec p4); case (positive_eq p3 p4); auto. -intros H1; apply f_equal with ( f := xI ); auto. -intros H1 H2; case H1; injection H2; auto. -intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4. -generalize (rec p4); case (positive_eq p3 p4); auto. -intros H1; apply f_equal with ( f := xO ); auto. -intros H1 H2; case H1; injection H2; auto. -Qed. - -Definition N_eq n1 n2 := - match n1, n2 with - | N0, N0 => true - | Npos p1, Npos p2 => positive_eq p1 p2 - | _, _ => false - end. - -Lemma N_eq_correct : forall n1 n2, if N_eq n1 n2 then n1 = n2 else n1 <> n2. -Proof. - intros [ |p1] [ |p2];simpl;trivial;try(intro H;discriminate H;fail). - assert (H:=positive_eq_correct p1 p2);destruct (positive_eq p1 p2); - [rewrite H;trivial | intro H1;injection H1;subst;apply H;trivial]. -Qed. - (* equality test *) Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := match e1, e2 with PEc c1, PEc c2 => ceqb c1 c2 - | PEX p1, PEX p2 => positive_eq p1 p2 + | PEX p1, PEX p2 => Pos.eqb p1 p2 | PEadd e3 e5, PEadd e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEopp e3, PEopp e4 => PExpr_eq e3 e4 - | PEpow e3 n3, PEpow e4 n4 => if N_eq n3 n4 then PExpr_eq e3 e4 else false + | PEpow e3 n3, PEpow e4 n4 => if N.eqb n3 n4 then PExpr_eq e3 e4 else false | _, _ => false end. @@ -446,22 +409,14 @@ Qed. Add Morphism (pow_N rI rmul) with signature req ==> eq ==> req as pow_N_morph. intros x y H [|p];simpl;auto. apply pow_morph;trivial. Qed. -(* -Lemma rpow_morph : forall x y n, x == y ->rpow x (Cp_phi n) == rpow y (Cp_phi n). -Proof. - intros; repeat rewrite pow_th.(rpow_pow_N). - destruct n;simpl. apply eq_refl. - induction p;simpl;try rewrite IHp;try rewrite H; apply eq_refl. -Qed. -*) + Theorem PExpr_eq_semi_correct: forall l e1 e2, PExpr_eq e1 e2 = true -> NPEeval l e1 == NPEeval l e2. intros l e1; elim e1. intros c1; intros e2; elim e2; simpl; (try (intros; discriminate)). intros c2; apply (morph_eq CRmorph). intros p1; intros e2; elim e2; simpl; (try (intros; discriminate)). -intros p2; generalize (positive_eq_correct p1 p2); case (positive_eq p1 p2); - (try (intros; discriminate)); intros H; rewrite H; auto. +intros p2; case Pos.eqb_spec; intros; now subst. intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)). intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4); (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6); @@ -478,9 +433,8 @@ intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))). intros e4; generalize (rec e4); case (PExpr_eq e3 e4); (try (intros; discriminate)); auto. intros e3 rec n3 e2;(case e2;simpl;(try (intros;discriminate))). -intros e4 n4;generalize (N_eq_correct n3 n4);destruct (N_eq n3 n4); -intros;try discriminate. -repeat rewrite pow_th.(rpow_pow_N);rewrite H;rewrite (rec _ H0);auto. +intros e4 n4; case N.eqb_spec; try discriminate; intros EQ H; subst. +repeat rewrite pow_th.(rpow_pow_N). rewrite (rec _ H);auto. Qed. (* add *) @@ -497,8 +451,8 @@ Theorem NPEadd_correct: forall l e1 e2, NPEeval l (NPEadd e1 e2) == NPEeval l (PEadd e1 e2). Proof. intros l e1 e2. -destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;try apply eq_refl; +destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect; + try (intro eq_c; rewrite eq_c); simpl;try apply eq_refl; try (ring [(morph0 CRmorph)]). apply (morph_add CRmorph). Qed. @@ -507,7 +461,7 @@ Definition NPEpow x n := match n with | N0 => PEc cI | Npos p => - if positive_eq p xH then x else + if Pos.eqb p xH then x else match x with | PEc c => if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (pow_pos cmul c p) @@ -520,10 +474,10 @@ Theorem NPEpow_correct : forall l e n, Proof. destruct n;simpl. rewrite pow_th.(rpow_pow_N);simpl;auto. - generalize (positive_eq_correct p xH). - destruct (positive_eq p 1);intros. - rewrite H;rewrite pow_th.(rpow_pow_N). trivial. - clear H;destruct e;simpl;auto. + fold (p =? 1)%positive. + case Pos.eqb_spec; intros H; (rewrite H || clear H). + now rewrite pow_th.(rpow_pow_N). + destruct e;simpl;auto. repeat apply ceqb_rect;simpl;intros;rewrite pow_th.(rpow_pow_N);simpl. symmetry;induction p;simpl;trivial; ring [IHp H CRmorph.(morph1)]. symmetry; induction p;simpl;trivial;ring [IHp CRmorph.(morph0)]. @@ -539,7 +493,7 @@ Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C := | _, PEc c => if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y | PEpow e1 n1, PEpow e2 n2 => - if N_eq n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y + if N.eqb n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y | _, _ => PEmul x y end. @@ -549,15 +503,15 @@ Qed. Theorem NPEmul_correct : forall l e1 e2, NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2). -induction e1;destruct e2; simpl in |- *;try reflexivity; +induction e1;destruct e2; simpl;try reflexivity; repeat apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; try reflexivity; + try (intro eq_c; rewrite eq_c); simpl; try reflexivity; try ring [(morph0 CRmorph) (morph1 CRmorph)]. apply (morph_mul CRmorph). -assert (H:=N_eq_correct n n0);destruct (N_eq n n0). +case N.eqb_spec; intros H; try rewrite <- H; clear H. rewrite NPEpow_correct. simpl. repeat rewrite pow_th.(rpow_pow_N). -rewrite IHe1;rewrite <- H;destruct n;simpl;try ring. +rewrite IHe1; destruct n;simpl;try ring. apply pow_pos_mul. simpl;auto. Qed. @@ -575,9 +529,9 @@ Definition NPEsub e1 e2 := Theorem NPEsub_correct: forall l e1 e2, NPEeval l (NPEsub e1 e2) == NPEeval l (PEsub e1 e2). intros l e1 e2. -destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; - try rewrite (morph0 CRmorph) in |- *; try reflexivity; +destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect; + try (intro eq_c; rewrite eq_c); simpl; + try rewrite (morph0 CRmorph); try reflexivity; try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r). apply (morph_sub CRmorph). Qed. @@ -697,8 +651,8 @@ destruct H; trivial. Qed. Theorem PCond_app_inv_l: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l1. -intros l l1 l2; elim l1; simpl app in |- *. - simpl in |- *; auto. +intros l l1 l2; elim l1; simpl app. + simpl; auto. destruct l0; simpl in *. destruct l2; firstorder. firstorder. @@ -713,8 +667,8 @@ Qed. Definition absurd_PCond := cons (PEc cO) nil. Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond. -unfold absurd_PCond in |- *; simpl in |- *. -red in |- *; intros. +unfold absurd_PCond; simpl. +red; intros. apply H. apply (morph0 CRmorph). Qed. @@ -743,10 +697,10 @@ Fixpoint isIn (e1:PExpr C) (p1:positive) end end | PEpow e3 N0 => None - | PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pmult p3 p2) + | PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pos.mul p3 p2) | _ => if PExpr_eq e1 e2 then - match Zminus (Zpos p1) (Zpos p2) with + match Z.pos_sub p1 p2 with | Zpos p => Some (Npos p, PEc cI) | Z0 => Some (N0, PEc cI) | Zneg p => Some (N0, NPEpow e2 (Npos p)) @@ -757,13 +711,19 @@ Fixpoint isIn (e1:PExpr C) (p1:positive) Definition ZtoN z := match z with Zpos p => Npos p | _ => N0 end. Definition NtoZ n := match n with Npos p => Zpos p | _ => Z0 end. - Notation pow_pos_plus := (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext) - ARth.(ARmul_comm) ARth.(ARmul_assoc)). + Notation pow_pos_add := + (Ring_theory.pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)). + + Lemma Z_pos_sub_gt p q : (p > q)%positive -> + Z.pos_sub p q = Zpos (p - q). + Proof. intros; now apply Z.pos_sub_gt, Pos.gt_lt. Qed. + + Ltac simpl_pos_sub := rewrite ?Z_pos_sub_gt in * by assumption. Lemma isIn_correct_aux : forall l e1 e2 p1 p2, match (if PExpr_eq e1 e2 then - match Zminus (Zpos p1) (Zpos p2) with + match Z.sub (Zpos p1) (Zpos p2) with | Zpos p => Some (Npos p, PEc cI) | Z0 => Some (N0, PEc cI) | Zneg p => Some (N0, NPEpow e2 (Npos p)) @@ -779,37 +739,29 @@ Fixpoint isIn (e1:PExpr C) (p1:positive) Proof. intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2); case (PExpr_eq e1 e2); simpl; auto; intros H. - case_eq ((p1 ?= p2)%positive Eq);intros;simpl. - repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _). - rewrite (Pcompare_Eq_eq _ _ H0). - rewrite H by trivial. ring [ (morph1 CRmorph)]. - fold (NPEpow e2 (Npos (p2 - p1))). - rewrite NPEpow_correct;simpl. - repeat rewrite pow_th.(rpow_pow_N);simpl. - rewrite H;trivial. split. 2:refine (refl_equal _). - rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial. - repeat rewrite pow_th.(rpow_pow_N);simpl. - rewrite H;trivial. - change (ZtoN - match (p1 ?= p1 - p2)%positive Eq with - | Eq => 0 - | Lt => Zneg (p1 - p2 - p1) - | Gt => Zpos (p1 - (p1 - p2)) - end) with (ZtoN (Zpos p1 - Zpos (p1 -p2))). - replace (Zpos (p1 - p2)) with (Zpos p1 - Zpos p2)%Z. - split. - repeat rewrite Zth.(Rsub_def). rewrite (Ring_theory.Ropp_add Zsth Zeqe Zth). - rewrite Zplus_assoc. simpl. rewrite Pcompare_refl. simpl. - ring [ (morph1 CRmorph)]. - assert (Zpos p1 > 0 /\ Zpos p2 > 0)%Z. split;refine (refl_equal _). - apply Zplus_gt_reg_l with (Zpos p2). - rewrite Zplus_minus. change (Zpos p2 + Zpos p1 > 0 + Zpos p1)%Z. - apply Zplus_gt_compat_r. refine (refl_equal _). - simpl;rewrite H0;trivial. + rewrite Z.pos_sub_spec. + case Pos.compare_spec;intros;simpl. + - repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:reflexivity. + subst. rewrite H by trivial. ring [ (morph1 CRmorph)]. + - fold (p2 - p1 =? 1)%positive. + fold (NPEpow e2 (Npos (p2 - p1))). + rewrite NPEpow_correct;simpl. + repeat rewrite pow_th.(rpow_pow_N);simpl. + rewrite H;trivial. split. 2:reflexivity. + rewrite <- pow_pos_add. now rewrite Pos.add_comm, Pos.sub_add. + - repeat rewrite pow_th.(rpow_pow_N);simpl. + rewrite H;trivial. + rewrite Z.pos_sub_gt by now apply Pos.sub_decr. + replace (p1 - (p1 - p2))%positive with p2; + [| rewrite Pos.sub_sub_distr, Pos.add_comm; + auto using Pos.add_sub, Pos.sub_decr ]. + split. + simpl. ring [ (morph1 CRmorph)]. + now apply Z.lt_gt, Pos.sub_decr. Qed. Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2). -induction p1;simpl;intros;repeat rewrite pow_pos_mul;repeat rewrite pow_pos_plus;simpl. +induction p1;simpl;intros;repeat rewrite pow_pos_mul;repeat rewrite pow_pos_add;simpl. ring [(IHp1 p2)]. ring [(IHp1 p2)]. auto. Qed. @@ -835,39 +787,39 @@ destruct n. destruct n;simpl. rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl. intros (H1,H2) (H3,H4). - unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3. + simpl_pos_sub. simpl in H3. rewrite pow_pos_mul. rewrite H1;rewrite H3. assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 * (pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) == pow_pos rmul (NPEeval l e1) p4 * pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *NPEeval l p5) by ring. rewrite H;clear H. - rewrite <- pow_pos_plus. rewrite Pplus_minus. - split. symmetry;apply ARth.(ARmul_assoc). refine (refl_equal _). trivial. + rewrite <- pow_pos_add. + rewrite Pos.add_comm, Pos.sub_add by (now apply Z.gt_lt in H4). + split. symmetry;apply ARth.(ARmul_assoc). reflexivity. repeat rewrite pow_th.(rpow_pow_N);simpl. intros (H1,H2) (H3,H4). - unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3. - rewrite H2 in H1;simpl in H1. + simpl_pos_sub. simpl in H1, H3. assert (Zpos p1 > Zpos p6)%Z. apply Zgt_trans with (Zpos p4). exact H4. exact H2. - unfold Zgt in H;simpl in H;rewrite H. + simpl_pos_sub. split. 2:exact H. rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3. assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 * (pow_pos rmul (NPEeval l e1) (p4 - p6) * NPEeval l p5) == pow_pos rmul (NPEeval l e1) (p1 - p4) * pow_pos rmul (NPEeval l e1) (p4 - p6) * NPEeval l p3 * NPEeval l p5) by ring. rewrite H0;clear H0. - rewrite <- pow_pos_plus. + rewrite <- pow_pos_add. replace (p1 - p4 + (p4 - p6))%positive with (p1 - p6)%positive. rewrite NPEmul_correct. simpl;ring. assert (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z. change ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z). - rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)). - simpl. rewrite Pcompare_refl. simpl. reflexivity. - unfold Zminus, Zopp in H0. simpl in H0. - rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial. + rewrite <- Z.add_assoc. rewrite (Z.add_assoc (- Zpos p4)). + simpl. rewrite Z.pos_sub_diag. simpl. reflexivity. + unfold Z.sub, Z.opp in H0. simpl in H0. + simpl_pos_sub. inversion H0; trivial. simpl. repeat rewrite pow_th.(rpow_pow_N). - intros H1 (H2,H3). unfold Zgt in H3;simpl in H3. rewrite H3 in H2;rewrite H3. + intros H1 (H2,H3). simpl_pos_sub. rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. simpl in H2. rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul. split. ring [H2]. exact H3. @@ -878,8 +830,7 @@ destruct n. rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul. intros (H1, H2);rewrite H1;split. - unfold Zgt in H2;simpl in H2;rewrite H2;rewrite H2 in H1. - simpl in H1;ring [H1]. trivial. + simpl_pos_sub. simpl in H1;ring [H1]. trivial. trivial. destruct n. trivial. generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3. @@ -910,7 +861,7 @@ Fixpoint split_aux (e1: PExpr C) (p:positive) (e2:PExpr C) {struct e1}: rsplit : (NPEmul (common r1) (common r2)) (right r2) | PEpow e3 N0 => mk_rsplit (PEc cI) (PEc cI) e2 - | PEpow e3 (Npos p3) => split_aux e3 (Pmult p3 p) e2 + | PEpow e3 (Npos p3) => split_aux e3 (Pos.mul p3 p) e2 | _ => match isIn e1 p e2 xH with | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3 @@ -937,9 +888,9 @@ Proof. repeat rewrite NPEpow_correct;simpl; repeat rewrite pow_th.(rpow_pow_N);simpl). intros (H, Hgt);split;try ring [H CRmorph.(morph1)]. - intros (H, Hgt). unfold Zgt in Hgt;simpl in Hgt;rewrite Hgt in H. - simpl in H;split;try ring [H]. - rewrite <- pow_pos_plus. rewrite Pplus_minus. reflexivity. trivial. + intros (H, Hgt). simpl_pos_sub. simpl in H;split;try ring [H]. + apply Z.gt_lt in Hgt. + now rewrite <- pow_pos_add, Pos.add_comm, Pos.sub_add. simpl;intros. repeat rewrite NPEmul_correct;simpl. rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)]. Qed. @@ -1061,13 +1012,13 @@ Theorem Pcond_Fnorm: forall l e, PCond l (condition (Fnorm e)) -> ~ NPEeval l (denum (Fnorm e)) == 0. intros l e; elim e. - simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO. - simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO. + simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO. + simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO. intros e1 Hrec1 e2 Hrec2 Hcond. simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. + simpl denum. + rewrite NPEmul_correct. + simpl. apply field_is_integral_domain. intros HH; case Hrec1; auto. apply PCond_app_inv_l with (1 := Hcond). @@ -1078,9 +1029,9 @@ intros l e; elim e. rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto. intros e1 Hrec1 e2 Hrec2 Hcond. simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. + simpl denum. + rewrite NPEmul_correct. + simpl. apply field_is_integral_domain. intros HH; case Hrec1; auto. apply PCond_app_inv_l with (1 := Hcond). @@ -1091,9 +1042,9 @@ intros l e; elim e. rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto. intros e1 Hrec1 e2 Hrec2 Hcond. simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. + simpl denum. + rewrite NPEmul_correct. + simpl. apply field_is_integral_domain. intros HH; apply Hrec1. apply PCond_app_inv_l with (1 := Hcond). @@ -1105,17 +1056,17 @@ intros l e; elim e. rewrite NPEmul_correct; simpl; rewrite HH; ring. intros e1 Hrec1 Hcond. simpl condition in Hcond. - simpl denum in |- *. + simpl denum. auto. intros e1 Hrec1 Hcond. simpl condition in Hcond. - simpl denum in |- *. + simpl denum. apply PCond_cons_inv_l with (1:=Hcond). intros e1 Hrec1 e2 Hrec2 Hcond. simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. + simpl denum. + rewrite NPEmul_correct. + simpl. apply field_is_integral_domain. intros HH; apply Hrec1. specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1. @@ -1258,9 +1209,9 @@ Theorem Fnorm_crossproduct: PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2. -rewrite Fnorm_FEeval_PEeval in |- * by +rewrite Fnorm_FEeval_PEeval by apply PCond_app_inv_l with (1 := Hcond). - rewrite Fnorm_FEeval_PEeval in |- * by + rewrite Fnorm_FEeval_PEeval by apply PCond_app_inv_r with (1 := Hcond). apply cross_product_eq; trivial. apply Pcond_Fnorm. @@ -1355,9 +1306,9 @@ apply Fnorm_crossproduct; trivial. match goal with [ |- NPEeval l ?x == NPEeval l ?y] => rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec - O nil l I (refl_equal nil) x (refl_equal (Nnorm O nil x))); + O nil l I Logic.eq_refl x Logic.eq_refl); rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec - O nil l I (refl_equal nil) y (refl_equal (Nnorm O nil y))) + O nil l I Logic.eq_refl y Logic.eq_refl) end. trivial. Qed. @@ -1377,28 +1328,28 @@ Proof. intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; subst nfe1 nfe2 den lmp. apply Fnorm_crossproduct; trivial. -simpl in |- *. -rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. -rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. -rewrite NPEmul_correct in |- *. -rewrite NPEmul_correct in |- *. -simpl in |- *. -repeat rewrite (ARmul_assoc ARth) in |- *. +simpl. +rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). +rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))). +rewrite NPEmul_correct. +rewrite NPEmul_correct. +simpl. +repeat rewrite (ARmul_assoc ARth). rewrite <-( let x := PEmul (num (Fnorm fe1)) (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l - Hlpe (refl_equal (Nmk_monpol_list lpe)) - x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. + Hlpe Logic.eq_refl + x Logic.eq_refl) in Hcrossprod. rewrite <-( let x := (PEmul (num (Fnorm fe2)) (rsplit_left (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l - Hlpe (refl_equal (Nmk_monpol_list lpe)) - x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. + Hlpe Logic.eq_refl + x Logic.eq_refl) in Hcrossprod. simpl in Hcrossprod. -rewrite Hcrossprod in |- *. +rewrite Hcrossprod. reflexivity. Qed. @@ -1417,28 +1368,28 @@ Proof. intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; subst nfe1 nfe2 den lmp. apply Fnorm_crossproduct; trivial. -simpl in |- *. -rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. -rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. -rewrite NPEmul_correct in |- *. -rewrite NPEmul_correct in |- *. -simpl in |- *. -repeat rewrite (ARmul_assoc ARth) in |- *. +simpl. +rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). +rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))). +rewrite NPEmul_correct. +rewrite NPEmul_correct. +simpl. +repeat rewrite (ARmul_assoc ARth). rewrite <-( let x := PEmul (num (Fnorm fe1)) (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l - Hlpe (refl_equal (Nmk_monpol_list lpe)) - x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. + Hlpe Logic.eq_refl + x Logic.eq_refl) in Hcrossprod. rewrite <-( let x := (PEmul (num (Fnorm fe2)) (rsplit_left (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l - Hlpe (refl_equal (Nmk_monpol_list lpe)) - x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. + Hlpe Logic.eq_refl + x Logic.eq_refl) in Hcrossprod. simpl in Hcrossprod. -rewrite Hcrossprod in |- *. +rewrite Hcrossprod. reflexivity. Qed. @@ -1558,7 +1509,7 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) := Lemma fcons_correct : forall l l1, PCond l (Fapp l1 nil) -> PCond l l1. -induction l1; simpl in |- *; intros. +induction l1; simpl; intros. trivial. elim PCond_fcons_inv with (1 := H); intros. destruct l1; auto. @@ -1639,7 +1590,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). simpl in H1. case (H _ H1); intros H2 H3. case (H0 _ H3); intros H4 H5; split; auto. - simpl in |- *. + simpl. apply field_is_integral_domain; trivial. simpl;intros. rewrite pow_th.(rpow_pow_N). destruct (H _ H0);split;auto. @@ -1667,7 +1618,7 @@ generalize (fun h => X (morph_eq CRmorph c1 c2 h)). generalize (@ceqb_complete c1 c2). case (c1 ?=! c2); auto; intros. apply X0. -red in |- *; intro. +red; intro. absurd (false = true); auto; discriminate. Qed. @@ -1683,18 +1634,18 @@ Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := Theorem PFcons1_fcons_inv: forall l a l1, PCond l (Fcons1 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). - simpl in |- *; intros c l1. + simpl; intros c l1. apply ceqb_rect_complete; intros. elim (@absurd_PCond_bottom l H0). split; trivial. - rewrite <- (morph0 CRmorph) in |- *; trivial. + rewrite <- (morph0 CRmorph); trivial. intros p H p0 H0 l1 H1. simpl in H1. case (H _ H1); intros H2 H3. case (H0 _ H3); intros H4 H5; split; auto. - simpl in |- *. + simpl. apply field_is_integral_domain; trivial. - simpl in |- *; intros p H l1. + simpl; intros p H l1. apply ceqb_rect_complete; intros. elim (@absurd_PCond_bottom l H1). destruct (H _ H1). @@ -1713,7 +1664,7 @@ Definition Fcons2 e l := Fcons1 (PExpr_simp e) l. Theorem PFcons2_fcons_inv: forall l a l1, PCond l (Fcons2 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. -unfold Fcons2 in |- *; intros l a l1 H; split; +unfold Fcons2; intros l a l1 H; split; case (PFcons1_fcons_inv l (PExpr_simp a) l1); auto. intros H1 H2 H3; case H1. transitivity (NPEeval l a); trivial. @@ -1792,61 +1743,55 @@ Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0. Lemma add_inj_r : forall p x y, gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y. intros p x y. -elim p using Pind; simpl in |- *; intros. +elim p using Pos.peano_ind; simpl; intros. apply S_inj; trivial. apply H. apply S_inj. - repeat rewrite (ARadd_assoc ARth) in |- *. - rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *; trivial. + repeat rewrite (ARadd_assoc ARth). + rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth); trivial. Qed. Lemma gen_phiPOS_inj : forall x y, gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y -> x = y. intros x y. -repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *. -ElimPcompare x y; intro. +repeat rewrite <- (same_gen Rsth Reqe ARth). +case (Pos.compare_spec x y). + intros. + trivial. intros. - apply Pcompare_Eq_eq; trivial. - intro. elim gen_phiPOS_not_0 with (y - x)%positive. apply add_inj_r with x. - symmetry in |- *. - rewrite (ARadd_0_r Rsth ARth) in |- *. - rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. - rewrite Pplus_minus in |- *; trivial. - change Eq with (CompOpp Eq) in |- *. - rewrite <- Pcompare_antisym in |- *; trivial. - rewrite H in |- *; trivial. - intro. + symmetry. + rewrite (ARadd_0_r Rsth ARth). + rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth). + now rewrite Pos.add_comm, Pos.sub_add. + intros. elim gen_phiPOS_not_0 with (x - y)%positive. apply add_inj_r with y. - rewrite (ARadd_0_r Rsth ARth) in |- *. - rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. - rewrite Pplus_minus in |- *; trivial. + rewrite (ARadd_0_r Rsth ARth). + rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth). + now rewrite Pos.add_comm, Pos.sub_add. Qed. Lemma gen_phiN_inj : forall x y, gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> x = y. -destruct x; destruct y; simpl in |- *; intros; trivial. +destruct x; destruct y; simpl; intros; trivial. elim gen_phiPOS_not_0 with p. - symmetry in |- *. - rewrite (same_gen Rsth Reqe ARth) in |- *; trivial. + symmetry . + rewrite (same_gen Rsth Reqe ARth); trivial. elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *; trivial. - rewrite gen_phiPOS_inj with (1 := H) in |- *; trivial. + rewrite (same_gen Rsth Reqe ARth); trivial. + rewrite gen_phiPOS_inj with (1 := H); trivial. Qed. Lemma gen_phiN_complete : forall x y, gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> - Neq_bool x y = true. -intros. - replace y with x. - unfold Neq_bool in |- *. - rewrite Ncompare_refl in |- *; trivial. - apply gen_phiN_inj; trivial. + N.eqb x y = true. +Proof. +intros. now apply N.eqb_eq, gen_phiN_inj. Qed. End AlmostField. @@ -1864,17 +1809,17 @@ Section Field. Lemma ring_S_inj : forall x y, 1+x==1+y -> x==y. intros. transitivity (x + (1 + - (1))). - rewrite (Ropp_def Rth) in |- *. - symmetry in |- *. + rewrite (Ropp_def Rth). + symmetry . apply (ARadd_0_r Rsth ARth). transitivity (y + (1 + - (1))). - repeat rewrite <- (ARplus_assoc ARth) in |- *. - repeat rewrite (ARadd_assoc ARth) in |- *. + repeat rewrite <- (ARplus_assoc ARth). + repeat rewrite (ARadd_assoc ARth). apply (Radd_ext Reqe). - repeat rewrite <- (ARadd_comm ARth 1) in |- *. + repeat rewrite <- (ARadd_comm ARth 1). trivial. reflexivity. - rewrite (Ropp_def Rth) in |- *. + rewrite (Ropp_def Rth). apply (ARadd_0_r Rsth ARth). Qed. @@ -1886,14 +1831,14 @@ Let gen_phiPOS_inject := Lemma gen_phiPOS_discr_sgn : forall x y, ~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y. -red in |- *; intros. +red; intros. apply gen_phiPOS_not_0 with (y + x)%positive. -rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. +rewrite (ARgen_phiPOS_add Rsth Reqe ARth). transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y). apply (Radd_ext Reqe); trivial. reflexivity. - rewrite (same_gen Rsth Reqe ARth) in |- *. - rewrite (same_gen Rsth Reqe ARth) in |- *. + rewrite (same_gen Rsth Reqe ARth). + rewrite (same_gen Rsth Reqe ARth). trivial. apply (Ropp_def Rth). Qed. @@ -1901,33 +1846,33 @@ Qed. Lemma gen_phiZ_inj : forall x y, gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> x = y. -destruct x; destruct y; simpl in |- *; intros. +destruct x; destruct y; simpl; intros. trivial. elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *. - symmetry in |- *; trivial. + rewrite (same_gen Rsth Reqe ARth). + symmetry ; trivial. elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *. - rewrite <- H in |- *. + rewrite (same_gen Rsth Reqe ARth). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). + rewrite <- H. apply (ARopp_zero Rsth Reqe ARth). elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *. + rewrite (same_gen Rsth Reqe ARth). trivial. - rewrite gen_phiPOS_inject with (1 := H) in |- *; trivial. + rewrite gen_phiPOS_inject with (1 := H); trivial. elim gen_phiPOS_discr_sgn with (1 := H). elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *. - rewrite H in |- *. + rewrite (same_gen Rsth Reqe ARth). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). + rewrite H. apply (ARopp_zero Rsth Reqe ARth). elim gen_phiPOS_discr_sgn with p0 p. - symmetry in |- *; trivial. + symmetry ; trivial. replace p0 with p; trivial. apply gen_phiPOS_inject. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)) in |- *. - rewrite H in |- *; trivial. + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)). + rewrite H; trivial. reflexivity. Qed. @@ -1936,8 +1881,8 @@ Lemma gen_phiZ_complete : forall x y, Zeq_bool x y = true. intros. replace y with x. - unfold Zeq_bool in |- *. - rewrite Zcompare_refl in |- *; trivial. + unfold Zeq_bool. + rewrite Z.compare_refl; trivial. apply gen_phiZ_inj; trivial. Qed. diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 026e70c8..e805151c 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,7 +13,6 @@ Require Import BinNat. Require Import Setoid. Require Import Ring_theory. Require Import Ring_polynom. -Require Import ZOdiv_def. Import List. Set Implicit Arguments. @@ -28,14 +27,14 @@ Definition NotConstant := false. Lemma Zsth : Setoid_Theory Z (@eq Z). Proof (Eqsth Z). -Lemma Zeqe : ring_eq_ext Zplus Zmult Zopp (@eq Z). -Proof (Eq_ext Zplus Zmult Zopp). +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) Zplus Zmult Zminus Zopp (@eq Z). +Lemma Zth : ring_theory Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z). Proof. - constructor. exact Zplus_0_l. exact Zplus_comm. exact Zplus_assoc. - exact Zmult_1_l. exact Zmult_comm. exact Zmult_assoc. - exact Zmult_plus_distr_l. trivial. exact Zminus_diag. + 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, *) @@ -93,12 +92,12 @@ Section ZMORPHISM. | _ => None end. - Lemma get_signZ_th : sign_theory Zopp Zeq_bool get_signZ. + Lemma get_signZ_th : sign_theory Z.opp Zeq_bool get_signZ. Proof. constructor. destruct c;intros;try discriminate. injection H;clear H;intros H1;subst c'. - simpl. unfold Zeq_bool. rewrite Zcompare_refl. trivial. + simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial. Qed. @@ -117,7 +116,7 @@ Section ZMORPHISM. Qed. Lemma ARgen_phiPOS_Psucc : forall x, - gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x). + gen_phiPOS1 (Pos.succ x) == 1 + (gen_phiPOS1 x). Proof. induction x;simpl;norm. rewrite IHx;norm. @@ -128,7 +127,7 @@ Section ZMORPHISM. gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y). Proof. induction x;destruct y;simpl;norm. - rewrite Pplus_carry_spec. + rewrite Pos.add_carry_spec. rewrite ARgen_phiPOS_Psucc. rewrite IHx;norm. add_push (gen_phiPOS1 y);add_push 1;rrefl. @@ -170,48 +169,28 @@ Section ZMORPHISM. rewrite H1;rrefl. Qed. - Lemma gen_phiZ1_add_pos_neg : forall x y, - gen_phiZ1 - match (x ?= y)%positive Eq with - | Eq => Z0 - | Lt => Zneg (y - x) - | Gt => Zpos (x - y) - end - == gen_phiPOS1 x + -gen_phiPOS1 y. + 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. - assert (H:= (Pcompare_Eq_eq x y)); assert (H0 := Pminus_mask_Gt x y). - generalize (Pminus_mask_Gt y x). - replace Eq with (CompOpp Eq);[intro H1;simpl|trivial]. - rewrite <- Pcompare_antisym in H1. - destruct ((x ?= y)%positive Eq). - rewrite H;trivial. rewrite (Ropp_def Rth);rrefl. - destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial. - unfold Pminus; rewrite Heq1;rewrite <- Heq2. + 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. - destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial. - unfold Pminus; rewrite Heq1;rewrite <- Heq2. + rewrite <- (Pos.sub_add x y H) at 2. rewrite (ARgen_phiPOS_add ARth);simpl;norm. - add_push (gen_phiPOS1 h);rewrite (Ropp_def Rth); norm. + add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); norm. Qed. - Lemma match_compOpp : forall x (B:Type) (be bl bg:B), - match CompOpp x with Eq => be | Lt => bl | Gt => bg end - = match x with Eq => be | Lt => bg | Gt => bl end. - Proof. destruct x;simpl;intros;trivial. 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. - induction x;destruct y;simpl;norm. + destruct x, y; simpl; norm. apply (ARgen_phiPOS_add ARth). - apply gen_phiZ1_add_pos_neg. - replace Eq with (CompOpp Eq);trivial. - rewrite <- Pcompare_antisym;simpl. - rewrite match_compOpp. - rewrite (Radd_comm Rth). - apply gen_phiZ1_add_pos_neg. + apply gen_phiZ1_pos_sub. + rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth). rewrite (ARgen_phiPOS_add ARth); norm. Qed. @@ -229,10 +208,10 @@ Section ZMORPHISM. (*proof that [.] satisfies morphism specifications*) Lemma gen_phiZ_morph : ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH) - Zplus Zmult Zminus Zopp Zeq_bool gen_phiZ. + 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) - Zplus Zmult Zeq_bool gen_phiZ). + 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). @@ -244,47 +223,28 @@ End ZMORPHISM. Lemma Nsth : Setoid_Theory N (@eq N). Proof (Eqsth N). -Lemma Nseqe : sring_eq_ext Nplus Nmult (@eq N). -Proof (Eq_s_ext Nplus Nmult). +Lemma Nseqe : sring_eq_ext N.add N.mul (@eq N). +Proof (Eq_s_ext N.add N.mul). -Lemma Nth : semi_ring_theory N0 (Npos xH) Nplus Nmult (@eq N). +Lemma Nth : semi_ring_theory 0%N 1%N N.add N.mul (@eq N). Proof. - constructor. exact Nplus_0_l. exact Nplus_comm. exact Nplus_assoc. - exact Nmult_1_l. exact Nmult_0_l. exact Nmult_comm. exact Nmult_assoc. - exact Nmult_plus_distr_r. + 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 Nplus. +Definition Nsub := SRsub N.add. Definition Nopp := (@SRopp N). -Lemma Neqe : ring_eq_ext Nplus Nmult Nopp (@eq N). +Lemma Neqe : ring_eq_ext N.add N.mul Nopp (@eq N). Proof (SReqe_Reqe Nseqe). Lemma Nath : - almost_ring_theory N0 (Npos xH) Nplus Nmult Nsub Nopp (@eq N). + almost_ring_theory 0%N 1%N N.add N.mul Nsub Nopp (@eq N). Proof (SRth_ARth Nsth Nth). -Definition Neq_bool (x y:N) := - match Ncompare x y with - | Eq => true - | _ => false - end. - -Lemma Neq_bool_ok : forall x y, Neq_bool x y = true -> x = y. - Proof. - intros x y;unfold Neq_bool. - assert (H:=Ncompare_Eq_eq x y); - destruct (Ncompare x y);intros;try discriminate. - rewrite H;trivial. - Qed. - -Lemma Neq_bool_complete : forall x y, Neq_bool x y = true -> x = y. - Proof. - intros x y;unfold Neq_bool. - assert (H:=Ncompare_Eq_eq x y); - destruct (Ncompare x y);intros;try discriminate. - rewrite H;trivial. - Qed. +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. (**Same as above : definition of two,extensionaly equal, generic morphisms *) (**from N to any semi-ring*) @@ -307,9 +267,7 @@ Section NMORPHISM. Notation "x == y" := (req x y). Add Morphism radd : radd_ext4. exact (Radd_ext Reqe). Qed. Add Morphism rmul : rmul_ext4. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext4. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext5. exact (ARsub_ext Rsth Reqe ARth). Qed. - Ltac norm := gen_srewrite Rsth Reqe ARth. + Ltac norm := gen_srewrite_sr Rsth Reqe ARth. Definition gen_phiN1 x := match x with @@ -326,8 +284,8 @@ Section NMORPHISM. Lemma same_genN : forall x, [x] == gen_phiN1 x. Proof. - destruct x;simpl. rrefl. - rewrite (same_gen Rsth Reqe ARth);rrefl. + destruct x;simpl. reflexivity. + now rewrite (same_gen Rsth Reqe ARth). Qed. Lemma gen_phiN_add : forall x y, [x + y] == [x] + [y]. @@ -349,11 +307,11 @@ Section NMORPHISM. (*gen_phiN satisfies morphism specifications*) Lemma gen_phiN_morph : ring_morph 0 1 radd rmul rsub ropp req - N0 (Npos xH) Nplus Nmult Nsub Nopp Neq_bool gen_phiN. + 0%N 1%N N.add N.mul Nsub Nopp N.eqb gen_phiN. Proof. - constructor;intros;simpl; try rrefl. - apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult. - rewrite (Neq_bool_ok x y);trivial. rrefl. + 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. @@ -402,7 +360,7 @@ Fixpoint Nw_is0 (w : Nword) : bool := Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool := match w1, w2 with | n1::w1', n2::w2' => - if Neq_bool n1 n2 then Nweq_bool w1' w2' else false + if N.eqb n1 n2 then Nweq_bool w1' w2' else false | nil, _ => Nw_is0 w2 | _, nil => Nw_is0 w1 end. @@ -438,14 +396,14 @@ Section NWORDMORPHISM. Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0. Proof. -induction w; simpl in |- *; intros; auto. +induction w; simpl; intros; auto. reflexivity. destruct a. destruct w. reflexivity. - rewrite IHw in |- *; trivial. + rewrite IHw; trivial. apply (ARopp_zero Rsth Reqe ARth). discriminate. @@ -454,7 +412,7 @@ 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 in |- *; norm. + destruct n; simpl; norm. intros. destruct n; norm. @@ -465,31 +423,31 @@ Qed. destruct w; intros. destruct n; norm. - unfold Nwcons in |- *. - rewrite gen_phiNword_cons in |- *. + 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 in |- *. - rewrite (gen_phiNword0_ok _ H) in |- *. + simpl. + rewrite (gen_phiNword0_ok _ H). reflexivity. - rewrite gen_phiNword_cons in |- *. + rewrite gen_phiNword_cons. destruct w2. simpl in H. destruct a; try discriminate. - rewrite (gen_phiNword0_ok _ H) in |- *. + rewrite (gen_phiNword0_ok _ H). norm. simpl in H. - rewrite gen_phiNword_cons in |- *. - case_eq (Neq_bool a n); intros. + rewrite gen_phiNword_cons. + case_eq (N.eqb a n); intros H0. rewrite H0 in H. - rewrite <- (Neq_bool_ok _ _ H0) in |- *. - rewrite (IHw1 _ H) in |- *. + apply N.eqb_eq in H0. rewrite <- H0. + rewrite (IHw1 _ H). reflexivity. rewrite H0 in H; discriminate H. @@ -499,27 +457,27 @@ Qed. Lemma Nwadd_ok : forall x y, gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y. induction x; intros. - simpl in |- *. + simpl. norm. destruct y. simpl Nwadd; norm. - simpl Nwadd in |- *. - repeat rewrite gen_phiNword_cons in |- *. - rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- * by + 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 in |- *. + rewrite IHx. norm. add_push (- gen_phiNword x); reflexivity. Qed. Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x. -simpl in |- *. -unfold Nwopp in |- *; simpl in |- *. +simpl. +unfold Nwopp; simpl. intros. -rewrite gen_phiNword_Nwcons in |- *; norm. +rewrite gen_phiNword_Nwcons; norm. Qed. Lemma Nwscal_ok : forall n x, @@ -527,12 +485,12 @@ Lemma Nwscal_ok : forall n x, induction x; intros. norm. - simpl Nwscal in |- *. - repeat rewrite gen_phiNword_cons in |- *. - rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- * + 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 in |- *. + rewrite IHx. norm. Qed. @@ -542,19 +500,19 @@ induction x; intros. norm. destruct a. - simpl Nwmul in |- *. - rewrite Nwopp_ok in |- *. - rewrite IHx in |- *. - rewrite gen_phiNword_cons in |- *. + simpl Nwmul. + rewrite Nwopp_ok. + rewrite IHx. + rewrite gen_phiNword_cons. norm. - simpl Nwmul in |- *. - unfold Nwsub in |- *. - rewrite Nwadd_ok in |- *. - rewrite Nwscal_ok in |- *. - rewrite Nwopp_ok in |- *. - rewrite IHx in |- *. - rewrite gen_phiNword_cons in |- *. + simpl Nwmul. + unfold Nwsub. + rewrite Nwadd_ok. + rewrite Nwscal_ok. + rewrite Nwopp_ok. + rewrite IHx. + rewrite gen_phiNword_cons. norm. Qed. @@ -570,9 +528,9 @@ constructor. exact Nwadd_ok. intros. - unfold Nwsub in |- *. - rewrite Nwadd_ok in |- *. - rewrite Nwopp_ok in |- *. + unfold Nwsub. + rewrite Nwadd_ok. + rewrite Nwopp_ok. norm. exact Nwmul_ok. @@ -632,19 +590,19 @@ Qed. Variable zphi : Z -> R. - Lemma Ztriv_div_th : div_theory req Zplus Zmult zphi ZOdiv_eucl. + Lemma Ztriv_div_th : div_theory req Z.add Z.mul zphi Z.quotrem. Proof. constructor. - intros; generalize (ZOdiv_eucl_correct a b); case ZOdiv_eucl; intros; subst. - rewrite Zmult_comm; rsimpl. + 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 Nplus Nmult nphi Ndiv_eucl. + Lemma Ntriv_div_th : div_theory req N.add N.mul nphi N.div_eucl. constructor. - intros; generalize (Ndiv_eucl_correct a b); case Ndiv_eucl; intros; subst. - rewrite Nmult_comm; rsimpl. + intros; generalize (N.div_eucl_spec a b); case N.div_eucl; intros; subst. + rewrite N.mul_comm; rsimpl. Qed. End GEN_DIV. @@ -783,10 +741,10 @@ Ltac gen_ring_sign morph sspec := 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 Zplus Zmult ?csub ?copp ?ceq_b ?phi => + 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 Nplus Nmult ?csub ?copp ?ceq_b ?phi => + 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 => @@ -878,7 +836,7 @@ Ltac isPcst t := | xO ?p => isPcst p | xH => constr:true (* nat -> positive *) - | P_of_succ_nat ?n => isnatcst n + | Pos.of_succ_nat ?n => isnatcst n | _ => constr:false end. @@ -895,9 +853,9 @@ Ltac isZcst t := | Zpos ?p => isPcst p | Zneg ?p => isPcst p (* injection nat -> Z *) - | Z_of_nat ?n => isnatcst n + | Z.of_nat ?n => isnatcst n (* injection N -> Z *) - | Z_of_N ?n => isNcst n + | Z.of_N ?n => isNcst n (* *) | _ => constr:false end. diff --git a/plugins/setoid_ring/Integral_domain.v b/plugins/setoid_ring/Integral_domain.v new file mode 100644 index 00000000..0c16fe1a --- /dev/null +++ b/plugins/setoid_ring/Integral_domain.v @@ -0,0 +1,43 @@ +Require Export Cring. + + +(* Definition of integral domains: commutative ring without zero divisor *) + +Class Integral_domain {R : Type}`{Rcr:Cring R} := { + integral_domain_product: + forall x y, x * y == 0 -> x == 0 \/ y == 0; + integral_domain_one_zero: not (1 == 0)}. + +Section integral_domain. + +Context {R:Type}`{Rid:Integral_domain R}. + +Lemma integral_domain_minus_one_zero: ~ - (1:R) == 0. +red;intro. apply integral_domain_one_zero. +assert (0 == - (0:R)). cring. +rewrite H0. rewrite <- H. cring. +Qed. + + +Definition pow (r : R) (n : nat) := Ring_theory.pow_N 1 mul r (N.of_nat n). + +Lemma pow_not_zero: forall p n, pow p n == 0 -> p == 0. +induction n. unfold pow; simpl. intros. absurd (1 == 0). +simpl. apply integral_domain_one_zero. + trivial. setoid_replace (pow p (S n)) with (p * (pow p n)). +intros. +case (integral_domain_product p (pow p n) H). trivial. trivial. +unfold pow; simpl. +clear IHn. induction n; simpl; try cring. + rewrite Ring_theory.pow_pos_succ. cring. apply ring_setoid. +apply ring_mult_comp. +apply ring_mul_assoc. +Qed. + +Lemma Rintegral_domain_pow: + forall c p r, ~c == 0 -> c * (pow p r) == ring0 -> p == ring0. +intros. case (integral_domain_product c (pow p r) H0). intros; absurd (c == ring0); auto. +intros. apply pow_not_zero with r. trivial. Qed. + +End integral_domain. + diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v index 8d7cb0ea..fae98d83 100644 --- a/plugins/setoid_ring/NArithRing.v +++ b/plugins/setoid_ring/NArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -18,4 +18,4 @@ Ltac Ncst t := | _ => constr:NotConstant end. -Add Ring Nr : Nth (decidable Neq_bool_ok, constants [Ncst]). +Add Ring Nr : Nth (decidable Neqb_ok, constants [Ncst]). diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v new file mode 100644 index 00000000..7789ba3e --- /dev/null +++ b/plugins/setoid_ring/Ncring.v @@ -0,0 +1,306 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* non commutative rings *) + +Require Import Setoid. +Require Import BinPos. +Require Import BinNat. +Require Export Morphisms Setoid Bool. +Require Export ZArith_base. +Require Export Algebra_syntax. + +Set Implicit Arguments. + +Class Ring_ops(T:Type) + {ring0:T} + {ring1:T} + {add:T->T->T} + {mul:T->T->T} + {sub:T->T->T} + {opp:T->T} + {ring_eq:T->T->Prop}. + +Instance zero_notation(T:Type)`{Ring_ops T}:Zero T:= ring0. +Instance one_notation(T:Type)`{Ring_ops T}:One T:= ring1. +Instance add_notation(T:Type)`{Ring_ops T}:Addition T:= add. +Instance mul_notation(T:Type)`{Ring_ops T}:@Multiplication T T:= mul. +Instance sub_notation(T:Type)`{Ring_ops T}:Subtraction T:= sub. +Instance opp_notation(T:Type)`{Ring_ops T}:Opposite T:= opp. +Instance eq_notation(T:Type)`{Ring_ops T}:@Equality T:= ring_eq. + +Class Ring `{Ro:Ring_ops}:={ + ring_setoid: Equivalence _==_; + ring_plus_comp: Proper (_==_ ==> _==_ ==>_==_) _+_; + ring_mult_comp: Proper (_==_ ==> _==_ ==>_==_) _*_; + ring_sub_comp: Proper (_==_ ==> _==_ ==>_==_) _-_; + ring_opp_comp: Proper (_==_==>_==_) -_; + ring_add_0_l : forall x, 0 + x == x; + ring_add_comm : forall x y, x + y == y + x; + ring_add_assoc : forall x y z, x + (y + z) == (x + y) + z; + ring_mul_1_l : forall x, 1 * x == x; + ring_mul_1_r : forall x, x * 1 == x; + ring_mul_assoc : forall x y z, x * (y * z) == (x * y) * z; + ring_distr_l : forall x y z, (x + y) * z == x * z + y * z; + ring_distr_r : forall x y z, z * ( x + y) == z * x + z * y; + ring_sub_def : forall x y, x - y == x + -y; + ring_opp_def : forall x, x + -x == 0 +}. +(* inutile! je sais plus pourquoi j'ai mis ca... +Instance ring_Ring_ops(R:Type)`{Ring R} + :@Ring_ops R 0 1 addition multiplication subtraction opposite equality. +*) +Existing Instance ring_setoid. +Existing Instance ring_plus_comp. +Existing Instance ring_mult_comp. +Existing Instance ring_sub_comp. +Existing Instance ring_opp_comp. + +Section Ring_power. + +Context {R:Type}`{Ring R}. + + Fixpoint pow_pos (x:R) (i:positive) {struct i}: R := + match i with + | xH => x + | xO i => let p := pow_pos x i in p * p + | xI i => let p := pow_pos x i in x * (p * p) + end. + + Definition pow_N (x:R) (p:N) := + match p with + | N0 => 1 + | Npos p => pow_pos x p + end. + +End Ring_power. + +Definition ZN(x:Z):= + match x with + Z0 => N0 + |Zpos p | Zneg p => Npos p +end. + +Instance power_ring {R:Type}`{Ring R} : Power:= + {power x y := pow_N x (ZN y)}. + +(** Interpretation morphisms definition*) + +Class Ring_morphism (C R:Type)`{Cr:Ring C} `{Rr:Ring R}`{Rh:Bracket C R}:= { + ring_morphism0 : [0] == 0; + ring_morphism1 : [1] == 1; + ring_morphism_add : forall x y, [x + y] == [x] + [y]; + ring_morphism_sub : forall x y, [x - y] == [x] - [y]; + ring_morphism_mul : forall x y, [x * y] == [x] * [y]; + ring_morphism_opp : forall x, [-x] == -[x]; + ring_morphism_eq : forall x y, x == y -> [x] == [y]}. + +Section Ring. + +Context {R:Type}`{Rr:Ring R}. + +(* Powers *) + +Lemma pow_pos_comm : forall x j, x * pow_pos x j == pow_pos x j * x. +Proof. +induction j; simpl. rewrite <- ring_mul_assoc. +rewrite <- ring_mul_assoc. +rewrite <- IHj. rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)). +rewrite <- IHj. rewrite <- ring_mul_assoc. reflexivity. +rewrite <- ring_mul_assoc. rewrite <- IHj. +rewrite ring_mul_assoc. rewrite IHj. +rewrite <- ring_mul_assoc. rewrite IHj. reflexivity. reflexivity. +Qed. + +Lemma pow_pos_succ : forall x j, pow_pos x (Pos.succ j) == x * pow_pos x j. +Proof. +induction j; simpl. + rewrite IHj. +rewrite <- (ring_mul_assoc x (pow_pos x j) (x * pow_pos x j)). +rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)). + rewrite <- pow_pos_comm. +rewrite <- ring_mul_assoc. reflexivity. +reflexivity. reflexivity. +Qed. + +Lemma pow_pos_add : forall x i j, + pow_pos x (i + j) == pow_pos x i * pow_pos x j. +Proof. + intro x;induction i;intros. + rewrite Pos.xI_succ_xO;rewrite <- Pos.add_1_r. + rewrite <- Pos.add_diag;repeat rewrite <- Pos.add_assoc. + repeat rewrite IHi. + rewrite Pos.add_comm;rewrite Pos.add_1_r; + rewrite pow_pos_succ. + simpl;repeat rewrite ring_mul_assoc. reflexivity. + rewrite <- Pos.add_diag;repeat rewrite <- Pos.add_assoc. + repeat rewrite IHi. rewrite ring_mul_assoc. reflexivity. + rewrite Pos.add_comm;rewrite Pos.add_1_r;rewrite pow_pos_succ. + simpl. reflexivity. + Qed. + + Definition id_phi_N (x:N) : N := x. + + Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n. + Proof. + intros; reflexivity. + Qed. + + (** Identity is a morphism *) + (* + Instance IDmorph : Ring_morphism _ _ _ (fun x => x). + Proof. + apply (Build_Ring_morphism H6 H6 (fun x => x));intros; + try reflexivity. trivial. + Qed. +*) + (** rings are almost rings*) + Lemma ring_mul_0_l : forall x, 0 * x == 0. + Proof. + intro x. setoid_replace (0*x) with ((0+1)*x + -x). + rewrite ring_add_0_l. rewrite ring_mul_1_l . + rewrite ring_opp_def . fold zero. reflexivity. + rewrite ring_distr_l . rewrite ring_mul_1_l . + rewrite <- ring_add_assoc ; rewrite ring_opp_def . + rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity. + Qed. + + Lemma ring_mul_0_r : forall x, x * 0 == 0. + Proof. + intro x; setoid_replace (x*0) with (x*(0+1) + -x). + rewrite ring_add_0_l ; rewrite ring_mul_1_r . + rewrite ring_opp_def ; fold zero; reflexivity. + + rewrite ring_distr_r ;rewrite ring_mul_1_r . + rewrite <- ring_add_assoc ; rewrite ring_opp_def . + rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity. + Qed. + + Lemma ring_opp_mul_l : forall x y, -(x * y) == -x * y. + Proof. + intros x y;rewrite <- (ring_add_0_l (- x * y)). + rewrite ring_add_comm . + rewrite <- (ring_opp_def (x*y)). + rewrite ring_add_assoc . + rewrite <- ring_distr_l. + rewrite (ring_add_comm (-x));rewrite ring_opp_def . + rewrite ring_mul_0_l;rewrite ring_add_0_l ;reflexivity. + Qed. + +Lemma ring_opp_mul_r : forall x y, -(x * y) == x * -y. + Proof. + intros x y;rewrite <- (ring_add_0_l (x * - y)). + rewrite ring_add_comm . + rewrite <- (ring_opp_def (x*y)). + rewrite ring_add_assoc . + rewrite <- ring_distr_r . + rewrite (ring_add_comm (-y));rewrite ring_opp_def . + rewrite ring_mul_0_r;rewrite ring_add_0_l ;reflexivity. + Qed. + + Lemma ring_opp_add : forall x y, -(x + y) == -x + -y. + Proof. + intros x y;rewrite <- (ring_add_0_l (-(x+y))). + rewrite <- (ring_opp_def x). + rewrite <- (ring_add_0_l (x + - x + - (x + y))). + rewrite <- (ring_opp_def y). + rewrite (ring_add_comm x). + rewrite (ring_add_comm y). + rewrite <- (ring_add_assoc (-y)). + rewrite <- (ring_add_assoc (- x)). + rewrite (ring_add_assoc y). + rewrite (ring_add_comm y). + rewrite <- (ring_add_assoc (- x)). + rewrite (ring_add_assoc y). + rewrite (ring_add_comm y);rewrite ring_opp_def . + rewrite (ring_add_comm (-x) 0);rewrite ring_add_0_l . + rewrite ring_add_comm; reflexivity. + Qed. + + Lemma ring_opp_opp : forall x, - -x == x. + Proof. + intros x; rewrite <- (ring_add_0_l (- -x)). + rewrite <- (ring_opp_def x). + rewrite <- ring_add_assoc ; rewrite ring_opp_def . + rewrite (ring_add_comm x); rewrite ring_add_0_l . reflexivity. + Qed. + + Lemma ring_sub_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2. + Proof. + intros. + setoid_replace (x1 - y1) with (x1 + -y1). + setoid_replace (x2 - y2) with (x2 + -y2). + rewrite H;rewrite H0;reflexivity. + rewrite ring_sub_def. reflexivity. + rewrite ring_sub_def. reflexivity. + Qed. + + Ltac mrewrite := + repeat first + [ rewrite ring_add_0_l + | rewrite <- (ring_add_comm 0) + | rewrite ring_mul_1_l + | rewrite ring_mul_0_l + | rewrite ring_distr_l + | reflexivity + ]. + + Lemma ring_add_0_r : forall x, (x + 0) == x. + Proof. intros; mrewrite. Qed. + + + Lemma ring_add_assoc1 : forall x y z, (x + y) + z == (y + z) + x. + Proof. + intros;rewrite <- (ring_add_assoc x). + rewrite (ring_add_comm x);reflexivity. + Qed. + + Lemma ring_add_assoc2 : forall x y z, (y + x) + z == (y + z) + x. + Proof. + intros; repeat rewrite <- ring_add_assoc. + rewrite (ring_add_comm x); reflexivity. + Qed. + + Lemma ring_opp_zero : -0 == 0. + Proof. + rewrite <- (ring_mul_0_r 0). rewrite ring_opp_mul_l. + repeat rewrite ring_mul_0_r. reflexivity. + Qed. + +End Ring. + +(** Some simplification tactics*) +Ltac gen_reflexivity := reflexivity. + +Ltac gen_rewrite := + repeat first + [ reflexivity + | progress rewrite ring_opp_zero + | rewrite ring_add_0_l + | rewrite ring_add_0_r + | rewrite ring_mul_1_l + | rewrite ring_mul_1_r + | rewrite ring_mul_0_l + | rewrite ring_mul_0_r + | rewrite ring_distr_l + | rewrite ring_distr_r + | rewrite ring_add_assoc + | rewrite ring_mul_assoc + | progress rewrite ring_opp_add + | progress rewrite ring_sub_def + | progress rewrite <- ring_opp_mul_l + | progress rewrite <- ring_opp_mul_r ]. + +Ltac gen_add_push x := +repeat (match goal with + | |- context [(?y + x) + ?z] => + progress rewrite (ring_add_assoc2 x y z) + | |- context [(x + ?y) + ?z] => + progress rewrite (ring_add_assoc1 x y z) + end). diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v new file mode 100644 index 00000000..528ad4f1 --- /dev/null +++ b/plugins/setoid_ring/Ncring_initial.v @@ -0,0 +1,209 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import ZArith_base. +Require Import Zpow_def. +Require Import BinInt. +Require Import BinNat. +Require Import Setoid. +Require Import BinList. +Require Import BinPos. +Require Import BinNat. +Require Import BinInt. +Require Import Setoid. +Require Export Ncring. +Require Export Ncring_polynom. +Import List. + +Set Implicit Arguments. + +(* An object to return when an expression is not recognized as a constant *) +Definition NotConstant := false. + +(** Z is a ring and a setoid*) + +Lemma Zsth : Equivalence (@eq Z). +Proof. exact Z.eq_equiv. Qed. + +Instance Zops:@Ring_ops Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z). + +Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops). +Proof. +constructor; try apply Zsth; try solve_proper. + exact Z.add_comm. exact Z.add_assoc. + exact Z.mul_1_l. exact Z.mul_1_r. exact Z.mul_assoc. + exact Z.mul_add_distr_r. intros; apply Z.mul_add_distr_l. exact Z.sub_diag. +Defined. + +(*Instance ZEquality: @Equality Z:= (@eq Z).*) + +(** Two generic morphisms from Z to (abrbitrary) rings, *) +(**second one is more convenient for proofs but they are ext. equal*) +Section ZMORPHISM. +Context {R:Type}`{Ring R}. + + Ltac rrefl := reflexivity. + + 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. + + Ltac norm := gen_rewrite. + Ltac add_push := Ncring.gen_add_push. +Ltac rsimpl := simpl. + + Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x. + Proof. + induction x;rsimpl. + rewrite IHx. destruct x;simpl;norm. + rewrite IHx;destruct x;simpl;norm. + reflexivity. + Qed. + + Lemma ARgen_phiPOS_Psucc : forall x, + gen_phiPOS1 (Pos.succ x) == 1 + (gen_phiPOS1 x). + Proof. + induction x;rsimpl;norm. + rewrite IHx. gen_rewrite. add_push 1. reflexivity. + 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;reflexivity. + rewrite IHx;norm;add_push (gen_phiPOS1 y);reflexivity. + rewrite ARgen_phiPOS_Psucc;norm;add_push 1;reflexivity. + rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;reflexivity. + rewrite IHx;norm;add_push(gen_phiPOS1 y);reflexivity. + add_push 1;reflexivity. + rewrite ARgen_phiPOS_Psucc;norm;add_push 1;reflexivity. + 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;reflexivity. + Qed. + + +(*morphisms are extensionaly equal*) + Lemma same_genZ : forall x, [x] == gen_phiZ1 x. + Proof. + destruct x;rsimpl; try rewrite same_gen; reflexivity. + Qed. + + Lemma gen_Zeqb_ok : forall x y, + Zeq_bool x y = true -> [x] == [y]. + Proof. + intros x y H7. + assert (H10 := Zeq_bool_eq x y H7);unfold IDphi in H10. + rewrite H10;reflexivity. + Qed. + + Lemma gen_phiZ1_add_pos_neg : forall x y, + gen_phiZ1 (Z.pos_sub x y) + == gen_phiPOS1 x + -gen_phiPOS1 y. + Proof. + intros x y. + generalize (Z.pos_sub_discr x y). + destruct (Z.pos_sub x y) as [|p|p]; intros; subst. + - now rewrite ring_opp_def. + - rewrite ARgen_phiPOS_add;simpl;norm. + add_push (gen_phiPOS1 p). rewrite ring_opp_def;norm. + - rewrite ARgen_phiPOS_add;simpl;norm. + rewrite ring_opp_def;norm. + Qed. + + Lemma match_compOpp : forall x (B:Type) (be bl bg:B), + match CompOpp x with Eq => be | Lt => bl | Gt => bg end + = match x with Eq => be | Lt => bg | Gt => bl end. + Proof. destruct x;simpl;intros;trivial. 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. + induction x;destruct y;simpl;norm. + apply ARgen_phiPOS_add. + apply gen_phiZ1_add_pos_neg. + rewrite gen_phiZ1_add_pos_neg. rewrite ring_add_comm. +reflexivity. + rewrite ARgen_phiPOS_add. rewrite ring_opp_add. reflexivity. +Qed. + +Lemma gen_phiZ_opp : forall x, [- x] == - [x]. + Proof. + intros x. repeat rewrite same_genZ. generalize x ;clear x. + induction x;simpl;norm. + rewrite ring_opp_opp. reflexivity. + 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;try (norm;fail). + rewrite ring_opp_opp ;reflexivity. + Qed. + + Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y]. + Proof. intros;subst;reflexivity. Qed. + +(*proof that [.] satisfies morphism specifications*) +Global Instance gen_phiZ_morph : +(@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*) + apply Build_Ring_morphism; simpl;try reflexivity. + apply gen_phiZ_add. intros. rewrite ring_sub_def. +replace (x-y)%Z with (x + (-y))%Z. +now rewrite gen_phiZ_add, gen_phiZ_opp, ring_sub_def. +reflexivity. + apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext. + Defined. + +End ZMORPHISM. + +Instance multiplication_phi_ring{R:Type}`{Ring R} : Multiplication := + {multiplication x y := (gen_phiZ x) * y}. diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v new file mode 100644 index 00000000..8e4b613f --- /dev/null +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -0,0 +1,584 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* A <X1,...,Xn>: non commutative polynomials on a commutative ring A *) + +Set Implicit Arguments. +Require Import Setoid. +Require Import BinList. +Require Import BinPos. +Require Import BinNat. +Require Import BinInt. +Require Export Ring_polynom. (* n'utilise que PExpr *) +Require Export Ncring. + +Section MakeRingPol. + +Context (C R:Type) `{Rh:Ring_morphism C R}. + +Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. + + Ltac rsimpl := repeat (gen_rewrite || rewrite phiCR_comm). + Ltac add_push := gen_add_push . + +(* Definition of non commutative multivariable polynomials + with coefficients in C : + *) + + Inductive Pol : Type := + | Pc : C -> Pol + | PX : Pol -> positive -> positive -> Pol -> Pol. + (* PX P i n Q represents P * X_i^n + Q *) +Definition cO:C . exact ring0. Defined. +Definition cI:C . exact ring1. Defined. + + Definition P0 := Pc 0. + Definition P1 := Pc 1. + +Variable Ceqb:C->C->bool. +Class Equalityb (A : Type):= {equalityb : A -> A -> bool}. +Notation "x =? y" := (equalityb x y) (at level 70, no associativity). +Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y). + +Instance equalityb_coef : Equalityb C := + {equalityb x y := Ceqb x y}. + + Fixpoint Peq (P P' : Pol) {struct P'} : bool := + match P, P' with + | Pc c, Pc c' => c =? c' + | PX P i n Q, PX P' i' n' Q' => + match Pos.compare i i', Pos.compare n n' with + | Eq, Eq => if Peq P P' then Peq Q Q' else false + | _,_ => false + end + | _, _ => false + end. + +Instance equalityb_pol : Equalityb Pol := + {equalityb x y := Peq x y}. + +(* Q a ses variables de queue < i *) + Definition mkPX P i n Q := + match P with + | Pc c => if c =? 0 then Q else PX P i n Q + | PX P' i' n' Q' => + match Pos.compare i i' with + | Eq => if Q' =? P0 then PX P' i (n + n') Q else PX P i n Q + | _ => PX P i n Q + end + end. + + Definition mkXi i n := PX P1 i n P0. + + Definition mkX i := mkXi i 1. + + (** Opposite of addition *) + + Fixpoint Popp (P:Pol) : Pol := + match P with + | Pc c => Pc (- c) + | PX P i n Q => PX (Popp P) i n (Popp Q) + end. + + Notation "-- P" := (Popp P)(at level 30). + + (** Addition et subtraction *) + + Fixpoint PaddCl (c:C)(P:Pol) {struct P} : Pol := + match P with + | Pc c1 => Pc (c + c1) + | PX P i n Q => PX P i n (PaddCl c Q) + end. + +(* Q quelconque *) + +Section PaddX. +Variable Padd:Pol->Pol->Pol. +Variable P:Pol. + +(* Xi^n * P + Q +les variables de tete de Q ne sont pas forcement < i +mais Q est normalisé : variables de tete decroissantes *) + +Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:= + match Q with + | Pc c => mkPX P i n Q + | PX P' i' n' Q' => + match Pos.compare i i' with + | (* i > i' *) + Gt => mkPX P i n Q + | (* i < i' *) + Lt => mkPX P' i' n' (PaddX i n Q') + | (* i = i' *) + Eq => match Z.pos_sub n n' with + | (* n > n' *) + Zpos k => mkPX (PaddX i k P') i' n' Q' + | (* n = n' *) + Z0 => mkPX (Padd P P') i n Q' + | (* n < n' *) + Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q' + end + end + end. + +End PaddX. + +Fixpoint Padd (P1 P2: Pol) {struct P1} : Pol := + match P1 with + | Pc c => PaddCl c P2 + | PX P' i' n' Q' => + PaddX Padd P' i' n' (Padd Q' P2) + end. + + Notation "P ++ P'" := (Padd P P'). + +Definition Psub(P P':Pol):= P ++ (--P'). + + Notation "P -- P'" := (Psub P P')(at level 50). + + (** Multiplication *) + + Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol := + match P with + | Pc c' => Pc (c' * c) + | PX P i n Q => mkPX (PmulC_aux P c) i n (PmulC_aux Q c) + end. + + Definition PmulC P c := + if c =? 0 then P0 else + if c =? 1 then P else PmulC_aux P c. + + Fixpoint Pmul (P1 P2 : Pol) {struct P2} : Pol := + match P2 with + | Pc c => PmulC P1 c + | PX P i n Q => + PaddX Padd (Pmul P1 P) i n (Pmul P1 Q) + end. + + Notation "P ** P'" := (Pmul P P')(at level 40). + + Definition Psquare (P:Pol) : Pol := P ** P. + + + (** Evaluation of a polynomial towards R *) + + Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R := + match P with + | Pc c => [c] + | PX P i n Q => + let x := nth 0 i l in + let xn := pow_pos x n in + (Pphi l P) * xn + (Pphi l Q) + end. + + Reserved Notation "P @ l " (at level 10, no associativity). + Notation "P @ l " := (Pphi l P). + + (** Proofs *) + + Ltac destr_pos_sub H := + match goal with |- context [Z.pos_sub ?x ?y] => + assert (H := Z.pos_sub_discr x y); destruct (Z.pos_sub x y) + end. + + Lemma Peq_ok : forall P P', + (P =? P') = true -> forall l, P@l == P'@ l. + Proof. + induction P;destruct P';simpl;intros ;try easy. + - now apply ring_morphism_eq, Ceqb_eq. + - specialize (IHP1 P'1). specialize (IHP2 P'2). + simpl in IHP1, IHP2. + destruct (Pos.compare_spec p p1); try discriminate; + destruct (Pos.compare_spec p0 p2); try discriminate. + destruct (Peq P2 P'1); try discriminate. + subst; now rewrite IHP1, IHP2. + Qed. + + Lemma Pphi0 : forall l, P0@l == 0. + Proof. + intros;simpl. + rewrite ring_morphism0. reflexivity. + Qed. + + Lemma Pphi1 : forall l, P1@l == 1. + Proof. + intros;simpl; rewrite ring_morphism1. reflexivity. + Qed. + + Lemma mkPX_ok : forall l P i n Q, + (mkPX P i n Q)@l == P@l * (pow_pos (nth 0 i l) n) + Q@l. + Proof. + intros l P i n Q;unfold mkPX. + destruct P;try (simpl;reflexivity). + assert (Hh := ring_morphism_eq c 0). +simpl; case_eq (Ceqb c 0);simpl;try reflexivity. +intros. + rewrite Hh. rewrite ring_morphism0. + rsimpl. apply Ceqb_eq. trivial. + destruct (Pos.compare_spec i p). + assert (Hh := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl. + rewrite Hh. + rewrite Pphi0. rsimpl. rewrite Pos.add_comm. rewrite pow_pos_add;rsimpl. + subst;trivial. reflexivity. trivial. intros. simpl. reflexivity. simpl. reflexivity. + simpl. reflexivity. + Qed. + +Ltac Esimpl := + repeat (progress ( + match goal with + | |- context [?P@?l] => + match P with + | P0 => rewrite (Pphi0 l) + | P1 => rewrite (Pphi1 l) + | (mkPX ?P ?i ?n ?Q) => rewrite (mkPX_ok l P i n Q) + end + | |- context [[?c]] => + match c with + | 0 => rewrite ring_morphism0 + | 1 => rewrite ring_morphism1 + | ?x + ?y => rewrite ring_morphism_add + | ?x * ?y => rewrite ring_morphism_mul + | ?x - ?y => rewrite ring_morphism_sub + | - ?x => rewrite ring_morphism_opp + end + end)); + simpl; rsimpl. + + Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l . + Proof. + induction P; simpl; intros; Esimpl; try reflexivity. + rewrite IHP2. rsimpl. +rewrite (ring_add_comm (P2 @ l * pow_pos (nth 0 p l) p0) [c]). +reflexivity. + Qed. + + Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l == P@l * [c]. + Proof. + induction P;simpl;intros. rewrite ring_morphism_mul. +try reflexivity. + simpl. Esimpl. rewrite IHP1;rewrite IHP2;rsimpl. + Qed. + + Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c]. + Proof. + intros c P l; unfold PmulC. + assert (Hh:= ring_morphism_eq c 0);case_eq (c =? 0). intros. + rewrite Hh;Esimpl. apply Ceqb_eq;trivial. + assert (H1h:= ring_morphism_eq c 1);case_eq (c =? 1);intros. + rewrite H1h;Esimpl. apply Ceqb_eq;trivial. + apply PmulC_aux_ok. + Qed. + + Lemma Popp_ok : forall P l, (--P)@l == - P@l. + Proof. + induction P;simpl;intros. + Esimpl. + rewrite IHP1;rewrite IHP2;rsimpl. + Qed. + + Ltac Esimpl2 := + Esimpl; + repeat (progress ( + match goal with + | |- context [(PaddCl ?c ?P)@?l] => rewrite (PaddCl_ok c P l) + | |- context [(PmulC ?P ?c)@?l] => rewrite (PmulC_ok c P l) + | |- context [(--?P)@?l] => rewrite (Popp_ok P l) + end)); Esimpl. + +Lemma PaddXPX: forall P i n Q, + PaddX Padd P i n Q = + match Q with + | Pc c => mkPX P i n Q + | PX P' i' n' Q' => + match Pos.compare i i' with + | (* i > i' *) + Gt => mkPX P i n Q + | (* i < i' *) + Lt => mkPX P' i' n' (PaddX Padd P i n Q') + | (* i = i' *) + Eq => match Z.pos_sub n n' with + | (* n > n' *) + Zpos k => mkPX (PaddX Padd P i k P') i' n' Q' + | (* n = n' *) + Z0 => mkPX (Padd P P') i n Q' + | (* n < n' *) + Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q' + end + end + end. +induction Q; reflexivity. +Qed. + +Lemma PaddX_ok2 : forall P2, + (forall P l, (P2 ++ P) @ l == P2 @ l + P @ l) + /\ + (forall P k n l, + (PaddX Padd P2 k n P) @ l == + P2 @ l * pow_pos (nth 0 k l) n + P @ l). +induction P2;simpl;intros. split. intros. apply PaddCl_ok. + induction P. unfold PaddX. intros. rewrite mkPX_ok. + simpl. rsimpl. +intros. simpl. + destruct (Pos.compare_spec k p) as [Hh|Hh|Hh]. + destr_pos_sub H1h. Esimpl2. +rewrite Hh; trivial. rewrite H1h. reflexivity. +simpl. rewrite mkPX_ok. rewrite IHP1. Esimpl2. + rewrite Pos.add_comm in H1h. +rewrite H1h. +rewrite pow_pos_add. Esimpl2. +rewrite Hh; trivial. reflexivity. +rewrite mkPX_ok. rewrite PaddCl_ok. Esimpl2. rewrite Pos.add_comm in H1h. +rewrite H1h. Esimpl2. rewrite pow_pos_add. Esimpl2. +rewrite Hh; trivial. reflexivity. +rewrite mkPX_ok. rewrite IHP2. Esimpl2. +rewrite (ring_add_comm (P2 @ l * pow_pos (nth 0 p l) p0) + ([c] * pow_pos (nth 0 k l) n)). +reflexivity. assert (H1h := ring_morphism_eq c 0);case_eq (Ceqb c 0); + intros; simpl. +rewrite H1h;trivial. Esimpl2. apply Ceqb_eq; trivial. reflexivity. +decompose [and] IHP2_1. decompose [and] IHP2_2. clear IHP2_1 IHP2_2. +split. intros. rewrite H0. rewrite H1. +Esimpl2. +induction P. unfold PaddX. intros. rewrite mkPX_ok. simpl. reflexivity. +intros. rewrite PaddXPX. +destruct (Pos.compare_spec k p1) as [H3h|H3h|H3h]. +destr_pos_sub H4h. +rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. Esimpl2. +rewrite H4h. rewrite H3h;trivial. reflexivity. +rewrite mkPX_ok. rewrite IHP1. Esimpl2. rewrite H3h;trivial. +rewrite Pos.add_comm in H4h. +rewrite H4h. rewrite pow_pos_add. Esimpl2. +rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. +rewrite mkPX_ok. + Esimpl2. rewrite H3h;trivial. + rewrite Pos.add_comm in H4h. +rewrite H4h. rewrite pow_pos_add. Esimpl2. +rewrite mkPX_ok. simpl. rewrite IHP2. Esimpl2. +gen_add_push (P2 @ l * pow_pos (nth 0 p1 l) p2). try reflexivity. +rewrite mkPX_ok. simpl. reflexivity. +Qed. + +Lemma Padd_ok : forall P Q l, (P ++ Q) @ l == P @ l + Q @ l. +intro P. elim (PaddX_ok2 P); auto. +Qed. + +Lemma PaddX_ok : forall P2 P k n l, + (PaddX Padd P2 k n P) @ l == P2 @ l * pow_pos (nth 0 k l) n + P @ l. +intro P2. elim (PaddX_ok2 P2); auto. +Qed. + + Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l. +unfold Psub. intros. rewrite Padd_ok. rewrite Popp_ok. rsimpl. + Qed. + + Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. +induction P'; simpl; intros. rewrite PmulC_ok. reflexivity. +rewrite PaddX_ok. rewrite IHP'1. rewrite IHP'2. Esimpl2. +Qed. + + Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l. + Proof. + intros. unfold Psquare. apply Pmul_ok. + Qed. + + (** Definition of polynomial expressions *) + +(* + Inductive PExpr : Type := + | PEc : C -> PExpr + | PEX : positive -> PExpr + | PEadd : PExpr -> PExpr -> PExpr + | PEsub : PExpr -> PExpr -> PExpr + | PEmul : PExpr -> PExpr -> PExpr + | PEopp : PExpr -> PExpr + | PEpow : PExpr -> N -> PExpr. +*) + + (** Specification of the power function *) + Section POWER. + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + + Record power_theory : Prop := mkpow_th { + rpow_pow_N : forall r n, (rpow r (Cp_phi n))== (pow_N r n) + }. + + End POWER. + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + Variable pow_th : power_theory Cp_phi rpow. + + (** evaluation of polynomial expressions towards R *) + Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R := + match pe with + | PEc c => [c] + | PEX j => nth 0 j l + | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) + | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2) + | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2) + | PEopp pe1 => - (PEeval l pe1) + | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n) + end. + +Strategy expand [PEeval]. + + Definition mk_X j := mkX j. + + (** Correctness proofs *) + + Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l. + Proof. + destruct p;simpl;intros;Esimpl;trivial. + Qed. + + Ltac Esimpl3 := + repeat match goal with + | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P1 P2 l) + | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P1 P2 l) + end;try Esimpl2;try reflexivity;try apply ring_add_comm. + +(* Power using the chinise algorithm *) + +Section POWER2. + Variable subst_l : Pol -> Pol. + Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol := + match p with + | xH => subst_l (Pmul P res) + | xO p => Ppow_pos (Ppow_pos res P p) P p + | xI p => subst_l (Pmul P (Ppow_pos (Ppow_pos res P p) P p)) + end. + + Definition Ppow_N P n := + match n with + | N0 => P1 + | Npos p => Ppow_pos P1 P p + end. + + Fixpoint pow_pos_gen (R:Type)(m:R->R->R)(x:R) (i:positive) {struct i}: R := + match i with + | xH => x + | xO i => let p := pow_pos_gen m x i in m p p + | xI i => let p := pow_pos_gen m x i in m x (m p p) + end. + +Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) -> + forall res P p, (Ppow_pos res P p)@l == (pow_pos_gen Pmul P p)@l * res@l. + Proof. + intros l subst_l_ok res P p. generalize res;clear res. + induction p;simpl;intros. try rewrite subst_l_ok. + repeat rewrite Pmul_ok. repeat rewrite IHp. + rsimpl. repeat rewrite Pmul_ok. repeat rewrite IHp. rsimpl. + try rewrite subst_l_ok. + repeat rewrite Pmul_ok. reflexivity. + Qed. + +Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) := + match p with + | N0 => x1 + | Npos p => pow_pos_gen m x p + end. + + Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) -> + forall P n, (Ppow_N P n)@l == (pow_N_gen P1 Pmul P n)@l. + Proof. destruct n;simpl. reflexivity. rewrite Ppow_pos_ok; trivial. Esimpl. Qed. + + End POWER2. + + (** Normalization and rewriting *) + + Section NORM_SUBST_REC. + Let subst_l (P:Pol) := P. + Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2). + Let Ppow_subst := Ppow_N subst_l. + + Fixpoint norm_aux (pe:PExpr C) : Pol := + match pe with + | PEc c => Pc c + | PEX j => mk_X j + | PEadd pe1 (PEopp pe2) => + Psub (norm_aux pe1) (norm_aux pe2) + | PEadd pe1 pe2 => Padd (norm_aux pe1) (norm_aux pe2) + | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2) + | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2) + | PEopp pe1 => Popp (norm_aux pe1) + | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n + end. + + Definition norm_subst pe := subst_l (norm_aux pe). + + + Lemma norm_aux_spec : + forall l pe, + PEeval l pe == (norm_aux pe)@l. + Proof. + intros. + induction pe. +Esimpl3. Esimpl3. simpl. + rewrite IHpe1;rewrite IHpe2. + destruct pe2; Esimpl3. +unfold Psub. +destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity. +simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2. +destruct pe1. destruct pe2; rewrite Padd_ok; rewrite Popp_ok; try reflexivity. +Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. + Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. +simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity. +simpl. rewrite IHpe; Esimpl3. +simpl. + rewrite Ppow_N_ok; (intros;try reflexivity). + rewrite rpow_pow_N. Esimpl3. + induction n;simpl. Esimpl3. induction p; simpl. + try rewrite IHp;try rewrite IHpe; + repeat rewrite Pms_ok; + repeat rewrite Pmul_ok;reflexivity. +rewrite Pmul_ok. try rewrite IHp;try rewrite IHpe; + repeat rewrite Pms_ok; + repeat rewrite Pmul_ok;reflexivity. trivial. +exact pow_th. + Qed. + + Lemma norm_subst_spec : + forall l pe, + PEeval l pe == (norm_subst pe)@l. + Proof. + intros;unfold norm_subst. + unfold subst_l. apply norm_aux_spec. + Qed. + + End NORM_SUBST_REC. + + Fixpoint interp_PElist (l:list R) (lpe:list (PExpr C * PExpr C)) {struct lpe} : Prop := + match lpe with + | nil => True + | (me,pe)::lpe => + match lpe with + | nil => PEeval l me == PEeval l pe + | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe + end + end. + + + Lemma norm_subst_ok : forall l pe, + PEeval l pe == (norm_subst pe)@l. + Proof. + intros;apply norm_subst_spec. + Qed. + + + Lemma ring_correct : forall l pe1 pe2, + (norm_subst pe1 =? norm_subst pe2) = true -> + PEeval l pe1 == PEeval l pe2. + Proof. + simpl;intros. + do 2 (rewrite (norm_subst_ok l);trivial). + apply Peq_ok;trivial. + Qed. + +End MakeRingPol. diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v new file mode 100644 index 00000000..44f8e7ff --- /dev/null +++ b/plugins/setoid_ring/Ncring_tac.v @@ -0,0 +1,308 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import List. +Require Import Setoid. +Require Import BinPos. +Require Import BinList. +Require Import Znumtheory. +Require Export Morphisms Setoid Bool. +Require Import ZArith. +Require Import Algebra_syntax. +Require Export Ncring. +Require Import Ncring_polynom. +Require Import Ncring_initial. + + +Set Implicit Arguments. + +Class nth (R:Type) (t:R) (l:list R) (i:nat). + +Instance Ifind0 (R:Type) (t:R) l + : nth t(t::l) 0. + +Instance IfindS (R:Type) (t2 t1:R) l i + {_:nth t1 l i} + : nth t1 (t2::l) (S i) | 1. + +Class closed (T:Type) (l:list T). + +Instance Iclosed_nil T + : closed (T:=T) nil. + +Instance Iclosed_cons T t (l:list T) + {_:closed l} + : closed (t::l). + +Class reify (R:Type)`{Rr:Ring (T:=R)} (e:PExpr Z) (lvar:list R) (t:R). + +Instance reify_zero (R:Type) lvar op + `{Ring (T:=R)(ring0:=op)} + : reify (ring0:=op)(PEc 0%Z) lvar op. + +Instance reify_one (R:Type) lvar op + `{Ring (T:=R)(ring1:=op)} + : reify (ring1:=op) (PEc 1%Z) lvar op. + +Instance reifyZ0 (R:Type) lvar + `{Ring (T:=R)} + : reify (PEc Z0) lvar Z0|11. + +Instance reifyZpos (R:Type) lvar (p:positive) + `{Ring (T:=R)} + : reify (PEc (Zpos p)) lvar (Zpos p)|11. + +Instance reifyZneg (R:Type) lvar (p:positive) + `{Ring (T:=R)} + : reify (PEc (Zneg p)) lvar (Zneg p)|11. + +Instance reify_add (R:Type) + e1 lvar t1 e2 t2 op + `{Ring (T:=R)(add:=op)} + {_:reify (add:=op) e1 lvar t1} + {_:reify (add:=op) e2 lvar t2} + : reify (add:=op) (PEadd e1 e2) lvar (op t1 t2). + +Instance reify_mul (R:Type) + e1 lvar t1 e2 t2 op + `{Ring (T:=R)(mul:=op)} + {_:reify (mul:=op) e1 lvar t1} + {_:reify (mul:=op) e2 lvar t2} + : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10. + +Instance reify_mul_ext (R:Type) `{Ring R} + lvar z e2 t2 + `{Ring (T:=R)} + {_:reify e2 lvar t2} + : reify (PEmul (PEc z) e2) lvar + (@multiplication Z _ _ z t2)|9. + +Instance reify_sub (R:Type) + e1 lvar t1 e2 t2 op + `{Ring (T:=R)(sub:=op)} + {_:reify (sub:=op) e1 lvar t1} + {_:reify (sub:=op) e2 lvar t2} + : reify (sub:=op) (PEsub e1 e2) lvar (op t1 t2). + +Instance reify_opp (R:Type) + e1 lvar t1 op + `{Ring (T:=R)(opp:=op)} + {_:reify (opp:=op) e1 lvar t1} + : reify (opp:=op) (PEopp e1) lvar (op t1). + +Instance reify_pow (R:Type) `{Ring R} + e1 lvar t1 n + `{Ring (T:=R)} + {_:reify e1 lvar t1} + : reify (PEpow e1 n) lvar (pow_N t1 n)|1. + +Instance reify_var (R:Type) t lvar i + `{nth R t lvar i} + `{Rr: Ring (T:=R)} + : reify (Rr:= Rr) (PEX Z (Pos.of_succ_nat i))lvar t + | 100. + +Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) + (lterm:list R). + +Instance reify_nil (R:Type) lvar + `{Rr: Ring (T:=R)} + : reifylist (Rr:= Rr) nil lvar (@nil R). + +Instance reify_cons (R:Type) e1 lvar t1 lexpr2 lterm2 + `{Rr: Ring (T:=R)} + {_:reify (Rr:= Rr) e1 lvar t1} + {_:reifylist (Rr:= Rr) lexpr2 lvar lterm2} + : reifylist (Rr:= Rr) (e1::lexpr2) lvar (t1::lterm2). + +Definition list_reifyl (R:Type) lexpr lvar lterm + `{Rr: Ring (T:=R)} + {_:reifylist (Rr:= Rr) lexpr lvar lterm} + `{closed (T:=R) lvar} := (lvar,lexpr). + +Unset Implicit Arguments. + + +Ltac lterm_goal g := + match g with + | ?t1 == ?t2 => constr:(t1::t2::nil) + | ?t1 = ?t2 => constr:(t1::t2::nil) + | (_ ?t1 ?t2) => constr:(t1::t2::nil) + end. + +Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y. + intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed. + +Ltac reify_goal lvar lexpr lterm:= + (*idtac lvar; idtac lexpr; idtac lterm;*) + match lexpr with + nil => idtac + | ?e1::?e2::_ => + match goal with + |- (?op ?u1 ?u2) => + change (op + (@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N + (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _) + lvar e1) + (@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N + (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _) + lvar e2)) + end + end. + +Lemma comm: forall (R:Type)`{Ring R}(c : Z) (x : R), + x * (gen_phiZ c) == (gen_phiZ c) * x. +induction c. intros. simpl. gen_rewrite. simpl. intros. +rewrite <- same_gen. +induction p. simpl. gen_rewrite. rewrite IHp. reflexivity. +simpl. gen_rewrite. rewrite IHp. reflexivity. +simpl. gen_rewrite. +simpl. intros. rewrite <- same_gen. +induction p. simpl. generalize IHp. clear IHp. +gen_rewrite. intro IHp. rewrite IHp. reflexivity. +simpl. generalize IHp. clear IHp. +gen_rewrite. intro IHp. rewrite IHp. reflexivity. +simpl. gen_rewrite. Qed. + +Ltac ring_gen := + match goal with + |- ?g => let lterm := lterm_goal g in + match eval red in (list_reifyl (lterm:=lterm)) with + | (?fv, ?lexpr) => + (*idtac "variables:";idtac fv; + idtac "terms:"; idtac lterm; + idtac "reifications:"; idtac lexpr; *) + reify_goal fv lexpr lterm; + match goal with + |- ?g => + apply (@ring_correct Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ + (@gen_phiZ _ _ _ _ _ _ _ _ _) _ + (@comm _ _ _ _ _ _ _ _ _ _) Zeq_bool Zeqb_ok N (fun n:N => n) + (@pow_N _ _ _ _ _ _ _ _ _)); + [apply mkpow_th; reflexivity + |vm_compute; reflexivity] + end + end + end. + +Ltac non_commutative_ring:= + intros; + ring_gen. + +(* simplification *) + +Ltac ring_simplify_aux lterm fv lexpr hyp := + match lterm with + | ?t0::?lterm => + match lexpr with + | ?e::?le => (* e:PExpr Z est la réification de t0:R *) + let t := constr:(@Ncring_polynom.norm_subst + Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z) Zops Zeq_bool e) in + (* t:Pol Z *) + let te := + constr:(@Ncring_polynom.Pphi Z + _ 0 1 _+_ _*_ _-_ -_ _==_ _ Ncring_initial.gen_phiZ fv t) in + let eq1 := fresh "ring" in + let nft := eval vm_compute in t in + let t':= fresh "t" in + pose (t' := nft); + assert (eq1 : t = t'); + [vm_cast_no_check (eq_refl t')| + let eq2 := fresh "ring" in + assert (eq2:(@Ncring_polynom.PEeval Z + _ 0 1 _+_ _*_ _-_ -_ _==_ _ Ncring_initial.gen_phiZ N (fun n:N => n) + (@Ring_theory.pow_N _ 1 multiplication) fv e) == te); + [apply (@Ncring_polynom.norm_subst_ok + Z _ 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z) + _ _ 0 1 _+_ _*_ _-_ -_ _==_ _ _ Ncring_initial.gen_phiZ _ + (@comm _ 0 1 _+_ _*_ _-_ -_ _==_ _ _) _ Zeqb_ok); + apply mkpow_th; reflexivity + | match hyp with + | 1%nat => rewrite eq2 + | ?H => try rewrite eq2 in H + end]; + let P:= fresh "P" in + match hyp with + | 1%nat => idtac "ok"; + rewrite eq1; + pattern (@Ncring_polynom.Pphi Z _ 0 1 _+_ _*_ _-_ -_ _==_ + _ Ncring_initial.gen_phiZ fv t'); + match goal with + |- (?p ?t) => set (P:=p) + end; + unfold t' in *; clear t' eq1 eq2; simpl + | ?H => + rewrite eq1 in H; + pattern (@Ncring_polynom.Pphi Z _ 0 1 _+_ _*_ _-_ -_ _==_ + _ Ncring_initial.gen_phiZ fv t') in H; + match type of H with + | (?p ?t) => set (P:=p) in H + end; + unfold t' in *; clear t' eq1 eq2; simpl in H + end; unfold P in *; clear P + ]; ring_simplify_aux lterm fv le hyp + | nil => idtac + end + | nil => idtac + end. + +Ltac set_variables fv := + match fv with + | nil => idtac + | ?t::?fv => + let v := fresh "X" in + set (v:=t) in *; set_variables fv + end. + +Ltac deset n:= + match n with + | 0%nat => idtac + | S ?n1 => + match goal with + | h:= ?v : ?t |- ?g => unfold h in *; clear h; deset n1 + end + end. + +(* a est soit un terme de l'anneau, soit une liste de termes. +J'ai pas réussi à un décomposer les Vlists obtenues avec ne_constr_list + dans Tactic Notation *) + +Ltac ring_simplify_gen a hyp := + let lterm := + match a with + | _::_ => a + | _ => constr:(a::nil) + end in + match eval red in (list_reifyl (lterm:=lterm)) with + | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr; + let n := eval compute in (length fv) in + idtac n; + let lt:=fresh "lt" in + set (lt:= lterm); + let lv:=fresh "fv" in + set (lv:= fv); + (* les termes de fv sont remplacés par des variables + pour pouvoir utiliser simpl ensuite sans risquer + des simplifications indésirables *) + set_variables fv; + let lterm1 := eval unfold lt in lt in + let lv1 := eval unfold lv in lv in + idtac lterm1; idtac lv1; + ring_simplify_aux lterm1 lv1 lexpr hyp; + clear lt lv; + (* on remet les termes de fv *) + deset n + end. + +Tactic Notation "non_commutative_ring_simplify" constr(lterm):= + ring_simplify_gen lterm 1%nat. + +Tactic Notation "non_commutative_ring_simplify" constr(lterm) "in" ident(H):= + ring_simplify_gen lterm H. + + diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v index 56473adb..29372212 100644 --- a/plugins/setoid_ring/RealField.v +++ b/plugins/setoid_ring/RealField.v @@ -5,21 +5,21 @@ Require Import Rdefinitions. Require Import Rpow_def. Require Import Raxioms. -Open Local Scope R_scope. +Local Open Scope R_scope. Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)). Proof. constructor. intro; apply Rplus_0_l. exact Rplus_comm. - symmetry in |- *; apply Rplus_assoc. + symmetry ; apply Rplus_assoc. intro; apply Rmult_1_l. exact Rmult_comm. - symmetry in |- *; apply Rmult_assoc. + symmetry ; apply Rmult_assoc. intros m n p. - rewrite Rmult_comm in |- *. - rewrite (Rmult_comm n p) in |- *. - rewrite (Rmult_comm m p) in |- *. + rewrite Rmult_comm. + rewrite (Rmult_comm n p). + rewrite (Rmult_comm m p). apply Rmult_plus_distr_l. reflexivity. exact Rplus_opp_r. @@ -42,17 +42,17 @@ destruct H0. apply Rlt_trans with (IZR (up x)); trivial. replace (IZR (up x)) with (x + (IZR (up x) - x))%R. apply Rplus_lt_compat_l; trivial. - unfold Rminus in |- *. - rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *. - rewrite <- Rplus_assoc in |- *. - rewrite Rplus_opp_r in |- *. + unfold Rminus. + rewrite (Rplus_comm (IZR (up x)) (- x)). + rewrite <- Rplus_assoc. + rewrite Rplus_opp_r. apply Rplus_0_l. elim H0. - unfold Rminus in |- *. - rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *. - rewrite <- Rplus_assoc in |- *. - rewrite Rplus_opp_r in |- *. - rewrite Rplus_0_l in |- *; trivial. + unfold Rminus. + rewrite (Rplus_comm (IZR (up x)) (- x)). + rewrite <- Rplus_assoc. + rewrite Rplus_opp_r. + rewrite Rplus_0_l; trivial. Qed. Notation Rset := (Eqsth R). @@ -61,7 +61,7 @@ Notation Rext := (Eq_ext Rplus Rmult Ropp). Lemma Rlt_0_2 : 0 < 2. apply Rlt_trans with (0 + 1). apply Rlt_n_Sn. - rewrite Rplus_comm in |- *. + rewrite Rplus_comm. apply Rplus_lt_compat_l. replace 1 with (0 + 1). apply Rlt_n_Sn. @@ -69,19 +69,19 @@ apply Rlt_trans with (0 + 1). Qed. Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0. -unfold Rgt in |- *. -induction x; simpl in |- *; intros. +unfold Rgt. +induction x; simpl; intros. apply Rlt_trans with (1 + 0). - rewrite Rplus_comm in |- *. + rewrite Rplus_comm. apply Rlt_n_Sn. apply Rplus_lt_compat_l. - rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *. - rewrite Rmult_comm in |- *. + rewrite <- (Rmul_0_l Rset Rext RTheory 2). + rewrite Rmult_comm. apply Rmult_lt_compat_l. apply Rlt_0_2. trivial. - rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *. - rewrite Rmult_comm in |- *. + rewrite <- (Rmul_0_l Rset Rext RTheory 2). + rewrite Rmult_comm. apply Rmult_lt_compat_l. apply Rlt_0_2. trivial. @@ -93,9 +93,9 @@ Qed. Lemma Rgen_phiPOS_not_0 : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0. -red in |- *; intros. +red; intros. specialize (Rgen_phiPOS x). -rewrite H in |- *; intro. +rewrite H; intro. apply (Rlt_asym 0 0); trivial. Qed. @@ -107,23 +107,23 @@ Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0. Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x (n + m) = pow x n * pow x m. Proof. - intros x n; elim n; simpl in |- *; auto with real. + intros x n; elim n; simpl; auto with real. intros n0 H' m; rewrite H'; auto with real. Qed. -Lemma R_power_theory : power_theory 1%R Rmult (eq (A:=R)) nat_of_N pow. +Lemma R_power_theory : power_theory 1%R Rmult (@eq R) N.to_nat pow. Proof. constructor. destruct n. reflexivity. - simpl. induction p;simpl. - rewrite ZL6. rewrite Rdef_pow_add;rewrite IHp. reflexivity. - unfold nat_of_P;simpl;rewrite ZL6;rewrite Rdef_pow_add;rewrite IHp;trivial. - rewrite Rmult_comm;apply Rmult_1_l. + simpl. induction p. + - rewrite Pos2Nat.inj_xI. simpl. now rewrite plus_0_r, Rdef_pow_add, IHp. + - rewrite Pos2Nat.inj_xO. simpl. now rewrite plus_0_r, Rdef_pow_add, IHp. + - simpl. rewrite Rmult_comm;apply Rmult_1_l. Qed. Ltac Rpow_tac t := match isnatcst t with | false => constr:(InitialRing.NotConstant) - | _ => constr:(N_of_nat t) + | _ => constr:(N.of_nat t) end. Add Field RField : Rfield diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v index 7b48f590..7c1bf981 100644 --- a/plugins/setoid_ring/Ring.v +++ b/plugins/setoid_ring/Ring.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -14,7 +14,7 @@ Require Export Ring_tac. Lemma BoolTheory : ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)). -split; simpl in |- *. +split; simpl. destruct x; reflexivity. destruct x; destruct y; reflexivity. destruct x; destruct y; destruct z; reflexivity. diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v index 9bc95a7f..dc5248b2 100644 --- a/plugins/setoid_ring/Ring_base.v +++ b/plugins/setoid_ring/Ring_base.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index d33a095f..b23ba352 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -1,20 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) Set Implicit Arguments. -Require Import Setoid. -Require Import BinList. -Require Import BinPos. -Require Import BinNat. -Require Import BinInt. +Require Import Setoid Morphisms BinList BinPos BinNat BinInt. Require Export Ring_theory. -Open Local Scope positive_scope. +Local Open Scope positive_scope. Import RingSyntax. Section MakeRingPol. @@ -25,7 +21,7 @@ Section MakeRingPol. Variable req : R -> R -> Prop. (* Ring properties *) - Variable Rsth : Setoid_Theory R req. + Variable Rsth : Equivalence req. Variable Reqe : ring_eq_ext radd rmul ropp req. Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req. @@ -37,8 +33,8 @@ Section MakeRingPol. Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi. - (* Power coefficients *) - Variable Cpow : Set. + (* Power coefficients *) + Variable Cpow : Type. Variable Cp_phi : N -> Cpow. Variable rpow : R -> Cpow -> R. Variable pow_th : power_theory rI rmul req Cp_phi rpow. @@ -50,26 +46,47 @@ Section MakeRingPol. (* R notations *) 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). + Infix "+" := radd. Infix "*" := rmul. + Infix "-" := rsub. Notation "- x" := (ropp x). + Infix "==" := req. + Infix "^" := (pow_pos rmul). (* C notations *) - Notation "x +! y" := (cadd x y). Notation "x *! y " := (cmul x y). - Notation "x -! y " := (csub x y). Notation "-! x" := (copp x). - Notation " x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x). + Infix "+!" := cadd. Infix "*!" := cmul. + Infix "-! " := csub. Notation "-! x" := (copp x). + Infix "?=!" := ceqb. Notation "[ x ]" := (phi x). (* Useful tactics *) - Add Setoid R req Rsth as R_set1. - Ltac rrefl := gen_reflexivity Rsth. - Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. + Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac rsimpl := gen_srewrite Rsth Reqe ARth. + Ltac add_push := gen_add_push radd Rsth Reqe ARth. Ltac mul_push := gen_mul_push rmul Rsth Reqe ARth. + Ltac add_permut_rec t := + match t with + | ?x + ?y => add_permut_rec y || add_permut_rec x + | _ => add_push t; apply (Radd_ext Reqe); [|reflexivity] + end. + + Ltac add_permut := + repeat (reflexivity || + match goal with |- ?t == _ => add_permut_rec t end). + + Ltac mul_permut_rec t := + match t with + | ?x * ?y => mul_permut_rec y || mul_permut_rec x + | _ => mul_push t; apply (Rmul_ext Reqe); [|reflexivity] + end. + + Ltac mul_permut := + repeat (reflexivity || + match goal with |- ?t == _ => mul_permut_rec t end). + + (* Definition of multivariable polynomials with coefficients in C : Type [Pol] represents [X1 ... Xn]. The representation is Horner's where a [n] variable polynomial @@ -104,31 +121,31 @@ Section MakeRingPol. match P, P' with | Pc c, Pc c' => c ?=! c' | Pinj j Q, Pinj j' Q' => - match Pcompare j j' Eq with + match j ?= j' with | Eq => Peq Q Q' | _ => false end | PX P i Q, PX P' i' Q' => - match Pcompare i i' Eq with + match i ?= i' with | Eq => if Peq P P' then Peq Q Q' else false | _ => false end | _, _ => false end. - Notation " P ?== P' " := (Peq P P'). + Infix "?==" := Peq. Definition mkPinj j P := match P with | Pc _ => P - | Pinj j' Q => Pinj ((j + j'):positive) Q + | Pinj j' Q => Pinj (j + j') Q | _ => Pinj j P end. Definition mkPinj_pred j P:= match j with | xH => P - | xO j => Pinj (Pdouble_minus_one j) P + | xO j => Pinj (Pos.pred_double j) P | xI j => Pinj (xO j) P end. @@ -156,14 +173,14 @@ Section MakeRingPol. (** Addition et subtraction *) - Fixpoint PaddC (P:Pol) (c:C) {struct P} : Pol := + Fixpoint PaddC (P:Pol) (c:C) : Pol := match P with | Pc c1 => Pc (c1 +! c) | Pinj j Q => Pinj j (PaddC Q c) | PX P i Q => PX P i (PaddC Q c) end. - Fixpoint PsubC (P:Pol) (c:C) {struct P} : Pol := + Fixpoint PsubC (P:Pol) (c:C) : Pol := match P with | Pc c1 => Pc (c1 -! c) | Pinj j Q => Pinj j (PsubC Q c) @@ -175,11 +192,11 @@ Section MakeRingPol. Variable Pop : Pol -> Pol -> Pol. Variable Q : Pol. - Fixpoint PaddI (j:positive) (P:Pol){struct P} : Pol := + Fixpoint PaddI (j:positive) (P:Pol) : Pol := match P with | Pc c => mkPinj j (PaddC Q c) | Pinj j' Q' => - match ZPminus j' j with + match Z.pos_sub j' j with | Zpos k => mkPinj j (Pop (Pinj k Q') Q) | Z0 => mkPinj j (Pop Q' Q) | Zneg k => mkPinj j' (PaddI k Q') @@ -187,16 +204,16 @@ Section MakeRingPol. | PX P i Q' => match j with | xH => PX P i (Pop Q' Q) - | xO j => PX P i (PaddI (Pdouble_minus_one j) Q') + | xO j => PX P i (PaddI (Pos.pred_double j) Q') | xI j => PX P i (PaddI (xO j) Q') end end. - Fixpoint PsubI (j:positive) (P:Pol){struct P} : Pol := + Fixpoint PsubI (j:positive) (P:Pol) : Pol := match P with | Pc c => mkPinj j (PaddC (--Q) c) | Pinj j' Q' => - match ZPminus j' j with + match Z.pos_sub j' j with | Zpos k => mkPinj j (Pop (Pinj k Q') Q) | Z0 => mkPinj j (Pop Q' Q) | Zneg k => mkPinj j' (PsubI k Q') @@ -204,41 +221,41 @@ Section MakeRingPol. | PX P i Q' => match j with | xH => PX P i (Pop Q' Q) - | xO j => PX P i (PsubI (Pdouble_minus_one j) Q') + | xO j => PX P i (PsubI (Pos.pred_double j) Q') | xI j => PX P i (PsubI (xO j) Q') end end. Variable P' : Pol. - Fixpoint PaddX (i':positive) (P:Pol) {struct P} : Pol := + Fixpoint PaddX (i':positive) (P:Pol) : Pol := match P with | Pc c => PX P' i' P | Pinj j Q' => match j with | xH => PX P' i' Q' - | xO j => PX P' i' (Pinj (Pdouble_minus_one j) Q') + | xO j => PX P' i' (Pinj (Pos.pred_double j) Q') | xI j => PX P' i' (Pinj (xO j) Q') end | PX P i Q' => - match ZPminus i i' with + match Z.pos_sub i i' with | Zpos k => mkPX (Pop (PX P k P0) P') i' Q' | Z0 => mkPX (Pop P P') i Q' | Zneg k => mkPX (PaddX k P) i Q' end end. - Fixpoint PsubX (i':positive) (P:Pol) {struct P} : Pol := + Fixpoint PsubX (i':positive) (P:Pol) : Pol := match P with | Pc c => PX (--P') i' P | Pinj j Q' => match j with | xH => PX (--P') i' Q' - | xO j => PX (--P') i' (Pinj (Pdouble_minus_one j) Q') + | xO j => PX (--P') i' (Pinj (Pos.pred_double j) Q') | xI j => PX (--P') i' (Pinj (xO j) Q') end | PX P i Q' => - match ZPminus i i' with + match Z.pos_sub i i' with | Zpos k => mkPX (Pop (PX P k P0) P') i' Q' | Z0 => mkPX (Pop P P') i Q' | Zneg k => mkPX (PsubX k P) i Q' @@ -258,18 +275,18 @@ Section MakeRingPol. | Pinj j Q => match j with | xH => PX P' i' (Padd Q Q') - | xO j => PX P' i' (Padd (Pinj (Pdouble_minus_one j) Q) Q') + | xO j => PX P' i' (Padd (Pinj (Pos.pred_double j) Q) Q') | xI j => PX P' i' (Padd (Pinj (xO j) Q) Q') end | PX P i Q => - match ZPminus i i' with + match Z.pos_sub i i' with | Zpos k => mkPX (Padd (PX P k P0) P') i' (Padd Q Q') | Z0 => mkPX (Padd P P') i (Padd Q Q') | Zneg k => mkPX (PaddX Padd P' k P) i (Padd Q Q') end end end. - Notation "P ++ P'" := (Padd P P'). + Infix "++" := Padd. Fixpoint Psub (P P': Pol) {struct P'} : Pol := match P' with @@ -281,22 +298,22 @@ Section MakeRingPol. | Pinj j Q => match j with | xH => PX (--P') i' (Psub Q Q') - | xO j => PX (--P') i' (Psub (Pinj (Pdouble_minus_one j) Q) Q') + | xO j => PX (--P') i' (Psub (Pinj (Pos.pred_double j) Q) Q') | xI j => PX (--P') i' (Psub (Pinj (xO j) Q) Q') end | PX P i Q => - match ZPminus i i' with + match Z.pos_sub i i' with | Zpos k => mkPX (Psub (PX P k P0) P') i' (Psub Q Q') | Z0 => mkPX (Psub P P') i (Psub Q Q') | Zneg k => mkPX (PsubX Psub P' k P) i (Psub Q Q') end end end. - Notation "P -- P'" := (Psub P P'). + Infix "--" := Psub. (** Multiplication *) - Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol := + Fixpoint PmulC_aux (P:Pol) (c:C) : Pol := match P with | Pc c' => Pc (c' *! c) | Pinj j Q => mkPinj j (PmulC_aux Q c) @@ -310,11 +327,11 @@ Section MakeRingPol. Section PmulI. Variable Pmul : Pol -> Pol -> Pol. Variable Q : Pol. - Fixpoint PmulI (j:positive) (P:Pol) {struct P} : Pol := + Fixpoint PmulI (j:positive) (P:Pol) : Pol := match P with | Pc c => mkPinj j (PmulC Q c) | Pinj j' Q' => - match ZPminus j' j with + match Z.pos_sub j' j with | Zpos k => mkPinj j (Pmul (Pinj k Q') Q) | Z0 => mkPinj j (Pmul Q' Q) | Zneg k => mkPinj j' (PmulI k Q') @@ -322,13 +339,12 @@ Section MakeRingPol. | PX P' i' Q' => match j with | xH => mkPX (PmulI xH P') i' (Pmul Q' Q) - | xO j' => mkPX (PmulI j P') i' (PmulI (Pdouble_minus_one j') Q') + | xO j' => mkPX (PmulI j P') i' (PmulI (Pos.pred_double j') Q') | xI j' => mkPX (PmulI j P') i' (PmulI (xO j') Q') end end. End PmulI. -(* A symmetric version of the multiplication *) Fixpoint Pmul (P P'' : Pol) {struct P''} : Pol := match P'' with @@ -341,7 +357,7 @@ Section MakeRingPol. let QQ' := match j with | xH => Pmul Q Q' - | xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q' + | xO j => Pmul (Pinj (Pos.pred_double j) Q) Q' | xI j => Pmul (Pinj (xO j) Q) Q' end in mkPX (Pmul P P') i' QQ' @@ -354,25 +370,7 @@ Section MakeRingPol. end end. -(* Non symmetric *) -(* - Fixpoint Pmul_aux (P P' : Pol) {struct P'} : Pol := - match P' with - | Pc c' => PmulC P c' - | Pinj j' Q' => PmulI Pmul_aux Q' j' P - | PX P' i' Q' => - (mkPX (Pmul_aux P P') i' P0) ++ (PmulI Pmul_aux Q' xH P) - end. - - Definition Pmul P P' := - match P with - | Pc c => PmulC P' c - | Pinj j Q => PmulI Pmul_aux Q j P' - | PX P i Q => - (mkPX (Pmul_aux P P') i P0) ++ (PmulI Pmul_aux Q xH P') - end. -*) - Notation "P ** P'" := (Pmul P P'). + Infix "**" := Pmul. Fixpoint Psquare (P:Pol) : Pol := match P with @@ -387,26 +385,26 @@ Section MakeRingPol. (** Monomial **) + (** A monomial is X1^k1...Xi^ki. Its representation + is a simplified version of the polynomial representation: + + - [mon0] correspond to the polynom [P1]. + - [(zmon j M)] corresponds to [(Pinj j ...)], + i.e. skip j variable indices. + - [(vmon i M)] is X^i*M with X the current variable, + its corresponds to (PX P1 i ...)] + *) + Inductive Mon: Set := - mon0: Mon + | mon0: Mon | zmon: positive -> Mon -> Mon | vmon: positive -> Mon -> Mon. - Fixpoint Mphi(l:list R) (M: Mon) {struct M} : R := - match M with - mon0 => rI - | zmon j M1 => Mphi (jump j l) M1 - | vmon i M1 => - let x := hd 0 l in - let xi := pow_pos rmul x i in - (Mphi (tail l) M1) * xi - end. - Definition mkZmon j M := match M with mon0 => mon0 | _ => zmon j M end. Definition zmon_pred j M := - match j with xH => M | _ => mkZmon (Ppred j) M end. + match j with xH => M | _ => mkZmon (Pos.pred j) M end. Definition mkVmon i M := match M with @@ -421,7 +419,7 @@ Section MakeRingPol. | Pinj j1 P1 => let (R,S) := CFactor P1 c in (mkPinj j1 R, mkPinj j1 S) - | PX P1 i Q1 => + | PX P1 i Q1 => let (R1, S1) := CFactor P1 c in let (R2, S2) := CFactor Q1 c in (mkPX R1 i R2, mkPX S1 i S2) @@ -429,13 +427,10 @@ Section MakeRingPol. Fixpoint MFactor (P: Pol) (c: C) (M: Mon) {struct P}: Pol * Pol := match P, M with - _, mon0 => - if (ceqb c cI) then (Pc cO, P) else -(* if (ceqb c (copp cI)) then (Pc cO, Popp P) else Not in almost ring *) - CFactor P c + _, mon0 => if (ceqb c cI) then (Pc cO, P) else CFactor P c | Pc _, _ => (P, Pc cO) | Pinj j1 P1, zmon j2 M1 => - match (j1 ?= j2) Eq with + match j1 ?= j2 with Eq => let (R,S) := MFactor P1 c M1 in (mkPinj j1 R, mkPinj j1 S) | Lt => let (R,S) := MFactor P1 c (zmon (j2 - j1) M1) in @@ -449,7 +444,7 @@ Section MakeRingPol. let (R2, S2) := MFactor Q1 c M2 in (mkPX R1 i R2, mkPX S1 i S2) | PX P1 i Q1, vmon j M1 => - match (i ?= j) Eq with + match i ?= j with Eq => let (R1,S1) := MFactor P1 c (mkZmon xH M1) in (mkPX R1 i Q1, S1) | Lt => let (R1,S1) := MFactor P1 c (vmon (j - i) M1) in @@ -468,7 +463,7 @@ Section MakeRingPol. | _ => Some (Padd Q1 (Pmul P2 R1)) end. - Fixpoint PNSubst1 (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat) {struct n}: Pol := + Fixpoint PNSubst1 (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat) : Pol := match POneSubst P1 cM1 P2 with Some P3 => match n with S n1 => PNSubst1 P3 cM1 P2 n1 | _ => P3 end | _ => P1 @@ -480,14 +475,13 @@ Section MakeRingPol. | _ => None end. - Fixpoint PSubstL1 (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: - Pol := + Fixpoint PSubstL1 (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) : Pol := match LM1 with cons (M1,P2) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n | _ => P1 end. - Fixpoint PSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: option Pol := + Fixpoint PSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) : option Pol := match LM1 with cons (M1,P2) LM2 => match PNSubst P1 M1 P2 n with @@ -497,7 +491,7 @@ Section MakeRingPol. | _ => None end. - Fixpoint PNSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (m n: nat) {struct m}: Pol := + Fixpoint PNSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (m n: nat) : Pol := match PSubstL P1 LM1 n with Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end | _ => P1 @@ -505,658 +499,409 @@ Section MakeRingPol. (** Evaluation of a polynomial towards R *) - Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R := + Local Notation hd := (List.hd 0). + + Fixpoint Pphi(l:list R) (P:Pol) : R := match P with | Pc c => [c] | Pinj j Q => Pphi (jump j l) Q - | PX P i Q => - let x := hd 0 l in - let xi := pow_pos rmul x i in - (Pphi l P) * xi + (Pphi (tail l) Q) + | PX P i Q => Pphi l P * (hd l) ^ i + Pphi (tail l) Q end. Reserved Notation "P @ l " (at level 10, no associativity). Notation "P @ l " := (Pphi l P). + + (** Evaluation of a monomial towards R *) + + Fixpoint Mphi(l:list R) (M: Mon) : R := + match M with + | mon0 => rI + | zmon j M1 => Mphi (jump j l) M1 + | vmon i M1 => Mphi (tail l) M1 * (hd l) ^ i + end. + + Notation "M @@ l" := (Mphi l M) (at level 10, no associativity). + (** Proofs *) - Lemma ZPminus_spec : forall x y, - match ZPminus x y with - | Z0 => x = y - | Zpos k => x = (y + k)%positive - | Zneg k => y = (x + k)%positive + + Ltac destr_pos_sub := + match goal with |- context [Z.pos_sub ?x ?y] => + generalize (Z.pos_sub_discr x y); destruct (Z.pos_sub x y) end. + + Lemma jump_add' i j (l:list R) : jump (i + j) l = jump j (jump i l). + Proof. rewrite Pos.add_comm. apply jump_add. Qed. + + Lemma Peq_ok P P' : (P ?== P') = true -> forall l, P@l == P'@ l. Proof. - induction x;destruct y. - replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial. - assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial. - replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y));trivial. - assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one;rewrite H;trivial. - apply Pplus_xI_double_minus_one. - simpl;trivial. - replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y));trivial. - assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one;rewrite H;trivial. - apply Pplus_xI_double_minus_one. - replace (ZPminus (xO x) (xO y)) with (Zdouble (ZPminus x y));trivial. - assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial. - replace (ZPminus (xO x) xH) with (Zpos (Pdouble_minus_one x));trivial. - rewrite <- Pplus_one_succ_l. - rewrite Psucc_o_double_minus_one_eq_xO;trivial. - replace (ZPminus xH (xI y)) with (Zneg (xO y));trivial. - replace (ZPminus xH (xO y)) with (Zneg (Pdouble_minus_one y));trivial. - rewrite <- Pplus_one_succ_l. - rewrite Psucc_o_double_minus_one_eq_xO;trivial. - simpl;trivial. + revert P';induction P;destruct P';simpl; intros H l; try easy. + - now apply (morph_eq CRmorph). + - destruct (Pos.compare_spec p p0); [ subst | easy | easy ]. + now rewrite IHP. + - specialize (IHP1 P'1); specialize (IHP2 P'2). + destruct (Pos.compare_spec p p0); [ subst | easy | easy ]. + destruct (P2 ?== P'1); [|easy]. + rewrite H in *. + now rewrite IHP1, IHP2. Qed. - Lemma Peq_ok : forall P P', - (P ?== P') = true -> forall l, P@l == P'@ l. + Lemma Peq_spec P P' : + BoolSpec (forall l, P@l == P'@l) True (P ?== P'). Proof. - induction P;destruct P';simpl;intros;try discriminate;trivial. - apply (morph_eq CRmorph);trivial. - assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq); - try discriminate H. - rewrite (IHP P' H); rewrite H1;trivial;rrefl. - assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq); - try discriminate H. - rewrite H1;trivial. clear H1. - assert (H1 := IHP1 P'1);assert (H2 := IHP2 P'2); - destruct (P2 ?== P'1);[destruct (P3 ?== P'2); [idtac|discriminate H] - |discriminate H]. - rewrite (H1 H);rewrite (H2 H);rrefl. + generalize (Peq_ok P P'). destruct (P ?== P'); auto. Qed. - Lemma Pphi0 : forall l, P0@l == 0. + Lemma Pphi0 l : P0@l == 0. Proof. - intros;simpl;apply (morph0 CRmorph). + simpl;apply (morph0 CRmorph). Qed. - Lemma Pphi1 : forall l, P1@l == 1. + Lemma Pphi1 l : P1@l == 1. Proof. - intros;simpl;apply (morph1 CRmorph). + simpl;apply (morph1 CRmorph). Qed. - Lemma mkPinj_ok : forall j l P, (mkPinj j P)@l == P@(jump j l). + Lemma mkPinj_ok j l P : (mkPinj j P)@l == P@(jump j l). Proof. - intros j l p;destruct p;simpl;rsimpl. - rewrite <-jump_Pplus;rewrite Pplus_comm;rrefl. + destruct P;simpl;rsimpl. + now rewrite jump_add'. Qed. - Let pow_pos_Pplus := - pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc). + Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j. + Proof. + rewrite Pos.add_comm. + apply (pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)). + Qed. - Lemma mkPX_ok : forall l P i Q, - (mkPX P i Q)@l == P@l*(pow_pos rmul (hd 0 l) i) + Q@(tail l). + Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c ?=! c'). Proof. - intros l P i Q;unfold mkPX. - destruct P;try (simpl;rrefl). - assert (H := morph_eq CRmorph c cO);destruct (c ?=! cO);simpl;try rrefl. - rewrite (H (refl_equal true));rewrite (morph0 CRmorph). - rewrite mkPinj_ok;rsimpl;simpl;rrefl. - assert (H := @Peq_ok P3 P0);destruct (P3 ?== P0);simpl;try rrefl. - rewrite (H (refl_equal true));trivial. - rewrite Pphi0. rewrite pow_pos_Pplus;rsimpl. + generalize (morph_eq CRmorph c c'). + destruct (c ?=! c'); auto. Qed. - Ltac Esimpl := - repeat (progress ( - match goal with - | |- context [?P@?l] => - match P with - | P0 => rewrite (Pphi0 l) - | P1 => rewrite (Pphi1 l) - | (mkPinj ?j ?P) => rewrite (mkPinj_ok j l P) - | (mkPX ?P ?i ?Q) => rewrite (mkPX_ok l P i Q) - end - | |- context [[?c]] => - match c with - | cO => rewrite (morph0 CRmorph) - | cI => rewrite (morph1 CRmorph) - | ?x +! ?y => rewrite ((morph_add CRmorph) x y) - | ?x *! ?y => rewrite ((morph_mul CRmorph) x y) - | ?x -! ?y => rewrite ((morph_sub CRmorph) x y) - | -! ?x => rewrite ((morph_opp CRmorph) x) - end - end)); - rsimpl; simpl. - - Lemma PaddC_ok : forall c P l, (PaddC P c)@l == P@l + [c]. + Lemma mkPX_ok l P i Q : + (mkPX P i Q)@l == P@l * (hd l)^i + Q@(tail l). Proof. - induction P;simpl;intros;Esimpl;trivial. - rewrite IHP2;rsimpl. + unfold mkPX. destruct P. + - case ceqb_spec; intros H; simpl; try reflexivity. + rewrite H, (morph0 CRmorph), mkPinj_ok; rsimpl. + - reflexivity. + - case Peq_spec; intros H; simpl; try reflexivity. + rewrite H, Pphi0, Pos.add_comm, pow_pos_add; rsimpl. Qed. - Lemma PsubC_ok : forall c P l, (PsubC P c)@l == P@l - [c]. + Hint Rewrite + Pphi0 + Pphi1 + mkPinj_ok + mkPX_ok + (morph0 CRmorph) + (morph1 CRmorph) + (morph0 CRmorph) + (morph_add CRmorph) + (morph_mul CRmorph) + (morph_sub CRmorph) + (morph_opp CRmorph) + : Esimpl. + + (* Quicker than autorewrite with Esimpl :-) *) + Ltac Esimpl := try rewrite_db Esimpl; rsimpl; simpl. + + Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c]. Proof. - induction P;simpl;intros. - Esimpl. - rewrite IHP;rsimpl. + revert l;induction P;simpl;intros;Esimpl;trivial. rewrite IHP2;rsimpl. Qed. - Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l == P@l * [c]. + Lemma PsubC_ok c P l : (PsubC P c)@l == P@l - [c]. Proof. - induction P;simpl;intros;Esimpl;trivial. - rewrite IHP1;rewrite IHP2;rsimpl. - mul_push ([c]);rrefl. + revert l;induction P;simpl;intros. + - Esimpl. + - rewrite IHP;rsimpl. + - rewrite IHP2;rsimpl. Qed. - Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c]. + Lemma PmulC_aux_ok c P l : (PmulC_aux P c)@l == P@l * [c]. Proof. - intros c P l; unfold PmulC. - assert (H:= morph_eq CRmorph c cO);destruct (c ?=! cO). - rewrite (H (refl_equal true));Esimpl. - assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI). - rewrite (H1 (refl_equal true));Esimpl. - apply PmulC_aux_ok. + revert l;induction P;simpl;intros;Esimpl;trivial. + rewrite IHP1, IHP2;rsimpl. add_permut. mul_permut. Qed. - Lemma Popp_ok : forall P l, (--P)@l == - P@l. + Lemma PmulC_ok c P l : (PmulC P c)@l == P@l * [c]. Proof. - induction P;simpl;intros. - Esimpl. - apply IHP. - rewrite IHP1;rewrite IHP2;rsimpl. + unfold PmulC. + case ceqb_spec; intros H. + - rewrite H; Esimpl. + - case ceqb_spec; intros H'. + + rewrite H'; Esimpl. + + apply PmulC_aux_ok. Qed. - Ltac Esimpl2 := - Esimpl; - repeat (progress ( - match goal with - | |- context [(PaddC ?P ?c)@?l] => rewrite (PaddC_ok c P l) - | |- context [(PsubC ?P ?c)@?l] => rewrite (PsubC_ok c P l) - | |- context [(PmulC ?P ?c)@?l] => rewrite (PmulC_ok c P l) - | |- context [(--?P)@?l] => rewrite (Popp_ok P l) - end)); Esimpl. - - Lemma Padd_ok : forall P' P l, (P ++ P')@l == P@l + P'@l. + Lemma Popp_ok P l : (--P)@l == - P@l. Proof. - induction P';simpl;intros;Esimpl2. - generalize P p l;clear P p l. - induction P;simpl;intros. - Esimpl2;apply (ARadd_comm ARth). - assert (H := ZPminus_spec p p0);destruct (ZPminus p p0). - rewrite H;Esimpl. rewrite IHP';rrefl. - rewrite H;Esimpl. rewrite IHP';Esimpl. - rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl. - rewrite H;Esimpl. rewrite IHP. - rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl. - destruct p0;simpl. - rewrite IHP2;simpl;rsimpl. - rewrite IHP2;simpl. - rewrite jump_Pdouble_minus_one;rsimpl. - rewrite IHP';rsimpl. - destruct P;simpl. - Esimpl2;add_push [c];rrefl. - destruct p0;simpl;Esimpl2. - rewrite IHP'2;simpl. - rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl. - rewrite IHP'2;simpl. - rewrite jump_Pdouble_minus_one;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl. - rewrite IHP'2;rsimpl. add_push (P @ (tail l));rrefl. - assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. - rewrite IHP'1;rewrite IHP'2;rsimpl. - add_push (P3 @ (tail l));rewrite H;rrefl. - rewrite IHP'1;rewrite IHP'2;simpl;Esimpl. - rewrite H;rewrite Pplus_comm. - rewrite pow_pos_Pplus;rsimpl. - add_push (P3 @ (tail l));rrefl. - assert (forall P k l, - (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow_pos rmul (hd 0 l) k). - induction P;simpl;intros;try apply (ARadd_comm ARth). - destruct p2;simpl;try apply (ARadd_comm ARth). - rewrite jump_Pdouble_minus_one;apply (ARadd_comm ARth). - assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2. - rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl. - rewrite IHP'1;simpl;Esimpl. - rewrite H1;rewrite Pplus_comm. - rewrite pow_pos_Pplus;simpl;Esimpl. - add_push (P5 @ (tail l0));rrefl. - rewrite IHP1;rewrite H1;rewrite Pplus_comm. - rewrite pow_pos_Pplus;simpl;rsimpl. - add_push (P5 @ (tail l0));rrefl. - rewrite H0;rsimpl. - add_push (P3 @ (tail l)). - rewrite H;rewrite Pplus_comm. - rewrite IHP'2;rewrite pow_pos_Pplus;rsimpl. - add_push (P3 @ (tail l));rrefl. + revert l;induction P;simpl;intros. + - Esimpl. + - apply IHP. + - rewrite IHP1, IHP2;rsimpl. Qed. - Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l. + Hint Rewrite PaddC_ok PsubC_ok PmulC_ok Popp_ok : Esimpl. + + Lemma PaddX_ok P' P k l : + (forall P l, (P++P')@l == P@l + P'@l) -> + (PaddX Padd P' k P) @ l == P@l + P'@l * (hd l)^k. Proof. - induction P';simpl;intros;Esimpl2;trivial. - generalize P p l;clear P p l. - induction P;simpl;intros. - Esimpl2;apply (ARadd_comm ARth). - assert (H := ZPminus_spec p p0);destruct (ZPminus p p0). - rewrite H;Esimpl. rewrite IHP';rsimpl. - rewrite H;Esimpl. rewrite IHP';Esimpl. - rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl. - rewrite H;Esimpl. rewrite IHP. - rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl. - destruct p0;simpl. - rewrite IHP2;simpl;rsimpl. - rewrite IHP2;simpl. - rewrite jump_Pdouble_minus_one;rsimpl. - rewrite IHP';rsimpl. - destruct P;simpl. - repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try rrefl. - destruct p0;simpl;Esimpl2. - rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));trivial. - add_push (P @ (jump p0 (jump p0 (tail l))));rrefl. - rewrite IHP'2;simpl;rewrite jump_Pdouble_minus_one;rsimpl. - add_push (- (P'1 @ l * pow_pos rmul (hd 0 l) p));rrefl. - rewrite IHP'2;rsimpl;add_push (P @ (tail l));rrefl. - assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. - rewrite IHP'1; rewrite IHP'2;rsimpl. - add_push (P3 @ (tail l));rewrite H;rrefl. - rewrite IHP'1; rewrite IHP'2;rsimpl;simpl;Esimpl. - rewrite H;rewrite Pplus_comm. - rewrite pow_pos_Pplus;rsimpl. - add_push (P3 @ (tail l));rrefl. - assert (forall P k l, - (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow_pos rmul (hd 0 l) k). - induction P;simpl;intros. - rewrite Popp_ok;rsimpl;apply (ARadd_comm ARth);trivial. - destruct p2;simpl;rewrite Popp_ok;rsimpl. - apply (ARadd_comm ARth);trivial. - rewrite jump_Pdouble_minus_one;apply (ARadd_comm ARth);trivial. - apply (ARadd_comm ARth);trivial. - assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl. - rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;rrefl. - rewrite IHP'1;rewrite H1;rewrite Pplus_comm. - rewrite pow_pos_Pplus;simpl;Esimpl. - add_push (P5 @ (tail l0));rrefl. - rewrite IHP1;rewrite H1;rewrite Pplus_comm. - rewrite pow_pos_Pplus;simpl;rsimpl. - add_push (P5 @ (tail l0));rrefl. - rewrite H0;rsimpl. - rewrite IHP'2;rsimpl;add_push (P3 @ (tail l)). - rewrite H;rewrite Pplus_comm. - rewrite pow_pos_Pplus;rsimpl. + intros IHP'. + revert k l. induction P;simpl;intros. + - add_permut. + - destruct p; simpl; + rewrite ?jump_pred_double; add_permut. + - destr_pos_sub; intros ->;Esimpl. + + rewrite IHP';rsimpl. add_permut. + + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut. + + rewrite IHP1, pow_pos_add;rsimpl. add_permut. Qed. -(* Proof for the symmetriv version *) - Lemma PmulI_ok : - forall P', - (forall (P : Pol) (l : list R), (Pmul P P') @ l == P @ l * P' @ l) -> - forall (P : Pol) (p : positive) (l : list R), - (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l). + Lemma Padd_ok P' P l : (P ++ P')@l == P@l + P'@l. Proof. - induction P;simpl;intros. - Esimpl2;apply (ARmul_comm ARth). - assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2. - rewrite H1; rewrite H;rrefl. - rewrite H1; rewrite H. - rewrite Pplus_comm. - rewrite jump_Pplus;simpl;rrefl. - rewrite H1;rewrite Pplus_comm. - rewrite jump_Pplus;rewrite IHP;rrefl. - destruct p0;Esimpl2. - rewrite IHP1;rewrite IHP2;simpl;rsimpl. - mul_push (pow_pos rmul (hd 0 l) p);rrefl. - rewrite IHP1;rewrite IHP2;simpl;rsimpl. - mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl. - rewrite IHP1;simpl;rsimpl. - mul_push (pow_pos rmul (hd 0 l) p). - rewrite H;rrefl. + revert P l; induction P';simpl;intros;Esimpl. + - revert p l; induction P;simpl;intros. + + Esimpl; add_permut. + + destr_pos_sub; intros ->;Esimpl. + * now rewrite IHP'. + * rewrite IHP';Esimpl. now rewrite jump_add'. + * rewrite IHP. now rewrite jump_add'. + + destruct p0;simpl. + * rewrite IHP2;simpl. rsimpl. + * rewrite IHP2;simpl. rewrite jump_pred_double. rsimpl. + * rewrite IHP'. rsimpl. + - destruct P;simpl. + + Esimpl. add_permut. + + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl. + * rsimpl. add_permut. + * rewrite jump_pred_double. rsimpl. add_permut. + * rsimpl. add_permut. + + destr_pos_sub; intros ->; Esimpl. + * rewrite IHP'1, IHP'2;rsimpl. add_permut. + * rewrite IHP'1, IHP'2;simpl;Esimpl. + rewrite pow_pos_add;rsimpl. add_permut. + * rewrite PaddX_ok by trivial; rsimpl. + rewrite IHP'2, pow_pos_add; rsimpl. add_permut. Qed. -(* - Lemma PmulI_ok : - forall P', - (forall (P : Pol) (l : list R), (Pmul_aux P P') @ l == P @ l * P' @ l) -> - forall (P : Pol) (p : positive) (l : list R), - (PmulI Pmul_aux P' p P) @ l == P @ l * P' @ (jump p l). + Lemma PsubX_ok P' P k l : + (forall P l, (P--P')@l == P@l - P'@l) -> + (PsubX Psub P' k P) @ l == P@l - P'@l * (hd l)^k. Proof. - induction P;simpl;intros. - Esimpl2;apply (ARmul_comm ARth). - assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2. - rewrite H1; rewrite H;rrefl. - rewrite H1; rewrite H. - rewrite Pplus_comm. - rewrite jump_Pplus;simpl;rrefl. - rewrite H1;rewrite Pplus_comm. - rewrite jump_Pplus;rewrite IHP;rrefl. - destruct p0;Esimpl2. - rewrite IHP1;rewrite IHP2;simpl;rsimpl. - mul_push (pow_pos rmul (hd 0 l) p);rrefl. - rewrite IHP1;rewrite IHP2;simpl;rsimpl. - mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl. - rewrite IHP1;simpl;rsimpl. - mul_push (pow_pos rmul (hd 0 l) p). - rewrite H;rrefl. + intros IHP'. + revert k l. induction P;simpl;intros. + - rewrite Popp_ok;rsimpl; add_permut. + - destruct p; simpl; + rewrite Popp_ok;rsimpl; + rewrite ?jump_pred_double; add_permut. + - destr_pos_sub; intros ->; Esimpl. + + rewrite IHP';rsimpl. add_permut. + + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut. + + rewrite IHP1, pow_pos_add;rsimpl. add_permut. Qed. - Lemma Pmul_aux_ok : forall P' P l,(Pmul_aux P P')@l == P@l * P'@l. + Lemma Psub_ok P' P l : (P -- P')@l == P@l - P'@l. Proof. - induction P';simpl;intros. - Esimpl2;trivial. - apply PmulI_ok;trivial. - rewrite Padd_ok;Esimpl2. - rewrite (PmulI_ok P'2 IHP'2). rewrite IHP'1. rrefl. + revert P l; induction P';simpl;intros;Esimpl. + - revert p l; induction P;simpl;intros. + + Esimpl; add_permut. + + destr_pos_sub; intros ->;Esimpl. + * rewrite IHP';rsimpl. + * rewrite IHP';Esimpl. now rewrite jump_add'. + * rewrite IHP. now rewrite jump_add'. + + destruct p0;simpl. + * rewrite IHP2;simpl. rsimpl. + * rewrite IHP2;simpl. rewrite jump_pred_double. rsimpl. + * rewrite IHP'. rsimpl. + - destruct P;simpl. + + Esimpl; add_permut. + + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl. + * rsimpl. add_permut. + * rewrite jump_pred_double. rsimpl. add_permut. + * rsimpl. add_permut. + + destr_pos_sub; intros ->; Esimpl. + * rewrite IHP'1, IHP'2;rsimpl. add_permut. + * rewrite IHP'1, IHP'2;simpl;Esimpl. + rewrite pow_pos_add;rsimpl. add_permut. + * rewrite PsubX_ok by trivial;rsimpl. + rewrite IHP'2, pow_pos_add;rsimpl. add_permut. Qed. -*) -(* Proof for the symmetric version *) - Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. + Lemma PmulI_ok P' : + (forall P l, (Pmul P P') @ l == P @ l * P' @ l) -> + forall P p l, (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l). Proof. - intros P P';generalize P;clear P;induction P';simpl;intros. - apply PmulC_ok. apply PmulI_ok;trivial. - destruct P. - rewrite (ARmul_comm ARth);Esimpl2;Esimpl2. - Esimpl2. rewrite IHP'1;Esimpl2. - assert (match p0 with - | xI j => Pinj (xO j) P ** P'2 - | xO j => Pinj (Pdouble_minus_one j) P ** P'2 - | 1 => P ** P'2 - end @ (tail l) == P @ (jump p0 l) * P'2 @ (tail l)). - destruct p0;simpl;rewrite IHP'2;Esimpl. - rewrite jump_Pdouble_minus_one;Esimpl. - rewrite H;Esimpl. - rewrite Padd_ok; Esimpl2. rewrite Padd_ok; Esimpl2. - repeat (rewrite IHP'1 || rewrite IHP'2);simpl. - rewrite PmulI_ok;trivial. - mul_push (P'1@l). simpl. mul_push (P'2 @ (tail l)). Esimpl. + intros IHP'. + induction P;simpl;intros. + - Esimpl; mul_permut. + - destr_pos_sub; intros ->;Esimpl. + + now rewrite IHP'. + + now rewrite IHP', jump_add'. + + now rewrite IHP, jump_add'. + - destruct p0;Esimpl; rewrite ?IHP1, ?IHP2; rsimpl. + + f_equiv. mul_permut. + + rewrite jump_pred_double. f_equiv. mul_permut. + + rewrite IHP'. f_equiv. mul_permut. Qed. -(* -Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. + Lemma Pmul_ok P P' l : (P**P')@l == P@l * P'@l. Proof. - destruct P;simpl;intros. - Esimpl2;apply (ARmul_comm ARth). - rewrite (PmulI_ok P (Pmul_aux_ok P)). - apply (ARmul_comm ARth). - rewrite Padd_ok; Esimpl2. - rewrite (PmulI_ok P3 (Pmul_aux_ok P3));trivial. - rewrite Pmul_aux_ok;mul_push (P' @ l). - rewrite (ARmul_comm ARth (P' @ l));rrefl. + revert P l;induction P';simpl;intros. + - apply PmulC_ok. + - apply PmulI_ok;trivial. + - destruct P. + + rewrite (ARmul_comm ARth). Esimpl. + + Esimpl. f_equiv. rewrite IHP'1; Esimpl. + destruct p0;rewrite IHP'2;Esimpl. + rewrite jump_pred_double; Esimpl. + + rewrite Padd_ok, !mkPX_ok, Padd_ok, !mkPX_ok, + !IHP'1, !IHP'2, PmulI_ok; trivial. simpl. Esimpl. + add_permut; f_equiv; mul_permut. Qed. -*) - Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l. + Lemma Psquare_ok P l : (Psquare P)@l == P@l * P@l. Proof. - induction P;simpl;intros;Esimpl2. - apply IHP. rewrite Padd_ok. rewrite Pmul_ok;Esimpl2. - rewrite IHP1;rewrite IHP2. - mul_push (pow_pos rmul (hd 0 l) p). mul_push (P2@l). - rrefl. + revert l;induction P;simpl;intros;Esimpl. + - apply IHP. + - rewrite Padd_ok, Pmul_ok;Esimpl. + rewrite IHP1, IHP2. + mul_push ((hd l)^p). now mul_push (P2@l). Qed. - - Lemma mkZmon_ok: forall M j l, - Mphi l (mkZmon j M) == Mphi l (zmon j M). - intros M j l; case M; simpl; intros; rsimpl. + Lemma mkZmon_ok M j l : + (mkZmon j M) @@ l == (zmon j M) @@ l. + Proof. + destruct M; simpl; rsimpl. Qed. - Lemma zmon_pred_ok : forall M j l, - Mphi (tail l) (zmon_pred j M) == Mphi l (zmon j M). + Lemma zmon_pred_ok M j l : + (zmon_pred j M) @@ (tail l) == (zmon j M) @@ l. Proof. - destruct j; simpl;intros auto; rsimpl. - rewrite mkZmon_ok;rsimpl. - rewrite mkZmon_ok;simpl. rewrite jump_Pdouble_minus_one; rsimpl. + destruct j; simpl; rewrite ?mkZmon_ok; simpl; rsimpl. + rewrite jump_pred_double; rsimpl. Qed. - Lemma mkVmon_ok : forall M i l, Mphi l (mkVmon i M) == Mphi l M*pow_pos rmul (hd 0 l) i. + Lemma mkVmon_ok M i l : + (mkVmon i M)@@l == M@@l * (hd l)^i. Proof. destruct M;simpl;intros;rsimpl. - rewrite zmon_pred_ok;simpl;rsimpl. - rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl. + - rewrite zmon_pred_ok;simpl;rsimpl. + - rewrite pow_pos_add;rsimpl. Qed. - Lemma Mcphi_ok: forall P c l, - let (Q,R) := CFactor P c in - P@l == Q@l + (phi c) * (R@l). + Ltac destr_factor := match goal with + | H : context [CFactor ?P _] |- context [CFactor ?P ?c] => + destruct (CFactor P c); destr_factor; rewrite H; clear H + | H : context [MFactor ?P _ _] |- context [MFactor ?P ?c ?M] => + specialize (H M); destruct (MFactor P c M); destr_factor; rewrite H; clear H + | _ => idtac + end. + + Lemma Mcphi_ok P c l : + let (Q,R) := CFactor P c in + P@l == Q@l + [c] * R@l. Proof. - intros P; elim P; simpl; auto; clear P. - intros c c1 l; generalize (div_th.(div_eucl_th) c c1); case cdiv. - intros q r H; rewrite H. - Esimpl. - rewrite (ARadd_comm ARth); rsimpl. - intros i P Hrec c l. - generalize (Hrec c (jump i l)); case CFactor. - intros R1 S1; Esimpl; auto. - intros Q1 Qrec i R1 Rrec c l. - generalize (Qrec c l); case CFactor; intros S1 S2 HS. - generalize (Rrec c (tail l)); case CFactor; intros S3 S4 HS1. - rewrite HS; rewrite HS1; Esimpl. - apply (Radd_ext Reqe); rsimpl. - repeat rewrite <- (ARadd_assoc ARth). - apply (Radd_ext Reqe); rsimpl. - rewrite (ARadd_comm ARth); rsimpl. + revert l. + induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl. + - assert (H := div_th.(div_eucl_th) c0 c). + destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. + - destr_factor. Esimpl. + - destr_factor. Esimpl. add_permut. Qed. - Lemma Mphi_ok: forall P (cM: C * Mon) l, - let (c,M) := cM in - let (Q,R) := MFactor P c M in - P@l == Q@l + (phi c) * (Mphi l M) * (R@l). + Lemma Mphi_ok P (cM: C * Mon) l : + let (c,M) := cM in + let (Q,R) := MFactor P c M in + P@l == Q@l + [c] * M@@l * R@l. Proof. - intros P; elim P; simpl; auto; clear P. - intros c (c1, M) l; case M; simpl; auto. - assert (H1:= morph_eq CRmorph c1 cI);destruct (c1 ?=! cI). - rewrite (H1 (refl_equal true));Esimpl. - try rewrite (morph0 CRmorph); rsimpl. - generalize (div_th.(div_eucl_th) c c1); case (cdiv c c1). - intros q r H; rewrite H; clear H H1. - Esimpl. - rewrite (ARadd_comm ARth); rsimpl. - intros p m; Esimpl. - intros p m; Esimpl. - intros i P Hrec (c,M) l; case M; simpl; clear M. - assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI). - rewrite (H1 (refl_equal true));Esimpl. - Esimpl. - generalize (Mcphi_ok P c (jump i l)); case CFactor. - intros R1 Q1 HH; rewrite HH; Esimpl. - intros j M. - case_eq ((i ?= j) Eq); intros He; simpl. - rewrite (Pcompare_Eq_eq _ _ He). - generalize (Hrec (c, M) (jump j l)); case (MFactor P c M); - simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto. - generalize (Hrec (c, (zmon (j -i) M)) (jump i l)); - case (MFactor P c (zmon (j -i) M)); simpl. - intros P2 Q2 H; repeat rewrite mkPinj_ok; auto. - rewrite <- (Pplus_minus _ _ (ZC2 _ _ He)). - rewrite Pplus_comm; rewrite jump_Pplus; auto. - rewrite (morph0 CRmorph); rsimpl. - intros P2 m; rewrite (morph0 CRmorph); rsimpl. - - intros P2 Hrec1 i Q2 Hrec2 (c, M) l; case M; simpl; auto. - assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI). - rewrite (H1 (refl_equal true));Esimpl. - Esimpl. - generalize (Mcphi_ok P2 c l); case CFactor. - intros S1 S2 HS. - generalize (Mcphi_ok Q2 c (tail l)); case CFactor. - intros S3 S4 HS1; Esimpl; rewrite HS; rewrite HS1. - rsimpl. - apply (Radd_ext Reqe); rsimpl. - repeat rewrite <- (ARadd_assoc ARth). - apply (Radd_ext Reqe); rsimpl. - rewrite (ARadd_comm ARth); rsimpl. - intros j M1. - generalize (Hrec1 (c,zmon j M1) l); - case (MFactor P2 c (zmon j M1)). - intros R1 S1 H1. - generalize (Hrec2 (c, zmon_pred j M1) (List.tail l)); - case (MFactor Q2 c (zmon_pred j M1)); simpl. - intros R2 S2 H2; rewrite H1; rewrite H2. - repeat rewrite mkPX_ok; simpl. - rsimpl. - apply radd_ext; rsimpl. - rewrite (ARadd_comm ARth); rsimpl. - apply radd_ext; rsimpl. - rewrite (ARadd_comm ARth); rsimpl. - rewrite zmon_pred_ok;rsimpl. - intros j M1. - case_eq ((i ?= j) Eq); intros He; simpl. - rewrite (Pcompare_Eq_eq _ _ He). - generalize (Hrec1 (c, mkZmon xH M1) l); case (MFactor P2 c (mkZmon xH M1)); - simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. - rewrite H; rewrite mkPX_ok; rsimpl. - repeat (rewrite <-(ARadd_assoc ARth)). - apply radd_ext; rsimpl. - rewrite (ARadd_comm ARth); rsimpl. - apply radd_ext; rsimpl. - repeat (rewrite <-(ARmul_assoc ARth)). - rewrite mkZmon_ok. - apply rmul_ext; rsimpl. - repeat (rewrite <-(ARmul_assoc ARth)). - apply rmul_ext; rsimpl. - rewrite (ARmul_comm ARth); rsimpl. - generalize (Hrec1 (c, vmon (j - i) M1) l); - case (MFactor P2 c (vmon (j - i) M1)); - simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. - rewrite H; rsimpl; repeat rewrite mkPinj_ok; auto. - rewrite mkPX_ok; rsimpl. - repeat (rewrite <-(ARadd_assoc ARth)). - apply radd_ext; rsimpl. - rewrite (ARadd_comm ARth); rsimpl. - apply radd_ext; rsimpl. - repeat (rewrite <-(ARmul_assoc ARth)). - apply rmul_ext; rsimpl. - rewrite (ARmul_comm ARth); rsimpl. - apply rmul_ext; rsimpl. - rewrite <- (ARmul_comm ARth (Mphi (tail l) M1)); rsimpl. - repeat (rewrite <-(ARmul_assoc ARth)). - apply rmul_ext; rsimpl. - rewrite <- pow_pos_Pplus. - rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl. - generalize (Hrec1 (c, mkZmon 1 M1) l); - case (MFactor P2 c (mkZmon 1 M1)); - simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. - rewrite H; rsimpl. - rewrite mkPX_ok; rsimpl. - repeat (rewrite <-(ARadd_assoc ARth)). - apply radd_ext; rsimpl. - rewrite (ARadd_comm ARth); rsimpl. - apply radd_ext; rsimpl. - rewrite mkZmon_ok. - repeat (rewrite <-(ARmul_assoc ARth)). - apply rmul_ext; rsimpl. - rewrite (ARmul_comm ARth); rsimpl. - rewrite mkPX_ok; simpl; rsimpl. - rewrite (morph0 CRmorph); rsimpl. - repeat (rewrite <-(ARmul_assoc ARth)). - rewrite (ARmul_comm ARth (Q3@l)); rsimpl. - apply rmul_ext; rsimpl. - rewrite (ARmul_comm ARth); rsimpl. - repeat (rewrite <- (ARmul_assoc ARth)). - apply rmul_ext; rsimpl. - rewrite <- pow_pos_Pplus. - rewrite (Pplus_minus _ _ He); rsimpl. + destruct cM as (c,M). revert M l. + induction P; destruct M; intros l; simpl; auto; + try (case ceqb_spec; intro He); + try (case Pos.compare_spec; intros He); rewrite ?He; + destr_factor; simpl; Esimpl. + - assert (H := div_th.(div_eucl_th) c0 c). + destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. + - assert (H := Mcphi_ok P c). destr_factor. Esimpl. + - now rewrite <- jump_add, Pos.sub_add. + - assert (H2 := Mcphi_ok P2 c). assert (H3 := Mcphi_ok P3 c). + destr_factor. Esimpl. add_permut. + - rewrite zmon_pred_ok. simpl. add_permut. + - rewrite mkZmon_ok. simpl. add_permut. mul_permut. + - add_permut. mul_permut. + rewrite <- pow_pos_add, Pos.add_comm, Pos.sub_add by trivial; rsimpl. + - rewrite mkZmon_ok. simpl. Esimpl. add_permut. mul_permut. + rewrite <- pow_pos_add, Pos.sub_add by trivial; rsimpl. Qed. -(* Proof for the symmetric version *) - - Lemma POneSubst_ok: forall P1 M1 P2 P3 l, - POneSubst P1 M1 P2 = Some P3 -> phi (fst M1) * Mphi l (snd M1) == P2@l -> P1@l == P3@l. + Lemma POneSubst_ok P1 cM1 P2 P3 l : + POneSubst P1 cM1 P2 = Some P3 -> + [fst cM1] * (snd cM1)@@l == P2@l -> P1@l == P3@l. Proof. - intros P2 (cc,M1) P3 P4 l; unfold POneSubst. - generalize (Mphi_ok P2 (cc, M1) l); case (MFactor P2 cc M1); simpl; auto. - intros Q1 R1; case R1. - intros c H; rewrite H. - generalize (morph_eq CRmorph c cO); - case (c ?=! cO); simpl; auto. - intros H1 H2; rewrite H1; auto; rsimpl. - discriminate. - intros _ H1 H2; injection H1; intros; subst. - rewrite H2; rsimpl. - (* new version *) - rewrite Padd_ok; rewrite PmulC_ok; rsimpl. - intros i P5 H; rewrite H. - intros HH H1; injection HH; intros; subst; rsimpl. - rewrite Padd_ok; rewrite PmulI_ok by (intros;apply Pmul_ok). rewrite H1; rsimpl. - intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3. - assert (P4 = Q1 ++ P3 ** PX i P5 P6). - injection H2; intros; subst;trivial. - rewrite H;rewrite Padd_ok;rewrite Pmul_ok;rsimpl. - Qed. -(* - Lemma POneSubst_ok: forall P1 M1 P2 P3 l, - POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l. -Proof. - intros P2 M1 P3 P4 l; unfold POneSubst. - generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto. - intros Q1 R1; case R1. - intros c H; rewrite H. - generalize (morph_eq CRmorph c cO); - case (c ?=! cO); simpl; auto. - intros H1 H2; rewrite H1; auto; rsimpl. - discriminate. - intros _ H1 H2; injection H1; intros; subst. - rewrite H2; rsimpl. - rewrite Padd_ok; rewrite Pmul_ok; rsimpl. - intros i P5 H; rewrite H. - intros HH H1; injection HH; intros; subst; rsimpl. - rewrite Padd_ok; rewrite Pmul_ok. rewrite H1; rsimpl. - intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3. - injection H2; intros; subst; rsimpl. - rewrite Padd_ok. - rewrite Pmul_ok; rsimpl. + destruct cM1 as (cc,M1). + unfold POneSubst. + assert (H := Mphi_ok P1 (cc, M1) l). simpl in H. + destruct MFactor as (R1,S1); simpl. rewrite H. clear H. + intros EQ EQ'. replace P3 with (R1 ++ P2 ** S1). + - rewrite EQ', Padd_ok, Pmul_ok; rsimpl. + - revert EQ. destruct S1; try now injection 1. + case ceqb_spec; now inversion 2. Qed. -*) - Lemma PNSubst1_ok: forall n P1 M1 P2 l, - [fst M1] * Mphi l (snd M1) == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l. + + Lemma PNSubst1_ok n P1 cM1 P2 l : + [fst cM1] * (snd cM1)@@l == P2@l -> + P1@l == (PNSubst1 P1 cM1 P2 n)@l. Proof. - intros n; elim n; simpl; auto. - intros P2 M1 P3 l H. - generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); - case (POneSubst P2 M1 P3); [idtac | intros; rsimpl]. - intros P4 Hrec; rewrite (Hrec P4); auto; rsimpl. - intros n1 Hrec P2 M1 P3 l H. - generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); - case (POneSubst P2 M1 P3); [idtac | intros; rsimpl]. - intros P4 Hrec1; rewrite (Hrec1 P4); auto; rsimpl. + revert P1. induction n; simpl; intros P1; + generalize (POneSubst_ok P1 cM1 P2); destruct POneSubst; + intros; rewrite <- ?IHn; auto; reflexivity. Qed. - Lemma PNSubst_ok: forall n P1 M1 P2 l P3, - PNSubst P1 M1 P2 n = Some P3 -> [fst M1] * Mphi l (snd M1) == P2@l -> P1@l == P3@l. + Lemma PNSubst_ok n P1 cM1 P2 l P3 : + PNSubst P1 cM1 P2 n = Some P3 -> + [fst cM1] * (snd cM1)@@l == P2@l -> P1@l == P3@l. Proof. - intros n P2 (cc, M1) P3 l P4; unfold PNSubst. - generalize (fun P4 => @POneSubst_ok P2 (cc,M1) P3 P4 l); - case (POneSubst P2 (cc,M1) P3); [idtac | intros; discriminate]. - intros P5 H1; case n; try (intros; discriminate). - intros n1 H2; injection H2; intros; subst. - rewrite <- PNSubst1_ok; auto. + unfold PNSubst. + assert (H := POneSubst_ok P1 cM1 P2); destruct POneSubst; try discriminate. + destruct n; inversion_clear 1. + intros. rewrite <- PNSubst1_ok; auto. Qed. - Fixpoint MPcond (LM1: list (C * Mon * Pol)) (l: list R) {struct LM1} : Prop := - match LM1 with - cons (M1,P2) LM2 => ([fst M1] * Mphi l (snd M1) == P2@l) /\ (MPcond LM2 l) - | _ => True - end. + Fixpoint MPcond (LM1: list (C * Mon * Pol)) (l: list R) : Prop := + match LM1 with + | (M1,P2) :: LM2 => ([fst M1] * (snd M1)@@l == P2@l) /\ MPcond LM2 l + | _ => True + end. - Lemma PSubstL1_ok: forall n LM1 P1 l, - MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l. + Lemma PSubstL1_ok n LM1 P1 l : + MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l. Proof. - intros n LM1; elim LM1; simpl; auto. - intros; rsimpl. - intros (M2,P2) LM2 Hrec P3 l [H H1]. - rewrite <- Hrec; auto. - apply PNSubst1_ok; auto. + revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros. + - reflexivity. + - rewrite <- IH by intuition. now apply PNSubst1_ok. Qed. - Lemma PSubstL_ok: forall n LM1 P1 P2 l, - PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l. + Lemma PSubstL_ok n LM1 P1 P2 l : + PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l. Proof. - intros n LM1; elim LM1; simpl; auto. - intros; discriminate. - intros (M2,P2) LM2 Hrec P3 P4 l. - generalize (PNSubst_ok n P3 M2 P2); case (PNSubst P3 M2 P2 n). - intros P5 H0 H1 [H2 H3]; injection H1; intros; subst. - rewrite <- PSubstL1_ok; auto. - intros l1 H [H1 H2]; auto. + revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. + - discriminate. + - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. + * injection H; intros <-. rewrite <- PSubstL1_ok; intuition. + * now apply IH. Qed. - Lemma PNSubstL_ok: forall m n LM1 P1 l, - MPcond LM1 l -> P1@l == (PNSubstL P1 LM1 m n)@l. + Lemma PNSubstL_ok m n LM1 P1 l : + MPcond LM1 l -> P1@l == (PNSubstL P1 LM1 m n)@l. Proof. - intros m; elim m; simpl; auto. - intros n LM1 P2 l H; generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l); - case (PSubstL P2 LM1 n); intros; rsimpl; auto. - intros m1 Hrec n LM1 P2 l H. - generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l); - case (PSubstL P2 LM1 n); intros; rsimpl; auto. - rewrite <- Hrec; auto. + revert LM1 P1. induction m; simpl; intros; + assert (H' := PSubstL_ok n LM1 P2); destruct PSubstL; + auto; try reflexivity. + rewrite <- IHm; auto. Qed. (** Definition of polynomial expressions *) @@ -1190,58 +935,22 @@ Strategy expand [PEeval]. (** Correctness proofs *) - Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l. + Lemma mkX_ok p l : nth 0 p l == (mk_X p) @ l. Proof. destruct p;simpl;intros;Esimpl;trivial. - rewrite <-jump_tl;rewrite nth_jump;rrefl. - rewrite <- nth_jump. - rewrite nth_Pdouble_minus_one;rrefl. + - now rewrite <-jump_tl, nth_jump. + - now rewrite <- nth_jump, nth_pred_double. Qed. - Ltac Esimpl3 := - repeat match goal with - | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P2 P1 l) - | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l) - end;Esimpl2;try rrefl;try apply (ARadd_comm ARth). - -(* Power using the chinise algorithm *) -(*Section POWER. - Variable subst_l : Pol -> Pol. - Fixpoint Ppow_pos (P:Pol) (p:positive){struct p} : Pol := - match p with - | xH => P - | xO p => subst_l (Psquare (Ppow_pos P p)) - | xI p => subst_l (Pmul P (Psquare (Ppow_pos P p))) - end. - - Definition Ppow_N P n := - match n with - | N0 => P1 - | Npos p => Ppow_pos P p - end. - - Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) -> - forall P p, (Ppow_pos P p)@l == (pow_pos Pmul P p)@l. - Proof. - intros l subst_l_ok P. - induction p;simpl;intros;try rrefl;try rewrite subst_l_ok. - repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl. - repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl. - Qed. - - Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) -> - forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l. - Proof. destruct n;simpl. rrefl. apply Ppow_pos_ok. trivial. Qed. - - End POWER. *) + Hint Rewrite Padd_ok Psub_ok : Esimpl. Section POWER. Variable subst_l : Pol -> Pol. - Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol := + Fixpoint Ppow_pos (res P:Pol) (p:positive) : Pol := match p with - | xH => subst_l (Pmul res P) + | xH => subst_l (res ** P) | xO p => Ppow_pos (Ppow_pos res P p) P p - | xI p => subst_l (Pmul (Ppow_pos (Ppow_pos res P p) P p) P) + | xI p => subst_l ((Ppow_pos (Ppow_pos res P p) P p) ** P) end. Definition Ppow_N P n := @@ -1250,17 +959,23 @@ Section POWER. | Npos p => Ppow_pos P1 P p end. - Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) -> - forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l. + Lemma Ppow_pos_ok l : + (forall P, subst_l P@l == P@l) -> + forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l. Proof. - intros l subst_l_ok res P p. generalize res;clear res. - induction p;simpl;intros;try rewrite subst_l_ok; repeat rewrite Pmul_ok;repeat rewrite IHp. - rsimpl. mul_push (P@l);rsimpl. rsimpl. rrefl. + intros subst_l_ok res P p. revert res. + induction p;simpl;intros; rewrite ?subst_l_ok, ?Pmul_ok, ?IHp; + mul_permut. Qed. - Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) -> - forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l. - Proof. destruct n;simpl. rrefl. rewrite Ppow_pos_ok by trivial. Esimpl. Qed. + Lemma Ppow_N_ok l : + (forall P, subst_l P@l == P@l) -> + forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l. + Proof. + destruct n;simpl. + - reflexivity. + - rewrite Ppow_pos_ok by trivial. Esimpl. + Qed. End POWER. @@ -1277,69 +992,66 @@ Section POWER. match pe with | PEc c => Pc c | PEX j => mk_X j - | PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1) - | PEadd pe1 (PEopp pe2) => - Psub (norm_aux pe1) (norm_aux pe2) - | PEadd pe1 pe2 => Padd (norm_aux pe1) (norm_aux pe2) - | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2) - | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2) - | PEopp pe1 => Popp (norm_aux pe1) + | PEadd (PEopp pe1) pe2 => (norm_aux pe2) -- (norm_aux pe1) + | PEadd pe1 (PEopp pe2) => (norm_aux pe1) -- (norm_aux pe2) + | PEadd pe1 pe2 => (norm_aux pe1) ++ (norm_aux pe2) + | PEsub pe1 pe2 => (norm_aux pe1) -- (norm_aux pe2) + | PEmul pe1 pe2 => (norm_aux pe1) ** (norm_aux pe2) + | PEopp pe1 => -- (norm_aux pe1) | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n end. Definition norm_subst pe := subst_l (norm_aux pe). - (* - Fixpoint norm_subst (pe:PExpr) : Pol := + (** Internally, [norm_aux] is expanded in a large number of cases. + To speed-up proofs, we use an alternative definition. *) + + Definition get_PEopp pe := match pe with - | PEc c => Pc c - | PEX j => subst_l (mk_X j) - | PEadd (PEopp pe1) pe2 => Psub (norm_subst pe2) (norm_subst pe1) - | PEadd pe1 (PEopp pe2) => - Psub (norm_subst pe1) (norm_subst pe2) - | PEadd pe1 pe2 => Padd (norm_subst pe1) (norm_subst pe2) - | PEsub pe1 pe2 => Psub (norm_subst pe1) (norm_subst pe2) - | PEmul pe1 pe2 => Pmul_subst (norm_subst pe1) (norm_subst pe2) - | PEopp pe1 => Popp (norm_subst pe1) - | PEpow pe1 n => Ppow_subst (norm_subst pe1) n + | PEopp pe' => Some pe' + | _ => None end. - Lemma norm_subst_spec : - forall l pe, MPcond lmp l -> - PEeval l pe == (norm_subst pe)@l. + Lemma norm_aux_PEadd pe1 pe2 : + norm_aux (PEadd pe1 pe2) = + match get_PEopp pe1, get_PEopp pe2 with + | Some pe1', _ => (norm_aux pe2) -- (norm_aux pe1') + | None, Some pe2' => (norm_aux pe1) -- (norm_aux pe2') + | None, None => (norm_aux pe1) ++ (norm_aux pe2) + end. Proof. - intros;assert (subst_l_ok:forall P, (subst_l P)@l == P@l). - unfold subst_l;intros. - rewrite <- PNSubstL_ok;trivial. rrefl. - assert (Pms_ok:forall P1 P2, (Pmul_subst P1 P2)@l == P1@l*P2@l). - intros;unfold Pmul_subst;rewrite subst_l_ok;rewrite Pmul_ok;rrefl. - induction pe;simpl;Esimpl3. - rewrite subst_l_ok;apply mkX_ok. - rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. - rewrite IHpe1;rewrite IHpe2;rrefl. - rewrite Pms_ok;rewrite IHpe1;rewrite IHpe2;rrefl. - rewrite IHpe;rrefl. - unfold Ppow_subst. rewrite Ppow_N_ok. trivial. - rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3. - induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; - repeat rewrite Pmul_ok;rrefl. + simpl (norm_aux (PEadd _ _)). + destruct pe1; [ | | | | | reflexivity | ]; + destruct pe2; simpl get_PEopp; reflexivity. Qed. -*) - Lemma norm_aux_spec : - forall l pe, MPcond lmp l -> - PEeval l pe == (norm_aux pe)@l. + + Lemma norm_aux_PEopp pe : + match get_PEopp pe with + | Some pe' => norm_aux pe = -- (norm_aux pe') + | None => True + end. + Proof. + now destruct pe. + Qed. + + Lemma norm_aux_spec l pe : + PEeval l pe == (norm_aux pe)@l. Proof. intros. - induction pe;simpl;Esimpl3. - apply mkX_ok. - rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. - rewrite IHpe1;rewrite IHpe2;rrefl. - rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl. - rewrite IHpe;rrefl. - rewrite Ppow_N_ok by (intros;rrefl). - rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3. - induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; - repeat rewrite Pmul_ok;rrefl. + induction pe. + - reflexivity. + - apply mkX_ok. + - simpl PEeval. rewrite IHpe1, IHpe2. + assert (H1 := norm_aux_PEopp pe1). + assert (H2 := norm_aux_PEopp pe2). + rewrite norm_aux_PEadd. + do 2 destruct get_PEopp; rewrite ?H1, ?H2; Esimpl; add_permut. + - simpl. rewrite IHpe1, IHpe2. Esimpl. + - simpl. rewrite IHpe1, IHpe2. now rewrite Pmul_ok. + - simpl. rewrite IHpe. Esimpl. + - simpl. rewrite Ppow_N_ok by reflexivity. + rewrite pow_th.(rpow_pow_N). destruct n0; simpl; Esimpl. + induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok. Qed. Lemma norm_subst_spec : @@ -1347,7 +1059,7 @@ Section POWER. PEeval l pe == (norm_subst pe)@l. Proof. intros;unfold norm_subst. - unfold subst_l;rewrite <- PNSubstL_ok;trivial. apply norm_aux_spec. trivial. + unfold subst_l;rewrite <- PNSubstL_ok;trivial. apply norm_aux_spec. Qed. End NORM_SUBST_REC. @@ -1514,27 +1226,27 @@ Section POWER. (rP:R) (P:Pol) (fv:list R) (n:N) (lm:list (R*positive)) {struct P} : R := match P with | Pc c => - let lm := add_pow_list (hd 0 fv) n lm in + let lm := add_pow_list (hd fv) n lm in mkadd_mult rP c lm | Pinj j Q => - add_mult_dev rP Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm) + add_mult_dev rP Q (jump j fv) N0 (add_pow_list (hd fv) n lm) | PX P i Q => - let rP := add_mult_dev rP P fv (Nplus (Npos i) n) lm in + let rP := add_mult_dev rP P fv (N.add (Npos i) n) lm in if Q ?== P0 then rP - else add_mult_dev rP Q (tail fv) N0 (add_pow_list (hd 0 fv) n lm) + else add_mult_dev rP Q (tail fv) N0 (add_pow_list (hd fv) n lm) end. Fixpoint mult_dev (P:Pol) (fv : list R) (n:N) (lm:list (R*positive)) {struct P} : R := (* P@l * (hd 0 l)^n * lm *) match P with - | Pc c => mkmult_c c (add_pow_list (hd 0 fv) n lm) - | Pinj j Q => mult_dev Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm) + | Pc c => mkmult_c c (add_pow_list (hd fv) n lm) + | Pinj j Q => mult_dev Q (jump j fv) N0 (add_pow_list (hd fv) n lm) | PX P i Q => - let rP := mult_dev P fv (Nplus (Npos i) n) lm in + let rP := mult_dev P fv (N.add (Npos i) n) lm in if Q ?== P0 then rP else - let lmq := add_pow_list (hd 0 fv) n lm in + let lmq := add_pow_list (hd fv) n lm in add_mult_dev rP Q (tail fv) N0 lmq end. @@ -1575,7 +1287,7 @@ Section POWER. (forall l lr : list (R * positive), r_list_pow (rev_append l lr) == r_list_pow lr * r_list_pow l). induction l;intros;simpl;Esimpl. destruct a;rewrite IHl;Esimpl. - rewrite (ARmul_comm ARth (pow_pos rmul r p)). rrefl. + rewrite (ARmul_comm ARth (pow_pos rmul r p)). reflexivity. intros;unfold rev'. rewrite H;simpl;Esimpl. Qed. @@ -1617,11 +1329,11 @@ Qed. Qed. Lemma add_mult_dev_ok : forall P rP fv n lm, - add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (hd 0 fv) n * r_list_pow lm. + add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (hd fv) n * r_list_pow lm. Proof. induction P;simpl;intros. - rewrite mkadd_mult_ok. rewrite add_pow_list_ok; Esimpl. - rewrite IHP. simpl. rewrite add_pow_list_ok; Esimpl. + rewrite mkadd_mult_ok. rewrite add_pow_list_ok; Esimpl. + rewrite IHP. simpl. rewrite add_pow_list_ok; Esimpl. change (match P3 with | Pc c => c ?=! cO | Pinj _ _ => false @@ -1630,17 +1342,19 @@ Qed. change match n with | N0 => Npos p | Npos q => Npos (p + q) - end with (Nplus (Npos p) n);trivial. + end with (N.add (Npos p) n);trivial. assert (H := Peq_ok P3 P0). destruct (P3 ?== P0). - rewrite (H (refl_equal true)). - rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. - rewrite IHP2. - rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. + rewrite (H eq_refl). + rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl. + add_permut. mul_permut. + rewrite IHP2. + rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl. + add_permut. mul_permut. Qed. Lemma mult_dev_ok : forall P fv n lm, - mult_dev P fv n lm == P@fv * pow_N rI rmul (hd 0 fv) n * r_list_pow lm. + mult_dev P fv n lm == P@fv * pow_N rI rmul (hd fv) n * r_list_pow lm. Proof. induction P;simpl;intros;Esimpl. rewrite mkmult_c_ok;rewrite add_pow_list_ok;Esimpl. @@ -1653,13 +1367,15 @@ Qed. change match n with | N0 => Npos p | Npos q => Npos (p + q) - end with (Nplus (Npos p) n);trivial. + end with (N.add (Npos p) n);trivial. assert (H := Peq_ok P3 P0). destruct (P3 ?== P0). - rewrite (H (refl_equal true)). - rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. + rewrite (H eq_refl). + rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl. + mul_permut. rewrite add_mult_dev_ok. rewrite IHP1; rewrite add_pow_list_ok. - destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. + destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl. + add_permut; mul_permut. Qed. Lemma Pphi_avoid_ok : forall P fv, Pphi_avoid fv P == P@fv. @@ -1676,18 +1392,18 @@ Qed. let mkmult_pow r x p := rmul r (mkpow x p) in Pphi_avoid mkpow mkopp_pow mkmult_pow. - Lemma local_mkpow_ok : - forall (r : R) (p : positive), + Lemma local_mkpow_ok r p : match p with | xI _ => rpow r (Cp_phi (Npos p)) | xO _ => rpow r (Cp_phi (Npos p)) | 1 => r end == pow_pos rmul r p. - Proof. intros r p;destruct p;try rewrite pow_th.(rpow_pow_N);reflexivity. Qed. + Proof. destruct p; now rewrite ?pow_th.(rpow_pow_N). Qed. Lemma Pphi_pow_ok : forall P fv, Pphi_pow fv P == P@fv. Proof. - unfold Pphi_pow;intros;apply Pphi_avoid_ok;intros;try rewrite local_mkpow_ok;rrefl. + unfold Pphi_pow;intros;apply Pphi_avoid_ok;intros; + now rewrite ?local_mkpow_ok. Qed. Lemma ring_rw_pow_correct : forall n lH l, @@ -1697,7 +1413,7 @@ Qed. PEeval l pe == Pphi_pow l npe. Proof. intros n lH l H1 lmp Heq1 pe npe Heq2. - rewrite Pphi_pow_ok. rewrite <- Heq2;rewrite <- Heq1. + rewrite Pphi_pow_ok, <- Heq2, <- Heq1. apply norm_subst_ok. trivial. Qed. @@ -1711,58 +1427,48 @@ Qed. Definition mkpow x p := match p with | xH => x - | xO p => mkmult_pow x x (Pdouble_minus_one p) + | xO p => mkmult_pow x x (Pos.pred_double p) | xI p => mkmult_pow x x (xO p) end. Definition mkopp_pow x p := match p with | xH => -x - | xO p => mkmult_pow (-x) x (Pdouble_minus_one p) + | xO p => mkmult_pow (-x) x (Pos.pred_double p) | xI p => mkmult_pow (-x) x (xO p) end. Definition Pphi_dev := Pphi_avoid mkpow mkopp_pow mkmult_pow. - Lemma mkmult_pow_ok : forall p r x, mkmult_pow r x p == r*pow_pos rmul x p. + Lemma mkmult_pow_ok p r x : mkmult_pow r x p == r * x^p. Proof. - induction p;intros;simpl;Esimpl. - repeat rewrite IHp;Esimpl. - repeat rewrite IHp;Esimpl. + revert r; induction p;intros;simpl;Esimpl;rewrite !IHp;Esimpl. Qed. - Lemma mkpow_ok : forall p x, mkpow x p == pow_pos rmul x p. + Lemma mkpow_ok p x : mkpow x p == x^p. Proof. destruct p;simpl;intros;Esimpl. - repeat rewrite mkmult_pow_ok;Esimpl. - rewrite mkmult_pow_ok;Esimpl. - pattern x at 1;replace x with (pow_pos rmul x 1). - rewrite <- pow_pos_Pplus. - rewrite <- Pplus_one_succ_l. - rewrite Psucc_o_double_minus_one_eq_xO. - simpl;Esimpl. - trivial. + - rewrite !mkmult_pow_ok;Esimpl. + - rewrite mkmult_pow_ok;Esimpl. + change x with (x^1) at 1. + now rewrite <- pow_pos_add, Pos.add_1_r, Pos.succ_pred_double. Qed. - Lemma mkopp_pow_ok : forall p x, mkopp_pow x p == - pow_pos rmul x p. + Lemma mkopp_pow_ok p x : mkopp_pow x p == - x^p. Proof. destruct p;simpl;intros;Esimpl. - repeat rewrite mkmult_pow_ok;Esimpl. - rewrite mkmult_pow_ok;Esimpl. - pattern x at 1;replace x with (pow_pos rmul x 1). - rewrite <- pow_pos_Pplus. - rewrite <- Pplus_one_succ_l. - rewrite Psucc_o_double_minus_one_eq_xO. - simpl;Esimpl. - trivial. + - rewrite !mkmult_pow_ok;Esimpl. + - rewrite mkmult_pow_ok;Esimpl. + change x with (x^1) at 1. + now rewrite <- pow_pos_add, Pos.add_1_r, Pos.succ_pred_double. Qed. Lemma Pphi_dev_ok : forall P fv, Pphi_dev fv P == P@fv. Proof. unfold Pphi_dev;intros;apply Pphi_avoid_ok. - intros;apply mkpow_ok. - intros;apply mkopp_pow_ok. - intros;apply mkmult_pow_ok. + - intros;apply mkpow_ok. + - intros;apply mkopp_pow_ok. + - intros;apply mkmult_pow_ok. Qed. Lemma ring_rw_correct : forall n lH l, @@ -1776,6 +1482,4 @@ Qed. apply norm_subst_ok. trivial. Qed. - End MakeRingPol. - diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index d33e9a82..7a7ffcfd 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -3,6 +3,7 @@ Require Import Setoid. Require Import BinPos. Require Import Ring_polynom. Require Import BinList. +Require Export ListTactics. Require Import InitialRing. Require Import Quote. Declare ML Module "newring_plugin". @@ -14,7 +15,7 @@ Ltac compute_assertion eqn t' t := let nft := eval vm_compute in t in pose (t' := nft); assert (eqn : t = t'); - [vm_cast_no_check (refl_equal t')|idtac]. + [vm_cast_no_check (eq_refl t')|idtac]. Ltac relation_carrier req := let ty := type of req in @@ -340,7 +341,7 @@ Ltac Ring RNG lemma lH := || idtac "can not automatically proof hypothesis :"; idtac " maybe a left member of a hypothesis is not a monomial") | vm_compute; - (exact (refl_equal true) || fail "not a valid ring equation")]). + (exact (eq_refl true) || fail "not a valid ring equation")]). Ltac Ring_norm_gen f RNG lemma lH rl := let mkFV := get_RingFV RNG in @@ -385,7 +386,7 @@ Ltac Ring_simplify_gen f RNG lH rl := let lemma := get_SimplifyLemma RNG in let l := fresh "to_rewrite" in pose (l:= rl); - generalize (refl_equal l); + generalize (eq_refl l); unfold l at 2; get_Pre RNG (); let rl := diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 4fbdcbaa..42ce4edc 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -1,14 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Setoid. -Require Import BinPos. -Require Import BinNat. +Require Import Setoid Morphisms BinPos BinNat. Set Implicit Arguments. @@ -35,48 +33,42 @@ Section Power. Variable rI : R. Variable rmul : R -> R -> R. Variable req : R -> R -> Prop. - Variable Rsth : Setoid_Theory R req. - Notation "x * y " := (rmul x y). - Notation "x == y" := (req x y). + Variable Rsth : Equivalence req. + Infix "*" := rmul. + Infix "==" := req. - Hypothesis mul_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2. - Hypothesis mul_comm : forall x y, x * y == y * x. + Hypothesis mul_ext : Proper (req ==> req ==> req) rmul. Hypothesis mul_assoc : forall x y z, x * (y * z) == (x * y) * z. - Add Setoid R req Rsth as R_set_Power. - Add Morphism rmul : rmul_ext_Power. exact mul_ext. Qed. - - Fixpoint pow_pos (x:R) (i:positive) {struct i}: R := + Fixpoint pow_pos (x:R) (i:positive) : R := match i with | xH => x - | xO i => let p := pow_pos x i in rmul p p - | xI i => let p := pow_pos x i in rmul x (rmul p p) + | xO i => let p := pow_pos x i in p * p + | xI i => let p := pow_pos x i in x * (p * p) end. - Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j. + Lemma pow_pos_swap x j : pow_pos x j * x == x * pow_pos x j. + Proof. + induction j; simpl; rewrite <- ?mul_assoc. + - f_equiv. now do 2 (rewrite IHj, mul_assoc). + - now do 2 (rewrite IHj, mul_assoc). + - reflexivity. + Qed. + + Lemma pow_pos_succ x j : + pow_pos x (Pos.succ j) == x * pow_pos x j. Proof. - induction j;simpl. - rewrite IHj. - rewrite (mul_comm x (pow_pos x j *pow_pos x j)). - setoid_rewrite (mul_comm x (pow_pos x j)) at 2. - repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). - repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). - apply (Seq_refl _ _ Rsth). + induction j; simpl; try reflexivity. + rewrite IHj, <- mul_assoc; f_equiv. + now rewrite mul_assoc, pow_pos_swap, mul_assoc. Qed. - Lemma pow_pos_Pplus : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j. + Lemma pow_pos_add x i j : + pow_pos x (i + j) == pow_pos x i * pow_pos x j. Proof. - intro x;induction i;intros. - rewrite xI_succ_xO;rewrite Pplus_one_succ_r. - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat rewrite IHi. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc. - simpl;repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat rewrite IHi;rewrite mul_assoc. apply (Seq_refl _ _ Rsth). - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc; - simpl. apply (Seq_refl _ _ Rsth). + induction i using Pos.peano_ind. + - now rewrite Pos.add_1_l, pow_pos_succ. + - now rewrite Pos.add_succ_l, !pow_pos_succ, IHi, mul_assoc. Qed. Definition pow_N (x:R) (p:N) := @@ -87,9 +79,9 @@ Section Power. Definition id_phi_N (x:N) : N := x. - Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n. + Lemma pow_N_pow_N x n : pow_N x (id_phi_N n) == pow_N x n. Proof. - intros; apply (Seq_refl _ _ Rsth). + reflexivity. Qed. End Power. @@ -98,19 +90,18 @@ Section DEFINITIONS. 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). + Notation "0" := rO. Notation "1" := rI. + Infix "==" := req. Infix "+" := radd. Infix "*" := rmul. + Infix "-" := rsub. Notation "- x" := (ropp x). (** Semi Ring *) Record semi_ring_theory : Prop := mk_srt { SRadd_0_l : forall n, 0 + n == n; - SRadd_comm : forall n m, n + m == m + n ; + SRadd_comm : forall n m, n + m == m + n ; SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; SRmul_1_l : forall n, 1*n == n; SRmul_0_l : forall n, 0*n == 0; - SRmul_comm : forall n m, n*m == m*n; + SRmul_comm : forall n m, n*m == m*n; SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; SRdistr_l : forall n m p, (n + m)*p == n*p + m*p }. @@ -119,11 +110,11 @@ Section DEFINITIONS. (*Almost ring are no ring : Ropp_def is missing **) Record almost_ring_theory : Prop := mk_art { ARadd_0_l : forall x, 0 + x == x; - ARadd_comm : forall x y, x + y == y + x; + ARadd_comm : forall x y, x + y == y + x; ARadd_assoc : forall x y z, x + (y + z) == (x + y) + z; ARmul_1_l : forall x, 1 * x == x; ARmul_0_l : forall x, 0 * x == 0; - ARmul_comm : forall x y, x * y == y * x; + ARmul_comm : forall x y, x * y == y * x; ARmul_assoc : forall x y z, x * (y * z) == (x * y) * z; ARdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); ARopp_mul_l : forall x y, -(x * y) == -x * y; @@ -134,10 +125,10 @@ Section DEFINITIONS. (** Ring *) Record ring_theory : Prop := mk_rt { Radd_0_l : forall x, 0 + x == x; - Radd_comm : forall x y, x + y == y + x; + Radd_comm : forall x y, x + y == y + x; Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; Rmul_1_l : forall x, 1 * x == x; - Rmul_comm : forall x y, x * y == y * x; + Rmul_comm : forall x y, x * y == y * x; Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); Rsub_def : forall x y, x - y == x + -y; @@ -148,19 +139,15 @@ Section DEFINITIONS. Record sring_eq_ext : Prop := mk_seqe { (* SRing operators are compatible with equality *) - SRadd_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2; - SRmul_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2 + SRadd_ext : Proper (req ==> req ==> req) radd; + SRmul_ext : Proper (req ==> req ==> req) rmul }. Record ring_eq_ext : Prop := mk_reqe { (* Ring operators are compatible with equality *) - Radd_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2; - Rmul_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2; - Ropp_ext : forall x1 x2, x1 == x2 -> -x1 == -x2 + Radd_ext : Proper (req ==> req ==> req) radd; + Rmul_ext : Proper (req ==> req ==> req) rmul; + Ropp_ext : Proper (req ==> req) ropp }. (** Interpretation morphisms definition*) @@ -170,9 +157,9 @@ Section DEFINITIONS. Variable ceqb : C->C->bool. (* [phi] est un morphisme de [C] dans [R] *) Variable phi : C -> R. - Notation "x +! y" := (cadd x y). Notation "x -! y " := (csub x y). - Notation "x *! y " := (cmul x y). Notation "-! x" := (copp x). - Notation "x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x). + Infix "+!" := cadd. Infix "-!" := csub. + Infix "*!" := cmul. Notation "-! x" := (copp x). + Infix "?=!" := ceqb. Notation "[ x ]" := (phi x). (*for semi rings*) Record semi_morph : Prop := mkRmorph { @@ -216,20 +203,18 @@ Section DEFINITIONS. End MORPHISM. (** Identity is a morphism *) - Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid1. + Variable Rsth : Equivalence req. Variable reqb : R->R->bool. Hypothesis morph_req : forall x y, (reqb x y) = true -> x == y. Definition IDphi (x:R) := x. Lemma IDmorph : ring_morph rO rI radd rmul rsub ropp reqb IDphi. Proof. - apply (mkmorph rO rI radd rmul rsub ropp reqb IDphi);intros;unfold IDphi; - try apply (Seq_refl _ _ Rsth);auto. + now apply (mkmorph rO rI radd rmul rsub ropp reqb IDphi). Qed. (** Specification of the power function *) Section POWER. - Variable Cpow : Set. + Variable Cpow : Type. Variable Cp_phi : N -> Cpow. Variable rpow : R -> Cpow -> R. @@ -239,35 +224,31 @@ Section DEFINITIONS. End POWER. - Definition pow_N_th := mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth). + Definition pow_N_th := + mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth). End DEFINITIONS. - - Section ALMOST_RING. 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). + Notation "0" := rO. Notation "1" := rI. + Infix "==" := req. Infix "+" := radd. Infix "* " := rmul. + Infix "-" := rsub. Notation "- x" := (ropp x). (** Leibniz equality leads to a setoid theory and is extensional*) - Lemma Eqsth : Setoid_Theory R (@eq R). - Proof. constructor;red;intros;subst;trivial. Qed. + Lemma Eqsth : Equivalence (@eq R). + Proof. exact eq_equivalence. Qed. Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R). - Proof. constructor;intros;subst;trivial. Qed. + Proof. constructor;solve_proper. Qed. Lemma Eq_ext : ring_eq_ext radd rmul ropp (@eq R). - Proof. constructor;intros;subst;trivial. Qed. + Proof. constructor;solve_proper. Qed. - Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid2. - Ltac sreflexivity := apply (Seq_refl _ _ Rsth). + Variable Rsth : Equivalence req. Section SEMI_RING. Variable SReqe : sring_eq_ext radd rmul req. @@ -282,23 +263,24 @@ Section ALMOST_RING. Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y). Lemma SRopp_ext : forall x y, x == y -> -x == -y. - Proof. intros x y H;exact H. Qed. + Proof. intros x y H; exact H. Qed. Lemma SReqe_Reqe : ring_eq_ext radd rmul SRopp req. Proof. - constructor. exact (SRadd_ext SReqe). exact (SRmul_ext SReqe). - exact SRopp_ext. + constructor. + - exact (SRadd_ext SReqe). + - exact (SRmul_ext SReqe). + - exact SRopp_ext. Qed. Lemma SRopp_mul_l : forall x y, -(x * y) == -x * y. - Proof. intros;sreflexivity. Qed. + Proof. reflexivity. Qed. Lemma SRopp_add : forall x y, -(x + y) == -x + -y. - Proof. intros;sreflexivity. Qed. - + Proof. reflexivity. Qed. Lemma SRsub_def : forall x y, x - y == x + -y. - Proof. intros;sreflexivity. Qed. + Proof. reflexivity. Qed. Lemma SRth_ARth : almost_ring_theory 0 1 radd rmul SRsub SRopp req. Proof (mk_art 0 1 radd rmul SRsub SRopp req @@ -315,7 +297,7 @@ Section ALMOST_RING. Definition SRIDmorph : ring_morph 0 1 radd rmul SRsub SRopp req 0 1 radd rmul SRsub SRopp reqb (@IDphi R). Proof. - apply mkmorph;intros;try sreflexivity. unfold IDphi;auto. + now apply mkmorph. Qed. (* a semi_morph can be extended to a ring_morph for the almost_ring derived @@ -331,9 +313,7 @@ Section ALMOST_RING. ring_morph rO rI radd rmul SRsub SRopp req cO cI cadd cmul cadd (fun x => x) ceqb phi. Proof. - case Smorph; intros; constructor; auto. - unfold SRopp in |- *; intros. - setoid_reflexivity. + case Smorph; now constructor. Qed. End SEMI_RING. @@ -347,31 +327,28 @@ Section ALMOST_RING. Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. (** Rings are almost rings*) - Lemma Rmul_0_l : forall x, 0 * x == 0. + Lemma Rmul_0_l x : 0 * x == 0. Proof. - intro x; setoid_replace (0*x) with ((0+1)*x + -x). - rewrite (Radd_0_l Rth); rewrite (Rmul_1_l Rth). - rewrite (Ropp_def Rth);sreflexivity. + setoid_replace (0*x) with ((0+1)*x + -x). + now rewrite (Radd_0_l Rth), (Rmul_1_l Rth), (Ropp_def Rth). - rewrite (Rdistr_l Rth);rewrite (Rmul_1_l Rth). - rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). - rewrite (Radd_comm Rth); rewrite (Radd_0_l Rth);sreflexivity. + rewrite (Rdistr_l Rth), (Rmul_1_l Rth). + rewrite <- (Radd_assoc Rth), (Ropp_def Rth). + now rewrite (Radd_comm Rth), (Radd_0_l Rth). Qed. - Lemma Ropp_mul_l : forall x y, -(x * y) == -x * y. + Lemma Ropp_mul_l x y : -(x * y) == -x * y. Proof. - intros x y;rewrite <-(Radd_0_l Rth (- x * y)). - rewrite (Radd_comm Rth). - rewrite <-(Ropp_def Rth (x*y)). - rewrite (Radd_assoc Rth). - rewrite <- (Rdistr_l Rth). - rewrite (Rth.(Radd_comm) (-x));rewrite (Ropp_def Rth). - rewrite Rmul_0_l;rewrite (Radd_0_l Rth);sreflexivity. + rewrite <-(Radd_0_l Rth (- x * y)). + rewrite (Radd_comm Rth), <-(Ropp_def Rth (x*y)). + rewrite (Radd_assoc Rth), <- (Rdistr_l Rth). + rewrite (Rth.(Radd_comm) (-x)), (Ropp_def Rth). + now rewrite Rmul_0_l, (Radd_0_l Rth). Qed. - Lemma Ropp_add : forall x y, -(x + y) == -x + -y. + Lemma Ropp_add x y : -(x + y) == -x + -y. Proof. - intros x y;rewrite <- ((Radd_0_l Rth) (-(x+y))). + rewrite <- ((Radd_0_l Rth) (-(x+y))). rewrite <- ((Ropp_def Rth) x). rewrite <- ((Radd_0_l Rth) (x + - x + - (x + y))). rewrite <- ((Ropp_def Rth) y). @@ -383,17 +360,17 @@ Section ALMOST_RING. rewrite ((Radd_comm Rth) y). rewrite <- ((Radd_assoc Rth) (- x)). rewrite ((Radd_assoc Rth) y). - rewrite ((Radd_comm Rth) y);rewrite (Ropp_def Rth). - rewrite ((Radd_comm Rth) (-x) 0);rewrite (Radd_0_l Rth). - apply (Radd_comm Rth). + rewrite ((Radd_comm Rth) y), (Ropp_def Rth). + rewrite ((Radd_comm Rth) (-x) 0), (Radd_0_l Rth). + now apply (Radd_comm Rth). Qed. - Lemma Ropp_opp : forall x, - -x == x. + Lemma Ropp_opp x : - -x == x. Proof. - intros x; rewrite <- (Radd_0_l Rth (- -x)). + rewrite <- (Radd_0_l Rth (- -x)). rewrite <- (Ropp_def Rth x). - rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). - rewrite ((Radd_comm Rth) x);apply (Radd_0_l Rth). + rewrite <- (Radd_assoc Rth), (Ropp_def Rth). + rewrite ((Radd_comm Rth) x); now apply (Radd_0_l Rth). Qed. Lemma Rth_ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. @@ -407,10 +384,10 @@ Section ALMOST_RING. Variable (cO cI : C) (cadd cmul csub: C->C->C) (copp : C -> C). Variable (ceq : C -> C -> Prop) (ceqb : C -> C -> bool). Variable phi : C -> R. - Notation "x +! y" := (cadd x y). Notation "x *! y " := (cmul x y). - Notation "x -! y " := (csub x y). Notation "-! x" := (copp x). - Notation "x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x). - Variable Csth : Setoid_Theory C ceq. + Infix "+!" := cadd. Infix "*!" := cmul. + Infix "-!" := csub. Notation "-! x" := (copp x). + Notation "?=!" := ceqb. Notation "[ x ]" := (phi x). + Variable Csth : Equivalence ceq. Variable Ceqe : ring_eq_ext cadd cmul copp ceq. Add Setoid C ceq Csth as C_setoid. Add Morphism cadd : cadd_ext. exact (Radd_ext Ceqe). Qed. @@ -420,9 +397,9 @@ Section ALMOST_RING. Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi. Variable phi_ext : forall x y, ceq x y -> [x] == [y]. Add Morphism phi : phi_ext1. exact phi_ext. Qed. - Lemma Smorph_opp : forall x, [-!x] == -[x]. + Lemma Smorph_opp x : [-!x] == -[x]. Proof. - intros x;rewrite <- (Rth.(Radd_0_l) [-!x]). + rewrite <- (Rth.(Radd_0_l) [-!x]). rewrite <- ((Ropp_def Rth) [x]). rewrite ((Radd_comm Rth) [x]). rewrite <- (Radd_assoc Rth). @@ -430,17 +407,18 @@ Section ALMOST_RING. rewrite (Ropp_def Cth). rewrite (Smorph0 Smorph). rewrite (Radd_comm Rth (-[x])). - apply (Radd_0_l Rth);sreflexivity. + now apply (Radd_0_l Rth). Qed. - Lemma Smorph_sub : forall x y, [x -! y] == [x] - [y]. + Lemma Smorph_sub x y : [x -! y] == [x] - [y]. Proof. - intros x y; rewrite (Rsub_def Cth);rewrite (Rsub_def Rth). - rewrite (Smorph_add Smorph);rewrite Smorph_opp;sreflexivity. + rewrite (Rsub_def Cth), (Rsub_def Rth). + now rewrite (Smorph_add Smorph), Smorph_opp. Qed. - Lemma Smorph_morph : ring_morph 0 1 radd rmul rsub ropp req - cO cI cadd cmul csub copp ceqb phi. + Lemma Smorph_morph : + ring_morph 0 1 radd rmul rsub ropp req + cO cI cadd cmul csub copp ceqb phi. Proof (mkmorph 0 1 radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi (Smorph0 Smorph) (Smorph1 Smorph) @@ -458,17 +436,11 @@ elim ARth; intros. constructor; trivial. Qed. - Lemma ARsub_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2. + Instance ARsub_ext : Proper (req ==> req ==> req) rsub. Proof. - intros. - setoid_replace (x1 - y1) with (x1 + -y1). - setoid_replace (x2 - y2) with (x2 + -y2). - rewrite H;rewrite H0;sreflexivity. - apply (ARsub_def ARth). - apply (ARsub_def ARth). + intros x1 x2 Ex y1 y2 Ey. + now rewrite !(ARsub_def ARth), Ex, Ey. Qed. - Add Morphism rsub : rsub_ext. exact ARsub_ext. Qed. Ltac mrewrite := repeat first @@ -479,64 +451,56 @@ Qed. | rewrite (ARmul_0_l ARth) | rewrite <- ((ARmul_comm ARth) 0) | rewrite (ARdistr_l ARth) - | sreflexivity + | reflexivity | match goal with | |- context [?z * (?x + ?y)] => rewrite ((ARmul_comm ARth) z (x+y)) end]. - Lemma ARadd_0_r : forall x, (x + 0) == x. - Proof. intros; mrewrite. Qed. + Lemma ARadd_0_r x : x + 0 == x. + Proof. mrewrite. Qed. - Lemma ARmul_1_r : forall x, x * 1 == x. - Proof. intros;mrewrite. Qed. + Lemma ARmul_1_r x : x * 1 == x. + Proof. mrewrite. Qed. - Lemma ARmul_0_r : forall x, x * 0 == 0. - Proof. intros;mrewrite. Qed. + Lemma ARmul_0_r x : x * 0 == 0. + Proof. mrewrite. Qed. - Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y. + Lemma ARdistr_r x y z : z * (x + y) == z*x + z*y. Proof. - intros;mrewrite. - repeat rewrite (ARth.(ARmul_comm) z);sreflexivity. + mrewrite. now rewrite !(ARth.(ARmul_comm) z). Qed. - Lemma ARadd_assoc1 : forall x y z, (x + y) + z == (y + z) + x. + Lemma ARadd_assoc1 x y z : (x + y) + z == (y + z) + x. Proof. - intros;rewrite <-(ARth.(ARadd_assoc) x). - rewrite (ARth.(ARadd_comm) x);sreflexivity. + now rewrite <-(ARth.(ARadd_assoc) x), (ARth.(ARadd_comm) x). Qed. - Lemma ARadd_assoc2 : forall x y z, (y + x) + z == (y + z) + x. + Lemma ARadd_assoc2 x y z : (y + x) + z == (y + z) + x. Proof. - intros; repeat rewrite <- (ARadd_assoc ARth); - rewrite ((ARadd_comm ARth) x); sreflexivity. + now rewrite <- !(ARadd_assoc ARth), ((ARadd_comm ARth) x). Qed. - Lemma ARmul_assoc1 : forall x y z, (x * y) * z == (y * z) * x. + Lemma ARmul_assoc1 x y z : (x * y) * z == (y * z) * x. Proof. - intros;rewrite <-((ARmul_assoc ARth) x). - rewrite ((ARmul_comm ARth) x);sreflexivity. + now rewrite <- ((ARmul_assoc ARth) x), ((ARmul_comm ARth) x). Qed. - Lemma ARmul_assoc2 : forall x y z, (y * x) * z == (y * z) * x. + Lemma ARmul_assoc2 x y z : (y * x) * z == (y * z) * x. Proof. - intros; repeat rewrite <- (ARmul_assoc ARth); - rewrite ((ARmul_comm ARth) x); sreflexivity. + now rewrite <- !(ARmul_assoc ARth), ((ARmul_comm ARth) x). Qed. - Lemma ARopp_mul_r : forall x y, - (x * y) == x * -y. + Lemma ARopp_mul_r x y : - (x * y) == x * -y. Proof. - intros;rewrite ((ARmul_comm ARth) x y); - rewrite (ARopp_mul_l ARth); apply (ARmul_comm ARth). + rewrite ((ARmul_comm ARth) x y), (ARopp_mul_l ARth). + now apply (ARmul_comm ARth). Qed. Lemma ARopp_zero : -0 == 0. Proof. - rewrite <- (ARmul_0_r 0); rewrite (ARopp_mul_l ARth). - repeat rewrite ARmul_0_r; sreflexivity. + now rewrite <- (ARmul_0_r 0), (ARopp_mul_l ARth), !ARmul_0_r. Qed. - - End ALMOST_RING. @@ -590,12 +554,29 @@ Ltac gen_srewrite Rsth Reqe ARth := | progress rewrite <- (ARopp_mul_l ARth) | progress rewrite <- (ARopp_mul_r Rsth Reqe ARth) ]. +Ltac gen_srewrite_sr Rsth Reqe ARth := + repeat first + [ gen_reflexivity Rsth + | progress rewrite (ARopp_zero Rsth Reqe ARth) + | rewrite (ARadd_0_l ARth) + | rewrite (ARadd_0_r Rsth ARth) + | rewrite (ARmul_1_l ARth) + | rewrite (ARmul_1_r Rsth ARth) + | rewrite (ARmul_0_l ARth) + | rewrite (ARmul_0_r Rsth ARth) + | rewrite (ARdistr_l ARth) + | rewrite (ARdistr_r Rsth Reqe ARth) + | rewrite (ARadd_assoc ARth) + | rewrite (ARmul_assoc ARth) ]. + Ltac gen_add_push add Rsth Reqe ARth x := repeat (match goal with | |- context [add (add ?y x) ?z] => progress rewrite (ARadd_assoc2 Rsth Reqe ARth x y z) | |- context [add (add x ?y) ?z] => progress rewrite (ARadd_assoc1 Rsth ARth x y z) + | |- context [(add x ?y)] => + progress rewrite (ARadd_comm ARth x y) end). Ltac gen_mul_push mul Rsth Reqe ARth x := @@ -604,5 +585,6 @@ Ltac gen_mul_push mul Rsth Reqe ARth x := progress rewrite (ARmul_assoc2 Rsth Reqe ARth x y z) | |- context [mul (mul x ?y) ?z] => progress rewrite (ARmul_assoc1 Rsth ARth x y z) + | |- context [(mul x ?y)] => + progress rewrite (ARmul_comm ARth x y) end). - diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v new file mode 100644 index 00000000..fd765471 --- /dev/null +++ b/plugins/setoid_ring/Rings_Q.v @@ -0,0 +1,30 @@ +Require Export Cring. +Require Export Integral_domain. + +(* Rational numbers *) +Require Import QArith. + +Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). + +Instance Qri : (Ring (Ro:=Qops)). +constructor. +try apply Q_Setoid. +apply Qplus_comp. +apply Qmult_comp. +apply Qminus_comp. +apply Qopp_comp. + exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc. + exact Qmult_1_l. exact Qmult_1_r. apply Qmult_assoc. + apply Qmult_plus_distr_l. intros. apply Qmult_plus_distr_r. +reflexivity. exact Qplus_opp_r. +Defined. + +Instance Qcri: (Cring (Rr:=Qri)). +red. exact Qmult_comm. Defined. + +Lemma Q_one_zero: not (Qeq 1%Q 0%Q). +unfold Qeq. simpl. auto with *. Qed. + +Instance Qdi : (Integral_domain (Rcr:=Qcri)). +constructor. +exact Qmult_integral. exact Q_one_zero. Defined. diff --git a/plugins/setoid_ring/Rings_R.v b/plugins/setoid_ring/Rings_R.v new file mode 100644 index 00000000..fd219c23 --- /dev/null +++ b/plugins/setoid_ring/Rings_R.v @@ -0,0 +1,34 @@ +Require Export Cring. +Require Export Integral_domain. + +(* Real numbers *) +Require Import Reals. +Require Import RealField. + +Lemma Rsth : Setoid_Theory R (@eq R). +constructor;red;intros;subst;trivial. +Qed. + +Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)). + +Instance Rri : (Ring (Ro:=Rops)). +constructor; +try (try apply Rsth; + try (unfold respectful, Proper; unfold equality; unfold eq_notation in *; + intros; try rewrite H; try rewrite H0; reflexivity)). + exact Rplus_0_l. exact Rplus_comm. symmetry. apply Rplus_assoc. + exact Rmult_1_l. exact Rmult_1_r. symmetry. apply Rmult_assoc. + exact Rmult_plus_distr_r. intros; apply Rmult_plus_distr_l. +exact Rplus_opp_r. +Defined. + +Instance Rcri: (Cring (Rr:=Rri)). +red. exact Rmult_comm. Defined. + +Lemma R_one_zero: 1%R <> 0%R. +discrR. +Qed. + +Instance Rdi : (Integral_domain (Rcr:=Rcri)). +constructor. +exact Rmult_integral. exact R_one_zero. Defined. diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v new file mode 100644 index 00000000..58a4d7ea --- /dev/null +++ b/plugins/setoid_ring/Rings_Z.v @@ -0,0 +1,14 @@ +Require Export Cring. +Require Export Integral_domain. +Require Export Ncring_initial. + +Instance Zcri: (Cring (Rr:=Zr)). +red. exact Z.mul_comm. Defined. + +Lemma Z_one_zero: 1%Z <> 0%Z. +omega. +Qed. + +Instance Zdi : (Integral_domain (Rcr:=Zcri)). +constructor. +exact Zmult_integral. exact Z_one_zero. Defined. diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v index 362542b9..3c4f6b86 100644 --- a/plugins/setoid_ring/ZArithRing.v +++ b/plugins/setoid_ring/ZArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -27,11 +27,7 @@ Ltac isZpow_coef t := | _ => constr:false end. -Definition N_of_Z x := - match x with - | Zpos p => Npos p - | _ => N0 - end. +Notation N_of_Z := Z.to_N (only parsing). Ltac Zpow_tac t := match isZpow_coef t with @@ -43,14 +39,14 @@ Ltac Zpower_neg := repeat match goal with | [|- ?G] => match G with - | context c [Zpower _ (Zneg _)] => + | context c [Z.pow _ (Zneg _)] => let t := context c [Z0] in change t end end. Add Ring Zr : Zth - (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], + (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Z.succ], power_tac Zpower_theory [Zpow_tac], (* The two following option are not needed, it is the default chose when the set of coefficiant is usual ring Z *) diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 820246af..580e78f6 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: newring.ml4 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Pp open Util open Names @@ -18,8 +16,7 @@ open Closure open Environ open Libnames open Tactics -open Rawterm -open Termops +open Glob_term open Tacticals open Tacexpr open Pcoq @@ -87,7 +84,7 @@ let interp_map l c = with Not_found -> None let interp_map l t = - try Some(List.assoc t l) with Not_found -> None + try Some(list_assoc_f eq_constr t l) with Not_found -> None let protect_maps = ref Stringmap.empty let add_map s m = protect_maps := Stringmap.add s m !protect_maps @@ -98,13 +95,13 @@ let lookup_map map = let protect_red map env sigma c = kl (create_clos_infos betadeltaiota env) - (mk_clos_but (lookup_map map c) (Esubst.ESID 0) c);; + (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);; let protect_tac map = Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id,InHyp));; + Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Termops.InHyp));; TACTIC EXTEND protect_fv @@ -144,7 +141,7 @@ let closed_term_ast l = let l = List.map (fun gr -> ArgArg(dummy_loc,gr)) l in TacFun([Some(id_of_string"t")], TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term", - [Genarg.in_gen Genarg.globwit_constr (RVar(dummy_loc,id_of_string"t"),None); + [Genarg.in_gen Genarg.globwit_constr (GVar(dummy_loc,id_of_string"t"),None); Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l]))) (* let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term" @@ -161,18 +158,18 @@ let ty c = Typing.type_of (Global.env()) Evd.empty c let decl_constant na c = mkConst(declare_constant (id_of_string na) (DefinitionEntry { const_entry_body = c; + const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = true; - const_entry_boxed = true}, + const_entry_opaque = true }, IsProof Lemma)) (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = - TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) + TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) (* Calling a locally bound tactic *) let ltac_lcall tac args = - TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) + TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) let ltac_letin (x, e1) e2 = TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2) @@ -188,8 +185,10 @@ let ltac_record flds = let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c) let dummy_goal env = - {Evd.it = Evd.make_evar (named_context_val env) mkProp; - Evd.sigma = Evd.empty} + let (gl,_,sigma) = + Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Store.empty in + {Evd.it = gl; + Evd.sigma = sigma} let exec_tactic env n f args = let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in @@ -344,7 +343,7 @@ type ring_info = ring_pre_tac : glob_tactic_expr; ring_post_tac : glob_tactic_expr } -module Cmap = Map.Make(struct type t = constr let compare = compare end) +module Cmap = Map.Make(struct type t = constr let compare = constr_ord end) let from_carrier = ref Cmap.empty let from_relation = ref Cmap.empty @@ -415,7 +414,7 @@ let subst_th (subst,th) = let posttac'= subst_tactic subst th.ring_post_tac in if c' == th.ring_carrier && eq' == th.ring_req && - set' = th.ring_setoid && + eq_constr set' th.ring_setoid && ext' == th.ring_ext && morph' == th.ring_morph && th' == th.ring_th && @@ -440,7 +439,7 @@ let subst_th (subst,th) = ring_post_tac = posttac' } -let (theory_to_obj, obj_to_theory) = +let theory_to_obj : ring_info -> obj = let cache_th (name,th) = add_entry name th in declare_object {(default_object "tactic-new-ring-theory") with @@ -576,13 +575,13 @@ let dest_ring env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in match kind_of_term th_typ with App(f,[|r;zero;one;add;mul;sub;opp;req|]) - when f = Lazy.force coq_almost_ring_theory -> + when eq_constr f (Lazy.force coq_almost_ring_theory) -> (None,r,zero,one,add,mul,Some sub,Some opp,req) | App(f,[|r;zero;one;add;mul;req|]) - when f = Lazy.force coq_semi_ring_theory -> + when eq_constr f (Lazy.force coq_semi_ring_theory) -> (Some true,r,zero,one,add,mul,None,None,req) | App(f,[|r;zero;one;add;mul;sub;opp;req|]) - when f = Lazy.force coq_ring_theory -> + when eq_constr f (Lazy.force coq_ring_theory) -> (Some false,r,zero,one,add,mul,Some sub,Some opp,req) | _ -> error "bad ring structure" @@ -592,10 +591,10 @@ let dest_morph env sigma m_spec = match kind_of_term m_typ with App(f,[|r;zero;one;add;mul;sub;opp;req; c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) - when f = Lazy.force coq_ring_morph -> + when eq_constr f (Lazy.force coq_ring_morph) -> (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi) | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) - when f = Lazy.force coq_semi_morph -> + when eq_constr f (Lazy.force coq_semi_morph) -> (c,czero,cone,cadd,cmul,None,None,ceqb,phi) | _ -> error "bad morphism structure" @@ -626,23 +625,23 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = (match rk, opp, kind with Abstract, None, _ -> let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in - TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) + TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) | Abstract, Some opp, Some _ -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in - TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) + TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) | Abstract, Some opp, None -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in TacArg - (TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) + (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) | Computational _,_,_ -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in TacArg - (TacCall(dummy_loc,t,List.map carg [zero;one;zero;one])) + (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one])) | Morphism mth,_,_ -> let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in TacArg - (TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone]))) + (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone]))) let make_hyp env c = let t = Retyping.get_type_of env Evd.empty c in @@ -659,7 +658,7 @@ let interp_power env pow = match pow with | None -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in - (TacArg(TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) + (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with @@ -832,7 +831,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl = TACTIC EXTEND ring_lookup | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> - [ let (t,lr) = list_sep_last lrt in ring_lookup (fst f) lH lr t] + [ let (t,lr) = list_sep_last lrt in ring_lookup f lH lr t] END @@ -893,18 +892,18 @@ let dest_field env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in match kind_of_term th_typ with | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when f = Lazy.force afield_theory -> + when eq_constr f (Lazy.force afield_theory) -> let rth = lapp af_ar [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when f = Lazy.force field_theory -> + when eq_constr f (Lazy.force field_theory) -> let rth = lapp f_r [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;div;inv;req|]) - when f = Lazy.force sfield_theory -> + when eq_constr f (Lazy.force sfield_theory) -> let rth = lapp sf_sr [|r;zero;one;add;mul;div;inv;req;th_spec|] in (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) @@ -1016,7 +1015,7 @@ let subst_th (subst,th) = field_pre_tac = pretac'; field_post_tac = posttac' } -let (ftheory_to_obj, obj_to_ftheory) = +let ftheory_to_obj : field_info -> obj = let cache_th (name,th) = add_field_entry name th in declare_object {(default_object "tactic-new-field-theory") with @@ -1160,5 +1159,5 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl = TACTIC EXTEND field_lookup | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> - [ let (t,l) = list_sep_last lt in field_lookup (fst f) lH l t ] + [ let (t,l) = list_sep_last lt in field_lookup f lH l t ] END diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget index 6934375b..580df9b5 100644 --- a/plugins/setoid_ring/vo.itarget +++ b/plugins/setoid_ring/vo.itarget @@ -13,3 +13,13 @@ Ring_tac.vo Ring_theory.vo Ring.vo ZArithRing.vo +Algebra_syntax.vo +Cring.vo +Ncring.vo +Ncring_polynom.vo +Ncring_initial.vo +Ncring_tac.vo +Rings_Z.vo +Rings_R.vo +Rings_Q.vo +Integral_domain.vo
\ No newline at end of file |