diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /plugins/setoid_ring | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/ArithRing.v | 8 | ||||
| -rw-r--r-- | plugins/setoid_ring/BinList.v | 10 | ||||
| -rw-r--r-- | plugins/setoid_ring/Field_tac.v | 102 | ||||
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 228 | ||||
| -rw-r--r-- | plugins/setoid_ring/InitialRing.v | 126 | ||||
| -rw-r--r-- | plugins/setoid_ring/RealField.v | 14 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_polynom.v | 386 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 54 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_theory.v | 72 | ||||
| -rw-r--r-- | plugins/setoid_ring/ZArithRing.v | 10 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 98 |
11 files changed, 554 insertions, 554 deletions
diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v index 601cabe00..e5a4c8d17 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/plugins/setoid_ring/ArithRing.v @@ -16,11 +16,11 @@ Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat). Proof. constructor. exact plus_0_l. exact plus_comm. exact plus_assoc. exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc. - exact mult_plus_distr_r. + exact mult_plus_distr_r. Qed. -Lemma nat_morph_N : - semi_morph 0 1 plus mult (eq (A:=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. Proof. constructor;trivial. @@ -46,7 +46,7 @@ Ltac natprering := |- context C [S ?p] => match p with O => fail 1 (* avoid replacing 1 with 1+0 ! *) - | p => match isnatcst p with + | p => match isnatcst p with | true => fail 1 | false => let v := Ss_to_add p (S 0) in fold v; natprering diff --git a/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v index 509020042..d403c9efe 100644 --- a/plugins/setoid_ring/BinList.v +++ b/plugins/setoid_ring/BinList.v @@ -28,17 +28,17 @@ Section MakeBinList. | xH => hd default l | xO p => nth p (jump p l) | xI p => nth p (jump p (tail l)) - end. + end. Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l). - Proof. + Proof. induction j;simpl;intros. repeat rewrite IHj;trivial. repeat rewrite IHj;trivial. trivial. Qed. - Lemma jump_Psucc : forall j l, + Lemma jump_Psucc : forall j l, (jump (Psucc j) l) = (jump 1 (jump j l)). Proof. induction j;simpl;intros. @@ -47,7 +47,7 @@ Section MakeBinList. trivial. Qed. - Lemma jump_Pplus : forall i j l, + Lemma jump_Pplus : forall i j l, (jump (i + j) l) = (jump i (jump j l)). Proof. induction i;intros. @@ -69,7 +69,7 @@ Section MakeBinList. trivial. Qed. - + Lemma nth_jump : forall p l, nth p (tail l) = hd default (jump p l). Proof. induction p;simpl;intros. diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index 0082eb9af..7aff8e0cb 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -10,27 +10,27 @@ Require Import Ring_tac BinList Ring_polynom InitialRing. Require Export Field_theory. (* syntaxification *) - Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv := + Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv := let rec mkP t := let f := match Cst t with | InitialRing.NotConstant => - match t with - | (radd ?t1 ?t2) => + match t with + | (radd ?t1 ?t2) => fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(FEadd e1 e2) - | (rmul ?t1 ?t2) => + | (rmul ?t1 ?t2) => fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(FEmul e1 e2) - | (rsub ?t1 ?t2) => - fun _ => + | (rsub ?t1 ?t2) => + fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(FEsub e1 e2) | (ropp ?t1) => fun _ => let e1 := mkP t1 in constr:(FEopp e1) - | (rdiv ?t1 ?t2) => + | (rdiv ?t1 ?t2) => fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(FEdiv e1 e2) @@ -38,7 +38,7 @@ Require Export Field_theory. fun _ => let e1 := mkP t1 in constr:(FEinv e1) | (rpow ?t1 ?n) => match CstPow n with - | InitialRing.NotConstant => + | InitialRing.NotConstant => fun _ => let p := Find_at t fv in constr:(@FEX C p) @@ -74,7 +74,7 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv := | _ => AddFvTail t fv end | _ => fv - end + end in TFV t fv. (* packaging the field structure *) @@ -83,7 +83,7 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv := Ltac PackField F req Cst_tac Pow_tac L1 L2 L3 L4 cond_ok pre post := let FLD := match type of L1 with - | context [req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv + | context [req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] => (fun proj => proj Cst_tac Pow_tac pre post @@ -245,9 +245,9 @@ Ltac Field_norm_gen f n FLD lH rl := ReflexiveRewriteTactic mkFFV mkFE lemma_tac main_tac fv0 rl; try simpl_PCond FLD. -Ltac Field_simplify_gen f FLD lH rl := +Ltac Field_simplify_gen f FLD lH rl := get_FldPre FLD (); - Field_norm_gen f ring_subst_niter FLD lH rl; + Field_norm_gen f ring_subst_niter FLD lH rl; get_FldPost FLD (). Ltac Field_simplify := @@ -257,14 +257,14 @@ Tactic Notation (at level 0) "field_simplify" constr_list(rl) := let G := Get_goal in field_lookup (PackField Field_simplify) [] rl G. -Tactic Notation (at level 0) +Tactic Notation (at level 0) "field_simplify" "[" constr_list(lH) "]" constr_list(rl) := let G := Get_goal in field_lookup (PackField Field_simplify) [lH] rl G. -Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):= +Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):= let G := Get_goal in - let t := type of H in + let t := type of H in let g := fresh "goal" in set (g:= G); revert H; @@ -272,10 +272,10 @@ Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):= intro H; unfold g;clear g. -Tactic Notation "field_simplify" - "["constr_list(lH) "]" constr_list(rl) "in" hyp(H):= +Tactic Notation "field_simplify" + "["constr_list(lH) "]" constr_list(rl) "in" hyp(H):= let G := Get_goal in - let t := type of H in + let t := type of H in let g := fresh "goal" in set (g:= G); revert H; @@ -284,15 +284,15 @@ Tactic Notation "field_simplify" unfold g;clear g. (* -Ltac Field_simplify_in hyp:= +Ltac Field_simplify_in hyp:= Field_simplify_gen ltac:(fun H => rewrite H in hyp). -Tactic Notation (at level 0) +Tactic Notation (at level 0) "field_simplify" constr_list(rl) "in" hyp(h) := let t := type of h in field_lookup (Field_simplify_in h) [] rl t. -Tactic Notation (at level 0) +Tactic Notation (at level 0) "field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) := let t := type of h in field_lookup (Field_simplify_in h) [lH] rl t. @@ -317,10 +317,10 @@ Ltac Field_Scheme Simpl_tac n lemma FLD lH := pose (vlpe := lpe); let nlemma := fresh "field_lemma" in (assert (nlemma := lemma n fv vlpe fe1 fe2 prh) - || fail "field anomaly:failed to build lemma"); + || fail "field anomaly:failed to build lemma"); ProveLemmaHyps nlemma ltac:(fun ilemma => - apply ilemma + apply ilemma || fail "field anomaly: failed in applying lemma"; [ Simpl_tac | simpl_PCond FLD]); clear nlemma; @@ -333,11 +333,11 @@ Ltac Field_Scheme Simpl_tac n lemma FLD lH := Ltac FIELD FLD lH rl := let Simpl := vm_compute; reflexivity || fail "not a valid field equation" in let lemma := get_L1 FLD in - get_FldPre FLD (); + get_FldPre FLD (); Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH; try exact I; get_FldPost FLD(). - + Tactic Notation (at level 0) "field" := let G := Get_goal in field_lookup (PackField FIELD) [] G. @@ -351,15 +351,15 @@ Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" := Ltac FIELD_SIMPL FLD lH rl := let Simpl := (protect_fv "field") in let lemma := get_SimplifyEqLemma FLD in - get_FldPre FLD (); + get_FldPre FLD (); Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH; get_FldPost FLD (). -Tactic Notation (at level 0) "field_simplify_eq" := +Tactic Notation (at level 0) "field_simplify_eq" := let G := Get_goal in field_lookup (PackField FIELD_SIMPL) [] G. -Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" := +Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" := let G := Get_goal in field_lookup FIELD_SIMPL [lH] G. @@ -372,7 +372,7 @@ Ltac Field_simplify_eq n FLD lH := let mkFE := get_Meta FLD in let lemma := get_L4 FLD in let hyp := fresh "hyp" in - intro hyp; + intro hyp; OnEquationHyp req hyp ltac:(fun t1 t2 => let fv := FV_hypo_tac mkFV req lH in let fv := mkFFV t1 fv in @@ -385,16 +385,16 @@ Ltac Field_simplify_eq n FLD lH := ProveLemmaHyps (lemma n fv lpe fe1 fe2 prh) ltac:(fun ilemma => match type of ilemma with - | req _ _ -> _ -> ?EQ => + | req _ _ -> _ -> ?EQ => let tmp := fresh "tmp" in assert (tmp : EQ); [ apply ilemma; [ exact hyp | simpl_PCond_BEURK FLD] | protect_fv "field" in tmp; revert tmp ]; - clear hyp + clear hyp end)). Ltac FIELD_SIMPL_EQ FLD lH rl := - get_FldPre FLD (); + get_FldPre FLD (); Field_simplify_eq Ring_tac.ring_subst_niter FLD lH; get_FldPost(). @@ -406,15 +406,15 @@ Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) := | clear H;intro H]. -Tactic Notation (at level 0) - "field_simplify_eq" "[" constr_list(lH) "]" "in" hyp(H) := +Tactic Notation (at level 0) + "field_simplify_eq" "[" constr_list(lH) "]" "in" hyp(H) := let t := type of H in generalize H; field_lookup (PackField FIELD_SIMPL_EQ) [lH] t; [ try exact I |clear H;intro H]. - -(* More generic tactics to build variants of field *) + +(* More generic tactics to build variants of field *) (* This tactic reifies c and pass to F: - the FLD structure gathering all info in the field DB @@ -489,13 +489,13 @@ Ltac reduce_field_expr ope kont FLD fv expr := (* Hack to let a Ltac return a term in the context of a primitive tactic *) Ltac return_term x := generalize (refl_equal x). Ltac get_term := - match goal with + match goal with | |- ?x = _ -> _ => x end. (* Turn an operation on field expressions (FExpr) into a reduction on terms (in the field carrier). Because of field_lookup, - the tactic cannot return a term directly, so it is returned + the tactic cannot return a term directly, so it is returned via the conclusion of the goal (return_term). *) Ltac reduce_field_ope ope c := gen_with_field ltac:(reduce_field_expr ope return_term) c. @@ -526,7 +526,7 @@ Ltac field_elements set ext fspec pspec sspec dspec rk := Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk := let get_lemma := match pspec with None => fun x y => x | _ => fun x y => y end in - let simpl_eq_lemma := get_lemma + let simpl_eq_lemma := get_lemma Field_simplify_eq_correct Field_simplify_eq_pow_correct in let simpl_eq_in_lemma := get_lemma Field_simplify_eq_in_correct Field_simplify_eq_pow_in_correct in @@ -538,27 +538,27 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk := | _ => let field_ok1 := constr:(Field_correct set ext_r inv_m afth morph) in match p_spec with - | mkhypo ?pp_spec => + | mkhypo ?pp_spec => let field_ok2 := constr:(field_ok1 _ _ _ pp_spec) in match s_spec with - | mkhypo ?ss_spec => + | mkhypo ?ss_spec => let field_ok3 := constr:(field_ok2 _ ss_spec) in match d_spec with - | mkhypo ?dd_spec => + | mkhypo ?dd_spec => let field_ok := constr:(field_ok3 _ dd_spec) in - let mk_lemma lemma := - constr:(lemma _ _ _ _ _ _ _ _ _ _ - set ext_r inv_m afth - _ _ _ _ _ _ _ _ _ morph - _ _ _ pp_spec _ ss_spec _ dd_spec) in + let mk_lemma lemma := + constr:(lemma _ _ _ _ _ _ _ _ _ _ + set ext_r inv_m afth + _ _ _ _ _ _ _ _ _ morph + _ _ _ pp_spec _ ss_spec _ dd_spec) in let field_simpl_eq_ok := mk_lemma simpl_eq_lemma in let field_simpl_ok := mk_lemma rw_lemma in let field_simpl_eq_in := mk_lemma simpl_eq_in_lemma in - let cond1_ok := + let cond1_ok := constr:(Pcond_simpl_gen set ext_r afth morph pp_spec dd_spec) in - let cond2_ok := + let cond2_ok := constr:(Pcond_simpl_complete set ext_r afth morph pp_spec dd_spec) in - (fun f => + (fun f => f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in cond1_ok cond2_ok) | _ => fail 4 "field: bad coefficiant division specification" @@ -566,6 +566,6 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk := | _ => fail 3 "field: bad sign specification" end | _ => fail 2 "field: bad power specification" - end + end | _ => fail 1 "field internal error : field_lemmas, please report" end). diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index fd99f786f..205bef6d5 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -14,7 +14,7 @@ Set Implicit Arguments. Section MakeFieldPol. -(* Field elements *) +(* Field elements *) Variable R:Type. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R). Variable (rdiv : R -> R -> R) (rinv : R -> R). @@ -30,7 +30,7 @@ Section MakeFieldPol. Variable Rsth : Setoid_Theory R req. Variable Reqe : ring_eq_ext radd rmul ropp req. Variable SRinv_ext : forall p q, p == q -> / p == / q. - + (* Field properties *) Record almost_field_theory : Prop := mk_afield { AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req; @@ -47,10 +47,10 @@ Section AlmostField. Let rdiv_def := AFth.(AFdiv_def). Let rinv_l := AFth.(AFinv_l). - (* Coefficients *) + (* Coefficients *) Variable C: Type. Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C). - Variable ceqb : C->C->bool. + Variable ceqb : C->C->bool. Variable phi : C -> R. Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req @@ -65,7 +65,7 @@ case (ceqb c1 c2); auto. Qed. - (* C notations *) + (* C notations *) Notation "x +! y" := (cadd x y) (at level 50). Notation "x *! y " := (cmul x y) (at level 40). Notation "x -! y " := (csub x y) (at level 50). @@ -74,14 +74,14 @@ Qed. Notation "[ x ]" := (phi x) (at level 0). - (* Useful tactics *) + (* 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. Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. Add Morphism rinv : rinv_ext. exact SRinv_ext. Qed. - + Let eq_trans := Setoid.Seq_trans _ _ Rsth. Let eq_sym := Setoid.Seq_sym _ _ Rsth. Let eq_refl := Setoid.Seq_refl _ _ Rsth. @@ -90,15 +90,15 @@ Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO CRmorph.(morph1) . Hint Resolve (Rmul_ext Reqe) (Rmul_ext Reqe) (Radd_ext Reqe) (ARsub_ext Rsth Reqe ARth) (Ropp_ext Reqe) SRinv_ext. Hint Resolve (ARadd_0_l ARth) (ARadd_comm ARth) (ARadd_assoc ARth) - (ARmul_1_l ARth) (ARmul_0_l ARth) + (ARmul_1_l ARth) (ARmul_0_l ARth) (ARmul_comm ARth) (ARmul_assoc ARth) (ARdistr_l ARth) - (ARopp_mul_l ARth) (ARopp_add ARth) + (ARopp_mul_l ARth) (ARopp_add ARth) (ARsub_def ARth) . (* Power coefficients *) Variable Cpow : Set. Variable Cp_phi : N -> Cpow. - Variable rpow : R -> Cpow -> R. + Variable rpow : R -> Cpow -> R. Variable pow_th : power_theory rI rmul req Cp_phi rpow. (* sign function *) Variable get_sign : C -> option C. @@ -129,11 +129,11 @@ rewrite (ARopp_zero Rsth Reqe ARth) in |- *; ring. Qed. (*************************************************************************** - - Properties of division - + + Properties of division + ***************************************************************************) - + Theorem rdiv_simpl: forall p q, ~ q == 0 -> q * (p / q) == p. intros p q H. rewrite rdiv_def in |- *. @@ -141,7 +141,7 @@ transitivity (/ q * q * p); [ ring | idtac ]. rewrite rinv_l in |- *; 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. @@ -195,7 +195,7 @@ Qed. Theorem rdiv1: forall r, r == r / 1. intros r; transitivity (1 * (r / 1)); auto. Qed. - + Theorem rdiv2: forall r1 r2 r3 r4, ~ r2 == 0 -> @@ -224,7 +224,7 @@ intros r1 r2 r3 r4 r5 H H0. 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) +assert (HH4: ~ r2 * (r4 * r5) == 0) by complete (repeat apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * (r4 * r5)); trivial. rewrite rdiv_simpl in |- *; trivial. @@ -288,7 +288,7 @@ assert (~ r1 / r2 == 0) as Hk. repeat rewrite rinv_l in |- *; auto. Qed. Hint Resolve rdiv6 . - + Theorem rdiv4: forall r1 r2 r3 r4, ~ r2 == 0 -> @@ -385,9 +385,9 @@ transitivity (r1 / r2 * (r4 / r4)). Qed. (*************************************************************************** - - Some equality test - + + Some equality test + ***************************************************************************) Fixpoint positive_eq (p1 p2 : positive) {struct p1} : bool := @@ -397,7 +397,7 @@ Fixpoint positive_eq (p1 p2 : positive) {struct p1} : bool := | 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; @@ -411,8 +411,8 @@ 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 := + +Definition N_eq n1 n2 := match n1, n2 with | N0, N0 => true | Npos p1, Npos p2 => positive_eq p1 p2 @@ -438,7 +438,7 @@ Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := | PEpow e3 n3, PEpow e4 n4 => if N_eq n3 n4 then PExpr_eq e3 e4 else false | _, _ => false end. - + Add Morphism (pow_pos rmul) : pow_morph. intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH]. Qed. @@ -508,10 +508,10 @@ Definition NPEpow x n := | N0 => PEc cI | Npos p => if positive_eq 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) - | _ => PEpow x n + 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) + | _ => PEpow x n end end. @@ -530,7 +530,7 @@ Proof. induction p;simpl;auto;repeat rewrite CRmorph.(morph_mul);ring [IHp]. Qed. -(* mul *) +(* mul *) Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C := match x, y with PEc c1, PEc c2 => PEc (cmul c1 c2) @@ -546,7 +546,7 @@ Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C := Lemma pow_pos_mul : forall x y p, pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p. induction p;simpl;auto;try ring [IHp]. 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; @@ -581,17 +581,17 @@ destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r). apply (morph_sub CRmorph). Qed. - + (* opp *) Definition NPEopp e1 := match e1 with PEc c1 => PEc (copp c1) | _ => PEopp e1 end. - + Theorem NPEopp_correct: forall l e1, NPEeval l (NPEopp e1) == NPEeval l (PEopp e1). intros l e1; case e1; simpl; auto. intros; apply (morph_opp CRmorph). Qed. - + (* simplification *) Fixpoint PExpr_simp (e : PExpr C) : PExpr C := match e with @@ -602,7 +602,7 @@ Fixpoint PExpr_simp (e : PExpr C) : PExpr C := | PEpow e1 n1 => NPEpow (PExpr_simp e1) n1 | _ => e end. - + Theorem PExpr_simp_correct: forall l e, NPEeval l (PExpr_simp e) == NPEeval l e. intros l e; elim e; simpl; auto. @@ -630,9 +630,9 @@ Qed. (**************************************************************************** - - Datastructure - + + Datastructure + ***************************************************************************) (* The input: syntax of a field expression *) @@ -647,7 +647,7 @@ Inductive FExpr : Type := | FEinv: FExpr -> FExpr | FEdiv: FExpr -> FExpr -> FExpr | FEpow: FExpr -> N -> FExpr . - + Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := match pe with | FEc c => phi c @@ -664,7 +664,7 @@ Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := Strategy expand [FEeval]. (* The result of the normalisation *) - + Record linear : Type := mk_linear { num : PExpr C; denum : PExpr C; @@ -675,7 +675,7 @@ Record linear : Type := mk_linear { Semantics and properties of side condition ***************************************************************************) - + Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop := match le with | nil => True @@ -689,7 +689,7 @@ intros l a l1 H. destruct l1; simpl in H |- *; trivial. destruct H; trivial. Qed. - + Theorem PCond_cons_inv_r : forall l a l1, PCond l (a :: l1) -> PCond l l1. intros l a l1 H. destruct l1; simpl in H |- *; trivial. @@ -703,12 +703,12 @@ intros l l1 l2; elim l1; simpl app in |- *. destruct l2; firstorder. firstorder. Qed. - + Theorem PCond_app_inv_r: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l2. intros l l1 l2; elim l1; simpl app; auto. intros a l0 H H0; apply H; apply PCond_cons_inv_r with ( 1 := H0 ). Qed. - + (* An unsatisfiable condition: issued when a division by zero is detected *) Definition absurd_PCond := cons (PEc cO) nil. @@ -720,9 +720,9 @@ apply (morph0 CRmorph). Qed. (*************************************************************************** - - Normalisation - + + Normalisation + ***************************************************************************) Fixpoint isIn (e1:PExpr C) (p1:positive) @@ -731,18 +731,18 @@ Fixpoint isIn (e1:PExpr C) (p1:positive) | PEmul e3 e4 => match isIn e1 p1 e3 p2 with | Some (N0, e5) => Some (N0, NPEmul e5 (NPEpow e4 (Npos p2))) - | Some (Npos p, e5) => + | Some (Npos p, e5) => match isIn e1 p e4 p2 with | Some (n, e6) => Some (n, NPEmul e5 e6) | None => Some (Npos p, NPEmul e5 (NPEpow e4 (Npos p2))) end - | None => + | None => match isIn e1 p1 e4 p2 with | Some (n, e5) => Some (n,NPEmul (NPEpow e3 (Npos p2)) e5) | None => None end end - | PEpow e3 N0 => None + | PEpow e3 N0 => None | PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pmult p3 p2) | _ => if PExpr_eq e1 e2 then @@ -751,27 +751,27 @@ Fixpoint isIn (e1:PExpr C) (p1:positive) | Z0 => Some (N0, PEc cI) | Zneg p => Some (N0, NPEpow e2 (Npos p)) end - else None + else None end. - + 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) + Notation pow_pos_plus := (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc)). - Lemma isIn_correct_aux : forall l e1 e2 p1 p2, - match + Lemma isIn_correct_aux : forall l e1 e2 p1 p2, + match (if PExpr_eq e1 e2 then match Zminus (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)) end - else None) + else None) with - | Some(n, e3) => - NPEeval l (PEpow e2 (Npos p2)) == + | Some(n, e3) => + NPEeval l (PEpow e2 (Npos p2)) == NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\ (Zpos p1 > NtoZ n)%Z | _ => True @@ -779,15 +779,15 @@ 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. + 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 (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. + rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial. repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite H;trivial. change (ZtoN @@ -801,7 +801,7 @@ Proof. 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 _). + 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 _). @@ -815,9 +815,9 @@ Qed. Theorem isIn_correct: forall l e1 p1 e2 p2, - match isIn e1 p1 e2 p2 with - | Some(n, e3) => - NPEeval l (PEpow e2 (Npos p2)) == + match isIn e1 p1 e2 p2 with + | Some(n, e3) => + NPEeval l (PEpow e2 (Npos p2)) == NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\ (Zpos p1 > NtoZ n)%Z | _ => True @@ -827,7 +827,7 @@ Opaque NPEpow. intros l e1 p1 e2; generalize p1;clear p1;elim e2; intros; try (refine (isIn_correct_aux l e1 _ p1 p2);fail);simpl isIn. generalize (H p1 p2);clear H;destruct (isIn e1 p1 p p2). destruct p3. -destruct n. +destruct n. simpl. rewrite NPEmul_correct. simpl; rewrite NPEpow_correct;simpl. repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul;intros (H,H1);split;[ring[H]|trivial]. @@ -838,12 +838,12 @@ destruct n. unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;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 * 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. - repeat rewrite pow_th.(rpow_pow_N);simpl. + 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. @@ -857,16 +857,16 @@ destruct n. 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. - replace (p1 - p4 + (p4 - p6))%positive with (p1 - p6)%positive. + replace (p1 - p4 + (p4 - p6))%positive with (p1 - p6)%positive. rewrite NPEmul_correct. simpl;ring. - assert + 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. - simpl. repeat rewrite pow_th.(rpow_pow_N). + 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. rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. simpl in H2. rewrite pow_th.(rpow_pow_N);simpl. @@ -879,8 +879,8 @@ destruct n. 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. - trivial. + 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. destruct n;simpl. repeat rewrite pow_th.(rpow_pow_N). simpl. @@ -910,18 +910,18 @@ 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 (Pmult p3 p) e2 + | _ => match isIn e1 p e2 xH with - | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3 + | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3 | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3 | None => mk_rsplit (NPEpow e1 (Npos p)) (PEc cI) e2 end - end. + end. Lemma split_aux_correct_1 : forall l e1 p e2, let res := match isIn e1 p e2 xH with - | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3 + | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3 | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3 | None => mk_rsplit (NPEpow e1 (Npos p)) (PEc cI) e2 end in @@ -932,7 +932,7 @@ Proof. intros. unfold res;clear res; generalize (isIn_correct l e1 p e2 xH). destruct (isIn e1 p e2 1). destruct p0. Opaque NPEpow NPEmul. - destruct n;simpl; + destruct n;simpl; (repeat rewrite NPEmul_correct;simpl; repeat rewrite NPEpow_correct;simpl; repeat rewrite pow_th.(rpow_pow_N);simpl). @@ -945,7 +945,7 @@ Proof. Qed. Theorem split_aux_correct: forall l e1 p e2, - NPEeval l (PEpow e1 (Npos p)) == + NPEeval l (PEpow e1 (Npos p)) == NPEeval l (NPEmul (left (split_aux e1 p e2)) (common (split_aux e1 p e2))) /\ NPEeval l e2 == NPEeval l (NPEmul (right (split_aux e1 p e2)) @@ -953,9 +953,9 @@ Theorem split_aux_correct: forall l e1 p e2, Proof. intros l; induction e1;intros k e2; try refine (split_aux_correct_1 l _ k e2);simpl. generalize (IHe1_1 k e2); clear IHe1_1. -generalize (IHe1_2 k (rsplit_right (split_aux e1_1 k e2))); clear IHe1_2. +generalize (IHe1_2 k (rsplit_right (split_aux e1_1 k e2))); clear IHe1_2. simpl. repeat (rewrite NPEmul_correct;simpl). -repeat rewrite pow_th.(rpow_pow_N);simpl. +repeat rewrite pow_th.(rpow_pow_N);simpl. intros (H1,H2) (H3,H4);split. rewrite pow_pos_mul. rewrite H1;rewrite H3. ring. rewrite H4;rewrite H2;ring. @@ -971,7 +971,7 @@ rewrite pow_pos_pow_pos. intros [H1 H2];split;ring [H1 H2]. Qed. Definition split e1 e2 := split_aux e1 xH e2. - + Theorem split_correct_l: forall l e1 e2, NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2)) (common (split e1 e2))). @@ -987,7 +987,7 @@ Proof. intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl;auto. Qed. -Fixpoint Fnorm (e : FExpr) : linear := +Fixpoint Fnorm (e : FExpr) : linear := match e with | FEc c => mk_linear (PEc c) (PEc cI) nil | FEX x => mk_linear (PEX C x) (PEc cI) nil @@ -999,7 +999,7 @@ Fixpoint Fnorm (e : FExpr) : linear := (NPEadd (NPEmul (num x) (right s)) (NPEmul (num y) (left s))) (NPEmul (left s) (NPEmul (right s) (common s))) (condition x ++ condition y) - + | FEsub e1 e2 => let x := Fnorm e1 in let y := Fnorm e2 in @@ -1050,13 +1050,13 @@ Proof. induction p;simpl. intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H). apply IHp. - rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). + rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). reflexivity. - rewrite H1. ring. rewrite Hp;ring. + rewrite H1. ring. rewrite Hp;ring. intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). reflexivity. rewrite Hp;ring. trivial. Qed. - + Theorem Pcond_Fnorm: forall l e, PCond l (condition (Fnorm e)) -> ~ NPEeval l (denum (Fnorm e)) == 0. @@ -1135,9 +1135,9 @@ Hint Resolve Pcond_Fnorm. (*************************************************************************** - - Main theorem - + + Main theorem + ***************************************************************************) Theorem Fnorm_FEeval_PEeval: @@ -1242,8 +1242,8 @@ apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial. intro Hp. apply (pow_pos_not_0 Hdiff p). rewrite (@rmul_reg_l (pow_pos rmul r0 p) (pow_pos rmul r0 p) 0). - reflexivity. apply pow_pos_not_0;trivial. ring [Hp]. -rewrite <- rdiv4;trivial. + reflexivity. apply pow_pos_not_0;trivial. ring [Hp]. +rewrite <- rdiv4;trivial. rewrite IHp;reflexivity. apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial. reflexivity. @@ -1352,11 +1352,11 @@ Theorem Field_simplify_eq_old_correct : Proof. intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond; subst nfe1 nfe2. apply Fnorm_crossproduct; trivial. -match goal with +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))); - rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec + 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))) end. trivial. @@ -1368,7 +1368,7 @@ Theorem Field_simplify_eq_correct : forall lmp, Nmk_monpol_list lpe = lmp -> forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> - forall den, split (denum nfe1) (denum nfe2) = den -> + forall den, split (denum nfe1) (denum nfe2) = den -> NPphi_dev l (Nnorm n lmp (PEmul (num nfe1) (right den))) == NPphi_dev l (Nnorm n lmp (PEmul (num nfe2) (left den))) -> PCond l (condition nfe1 ++ condition nfe2) -> @@ -1387,14 +1387,14 @@ repeat rewrite (ARmul_assoc ARth) in |- *. 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 +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. 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 + 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. simpl in Hcrossprod. @@ -1408,7 +1408,7 @@ Theorem Field_simplify_eq_pow_correct : forall lmp, Nmk_monpol_list lpe = lmp -> forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> - forall den, split (denum nfe1) (denum nfe2) = den -> + forall den, split (denum nfe1) (denum nfe2) = den -> NPphi_pow l (Nnorm n lmp (PEmul (num nfe1) (right den))) == NPphi_pow l (Nnorm n lmp (PEmul (num nfe2) (left den))) -> PCond l (condition nfe1 ++ condition nfe2) -> @@ -1427,14 +1427,14 @@ repeat rewrite (ARmul_assoc ARth) in |- *. 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 +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. 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 + 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. simpl in Hcrossprod. @@ -1448,7 +1448,7 @@ Theorem Field_simplify_eq_pow_in_correct : forall lmp, Nmk_monpol_list lpe = lmp -> forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> - forall den, split (denum nfe1) (denum nfe2) = den -> + forall den, split (denum nfe1) (denum nfe2) = den -> forall np1, Nnorm n lmp (PEmul (num nfe1) (right den)) = np1 -> forall np2, Nnorm n lmp (PEmul (num nfe2) (left den)) = np2 -> FEeval l fe1 == FEeval l fe2 -> @@ -1461,7 +1461,7 @@ Proof. repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl. assert (N1 := Pcond_Fnorm _ _ (PCond_app_inv_l _ _ _ H7)). assert (N2 := Pcond_Fnorm _ _ (PCond_app_inv_r _ _ _ H7)). - apply (@rmul_reg_l (NPEeval l (rsplit_common den))). + apply (@rmul_reg_l (NPEeval l (rsplit_common den))). intro Heq;apply N1. rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq]. @@ -1498,7 +1498,7 @@ forall n l lpe fe1 fe2, forall lmp, Nmk_monpol_list lpe = lmp -> forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> - forall den, split (denum nfe1) (denum nfe2) = den -> + forall den, split (denum nfe1) (denum nfe2) = den -> forall np1, Nnorm n lmp (PEmul (num nfe1) (right den)) = np1 -> forall np2, Nnorm n lmp (PEmul (num nfe2) (left den)) = np2 -> FEeval l fe1 == FEeval l fe2 -> @@ -1511,7 +1511,7 @@ Proof. repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl. assert (N1 := Pcond_Fnorm _ _ (PCond_app_inv_l _ _ _ H7)). assert (N2 := Pcond_Fnorm _ _ (PCond_app_inv_r _ _ _ H7)). - apply (@rmul_reg_l (NPEeval l (rsplit_common den))). + apply (@rmul_reg_l (NPEeval l (rsplit_common den))). intro Heq;apply N1. rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq]. @@ -1539,7 +1539,7 @@ Proof. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))). repeat rewrite <- (AFth.(AFdiv_def)). repeat rewrite <- Fnorm_FEeval_PEeval;trivial. - apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7). + apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7). Qed. @@ -1576,7 +1576,7 @@ Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := nil => cons e nil | cons a l1 => if PExpr_eq e a then l else cons a (Fcons e l1) end. - + Theorem PFcons_fcons_inv: forall l a l1, PCond l (Fcons a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. intros l a l1; elim l1; simpl Fcons; auto. @@ -1603,7 +1603,7 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := if Peq ceqb (Nnorm O nil e) (Nnorm O nil a) then l else cons a (Fcons0 e l1) end. - + Theorem PFcons0_fcons_inv: forall l a l1, PCond l (Fcons0 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. intros l a l1; elim l1; simpl Fcons0; auto. @@ -1620,7 +1620,7 @@ split. generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. apply H0. generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto. -clear get_sign get_sign_spec. +clear get_sign get_sign_spec. generalize Hp; case l0; simpl; intuition. Qed. @@ -1647,7 +1647,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). apply pow_pos_not_0;trivial. Qed. -Definition Pcond_simpl_gen := +Definition Pcond_simpl_gen := fcons_correct _ PFcons00_fcons_inv. @@ -1674,7 +1674,7 @@ Qed. Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := match e with PEmul e1 e2 => Fcons1 e1 (Fcons1 e2 l) - | PEpow e _ => Fcons1 e l + | PEpow e _ => Fcons1 e l | PEopp e => if ceqb (copp cI) cO then absurd_PCond else Fcons1 e l | PEc c => if ceqb c cO then absurd_PCond else l | _ => Fcons0 e l @@ -1710,7 +1710,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). Qed. 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; @@ -1720,7 +1720,7 @@ transitivity (NPEeval l a); trivial. apply PExpr_simp_correct. Qed. -Definition Pcond_simpl_complete := +Definition Pcond_simpl_complete := fcons_correct _ PFcons2_fcons_inv. End Fcons_simpl. @@ -1751,7 +1751,7 @@ End FieldAndSemiField. End MakeFieldPol. - Definition SF2AF R (rO rI:R) radd rmul rdiv rinv req Rsth + Definition SF2AF R (rO rI:R) radd rmul rdiv rinv req Rsth (sf:semi_field_theory rO rI radd rmul rdiv rinv req) := mk_afield _ _ (SRth_ARth Rsth sf.(SF_SR)) diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index e664b3b76..b5384f80b 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -27,7 +27,7 @@ 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). @@ -65,7 +65,7 @@ Section ZMORPHISM. Fixpoint gen_phiPOS (p:positive) : R := match p with - | xH => 1 + | xH => 1 | xO xH => (1 + 1) | xO p => (1 + 1) * (gen_phiPOS p) | xI xH => 1 + (1 +1) @@ -78,18 +78,18 @@ Section ZMORPHISM. | Z0 => 0 | Zneg p => -(gen_phiPOS1 p) end. - - Definition gen_phiZ z := + + 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). + Notation "[ x ]" := (gen_phiZ x). Definition get_signZ z := match z with - | Zneg p => Some (Zpos p) + | Zneg p => Some (Zpos p) | _ => None end. @@ -101,16 +101,16 @@ Section ZMORPHISM. simpl. unfold Zeq_bool. rewrite Zcompare_refl. trivial. Qed. - + Section ALMOST_RING. Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. Add Morphism rsub : rsub_ext3. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. - + Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x. Proof. - induction x;simpl. + induction x;simpl. rewrite IHx;destruct x;simpl;norm. rewrite IHx;destruct x;simpl;norm. rrefl. @@ -155,28 +155,28 @@ Section ZMORPHISM. Add Morphism rsub : rsub_ext4. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. - + (*morphisms are extensionaly equal*) Lemma same_genZ : forall x, [x] == gen_phiZ1 x. Proof. destruct x;simpl; try rewrite (same_gen ARth);rrefl. Qed. - - Lemma gen_Zeqb_ok : forall x y, + + Lemma gen_Zeqb_ok : forall x y, Zeq_bool x y = true -> [x] == [y]. Proof. intros x y H. assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1. rewrite H1;rrefl. Qed. - + Lemma gen_phiZ1_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 + end == gen_phiPOS1 x + -gen_phiPOS1 y. Proof. intros x y. @@ -197,7 +197,7 @@ Section ZMORPHISM. Qed. Lemma match_compOpp : forall x (B:Type) (be bl bg:B), - match CompOpp x with Eq => be | Lt => bl | Gt => bg end + 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. @@ -209,7 +209,7 @@ Section ZMORPHISM. apply gen_phiZ1_add_pos_neg. replace Eq with (CompOpp Eq);trivial. rewrite <- Pcompare_antisym;simpl. - rewrite match_compOpp. + rewrite match_compOpp. rewrite (Radd_comm Rth). apply gen_phiZ1_add_pos_neg. rewrite (ARgen_phiPOS_add ARth); norm. @@ -227,11 +227,11 @@ Section ZMORPHISM. Proof. intros;subst;rrefl. Qed. (*proof that [.] satisfies morphism specifications*) - Lemma gen_phiZ_morph : - ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH) + Lemma gen_phiZ_morph : + ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH) Zplus Zmult Zminus Zopp Zeq_bool gen_phiZ. - Proof. - assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH) + Proof. + assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH) Zplus Zmult Zeq_bool gen_phiZ). apply mkRmorph;simpl;try rrefl. apply gen_phiZ_add. apply gen_phiZ_mul. apply gen_Zeqb_ok. @@ -251,7 +251,7 @@ Lemma Nth : semi_ring_theory N0 (Npos xH) Nplus Nmult (@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. + exact Nmult_plus_distr_r. Qed. Definition Nsub := SRsub Nplus. @@ -260,11 +260,11 @@ Definition Nopp := (@SRopp N). Lemma Neqe : ring_eq_ext Nplus Nmult Nopp (@eq N). Proof (SReqe_Reqe Nseqe). -Lemma Nath : +Lemma Nath : almost_ring_theory N0 (Npos xH) Nplus Nmult Nsub Nopp (@eq N). Proof (SRth_ARth Nsth Nth). - -Definition Neq_bool (x y:N) := + +Definition Neq_bool (x y:N) := match Ncompare x y with | Eq => true | _ => false @@ -273,17 +273,17 @@ Definition Neq_bool (x y:N) := 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); + assert (H:=Ncompare_Eq_eq x y); destruct (Ncompare x y);intros;try discriminate. - rewrite H;trivial. + 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); + assert (H:=Ncompare_Eq_eq x y); destruct (Ncompare x y);intros;try discriminate. - rewrite H;trivial. + rewrite H;trivial. Qed. (**Same as above : definition of two,extensionaly equal, generic morphisms *) @@ -298,7 +298,7 @@ Section NMORPHISM. Add Setoid R req Rsth as R_setoid4. Ltac rrefl := gen_reflexivity Rsth. Variable SReqe : sring_eq_ext radd rmul req. - Variable SRth : semi_ring_theory 0 1 radd rmul req. + Variable SRth : semi_ring_theory 0 1 radd rmul req. Let ARth := SRth_ARth Rsth SRth. Let Reqe := SReqe_Reqe SReqe. Let ropp := (@SRopp R). @@ -315,15 +315,15 @@ Section NMORPHISM. match x with | N0 => 0 | Npos x => gen_phiPOS1 1 radd rmul x - end. + end. Definition gen_phiN x := match x with | N0 => 0 | Npos x => gen_phiPOS 1 radd rmul x - end. - Notation "[ x ]" := (gen_phiN x). - + end. + Notation "[ x ]" := (gen_phiN x). + Lemma same_genN : forall x, [x] == gen_phiN1 x. Proof. destruct x;simpl. rrefl. @@ -336,7 +336,7 @@ Section NMORPHISM. destruct x;destruct y;simpl;norm. apply (ARgen_phiPOS_add Rsth Reqe ARth). Qed. - + Lemma gen_phiN_mult : forall x y, [x * y] == [x] * [y]. Proof. intros x y;repeat rewrite same_genN. @@ -397,7 +397,7 @@ Fixpoint Nw_is0 (w : Nword) : bool := | nil => true | 0%N :: w' => Nw_is0 w' | _ => false - end. + end. Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool := match w1, w2 with @@ -559,7 +559,7 @@ induction x; intros. Qed. (* Proof that [.] satisfies morphism specifications *) - Lemma gen_phiNword_morph : + Lemma gen_phiNword_morph : ring_morph 0 1 radd rmul rsub ropp req NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword. constructor. @@ -585,7 +585,7 @@ Qed. End NWORDMORPHISM. Section GEN_DIV. - + Variables (R : Type) (rO : R) (rI : R) (radd : R -> R -> R) (rmul : R -> R -> R) (rsub : R -> R -> R) (ropp : R -> R) (req : R -> R -> Prop) (C : Type) (cO : C) (cI : C) @@ -595,8 +595,8 @@ Section GEN_DIV. Variable Reqe : ring_eq_ext radd rmul ropp req. Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req. Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi. - - (* Useful tactics *) + + (* 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. @@ -605,7 +605,7 @@ Section GEN_DIV. Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac rsimpl := gen_srewrite Rsth Reqe ARth. - Definition triv_div x y := + Definition triv_div x y := if ceqb x y then (cI, cO) else (cO, x). @@ -715,7 +715,7 @@ End GEN_DIV. (* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above are only optimisations that directly returns the reifid constant instead of resorting to the constant propagation of the simplification - algorithm. *) + algorithm. *) Ltac inv_gen_phi rO rI cO cI t := match t with | rO => cO @@ -769,10 +769,10 @@ Ltac gen_ring_sign morph sspec := match sspec with | None => match type of morph with - | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req Z ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi => constr:(@mkhypo (sign_theory copp ceqb get_signZ) get_signZ_th) - | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi => constr:(mkhypo (@get_sign_None_th C copp ceqb)) | _ => fail 2 "ring anomaly : default_sign_spec" @@ -782,24 +782,24 @@ 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 + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req Z ?c0 ?c1 Zplus Zmult ?csub ?copp ?ceq_b ?phi => constr:(mkhypo (Ztriv_div_th set phi)) - | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req N ?c0 ?c1 Nplus Nmult ?csub ?copp ?ceq_b ?phi => - constr:(mkhypo (Ntriv_div_th set phi)) - | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + constr:(mkhypo (Ntriv_div_th set phi)) + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi => constr:(mkhypo (triv_div_th set reqe arth morph)) - | _ => fail 1 "ring anomaly : default_sign_spec" + | _ => fail 1 "ring anomaly : default_sign_spec" end. Ltac gen_ring_div set reqe arth morph dspec := match dspec with - | None => default_div_spec set reqe arth morph + | None => default_div_spec set reqe arth morph | Some ?t => constr:(t) end. - + Ltac ring_elements set ext rspec pspec sspec dspec rk := let arth := coerce_to_almost_ring set ext rspec in let ext_r := coerce_to_ring_ext ext in @@ -813,10 +813,10 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk := | _ => fail 2 "ring anomaly" end | @Morphism ?m => - match type of m with - | ring_morph _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => m - | @semi_morph _ _ _ _ _ _ _ _ _ _ _ _ _ => - constr:(SRmorph_Rmorph set m) + match type of m with + | ring_morph _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => m + | @semi_morph _ _ _ _ _ _ _ _ _ _ _ _ _ => + constr:(SRmorph_Rmorph set m) | _ => fail 2 "ring anomaly" end | _ => fail 1 "ill-formed ring kind" @@ -832,27 +832,27 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk := Ltac ring_lemmas set ext rspec pspec sspec dspec rk := let gen_lemma2 := match pspec with - | None => constr:(ring_rw_correct) + | None => constr:(ring_rw_correct) | Some _ => constr:(ring_rw_pow_correct) end in ring_elements set ext rspec pspec sspec dspec rk ltac:(fun arth ext_r morph p_spec s_spec d_spec => match type of morph with - | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi => - let gen_lemma2_0 := - constr:(gen_lemma2 R r0 rI radd rmul rsub ropp req set ext_r arth + let gen_lemma2_0 := + constr:(gen_lemma2 R r0 rI radd rmul rsub ropp req set ext_r arth C c0 c1 cadd cmul csub copp ceq_b phi morph) in match p_spec with - | @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec => + | @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec => let gen_lemma2_1 := constr:(gen_lemma2_0 _ Cp_phi rpow pp_spec) in match d_spec with | @mkhypo (div_theory _ _ _ _ ?cdiv) ?dd_spec => let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in match s_spec with - | @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec => - let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in - let lemma1 := + | @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec => + let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in + let lemma1 := constr:(ring_correct set ext_r arth morph pp_spec dd_spec) in fun f => f arth ext_r morph lemma1 lemma2 | _ => fail 4 "ring: bad sign specification" @@ -878,7 +878,7 @@ Ltac isPcst t := | xO ?p => isPcst p | xH => constr:true (* nat -> positive *) - | P_of_succ_nat ?n => isnatcst n + | P_of_succ_nat ?n => isnatcst n | _ => constr:false end. diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v index 60641bcf9..56473adb9 100644 --- a/plugins/setoid_ring/RealField.v +++ b/plugins/setoid_ring/RealField.v @@ -1,5 +1,5 @@ Require Import Nnat. -Require Import ArithRing. +Require Import ArithRing. Require Export Ring Field. Require Import Rdefinitions. Require Import Rpow_def. @@ -99,7 +99,7 @@ rewrite H in |- *; intro. apply (Rlt_asym 0 0); trivial. Qed. -Lemma Zeq_bool_complete : forall x y, +Lemma Zeq_bool_complete : forall x y, InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x = InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y -> Zeq_bool x y = true. @@ -114,21 +114,21 @@ Qed. Lemma R_power_theory : power_theory 1%R Rmult (eq (A:=R)) nat_of_N pow. Proof. constructor. destruct n. reflexivity. - simpl. induction p;simpl. + 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. Qed. -Ltac Rpow_tac t := +Ltac Rpow_tac t := match isnatcst t with | false => constr:(InitialRing.NotConstant) | _ => constr:(N_of_nat t) - end. + end. -Add Field RField : Rfield +Add Field RField : Rfield (completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]). - + diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index d88470369..faa83dedc 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -18,21 +18,21 @@ Open Local Scope positive_scope. Import RingSyntax. Section MakeRingPol. - - (* Ring elements *) + + (* Ring elements *) Variable R:Type. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R). Variable req : R -> R -> Prop. - + (* Ring properties *) Variable Rsth : Setoid_Theory R req. Variable Reqe : ring_eq_ext radd rmul ropp req. Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req. - (* Coefficients *) + (* Coefficients *) Variable C: Type. Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C). - Variable ceqb : C->C->bool. + Variable ceqb : C->C->bool. Variable phi : C -> R. Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi. @@ -40,7 +40,7 @@ Section MakeRingPol. (* Power coefficients *) Variable Cpow : Set. Variable Cp_phi : N -> Cpow. - Variable rpow : R -> Cpow -> R. + Variable rpow : R -> Cpow -> R. Variable pow_th : power_theory rI rmul req Cp_phi rpow. (* division is ok *) @@ -54,12 +54,12 @@ Section MakeRingPol. Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). Notation "x == y" := (req x y). - (* C notations *) + (* 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). - (* Useful tactics *) + (* 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. @@ -93,20 +93,20 @@ Section MakeRingPol. *) Inductive Pol : Type := - | Pc : C -> Pol - | Pinj : positive -> Pol -> Pol + | Pc : C -> Pol + | Pinj : positive -> Pol -> Pol | PX : Pol -> positive -> Pol -> Pol. Definition P0 := Pc cO. Definition P1 := Pc cI. - - Fixpoint Peq (P P' : Pol) {struct P'} : bool := + + Fixpoint Peq (P P' : Pol) {struct P'} : bool := match P, P' with | Pc c, Pc c' => c ?=! c' - | Pinj j Q, Pinj j' Q' => + | Pinj j Q, Pinj j' Q' => match Pcompare j j' Eq with - | Eq => Peq Q Q' - | _ => false + | Eq => Peq Q Q' + | _ => false end | PX P i Q, PX P' i' Q' => match Pcompare i i' Eq with @@ -119,7 +119,7 @@ Section MakeRingPol. Notation " P ?== P' " := (Peq P P'). Definition mkPinj j P := - match P with + match P with | Pc _ => P | Pinj j' Q => Pinj ((j + j'):positive) Q | _ => Pinj j P @@ -132,7 +132,7 @@ Section MakeRingPol. | xI j => Pinj (xO j) P end. - Definition mkPX P i Q := + Definition mkPX P i Q := match P with | Pc c => if c ?=! cO then mkPinj xH Q else PX P i Q | Pinj _ _ => PX P i Q @@ -142,20 +142,20 @@ Section MakeRingPol. Definition mkXi i := PX P1 i P0. Definition mkX := mkXi 1. - + (** Opposite of addition *) - - Fixpoint Popp (P:Pol) : Pol := + + Fixpoint Popp (P:Pol) : Pol := match P with | Pc c => Pc (-! c) | Pinj j Q => Pinj j (Popp Q) | PX P i Q => PX (Popp P) i (Popp Q) end. - + Notation "-- P" := (Popp P). (** Addition et subtraction *) - + Fixpoint PaddC (P:Pol) (c:C) {struct P} : Pol := match P with | Pc c1 => Pc (c1 +! c) @@ -178,39 +178,39 @@ Section MakeRingPol. Fixpoint PaddI (j:positive) (P:Pol){struct P} : Pol := match P with | Pc c => mkPinj j (PaddC Q c) - | Pinj j' Q' => + | Pinj j' Q' => match ZPminus 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') end - | PX P i Q' => + | 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') | xI j => PX P i (PaddI (xO j) Q') - end + end end. Fixpoint PsubI (j:positive) (P:Pol){struct P} : Pol := match P with | Pc c => mkPinj j (PaddC (--Q) c) - | Pinj j' Q' => + | Pinj j' Q' => match ZPminus 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') end - | PX P i Q' => + | 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') | xI j => PX P i (PsubI (xO j) Q') - end + end end. - + Variable P' : Pol. - + Fixpoint PaddX (i':positive) (P:Pol) {struct P} : Pol := match P with | Pc c => PX P' i' P @@ -245,7 +245,7 @@ Section MakeRingPol. end end. - + End PopI. Fixpoint Padd (P P': Pol) {struct P'} : Pol := @@ -255,12 +255,12 @@ Section MakeRingPol. | PX P' i' Q' => match P with | Pc c => PX P' i' (PaddC Q' c) - | Pinj j Q => + | 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') | xI j => PX P' i' (Padd (Pinj (xO j) Q) Q') - end + end | PX P i Q => match ZPminus i i' with | Zpos k => mkPX (Padd (PX P k P0) P') i' (Padd Q Q') @@ -278,12 +278,12 @@ Section MakeRingPol. | PX P' i' Q' => match P with | Pc c => PX (--P') i' (*(--(PsubC Q' c))*) (PaddC (--Q') c) - | Pinj j Q => + | 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') | xI j => PX (--P') i' (Psub (Pinj (xO j) Q) Q') - end + end | PX P i Q => match ZPminus i i' with | Zpos k => mkPX (Psub (PX P k P0) P') i' (Psub Q Q') @@ -293,8 +293,8 @@ Section MakeRingPol. end end. Notation "P -- P'" := (Psub P P'). - - (** Multiplication *) + + (** Multiplication *) Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol := match P with @@ -306,14 +306,14 @@ Section MakeRingPol. Definition PmulC P c := if c ?=! cO then P0 else if c ?=! cI then P else PmulC_aux P c. - - Section PmulI. + + Section PmulI. Variable Pmul : Pol -> Pol -> Pol. Variable Q : Pol. Fixpoint PmulI (j:positive) (P:Pol) {struct P} : Pol := match P with | Pc c => mkPinj j (PmulC Q c) - | Pinj j' Q' => + | Pinj j' Q' => match ZPminus j' j with | Zpos k => mkPinj j (Pmul (Pinj k Q') Q) | Z0 => mkPinj j (Pmul Q' Q) @@ -326,7 +326,7 @@ Section MakeRingPol. | xI j' => mkPX (PmulI j P') i' (PmulI (xO j') Q') end end. - + End PmulI. (* A symmetric version of the multiplication *) @@ -338,10 +338,10 @@ Section MakeRingPol. match P with | Pc c => PmulC P'' c | Pinj j Q => - let QQ' := + let QQ' := match j with | xH => Pmul Q Q' - | xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q' + | xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q' | xI j => Pmul (Pinj (xO j) Q) Q' end in mkPX (Pmul P P') i' QQ' @@ -352,15 +352,15 @@ Section MakeRingPol. let PP' := Pmul P P' in (mkPX (mkPX PP' i P0 ++ QP') i' P0) ++ mkPX PQ' i QQ' end - 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' => + | PX P' i' Q' => (mkPX (Pmul_aux P P') i' P0) ++ (PmulI Pmul_aux Q' xH P) end. @@ -368,7 +368,7 @@ Section MakeRingPol. match P with | Pc c => PmulC P' c | Pinj j Q => PmulI Pmul_aux Q j P' - | PX P i Q => + | PX P i Q => (mkPX (Pmul_aux P P') i P0) ++ (PmulI Pmul_aux Q xH P') end. *) @@ -378,7 +378,7 @@ Section MakeRingPol. match P with | Pc c => Pc (c *! c) | Pinj j Q => Pinj j (Psquare Q) - | PX P i Q => + | PX P i Q => let twoPQ := Pmul P (mkPinj xH (PmulC Q (cI +! cI))) in let Q2 := Psquare Q in let P2 := Psquare P in @@ -386,10 +386,10 @@ Section MakeRingPol. end. (** Monomial **) - + Inductive Mon: Set := - mon0: Mon - | zmon: positive -> Mon -> Mon + mon0: Mon + | zmon: positive -> Mon -> Mon | vmon: positive -> Mon -> Mon. Fixpoint Mphi(l:list R) (M: Mon) {struct M} : R := @@ -399,7 +399,7 @@ Section MakeRingPol. | vmon i M1 => let x := hd 0 l in let xi := pow_pos rmul x i in - (Mphi (tail l) M1) * xi + (Mphi (tail l) M1) * xi end. Definition mkZmon j M := @@ -409,8 +409,8 @@ Section MakeRingPol. match j with xH => M | _ => mkZmon (Ppred j) M end. Definition mkVmon i M := - match M with - | mon0 => vmon i mon0 + match M with + | mon0 => vmon i mon0 | zmon j m => vmon i (zmon_pred j m) | vmon i' m => vmon (i+i') m end. @@ -462,35 +462,35 @@ Section MakeRingPol. Definition POneSubst (P1: Pol) (cM1: C * Mon) (P2: Pol): option Pol := let (c,M1) := cM1 in let (Q1,R1) := MFactor P1 c M1 in - match R1 with - (Pc c) => if c ?=! cO then None + match R1 with + (Pc c) => if c ?=! cO then None else Some (Padd Q1 (Pmul P2 R1)) | _ => Some (Padd Q1 (Pmul P2 R1)) end. Fixpoint PNSubst1 (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat) {struct n}: Pol := - match POneSubst P1 cM1 P2 with + match POneSubst P1 cM1 P2 with Some P3 => match n with S n1 => PNSubst1 P3 cM1 P2 n1 | _ => P3 end | _ => P1 end. Definition PNSubst (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat): option Pol := - match POneSubst P1 cM1 P2 with + match POneSubst P1 cM1 P2 with Some P3 => match n with S n1 => Some (PNSubst1 P3 cM1 P2 n1) | _ => None end | _ => None end. - - Fixpoint PSubstL1 (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: + + Fixpoint PSubstL1 (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: Pol := - match LM1 with + 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 := - match LM1 with + match LM1 with cons (M1,P2) LM2 => - match PNSubst P1 M1 P2 n with + match PNSubst P1 M1 P2 n with Some P3 => Some (PSubstL1 P3 LM2 n) | None => PSubstL P1 LM2 n end @@ -498,7 +498,7 @@ Section MakeRingPol. end. Fixpoint PNSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (m n: nat) {struct m}: Pol := - match PSubstL P1 LM1 n with + match PSubstL P1 LM1 n with Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end | _ => P1 end. @@ -509,10 +509,10 @@ Section MakeRingPol. match P with | Pc c => [c] | Pinj j Q => Pphi (jump j l) Q - | PX P i 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) + (Pphi l P) * xi + (Pphi (tail l) Q) end. Reserved Notation "P @ l " (at level 10, no associativity). @@ -546,8 +546,8 @@ Section MakeRingPol. rewrite Psucc_o_double_minus_one_eq_xO;trivial. simpl;trivial. Qed. - - Lemma Peq_ok : forall P P', + + Lemma Peq_ok : forall P P', (P ?== P') = true -> forall l, P@l == P'@ l. Proof. induction P;destruct P';simpl;intros;try discriminate;trivial. @@ -580,10 +580,10 @@ Section MakeRingPol. rewrite <-jump_Pplus;rewrite Pplus_comm;rrefl. Qed. - Let pow_pos_Pplus := + Let pow_pos_Pplus := pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc). - Lemma mkPX_ok : forall l P i Q, + 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). Proof. intros l P i Q;unfold mkPX. @@ -616,8 +616,8 @@ Section MakeRingPol. | -! ?x => rewrite ((morph_opp CRmorph) x) end end)); - rsimpl; simpl. - + rsimpl; simpl. + Lemma PaddC_ok : forall c P l, (PaddC P c)@l == P@l + [c]. Proof. induction P;simpl;intros;Esimpl;trivial. @@ -637,7 +637,7 @@ Section MakeRingPol. induction P;simpl;intros;Esimpl;trivial. rewrite IHP1;rewrite IHP2;rsimpl. mul_push ([c]);rrefl. - Qed. + Qed. Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c]. Proof. @@ -660,7 +660,7 @@ Section MakeRingPol. Ltac Esimpl2 := Esimpl; repeat (progress ( - match goal with + 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) @@ -684,7 +684,7 @@ Section MakeRingPol. rewrite IHP2;simpl. rewrite jump_Pdouble_minus_one;rsimpl. rewrite IHP';rsimpl. - destruct P;simpl. + destruct P;simpl. Esimpl2;add_push [c];rrefl. destruct p0;simpl;Esimpl2. rewrite IHP'2;simpl. @@ -699,7 +699,7 @@ Section MakeRingPol. rewrite H;rewrite Pplus_comm. rewrite pow_pos_Pplus;rsimpl. add_push (P3 @ (tail l));rrefl. - assert (forall P k l, + 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). @@ -727,7 +727,7 @@ Section MakeRingPol. 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';rsimpl. rewrite H;Esimpl. rewrite IHP';Esimpl. rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl. rewrite H;Esimpl. rewrite IHP. @@ -736,8 +736,8 @@ Section MakeRingPol. rewrite IHP2;simpl;rsimpl. rewrite IHP2;simpl. rewrite jump_Pdouble_minus_one;rsimpl. - rewrite IHP';rsimpl. - destruct P;simpl. + 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. @@ -752,7 +752,7 @@ Section MakeRingPol. rewrite H;rewrite Pplus_comm. rewrite pow_pos_Pplus;rsimpl. add_push (P3 @ (tail l));rrefl. - assert (forall P k l, + 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. @@ -775,8 +775,8 @@ Section MakeRingPol. Qed. (* Proof for the symmetriv version *) - Lemma PmulI_ok : - forall P', + 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). @@ -801,8 +801,8 @@ Section MakeRingPol. Qed. (* - Lemma PmulI_ok : - forall P', + 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). @@ -846,7 +846,7 @@ Section MakeRingPol. 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 + | 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. @@ -886,8 +886,8 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. Mphi l (mkZmon j M) == Mphi l (zmon j M). intros M j l; case M; simpl; intros; rsimpl. Qed. - - Lemma zmon_pred_ok : forall M j l, + + Lemma zmon_pred_ok : forall M j l, Mphi (tail l) (zmon_pred j M) == Mphi l (zmon j M). Proof. destruct j; simpl;intros auto; rsimpl. @@ -902,7 +902,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl. Qed. - Lemma Mcphi_ok: forall P c l, + Lemma Mcphi_ok: forall P c l, let (Q,R) := CFactor P c in P@l == Q@l + (phi c) * (R@l). Proof. @@ -924,7 +924,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. rewrite (ARadd_comm ARth); rsimpl. Qed. - Lemma Mphi_ok: forall P (cM: C * Mon) l, + 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). @@ -951,7 +951,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. 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)); + 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)). @@ -973,14 +973,14 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. apply (Radd_ext Reqe); rsimpl. rewrite (ARadd_comm ARth); rsimpl. intros j M1. - generalize (Hrec1 (c,zmon j M1) l); + 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)); + 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. + rsimpl. apply radd_ext; rsimpl. rewrite (ARadd_comm ARth); rsimpl. apply radd_ext; rsimpl. @@ -1002,7 +1002,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. repeat (rewrite <-(ARmul_assoc ARth)). apply rmul_ext; rsimpl. rewrite (ARmul_comm ARth); rsimpl. - generalize (Hrec1 (c, vmon (j - i) M1) l); + 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. @@ -1020,7 +1020,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. apply rmul_ext; rsimpl. rewrite <- pow_pos_Pplus. rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl. - generalize (Hrec1 (c, mkZmon 1 M1) l); + 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. @@ -1064,7 +1064,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. 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. + 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. @@ -1092,18 +1092,18 @@ Proof. injection H2; intros; subst; rsimpl. rewrite Padd_ok. rewrite Pmul_ok; rsimpl. - Qed. + 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. Proof. intros n; elim n; simpl; auto. intros P2 M1 P3 l H. - generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); + 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); + 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. Qed. @@ -1112,15 +1112,15 @@ Proof. PNSubst P1 M1 P2 n = Some P3 -> [fst M1] * Mphi l (snd M1) == 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); + 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 P5 H1; case n; try (intros; discriminate). intros n1 H2; injection H2; intros; subst. rewrite <- PNSubst1_ok; auto. Qed. - Fixpoint MPcond (LM1: list (C * Mon * Pol)) (l: list R) {struct LM1} : Prop := - match LM1 with + 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. @@ -1189,7 +1189,7 @@ Proof. Strategy expand [PEeval]. (** Correctness proofs *) - + Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l. Proof. destruct p;simpl;intros;Esimpl;trivial. @@ -1198,11 +1198,11 @@ Strategy expand [PEeval]. rewrite nth_Pdouble_minus_one;rrefl. Qed. - Ltac Esimpl3 := + 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). + end;Esimpl2;try rrefl;try apply (ARadd_comm ARth). (* Power using the chinise algorithm *) (*Section POWER. @@ -1213,13 +1213,13 @@ Strategy expand [PEeval]. | 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. @@ -1228,28 +1228,28 @@ Strategy expand [PEeval]. 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. *) Section POWER. Variable subst_l : Pol -> Pol. Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol := match p with - | xH => subst_l (Pmul res P) + | xH => subst_l (Pmul 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) end. - + Definition Ppow_N P n := match n with | N0 => P1 | 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. Proof. @@ -1257,11 +1257,11 @@ Section POWER. induction p;simpl;intros;try rewrite subst_l_ok; repeat rewrite Pmul_ok;repeat rewrite IHp. rsimpl. mul_push (P@l);rsimpl. rsimpl. 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. rewrite Ppow_pos_ok by trivial. Esimpl. Qed. - + End POWER. (** Normalization and rewriting *) @@ -1276,86 +1276,86 @@ Section POWER. Fixpoint norm_aux (pe:PExpr) : Pol := match pe with | PEc c => Pc c - | PEX j => mk_X j + | PEX j => mk_X j | PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1) - | PEadd pe1 (PEopp pe2) => + | 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) + | 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). - (* + (* Fixpoint norm_subst (pe:PExpr) : Pol := match pe with | PEc c => Pc c - | PEX j => subst_l (mk_X j) + | PEX j => subst_l (mk_X j) | PEadd (PEopp pe1) pe2 => Psub (norm_subst pe2) (norm_subst pe1) - | PEadd pe1 (PEopp pe2) => + | 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) + | 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 end. - Lemma norm_subst_spec : + Lemma norm_subst_spec : forall l pe, MPcond lmp l -> - PEeval l pe == (norm_subst pe)@l. + PEeval l pe == (norm_subst pe)@l. Proof. - intros;assert (subst_l_ok:forall P, (subst_l P)@l == P@l). + 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;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; + induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; repeat rewrite Pmul_ok;rrefl. Qed. *) - Lemma norm_aux_spec : + Lemma norm_aux_spec : forall l pe, MPcond lmp l -> - PEeval l pe == (norm_aux pe)@l. + 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;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; + induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; repeat rewrite Pmul_ok;rrefl. Qed. - Lemma norm_subst_spec : + Lemma norm_subst_spec : forall l pe, MPcond lmp l -> PEeval l pe == (norm_subst pe)@l. Proof. intros;unfold norm_subst. unfold subst_l;rewrite <- PNSubstL_ok;trivial. apply norm_aux_spec. trivial. - Qed. - + Qed. + End NORM_SUBST_REC. - + Fixpoint interp_PElist (l:list R) (lpe:list (PExpr*PExpr)) {struct lpe} : Prop := match lpe with | nil => True - | (me,pe)::lpe => + | (me,pe)::lpe => match lpe with | nil => PEeval l me == PEeval l pe | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe @@ -1366,9 +1366,9 @@ Section POWER. match P with | Pc c => if (c ?=! cO) then None else Some (c, mon0) | Pinj j P => - match mon_of_pol P with + match mon_of_pol P with | None => None - | Some (c,m) => Some (c, mkZmon j m) + | Some (c,m) => Some (c, mkZmon j m) end | PX P i Q => if Peq Q P0 then @@ -1384,15 +1384,15 @@ Section POWER. | nil => nil | (me,pe)::lpe => match mon_of_pol (norm_subst 0 nil me) with - | None => mk_monpol_list lpe - | Some m => (m,norm_subst 0 nil pe):: mk_monpol_list lpe + | None => mk_monpol_list lpe + | Some m => (m,norm_subst 0 nil pe):: mk_monpol_list lpe end end. Lemma mon_of_pol_ok : forall P m, mon_of_pol P = Some m -> forall l, [fst m] * Mphi l (snd m) == P@l. Proof. - induction P;simpl;intros;Esimpl. + induction P;simpl;intros;Esimpl. assert (H1 := (morph_eq CRmorph) c cO). destruct (c ?=! cO). discriminate. @@ -1418,14 +1418,14 @@ Section POWER. discriminate. intros;discriminate. Qed. - - Lemma interp_PElist_ok : forall l lpe, + + Lemma interp_PElist_ok : forall l lpe, interp_PElist l lpe -> MPcond (mk_monpol_list lpe) l. Proof. induction lpe;simpl. trivial. destruct a;simpl;intros. assert (HH:=mon_of_pol_ok (norm_subst 0 nil p)); - destruct (mon_of_pol (norm_subst 0 nil p)). + destruct (mon_of_pol (norm_subst 0 nil p)). split. rewrite <- norm_subst_spec by exact I. destruct lpe;try destruct H;rewrite <- H; @@ -1440,7 +1440,7 @@ Section POWER. Proof. intros;apply norm_subst_spec. apply interp_PElist_ok;trivial. Qed. - + Lemma ring_correct : forall n l lpe pe1 pe2, interp_PElist l lpe -> (let lmp := mk_monpol_list lpe in @@ -1448,9 +1448,9 @@ Section POWER. PEeval l pe1 == PEeval l pe2. Proof. simpl;intros. - do 2 (rewrite (norm_subst_ok n l lpe);trivial). + do 2 (rewrite (norm_subst_ok n l lpe);trivial). apply Peq_ok;trivial. - Qed. + Qed. @@ -1467,23 +1467,23 @@ Section POWER. Variable mkopp_pow : R -> positive -> R. (* [mkmult_pow r x p] = r * x^p *) Variable mkmult_pow : R -> R -> positive -> R. - + Fixpoint mkmult_rec (r:R) (lm:list (R*positive)) {struct lm}: R := match lm with | nil => r - | cons (x,p) t => mkmult_rec (mkmult_pow r x p) t + | cons (x,p) t => mkmult_rec (mkmult_pow r x p) t end. Definition mkmult1 lm := match lm with | nil => 1 - | cons (x,p) t => mkmult_rec (mkpow x p) t + | cons (x,p) t => mkmult_rec (mkpow x p) t end. Definition mkmultm1 lm := match lm with | nil => ropp rI - | cons (x,p) t => mkmult_rec (mkopp_pow x p) t + | cons (x,p) t => mkmult_rec (mkopp_pow x p) t end. Definition mkmult_c_pos c lm := @@ -1493,11 +1493,11 @@ Section POWER. Definition mkmult_c c lm := match get_sign c with | None => mkmult_c_pos c lm - | Some c' => + | Some c' => if c' ?=! cI then mkmultm1 (rev' lm) else mkmult_rec [c] (rev' lm) end. - + Definition mkadd_mult rP c lm := match get_sign c with | None => rP + mkmult_c_pos c lm @@ -1505,49 +1505,49 @@ Section POWER. end. Definition add_pow_list (r:R) n l := - match n with + match n with | N0 => l | Npos p => (r,p)::l end. - Fixpoint add_mult_dev + Fixpoint add_mult_dev (rP:R) (P:Pol) (fv:list R) (n:N) (lm:list (R*positive)) {struct P} : R := match P with - | Pc c => + | Pc c => let lm := add_pow_list (hd 0 fv) n lm in mkadd_mult rP c lm - | Pinj j Q => + | Pinj j Q => add_mult_dev rP Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm) - | PX P i Q => + | PX P i Q => let rP := add_mult_dev rP P fv (Nplus (Npos i) n) lm in - if Q ?== P0 then rP + if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) N0 (add_pow_list (hd 0 fv) n lm) end. - Fixpoint mult_dev (P:Pol) (fv : list R) (n:N) + Fixpoint mult_dev (P:Pol) (fv : list R) (n:N) (lm:list (R*positive)) {struct P} : R := - (* P@l * (hd 0 l)^n * lm *) + (* 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) - | PX P i Q => + | PX P i Q => let rP := mult_dev P fv (Nplus (Npos i) n) lm in - if Q ?== P0 then rP - else + if Q ?== P0 then rP + else let lmq := add_pow_list (hd 0 fv) n lm in add_mult_dev rP Q (tail fv) N0 lmq - end. + end. Definition Pphi_avoid fv P := mult_dev P fv N0 nil. - + Fixpoint r_list_pow (l:list (R*positive)) : R := match l with | nil => rI - | cons (r,p) l => pow_pos rmul r p * r_list_pow l + | cons (r,p) l => pow_pos rmul r p * r_list_pow l end. Hypothesis mkpow_spec : forall r p, mkpow r p == pow_pos rmul r p. - Hypothesis mkopp_pow_spec : forall r p, mkopp_pow r p == - (pow_pos rmul r p). + Hypothesis mkopp_pow_spec : forall r p, mkopp_pow r p == - (pow_pos rmul r p). Hypothesis mkmult_pow_spec : forall r x p, mkmult_pow r x p == r * pow_pos rmul x p. Lemma mkmult_rec_ok : forall lm r, mkmult_rec r lm == r * r_list_pow lm. @@ -1571,7 +1571,7 @@ Section POWER. Lemma r_list_pow_rev : forall l, r_list_pow (rev' l) == r_list_pow l. Proof. - assert + assert (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. @@ -1583,7 +1583,7 @@ Section POWER. Proof. intros;unfold mkmult_c_pos;simpl. assert (H := (morph_eq CRmorph) c cI). - rewrite <- r_list_pow_rev; destruct (c ?=! cI). + rewrite <- r_list_pow_rev; destruct (c ?=! cI). rewrite H;trivial;Esimpl. apply mkmult1_ok. apply mkmult_rec_ok. Qed. @@ -1610,16 +1610,16 @@ Qed. rewrite mkmult_c_pos_ok;Esimpl. Qed. - Lemma add_pow_list_ok : + Lemma add_pow_list_ok : forall r n l, r_list_pow (add_pow_list r n l) == pow_N rI rmul r n * r_list_pow l. Proof. destruct n;simpl;intros;Esimpl. Qed. - Lemma add_mult_dev_ok : forall P rP fv n lm, + 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. Proof. - induction P;simpl;intros. + induction P;simpl;intros. rewrite mkadd_mult_ok. rewrite add_pow_list_ok; Esimpl. rewrite IHP. simpl. rewrite add_pow_list_ok; Esimpl. change (match P3 with @@ -1639,7 +1639,7 @@ Qed. rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. Qed. - Lemma mult_dev_ok : forall P fv n lm, + 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. Proof. induction P;simpl;intros;Esimpl. @@ -1669,14 +1669,14 @@ Qed. End EVALUATION. - Definition Pphi_pow := - let mkpow x p := + Definition Pphi_pow := + let mkpow x p := match p with xH => x | _ => rpow x (Cp_phi (Npos p)) end in let mkopp_pow x p := ropp (mkpow x p) in let mkmult_pow r x p := rmul r (mkpow x p) in Pphi_avoid mkpow mkopp_pow mkmult_pow. - Lemma local_mkpow_ok : + Lemma local_mkpow_ok : forall (r : R) (p : positive), match p with | xI _ => rpow r (Cp_phi (Npos p)) @@ -1684,13 +1684,13 @@ Qed. | 1 => r end == pow_pos rmul r p. Proof. intros r p;destruct p;try rewrite pow_th.(rpow_pow_N);reflexivity. 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. Qed. - Lemma ring_rw_pow_correct : forall n lH l, + Lemma ring_rw_pow_correct : forall n lH l, interp_PElist l lH -> forall lmp, mk_monpol_list lH = lmp -> forall pe npe, norm_subst n lmp pe = npe -> @@ -1701,22 +1701,22 @@ Qed. apply norm_subst_ok. trivial. Qed. - Fixpoint mkmult_pow (r x:R) (p: positive) {struct p} : R := + Fixpoint mkmult_pow (r x:R) (p: positive) {struct p} : R := match p with - | xH => r*x + | xH => r*x | xO p => mkmult_pow (mkmult_pow r x p) x p | xI p => mkmult_pow (mkmult_pow (r*x) x p) x p end. - + Definition mkpow x p := - match p with + match p with | xH => x | xO p => mkmult_pow x x (Pdouble_minus_one p) | xI p => mkmult_pow x x (xO p) end. - + Definition mkopp_pow x p := - match p with + match p with | xH => -x | xO p => mkmult_pow (-x) x (Pdouble_minus_one p) | xI p => mkmult_pow (-x) x (xO p) @@ -1726,31 +1726,31 @@ Qed. Lemma mkmult_pow_ok : forall p r x, mkmult_pow r x p == r*pow_pos rmul x p. Proof. - induction p;intros;simpl;Esimpl. + induction p;intros;simpl;Esimpl. repeat rewrite IHp;Esimpl. repeat rewrite IHp;Esimpl. Qed. - + Lemma mkpow_ok : forall p x, mkpow x p == pow_pos rmul 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. + 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. Qed. - + Lemma mkopp_pow_ok : forall p x, mkopp_pow x p == - pow_pos rmul 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. + 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. @@ -1765,7 +1765,7 @@ Qed. intros;apply mkmult_pow_ok. Qed. - Lemma ring_rw_correct : forall n lH l, + Lemma ring_rw_correct : forall n lH l, interp_PElist l lH -> forall lmp, mk_monpol_list lH = lmp -> forall pe npe, norm_subst n lmp pe = npe -> diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index 44e97bda7..e3eb418ad 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -6,7 +6,7 @@ Require Import BinList. Require Import InitialRing. Require Import Quote. Declare ML Module "newring_plugin". - + (* adds a definition t' on the normal form of t and an hypothesis id stating that t = t' (tries to produces a proof as small as possible) *) @@ -58,8 +58,8 @@ Ltac OnMainSubgoal H ty := Ltac ProveLemmaHyp lemma := match type of lemma with forall x', ?x = x' -> _ => - (fun kont => - let x' := fresh "res" in + (fun kont => + let x' := fresh "res" in let H := fresh "res_eq" in compute_assertion H x' x; let lemma' := constr:(lemma x' H) in @@ -72,8 +72,8 @@ Ltac ProveLemmaHyp lemma := Ltac ProveLemmaHyps lemma := match type of lemma with forall x', ?x = x' -> _ => - (fun kont => - let x' := fresh "res" in + (fun kont => + let x' := fresh "res" in let H := fresh "res_eq" in compute_assertion H x' x; let lemma' := constr:(lemma x' H) in @@ -134,7 +134,7 @@ Ltac ReflexiveRewriteTactic FV_tac SYN_tac LEMMA_tac MAIN_tac fv terms := (* extend the atom list *) let fv := list_fold_left FV_tac fv terms in - let RW_tac lemma := + let RW_tac lemma := let fcons term CONT_tac := let expr := SYN_tac term fv in (ApplyLemmaThenAndCont lemma expr MAIN_tac CONT_tac) in @@ -154,8 +154,8 @@ Ltac FV_hypo_tac mkFV req lH := list_fold_right FV_hypo_r_tac fv lH. Ltac mkHyp_tac C req Reify lH := - let mkHyp h res := - match h with + let mkHyp h res := + match h with | @mkhypo (req ?r1 ?r2) _ => let pe1 := Reify r1 in let pe2 := Reify r2 in @@ -173,9 +173,9 @@ Ltac proofHyp_tac lH := match l with | nil => constr:(I) | cons ?h nil => get_proof h - | cons ?h ?tl => + | cons ?h ?tl => let l := get_proof h in - let r := bh tl in + let r := bh tl in constr:(conj l r) end in bh lH. @@ -213,22 +213,22 @@ Ltac FV Cst CstPow add mul sub opp pow t fv := in TFV t fv. (* syntaxification of ring expressions *) -Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := +Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := let rec mkP t := let f := match Cst t with | InitialRing.NotConstant => - match t with - | (radd ?t1 ?t2) => + match t with + | (radd ?t1 ?t2) => fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(PEadd e1 e2) - | (rmul ?t1 ?t2) => + | (rmul ?t1 ?t2) => fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(PEmul e1 e2) - | (rsub ?t1 ?t2) => - fun _ => + | (rsub ?t1 ?t2) => + fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(PEsub e1 e2) | (ropp ?t1) => @@ -236,7 +236,7 @@ Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := let e1 := mkP t1 in constr:(PEopp e1) | (rpow ?t1 ?n) => match CstPow n with - | InitialRing.NotConstant => + | InitialRing.NotConstant => fun _ => let p := Find_at t fv in constr:(PEX C p) | ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c) end @@ -311,7 +311,7 @@ Ltac get_RingHypTac RNG := (* ring tactics *) Definition ring_subst_niter := (10*10*10)%nat. - + Ltac Ring RNG lemma lH := let req := get_Eq RNG in OnEquation req ltac:(fun lhs rhs => @@ -343,7 +343,7 @@ Ltac Ring_norm_gen f RNG lemma lH rl := let mkHyp := get_RingHypTac RNG in let mk_monpol := get_MonPol lemma in let fv := FV_hypo_tac mkFV ltac:(get_Eq RNG) lH in - let lemma_tac fv kont := + let lemma_tac fv kont := let lpe := mkHyp fv lH in let vlpe := fresh "list_hyp" in let vlmp := fresh "list_hyp_norm" in @@ -390,25 +390,25 @@ Ltac Ring_simplify_gen f RNG lH rl := end in let Heq := fresh "Heq" in intros Heq;clear Heq l; - Ring_norm_gen f RNG (lemma ring_subst_niter) lH rl; + Ring_norm_gen f RNG (lemma ring_subst_niter) lH rl; get_Post RNG (). Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H). -Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := +Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := let G := Get_goal in ring_lookup (PackRing Ring_simplify) [] rl G. -Tactic Notation (at level 0) +Tactic Notation (at level 0) "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := let G := Get_goal in ring_lookup (PackRing Ring_simplify) [lH] rl G. (* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *) -Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= +Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= let G := Get_goal in - let t := type of H in + let t := type of H in let g := fresh "goal" in set (g:= G); generalize H;clear H; @@ -416,10 +416,10 @@ Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= intro H; unfold g;clear g. -Tactic Notation - "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):= +Tactic Notation + "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):= let G := Get_goal in - let t := type of H in + let t := type of H in let g := fresh "goal" in set (g:= G); generalize H;clear H; diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 531ab3ca5..b3250a510 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -39,7 +39,7 @@ Section Power. Notation "x * y " := (rmul x y). Notation "x == y" := (req x y). - Hypothesis mul_ext : + 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_assoc : forall x y z, x * (y * z) == (x * y) * z. @@ -79,11 +79,11 @@ Section Power. simpl. apply (Seq_refl _ _ Rsth). Qed. - Definition pow_N (x:R) (p:N) := + Definition pow_N (x:R) (p:N) := match p with | N0 => rI | Npos p => pow_pos x p - end. + end. Definition id_phi_N (x:N) : N := x. @@ -109,12 +109,12 @@ Section DEFINITIONS. 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_0_l : forall n, 0*n == 0; 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 }. - + (** Almost Ring *) (*Almost ring are no ring : Ropp_def is missing **) Record almost_ring_theory : Prop := mk_art { @@ -129,7 +129,7 @@ Section DEFINITIONS. ARopp_mul_l : forall x y, -(x * y) == -x * y; ARopp_add : forall x y, -(x + y) == -x + -y; ARsub_def : forall x y, x - y == x + -y - }. + }. (** Ring *) Record ring_theory : Prop := mk_rt { @@ -145,7 +145,7 @@ Section DEFINITIONS. }. (** Equality is extensional *) - + Record sring_eq_ext : Prop := mk_seqe { (* SRing operators are compatible with equality *) SRadd_ext : @@ -163,12 +163,12 @@ Section DEFINITIONS. Ropp_ext : forall x1 x2, x1 == x2 -> -x1 == -x2 }. - (** Interpretation morphisms definition*) + (** Interpretation morphisms definition*) Section MORPHISM. Variable C:Type. Variable (cO cI : C) (cadd cmul csub : C->C->C) (copp : C->C). Variable ceqb : C->C->bool. - (* [phi] est un morphisme de [C] dans [R] *) + (* [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). @@ -180,7 +180,7 @@ Section DEFINITIONS. Smorph1 : [cI] == 1; Smorph_add : forall x y, [x +! y] == [x]+[y]; Smorph_mul : forall x y, [x *! y] == [x]*[y]; - Smorph_eq : forall x y, x?=!y = true -> [x] == [y] + Smorph_eq : forall x y, x?=!y = true -> [x] == [y] }. (* for rings*) @@ -191,7 +191,7 @@ Section DEFINITIONS. morph_sub : forall x y, [x -! y] == [x]-[y]; morph_mul : forall x y, [x *! y] == [x]*[y]; morph_opp : forall x, [-!x] == -[x]; - morph_eq : forall x y, x?=!y = true -> [x] == [y] + morph_eq : forall x y, x?=!y = true -> [x] == [y] }. Section SIGN. @@ -213,7 +213,7 @@ Section DEFINITIONS. }. End DIV. - End MORPHISM. + End MORPHISM. (** Identity is a morphism *) Variable Rsth : Setoid_Theory R req. @@ -231,8 +231,8 @@ Section DEFINITIONS. Section POWER. Variable Cpow : Set. Variable Cp_phi : N -> Cpow. - Variable rpow : R -> Cpow -> R. - + Variable rpow : R -> Cpow -> R. + Record power_theory : Prop := mkpow_th { rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) }. @@ -241,7 +241,7 @@ Section DEFINITIONS. Definition pow_N_th := mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth). - + End DEFINITIONS. @@ -268,7 +268,7 @@ Section ALMOST_RING. Variable Rsth : Setoid_Theory R req. Add Setoid R req Rsth as R_setoid2. Ltac sreflexivity := apply (Seq_refl _ _ Rsth). - + Section SEMI_RING. Variable SReqe : sring_eq_ext radd rmul req. Add Morphism radd : radd_ext1. exact (SRadd_ext SReqe). Qed. @@ -278,7 +278,7 @@ Section ALMOST_RING. (** Every semi ring can be seen as an almost ring, by taking : -x = x and x - y = x + y *) Definition SRopp (x:R) := x. Notation "- x" := (SRopp x). - + Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y). Lemma SRopp_ext : forall x y, x == y -> -x == -y. @@ -296,7 +296,7 @@ Section ALMOST_RING. Lemma SRopp_add : forall x y, -(x + y) == -x + -y. Proof. intros;sreflexivity. Qed. - + Lemma SRsub_def : forall x y, x - y == x + -y. Proof. intros;sreflexivity. Qed. @@ -306,7 +306,7 @@ Section ALMOST_RING. (SRmul_1_l SRth) (SRmul_0_l SRth) (SRmul_comm SRth) (SRmul_assoc SRth) (SRdistr_l SRth) SRopp_mul_l SRopp_add SRsub_def). - + (** Identity morphism for semi-ring equipped with their almost-ring structure*) Variable reqb : R->R->bool. @@ -337,12 +337,12 @@ Section ALMOST_RING. Qed. End SEMI_RING. - + Variable Reqe : ring_eq_ext radd rmul ropp req. Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. Add Morphism rmul : rmul_ext2. exact (Rmul_ext Reqe). Qed. Add Morphism ropp : ropp_ext2. exact (Ropp_ext Reqe). Qed. - + Section RING. Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. @@ -368,7 +368,7 @@ Section ALMOST_RING. rewrite (Rth.(Radd_comm) (-x));rewrite (Ropp_def Rth). rewrite Rmul_0_l;rewrite (Radd_0_l Rth);sreflexivity. Qed. - + Lemma Ropp_add : forall x y, -(x + y) == -x + -y. Proof. intros x y;rewrite <- ((Radd_0_l Rth) (-(x+y))). @@ -387,7 +387,7 @@ Section ALMOST_RING. rewrite ((Radd_comm Rth) (-x) 0);rewrite (Radd_0_l Rth). apply (Radd_comm Rth). Qed. - + Lemma Ropp_opp : forall x, - -x == x. Proof. intros x; rewrite <- (Radd_0_l Rth (- -x)). @@ -402,7 +402,7 @@ Section ALMOST_RING. (Rmul_1_l Rth) Rmul_0_l (Rmul_comm Rth) (Rmul_assoc Rth) (Rdistr_l Rth) Ropp_mul_l Ropp_add (Rsub_def Rth)). - (** Every semi morphism between two rings is a morphism*) + (** Every semi morphism between two rings is a morphism*) Variable C : Type. Variable (cO cI : C) (cadd cmul csub: C->C->C) (copp : C -> C). Variable (ceq : C -> C -> Prop) (ceqb : C -> C -> bool). @@ -431,7 +431,7 @@ Section ALMOST_RING. rewrite (Smorph0 Smorph). rewrite (Radd_comm Rth (-[x])). apply (Radd_0_l Rth);sreflexivity. - Qed. + Qed. Lemma Smorph_sub : forall x y, [x -! y] == [x] - [y]. Proof. @@ -439,11 +439,11 @@ Section ALMOST_RING. rewrite (Smorph_add Smorph);rewrite Smorph_opp;sreflexivity. Qed. - Lemma Smorph_morph : ring_morph 0 1 radd rmul rsub ropp req + 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) + (Smorph0 Smorph) (Smorph1 Smorph) (Smorph_add Smorph) Smorph_sub (Smorph_mul Smorph) Smorph_opp (Smorph_eq Smorph)). @@ -462,7 +462,7 @@ Qed. 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 (x1 - y1) with (x1 + -y1). setoid_replace (x2 - y2) with (x2 + -y2). rewrite H;rewrite H0;sreflexivity. apply (ARsub_def ARth). @@ -483,10 +483,10 @@ Qed. | 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 ARmul_1_r : forall x, x * 1 == x. Proof. intros;mrewrite. Qed. @@ -495,7 +495,7 @@ Qed. Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y. Proof. - intros;mrewrite. + intros;mrewrite. repeat rewrite (ARth.(ARmul_comm) z);sreflexivity. Qed. @@ -516,7 +516,7 @@ Qed. intros;rewrite <-((ARmul_assoc ARth) x). rewrite ((ARmul_comm ARth) x);sreflexivity. Qed. - + Lemma ARmul_assoc2 : forall x y z, (y * x) * z == (y * z) * x. Proof. intros; repeat rewrite <- (ARmul_assoc ARth); @@ -592,17 +592,17 @@ Ltac gen_srewrite Rsth Reqe ARth := Ltac gen_add_push add Rsth Reqe ARth x := repeat (match goal with - | |- context [add (add ?y x) ?z] => + | |- context [add (add ?y x) ?z] => progress rewrite (ARadd_assoc2 Rsth Reqe ARth x y z) - | |- context [add (add x ?y) ?z] => + | |- context [add (add x ?y) ?z] => progress rewrite (ARadd_assoc1 Rsth ARth x y z) end). Ltac gen_mul_push mul Rsth Reqe ARth x := repeat (match goal with - | |- context [mul (mul ?y x) ?z] => + | |- context [mul (mul ?y x) ?z] => progress rewrite (ARmul_assoc2 Rsth Reqe ARth x y z) - | |- context [mul (mul x ?y) ?z] => + | |- context [mul (mul x ?y) ?z] => progress rewrite (ARmul_assoc1 Rsth ARth x y z) end). diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v index 942915abf..4cb5a05a3 100644 --- a/plugins/setoid_ring/ZArithRing.v +++ b/plugins/setoid_ring/ZArithRing.v @@ -21,7 +21,7 @@ Ltac Zcst t := end. Ltac isZpow_coef t := - match t with + match t with | Zpos ?p => isPcst p | Z0 => constr:true | _ => constr:false @@ -41,18 +41,18 @@ Ltac Zpow_tac t := Ltac Zpower_neg := repeat match goal with - | [|- ?G] => - match G with + | [|- ?G] => + match G with | context c [Zpower _ (Zneg _)] => let t := context c [Z0] in change t end - end. + end. Add Ring Zr : Zth (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], power_tac Zpower_theory [Zpow_tac], - (* The two following option are not needed, it is the default chose when the set of + (* The two following option are not needed, it is the default chose when the set of coefficiant is usual ring Z *) div (InitialRing.Ztriv_div_th (@Eqsth Z) (@IDphi Z)), sign get_signZ_th). diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 14d10e54f..c6d9bf44a 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -108,9 +108,9 @@ let protect_tac_in map id = TACTIC EXTEND protect_fv - [ "protect_fv" string(map) "in" ident(id) ] -> + [ "protect_fv" string(map) "in" ident(id) ] -> [ protect_tac_in map id ] -| [ "protect_fv" string(map) ] -> +| [ "protect_fv" string(map) ] -> [ protect_tac map ] END;; @@ -128,8 +128,8 @@ TACTIC EXTEND closed_term END ;; -TACTIC EXTEND echo -| [ "echo" constr(t) ] -> +TACTIC EXTEND echo +| [ "echo" constr(t) ] -> [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] END;; @@ -159,11 +159,11 @@ let ic c = let ty c = Typing.type_of (Global.env()) Evd.empty c let decl_constant na c = - mkConst(declare_constant (id_of_string na) (DefinitionEntry + mkConst(declare_constant (id_of_string na) (DefinitionEntry { const_entry_body = c; const_entry_type = None; const_entry_opaque = true; - const_entry_boxed = true}, + const_entry_boxed = true}, IsProof Lemma)) (* Calling a global tactic *) @@ -187,7 +187,7 @@ let ltac_record flds = let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c) -let dummy_goal env = +let dummy_goal env = {Evd.it = Evd.make_evar (named_context_val env) mkProp; Evd.sigma = Evd.empty} @@ -228,7 +228,7 @@ let coq_eq = coq_constant "eq" let lapp f args = mkApp(Lazy.force f,args) -let dest_rel0 t = +let dest_rel0 t = match kind_of_term t with | App(f,args) when Array.length args >= 2 -> let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in @@ -321,9 +321,9 @@ let _ = add_map "ring" (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); - pol_cst "Pphi_pow", + pol_cst "Pphi_pow", (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); - (* PEeval: evaluate morphism and polynomial, protect ring + (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)]) @@ -379,7 +379,7 @@ let find_ring_structure env sigma l = (str"cannot find a declared ring structure for equality"++ spc()++str"\""++pr_constr req++str"\"")) *) -let _ = +let _ = Summary.declare_summary "tactic-new-ring-table" { Summary.freeze_function = (fun () -> !from_carrier,!from_relation,!from_name); @@ -397,11 +397,11 @@ let add_entry (sp,_kn) e = *) from_carrier := Cmap.add e.ring_carrier e !from_carrier; from_relation := Cmap.add e.ring_req e !from_relation; - from_name := Spmap.add sp e !from_name + from_name := Spmap.add sp e !from_name -let subst_th (_,subst,th) = - let c' = subst_mps subst th.ring_carrier in +let subst_th (_,subst,th) = + let c' = subst_mps subst th.ring_carrier in let eq' = subst_mps subst th.ring_req in let set' = subst_mps subst th.ring_setoid in let ext' = subst_mps subst th.ring_ext in @@ -454,11 +454,11 @@ let (theory_to_obj, obj_to_theory) = let setoid_of_relation env a r = let evm = Evd.empty in - try + try lapp coq_mk_Setoid - [|a ; r ; - Rewrite.get_reflexive_proof env evm a r ; - Rewrite.get_symmetric_proof env evm a r ; + [|a ; r ; + Rewrite.get_reflexive_proof env evm a r ; + Rewrite.get_symmetric_proof env evm a r ; Rewrite.get_transitive_proof env evm a r |] with Not_found -> error "cannot find setoid relation" @@ -551,9 +551,9 @@ let ring_equality (r,add,mul,opp,req) = error "ring opposite should be declared as a morphism" in let op_morph = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in - Flags.if_verbose + Flags.if_verbose msgnl - (str"Using setoid \""++pr_constr req++str"\""++spc()++ + (str"Using setoid \""++pr_constr req++str"\""++spc()++ str"and morphisms \""++pr_constr add_m_lem ++ str"\","++spc()++ str"\""++pr_constr mul_m_lem++ str"\""++spc()++str"and \""++pr_constr opp_m_lem++ @@ -562,13 +562,13 @@ let ring_equality (r,add,mul,opp,req) = | None -> (Flags.if_verbose msgnl - (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ + (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ str"and morphisms \""++pr_constr add_m_lem ++ str"\""++spc()++str"and \""++ pr_constr mul_m_lem++str"\""); op_smorph r add mul req add_m_lem mul_m_lem) in (setoid,op_morph) - + let build_setoid_params r add mul opp req eqth = match eqth with Some th -> th @@ -652,18 +652,18 @@ let make_hyp env c = let make_hyp_list env lH = let carrier = Lazy.force coq_hypo in - List.fold_right + List.fold_right (fun c l -> lapp coq_cons [|carrier; (make_hyp env c); l|]) lH (lapp coq_nil [|carrier|]) -let interp_power env pow = +let interp_power env pow = let carrier = Lazy.force coq_hypo in match pow with - | None -> + | None -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in (TacArg(TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) - | Some (tac, spec) -> - let tac = + | Some (tac, spec) -> + let tac = match tac with | CstTac t -> Tacinterp.glob_tactic t | Closed lc -> @@ -674,8 +674,8 @@ let interp_power env pow = let interp_sign env sign = let carrier = Lazy.force coq_hypo in match sign with - | None -> lapp coq_None [|carrier|] - | Some spec -> + | None -> lapp coq_None [|carrier|] + | Some spec -> let spec = make_hyp env (ic spec) in lapp coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) @@ -683,8 +683,8 @@ let interp_sign env sign = let interp_div env div = let carrier = Lazy.force coq_hypo in match div with - | None -> lapp coq_None [|carrier|] - | Some spec -> + | None -> lapp coq_None [|carrier|] + | Some spec -> let spec = make_hyp env (ic spec) in lapp coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) @@ -695,12 +695,12 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div = let sigma = Evd.empty in let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in let (sth,ext) = build_setoid_params r add mul opp req eqth in - let (pow_tac, pspec) = interp_power env power in + let (pow_tac, pspec) = interp_power env power in let sspec = interp_sign env sign in let dspec = interp_div env div in let rk = reflect_coeff morphth in let params = - exec_tactic env 5 (zltac "ring_lemmas") + exec_tactic env 5 (zltac "ring_lemmas") (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in let lemma1 = constr_of params.(3) in let lemma2 = constr_of params.(4) in @@ -757,7 +757,7 @@ VERNAC ARGUMENT EXTEND ring_mod | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ] | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> - [ Pow_spec (Closed l, pow_spec) ] + [ Pow_spec (Closed l, pow_spec) ] | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> [ Pow_spec (CstTac cst_tac, pow_spec) ] | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] @@ -780,7 +780,7 @@ let process_ring_mods l = | Const_tac t -> set_once "tactic recognizing constants" cst_tac t | Pre_tac t -> set_once "preprocess tactic" pre t | Post_tac t -> set_once "postprocess tactic" post t - | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext) + | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext) | Pow_spec(t,spec) -> set_once "power" power (t,spec) | Sign_spec t -> set_once "sign" sign t | Div_spec t -> set_once "div" div t) l; @@ -797,7 +797,7 @@ END (* The tactics consist then only in a lookup in the ring database and call the appropriate ltac. *) -let make_args_list rl t = +let make_args_list rl t = match rl with | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2] | _ -> rl @@ -838,7 +838,7 @@ TACTIC EXTEND ring_lookup END - + (***********************************************************************) let new_field_path = @@ -861,12 +861,12 @@ let _ = add_map "field" (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); - pol_cst "Pphi_pow", + pol_cst "Pphi_pow", (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); - (* PEeval: evaluate morphism and polynomial, protect ring + (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot); - (* FEeval: evaluate morphism, protect field + (* FEeval: evaluate morphism, protect field operations and make recursive call on the var map *) my_constant "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; @@ -958,7 +958,7 @@ let find_field_structure env sigma l = (str"cannot find a declared field structure for equality"++ spc()++str"\""++pr_constr req++str"\"")) *) -let _ = +let _ = Summary.declare_summary "tactic-new-field-table" { Summary.freeze_function = (fun () -> !field_from_carrier,!field_from_relation,!field_from_name); @@ -980,10 +980,10 @@ let add_field_entry (sp,_kn) e = *) field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier; field_from_relation := Cmap.add e.field_req e !field_from_relation; - field_from_name := Spmap.add sp e !field_from_name + field_from_name := Spmap.add sp e !field_from_name -let subst_th (_,subst,th) = - let c' = subst_mps subst th.field_carrier in +let subst_th (_,subst,th) = + let c' = subst_mps subst th.field_carrier in let eq' = subst_mps subst th.field_req in let thm1' = subst_mps subst th.field_ok in let thm2' = subst_mps subst th.field_simpl_eq_ok in @@ -1041,7 +1041,7 @@ let field_equality r inv req = with Not_found -> error "field inverse should be declared as a morphism" in inv_m_lem - + let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odiv = check_required_library (cdir@["Field_tac"]); let env = Global.env() in @@ -1051,7 +1051,7 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi let (sth,ext) = build_setoid_params r add mul opp req eqth in let eqth = Some(sth,ext) in let _ = add_theory name rth eqth morphth cst_tac (None,None) power sign odiv in - let (pow_tac, pspec) = interp_power env power in + let (pow_tac, pspec) = interp_power env power in let sspec = interp_sign env sign in let dspec = interp_div env odiv in let inv_m = field_equality r inv req in @@ -1112,7 +1112,7 @@ let process_field_mods l = let cst_tac = ref None in let pre = ref None in let post = ref None in - let inj = ref None in + let inj = ref None in let sign = ref None in let power = ref None in let div = ref None in @@ -1131,7 +1131,7 @@ let process_field_mods l = (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) VERNAC COMMAND EXTEND AddSetoidField -| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> +| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] END @@ -1163,6 +1163,6 @@ 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) ] -> +| [ "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 ] END |