diff options
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r-- | plugins/setoid_ring/ArithRing.v | 2 | ||||
-rw-r--r-- | plugins/setoid_ring/BinList.v | 2 | ||||
-rw-r--r-- | plugins/setoid_ring/Cring.v | 7 | ||||
-rw-r--r-- | plugins/setoid_ring/Field.v | 2 | ||||
-rw-r--r-- | plugins/setoid_ring/Field_tac.v | 89 | ||||
-rw-r--r-- | plugins/setoid_ring/Field_theory.v | 2278 | ||||
-rw-r--r-- | plugins/setoid_ring/InitialRing.v | 8 | ||||
-rw-r--r-- | plugins/setoid_ring/NArithRing.v | 2 | ||||
-rw-r--r-- | plugins/setoid_ring/Ncring.v | 2 | ||||
-rw-r--r-- | plugins/setoid_ring/Ncring_initial.v | 3 | ||||
-rw-r--r-- | plugins/setoid_ring/Ncring_polynom.v | 63 | ||||
-rw-r--r-- | plugins/setoid_ring/Ncring_tac.v | 8 | ||||
-rw-r--r-- | plugins/setoid_ring/Ring.v | 2 | ||||
-rw-r--r-- | plugins/setoid_ring/Ring_base.v | 2 | ||||
-rw-r--r-- | plugins/setoid_ring/Ring_equiv.v | 74 | ||||
-rw-r--r-- | plugins/setoid_ring/Ring_polynom.v | 166 | ||||
-rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 58 | ||||
-rw-r--r-- | plugins/setoid_ring/Ring_theory.v | 7 | ||||
-rw-r--r-- | plugins/setoid_ring/Rings_Z.v | 1 | ||||
-rw-r--r-- | plugins/setoid_ring/ZArithRing.v | 6 | ||||
-rw-r--r-- | plugins/setoid_ring/newring.ml4 | 684 | ||||
-rw-r--r-- | plugins/setoid_ring/vo.itarget | 1 |
22 files changed, 1652 insertions, 1815 deletions
diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v index 92e61583..e7d0cd8e 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/plugins/setoid_ring/ArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v index 22448fd7..5dd1b86d 100644 --- a/plugins/setoid_ring/BinList.v +++ b/plugins/setoid_ring/BinList.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index f13f509a..4872c776 100644 --- a/plugins/setoid_ring/Cring.v +++ b/plugins/setoid_ring/Cring.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -21,6 +21,7 @@ Require Export Ncring_tac. Class Cring {R:Type}`{Rr:Ring R} := cring_mul_comm: forall x y:R, x * y == y * x. + Ltac reify_goal lvar lexpr lterm:= (*idtac lvar; idtac lexpr; idtac lterm;*) match lexpr with @@ -30,10 +31,10 @@ Ltac reify_goal lvar lexpr lterm:= |- (?op ?u1 ?u2) => change (op (@Ring_polynom.PEeval - _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) + _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e1) (@Ring_polynom.PEeval - _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) + _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e2)) end end. diff --git a/plugins/setoid_ring/Field.v b/plugins/setoid_ring/Field.v index d2ab9e0f..4de2efe3 100644 --- a/plugins/setoid_ring/Field.v +++ b/plugins/setoid_ring/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index 34a3018b..f867c6d0 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,55 +10,67 @@ 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 := + (* We do not assume that Cst recognizes the rO and rI terms as constants, as *) + (* the tactic could be used to discriminate occurrences of an opaque *) + (* constant phi, with (phi 0) not convertible to 0 for instance *) + Ltac mkFieldexpr C Cst CstPow rO rI radd rmul rsub ropp rdiv rinv rpow t fv := let rec mkP t := let f := match Cst t with | InitialRing.NotConstant => match t with + | rO => + fun _ => constr:(@FEO C) + | rI => + fun _ => constr:(@FEI C) | (radd ?t1 ?t2) => fun _ => let e1 := mkP t1 in - let e2 := mkP t2 in constr:(FEadd e1 e2) + let e2 := mkP t2 in constr:(@FEadd C e1 e2) | (rmul ?t1 ?t2) => fun _ => let e1 := mkP t1 in - let e2 := mkP t2 in constr:(FEmul e1 e2) + let e2 := mkP t2 in constr:(@FEmul C e1 e2) | (rsub ?t1 ?t2) => fun _ => let e1 := mkP t1 in - let e2 := mkP t2 in constr:(FEsub e1 e2) + let e2 := mkP t2 in constr:(@FEsub C e1 e2) | (ropp ?t1) => - fun _ => let e1 := mkP t1 in constr:(FEopp e1) + fun _ => let e1 := mkP t1 in constr:(@FEopp C e1) | (rdiv ?t1 ?t2) => fun _ => let e1 := mkP t1 in - let e2 := mkP t2 in constr:(FEdiv e1 e2) + let e2 := mkP t2 in constr:(@FEdiv C e1 e2) | (rinv ?t1) => - fun _ => let e1 := mkP t1 in constr:(FEinv e1) + fun _ => let e1 := mkP t1 in constr:(@FEinv C e1) | (rpow ?t1 ?n) => match CstPow n with | InitialRing.NotConstant => fun _ => let p := Find_at t fv in constr:(@FEX C p) - | ?c => fun _ => let e1 := mkP t1 in constr:(FEpow e1 c) + | ?c => fun _ => let e1 := mkP t1 in constr:(@FEpow C e1 c) end | _ => fun _ => let p := Find_at t fv in constr:(@FEX C p) end - | ?c => fun _ => constr:(FEc c) + | ?c => fun _ => constr:(@FEc C c) end in f () in mkP t. -Ltac FFV Cst CstPow add mul sub opp div inv pow t fv := + (* We do not assume that Cst recognizes the rO and rI terms as constants, as *) + (* the tactic could be used to discriminate occurrences of an opaque *) + (* constant phi, with (phi 0) not convertible to 0 for instance *) +Ltac FFV Cst CstPow rO rI add mul sub opp div inv pow t fv := let rec TFV t fv := match Cst t with | InitialRing.NotConstant => match t with + | rO => fv + | rI => fv | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) @@ -83,60 +95,60 @@ 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 ?rI ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] => (fun proj => proj Cst_tac Pow_tac pre post - req radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok) + req rO rI radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok) | _ => fail 1 "field anomaly: bad correctness lemma (parse)" end in F FLD. Ltac get_FldPre FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => pre). Ltac get_FldPost FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => post). Ltac get_L1 FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => L1). Ltac get_SimplifyEqLemma FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => L2). Ltac get_SimplifyLemma FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => L3). Ltac get_L4 FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => L4). Ltac get_CondLemma FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => cond_ok). Ltac get_FldEq FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => req). @@ -146,33 +158,33 @@ Ltac get_FldCarrier FLD := Ltac get_RingFV FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => - FV Cst_tac Pow_tac radd rmul rsub ropp rpow). + FV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow). Ltac get_FFV FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => - FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow). + FFV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow). Ltac get_RingMeta FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => - mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow). + mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow). Ltac get_Meta FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => - mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow). + mkFieldexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow). Ltac get_Hyp_tac FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => - let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow in fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH). Ltac get_FEeval FLD := @@ -180,8 +192,8 @@ Ltac get_FEeval FLD := match type of L1 with | context [(@FEeval - ?R ?r0 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] => - constr:(@FEeval R r0 add mul sub opp div inv C phi Cpow powphi pow) + ?R ?r0 ?r1 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] => + constr:(@FEeval R r0 r1 add mul sub opp div inv C phi Cpow powphi pow) | _ => fail 1 "field anomaly: bad correctness lemma (get_FEeval)" end. @@ -201,8 +213,7 @@ Ltac fold_field_cond req := Ltac simpl_PCond FLD := let req := get_FldEq FLD in let lemma := get_CondLemma FLD in - try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; - clear lock_def lock); + try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock); protect_fv "field_cond"; fold_field_cond req; try exact I. @@ -210,8 +221,7 @@ Ltac simpl_PCond FLD := Ltac simpl_PCond_BEURK FLD := let req := get_FldEq FLD in let lemma := get_CondLemma FLD in - try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; - clear lock_def lock); + (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock); protect_fv "field_cond"; fold_field_cond req. @@ -544,10 +554,9 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk := let field_ok2 := constr:(field_ok1 _ _ _ pp_spec) in match s_spec with | mkhypo ?ss_spec => - let field_ok3 := constr:(field_ok2 _ ss_spec) in match d_spec with | mkhypo ?dd_spec => - let field_ok := constr:(field_ok3 _ dd_spec) in + let field_ok := constr:(field_ok2 _ dd_spec) in let mk_lemma lemma := constr:(lemma _ _ _ _ _ _ _ _ _ _ set ext_r inv_m afth @@ -563,7 +572,7 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk := (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" + | _ => fail 4 "field: bad coefficient division specification" end | _ => fail 3 "field: bad sign specification" end diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 75d3ad86..0f5c49b0 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,123 +9,179 @@ Require Ring. Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List Morphisms. Require Import ZArith_base. -(*Require Import Omega.*) Set Implicit Arguments. +(* Set Universe Polymorphism. *) Section MakeFieldPol. -(* 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). - Variable req : R -> R -> Prop. - - Notation "0" := rO. Notation "1" := rI. - Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). - Notation "x - y " := (rsub x y). Notation "x / y" := (rdiv x y). - Notation "- x" := (ropp x). Notation "/ x" := (rinv x). - Notation "x == y" := (req x y) (at level 70, no associativity). - - (* Equality properties *) - Variable Rsth : Equivalence 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; - AF_1_neq_0 : ~ 1 == 0; - AFdiv_def : forall p q, p / q == p * / q; - AFinv_l : forall p, ~ p == 0 -> / p * p == 1 - }. +(* Field elements : R *) + +Variable R:Type. +Bind Scope R_scope with R. +Delimit Scope R_scope with ring. +Local Open Scope R_scope. + +Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R). +Variable (rdiv : R->R->R) (rinv : R->R). +Variable req : R -> R -> Prop. + +Notation "0" := rO : R_scope. +Notation "1" := rI : R_scope. +Infix "+" := radd : R_scope. +Infix "-" := rsub : R_scope. +Infix "*" := rmul : R_scope. +Infix "/" := rdiv : R_scope. +Notation "- x" := (ropp x) : R_scope. +Notation "/ x" := (rinv x) : R_scope. +Infix "==" := req (at level 70, no associativity) : R_scope. + +(* Equality properties *) +Variable Rsth : Equivalence 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; + AF_1_neq_0 : ~ 1 == 0; + AFdiv_def : forall p q, p / q == p * / q; + AFinv_l : forall p, ~ p == 0 -> / p * p == 1 +}. Section AlmostField. - Variable AFth : almost_field_theory. - Let ARth := AFth.(AF_AR). - Let rI_neq_rO := AFth.(AF_1_neq_0). - Let rdiv_def := AFth.(AFdiv_def). - Let rinv_l := AFth.(AFinv_l). +Variable AFth : almost_field_theory. +Let ARth := AFth.(AF_AR). +Let rI_neq_rO := AFth.(AF_1_neq_0). +Let rdiv_def := AFth.(AFdiv_def). +Let rinv_l := AFth.(AFinv_l). - (* Coefficients *) - Variable C: Type. - Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C). - Variable ceqb : C->C->bool. - Variable phi : C -> R. +Add Morphism radd : radd_ext. Proof. exact (Radd_ext Reqe). Qed. +Add Morphism rmul : rmul_ext. Proof. exact (Rmul_ext Reqe). Qed. +Add Morphism ropp : ropp_ext. Proof. exact (Ropp_ext Reqe). Qed. +Add Morphism rsub : rsub_ext. Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. +Add Morphism rinv : rinv_ext. Proof. exact SRinv_ext. Qed. - Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req - cO cI cadd cmul csub copp ceqb phi. +Let eq_trans := Setoid.Seq_trans _ _ Rsth. +Let eq_sym := Setoid.Seq_sym _ _ Rsth. +Let eq_refl := Setoid.Seq_refl _ _ Rsth. -Lemma ceqb_rect : forall c1 c2 (A:Type) (x y:A) (P:A->Type), - (phi c1 == phi c2 -> P x) -> P y -> P (if ceqb c1 c2 then x else y). +Let radd_0_l := ARadd_0_l ARth. +Let radd_comm := ARadd_comm ARth. +Let radd_assoc := ARadd_assoc ARth. +Let rmul_1_l := ARmul_1_l ARth. +Let rmul_0_l := ARmul_0_l ARth. +Let rmul_comm := ARmul_comm ARth. +Let rmul_assoc := ARmul_assoc ARth. +Let rdistr_l := ARdistr_l ARth. +Let ropp_mul_l := ARopp_mul_l ARth. +Let ropp_add := ARopp_add ARth. +Let rsub_def := ARsub_def ARth. + +Let radd_0_r := ARadd_0_r Rsth ARth. +Let rmul_0_r := ARmul_0_r Rsth ARth. +Let rmul_1_r := ARmul_1_r Rsth ARth. +Let ropp_0 := ARopp_zero Rsth Reqe ARth. +Let rdistr_r := ARdistr_r Rsth Reqe ARth. + +(* Coefficients : C *) + +Variable C: Type. +Bind Scope C_scope with C. +Delimit Scope C_scope with coef. + +Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C). +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. + +Notation "0" := cO : C_scope. +Notation "1" := cI : C_scope. +Infix "+" := cadd : C_scope. +Infix "-" := csub : C_scope. +Infix "*" := cmul : C_scope. +Notation "- x" := (copp x) : C_scope. +Infix "=?" := ceqb : C_scope. +Notation "[ x ]" := (phi x) (at level 0). + +Let phi_0 := CRmorph.(morph0). +Let phi_1 := CRmorph.(morph1). + +Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c =? c')%coef. Proof. -intros. -generalize (fun h => X (morph_eq CRmorph c1 c2 h)). -case (ceqb c1 c2); auto. +generalize (CRmorph.(morph_eq) c c'). +destruct (c =? c')%coef; auto. Qed. +(* Power coefficients : Cpow *) - (* 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). - Notation "-! x" := (copp x) (at level 35). - Notation " x ?=! y" := (ceqb x y) (at level 70, no associativity). - Notation "[ x ]" := (phi x) (at level 0). +Variable Cpow : Type. +Variable Cp_phi : N -> Cpow. +Variable rpow : R -> Cpow -> R. +Variable pow_th : power_theory rI rmul req Cp_phi rpow. +(* sign function *) +Variable get_sign : C -> option C. +Variable get_sign_spec : sign_theory copp ceqb get_sign. +Variable cdiv:C -> C -> C*C. +Variable cdiv_th : div_theory req cadd cmul phi cdiv. - (* Useful tactics *) - 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 rpow_pow := pow_th.(rpow_pow_N). -Let eq_trans := Setoid.Seq_trans _ _ Rsth. -Let eq_sym := Setoid.Seq_sym _ _ Rsth. -Let eq_refl := Setoid.Seq_refl _ _ Rsth. +(* Polynomial expressions : (PExpr C) *) + +Bind Scope PE_scope with PExpr. +Delimit Scope PE_scope with poly. + +Notation NPEeval := (PEeval rO rI radd rmul rsub ropp phi Cp_phi rpow). +Notation "P @ l" := (NPEeval l P) (at level 10, no associativity). + +Arguments PEc _ _%coef. + +Notation "0" := (PEc 0) : PE_scope. +Notation "1" := (PEc 1) : PE_scope. +Infix "+" := PEadd : PE_scope. +Infix "-" := PEsub : PE_scope. +Infix "*" := PEmul : PE_scope. +Notation "- e" := (PEopp e) : PE_scope. +Infix "^" := PEpow : PE_scope. + +Definition NPEequiv e e' := forall l, e@l == e'@l. +Infix "===" := NPEequiv (at level 70, no associativity) : PE_scope. -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_comm ARth) (ARmul_assoc ARth) (ARdistr_l ARth) - (ARopp_mul_l ARth) (ARopp_add ARth) - (ARsub_def ARth) . - - (* Power coefficients *) - Variable Cpow : Type. - Variable Cp_phi : N -> Cpow. - Variable rpow : R -> Cpow -> R. - Variable pow_th : power_theory rI rmul req Cp_phi rpow. - (* sign function *) - Variable get_sign : C -> option C. - Variable get_sign_spec : sign_theory copp ceqb get_sign. - - Variable cdiv:C -> C -> C*C. - Variable cdiv_th : div_theory req cadd cmul phi cdiv. - -Notation NPEeval := (PEeval rO radd rmul rsub ropp phi Cp_phi rpow). -Notation Nnorm:= (norm_subst cO cI cadd cmul csub copp ceqb cdiv). - -Notation NPphi_dev := (Pphi_dev rO rI radd rmul rsub ropp cO cI ceqb phi get_sign). -Notation NPphi_pow := (Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi rpow get_sign). +Instance NPEequiv_eq : Equivalence NPEequiv. +Proof. + split; red; unfold NPEequiv; intros; [reflexivity|symmetry|etransitivity]; + eauto. +Qed. + +Instance NPEeval_ext : Proper (eq ==> NPEequiv ==> req) NPEeval. +Proof. + intros l l' <- e e' He. now rewrite (He l). +Qed. + +Notation Nnorm := + (norm_subst cO cI cadd cmul csub copp ceqb cdiv). +Notation NPphi_dev := + (Pphi_dev rO rI radd rmul rsub ropp cO cI ceqb phi get_sign). +Notation NPphi_pow := + (Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi rpow get_sign). (* add abstract semi-ring to help with some proofs *) Add Ring Rring : (ARth_SRth ARth). -Local Hint Extern 2 (_ == _) => f_equiv. - (* additional ring properties *) -Lemma rsub_0_l : forall r, 0 - r == - r. -intros; rewrite (ARsub_def ARth);ring. +Lemma rsub_0_l r : 0 - r == - r. +Proof. +rewrite rsub_def; ring. Qed. -Lemma rsub_0_r : forall r, r - 0 == r. -intros; rewrite (ARsub_def ARth). -rewrite (ARopp_zero Rsth Reqe ARth); ring. +Lemma rsub_0_r r : r - 0 == r. +Proof. +rewrite rsub_def, ropp_0; ring. Qed. (*************************************************************************** @@ -134,452 +190,525 @@ Qed. ***************************************************************************) -Theorem rdiv_simpl: forall p q, ~ q == 0 -> q * (p / q) == p. +Theorem rdiv_simpl p q : ~ q == 0 -> q * (p / q) == p. Proof. -intros p q H. +intros. rewrite rdiv_def. -transitivity (/ q * q * p); [ ring | idtac ]. -rewrite rinv_l; auto. +transitivity (/ q * q * p); [ ring | ]. +now rewrite rinv_l. Qed. -Hint Resolve rdiv_simpl . -Instance SRdiv_ext: Proper (req ==> req ==> req) rdiv. +Instance rdiv_ext: Proper (req ==> req ==> req) rdiv. Proof. -intros p1 p2 Ep q1 q2 Eq. -transitivity (p1 * / q1); auto. -transitivity (p2 * / q2); auto. +intros p1 p2 Ep q1 q2 Eq. now rewrite !rdiv_def, Ep, Eq. Qed. -Hint Resolve SRdiv_ext. -Lemma rmul_reg_l : forall p q1 q2, +Lemma rmul_reg_l p q1 q2 : ~ p == 0 -> p * q1 == p * q2 -> q1 == q2. Proof. -intros p q1 q2 H EQ. -rewrite <- (@rdiv_simpl q1 p) by trivial. -rewrite <- (@rdiv_simpl q2 p) by trivial. -rewrite !rdiv_def, !(ARmul_assoc ARth). -now rewrite EQ. +intros H EQ. +assert (H' : p * (q1 / p) == p * (q2 / p)). +{ now rewrite !rdiv_def, !rmul_assoc, EQ. } +now rewrite !rdiv_simpl in H'. Qed. -Theorem field_is_integral_domain : forall r1 r2, +Theorem field_is_integral_domain r1 r2 : ~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0. Proof. -intros r1 r2 H1 H2. contradict H2. -transitivity (1 * r2); auto. -transitivity (/ r1 * r1 * r2); auto. -rewrite <- (ARmul_assoc ARth). -rewrite H2. -apply ARmul_0_r with (1 := Rsth) (2 := ARth). +intros H1 H2. contradict H2. +transitivity (/r1 * r1 * r2). +- now rewrite rinv_l. +- now rewrite <- rmul_assoc, H2. Qed. -Theorem ropp_neq_0 : forall r, +Theorem ropp_neq_0 r : ~ -(1) == 0 -> ~ r == 0 -> ~ -r == 0. +Proof. intros. setoid_replace (- r) with (- (1) * r). - apply field_is_integral_domain; trivial. - rewrite <- (ARopp_mul_l ARth). - rewrite (ARmul_1_l ARth). - reflexivity. +- apply field_is_integral_domain; trivial. +- now rewrite <- ropp_mul_l, rmul_1_l. Qed. -Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1. -intros. -rewrite (AFdiv_def AFth). -rewrite (ARmul_comm ARth). -apply (AFinv_l AFth). -trivial. +Theorem rdiv_r_r r : ~ r == 0 -> r / r == 1. +Proof. +intros. rewrite rdiv_def, rmul_comm. now apply rinv_l. Qed. -Theorem rdiv1: forall r, r == r / 1. -intros r; transitivity (1 * (r / 1)); auto. +Theorem rdiv1 r : r == r / 1. +Proof. +transitivity (1 * (r / 1)). +- symmetry; apply rdiv_simpl. apply rI_neq_rO. +- apply rmul_1_l. Qed. -Theorem rdiv2: - forall r1 r2 r3 r4, - ~ r2 == 0 -> - ~ r4 == 0 -> - r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4). +Theorem rdiv2 a b c d : + ~ b == 0 -> + ~ d == 0 -> + a / b + c / d == (a * d + c * b) / (b * d). Proof. -intros r1 r2 r3 r4 H H0. -assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). -apply rmul_reg_l with (r2 * r4); trivial. +intros H H0. +assert (~ b * d == 0) by now apply field_is_integral_domain. +apply rmul_reg_l with (b * d); trivial. rewrite rdiv_simpl; trivial. -rewrite (ARdistr_r Rsth Reqe ARth). -apply (Radd_ext Reqe). -- transitivity (r2 * (r1 / r2) * r4); [ ring | auto ]. -- transitivity (r2 * (r4 * (r3 / r4))); auto. - transitivity (r2 * r3); auto. +rewrite rdistr_r. +apply radd_ext. +- now rewrite <- rmul_assoc, (rmul_comm d), rmul_assoc, rdiv_simpl. +- now rewrite (rmul_comm c), <- rmul_assoc, rdiv_simpl. Qed. -Theorem rdiv2b: - forall r1 r2 r3 r4 r5, - ~ (r2*r5) == 0 -> - ~ (r4*r5) == 0 -> - r1 / (r2*r5) + r3 / (r4*r5) == (r1 * r4 + r3 * r2) / (r2 * (r4 * r5)). +Theorem rdiv2b a b c d e : + ~ (b*e) == 0 -> + ~ (d*e) == 0 -> + a / (b*e) + c / (d*e) == (a * d + c * b) / (b * (d * e)). Proof. -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) +intros H H0. +assert (~ b == 0) by (contradict H; rewrite H; ring). +assert (~ e == 0) by (contradict H; rewrite H; ring). +assert (~ d == 0) by (contradict H0; rewrite H0; ring). +assert (~ b * (d * e) == 0) by (repeat apply field_is_integral_domain; trivial). -apply rmul_reg_l with (r2 * (r4 * r5)); trivial. +apply rmul_reg_l with (b * (d * e)); trivial. rewrite rdiv_simpl; trivial. -rewrite (ARdistr_r Rsth Reqe ARth). -apply (Radd_ext Reqe). - transitivity ((r2 * r5) * (r1 / (r2 * r5)) * r4); [ ring | auto ]. - transitivity ((r4 * r5) * (r3 / (r4 * r5)) * r2); [ ring | auto ]. -Qed. - -Theorem rdiv5: forall r1 r2, - (r1 / r2) == - r1 / r2. -Proof. -intros r1 r2. -transitivity (- (r1 * / r2)); auto. -transitivity (- r1 * / r2); auto. -Qed. -Hint Resolve rdiv5 . - -Theorem rdiv3 r1 r2 r3 r4 : - ~ r2 == 0 -> - ~ r4 == 0 -> - r1 / r2 - r3 / r4 == (r1 * r4 - r3 * r2) / (r2 * r4). -Proof. -intros H2 H4. -assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). -transitivity (r1 / r2 + - (r3 / r4)); auto. -transitivity (r1 / r2 + - r3 / r4); auto. -transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)). -apply rdiv2; auto. -f_equiv. -transitivity (r1 * r4 + - (r3 * r2)); auto. -Qed. - - -Theorem rdiv3b: - forall r1 r2 r3 r4 r5, - ~ (r2 * r5) == 0 -> - ~ (r4 * r5) == 0 -> - r1 / (r2*r5) - r3 / (r4*r5) == (r1 * r4 - r3 * r2) / (r2 * (r4 * r5)). -Proof. -intros r1 r2 r3 r4 r5 H H0. -transitivity (r1 / (r2 * r5) + - (r3 / (r4 * r5))); auto. -transitivity (r1 / (r2 * r5) + - r3 / (r4 * r5)); auto. -transitivity ((r1 * r4 + - r3 * r2) / (r2 * (r4 * r5))). -apply rdiv2b; auto; try ring. -apply (SRdiv_ext); auto. -transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto. -Qed. - -Theorem rdiv6: - forall r1 r2, - ~ r1 == 0 -> ~ r2 == 0 -> / (r1 / r2) == r2 / r1. -intros r1 r2 H H0. -assert (~ r1 / r2 == 0) as Hk. - intros H1; case H. - transitivity (r2 * (r1 / r2)); auto. - rewrite H1; ring. - apply rmul_reg_l with (r1 / r2); auto. - transitivity (/ (r1 / r2) * (r1 / r2)); auto. - transitivity 1; auto. - repeat rewrite rdiv_def. - transitivity (/ r1 * r1 * (/ r2 * r2)); [ idtac | ring ]. - repeat rewrite rinv_l; auto. -Qed. -Hint Resolve rdiv6 . - - Theorem rdiv4: - forall r1 r2 r3 r4, - ~ r2 == 0 -> - ~ r4 == 0 -> - (r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4). -Proof. -intros r1 r2 r3 r4 H H0. -assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). -apply rmul_reg_l with (r2 * r4); trivial. -rewrite rdiv_simpl; trivial. -transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ]. -repeat rewrite rdiv_simpl; trivial. +rewrite rdistr_r. +apply radd_ext. +- transitivity ((b * e) * (a / (b * e)) * d); + [ ring | now rewrite rdiv_simpl ]. +- transitivity ((d * e) * (c / (d * e)) * b); + [ ring | now rewrite rdiv_simpl ]. Qed. - Theorem rdiv4b: - forall r1 r2 r3 r4 r5 r6, - ~ r2 * r5 == 0 -> - ~ r4 * r6 == 0 -> - ((r1 * r6) / (r2 * r5)) * ((r3 * r5) / (r4 * r6)) == (r1 * r3) / (r2 * r4). +Theorem rdiv5 a b : - (a / b) == - a / b. Proof. -intros r1 r2 r3 r4 r5 r6 H H0. -rewrite rdiv4; auto. -transitivity ((r5 * r6) * (r1 * r3) / ((r5 * r6) * (r2 * r4))). -apply SRdiv_ext; ring. -assert (HH: ~ r5*r6 == 0). - apply field_is_integral_domain. - intros H1; case H; rewrite H1; ring. - intros H1; case H0; rewrite H1; ring. -rewrite <- rdiv4 ; auto. - rewrite rdiv_r_r; auto. +now rewrite !rdiv_def, ropp_mul_l. +Qed. - apply field_is_integral_domain. - intros H1; case H; rewrite H1; ring. - intros H1; case H0; rewrite H1; ring. +Theorem rdiv3b a b c d e : + ~ (b * e) == 0 -> + ~ (d * e) == 0 -> + a / (b*e) - c / (d*e) == (a * d - c * b) / (b * (d * e)). +Proof. +intros H H0. +rewrite !rsub_def, rdiv5, ropp_mul_l. +now apply rdiv2b. Qed. +Theorem rdiv6 a b : + ~ a == 0 -> ~ b == 0 -> / (a / b) == b / a. +Proof. +intros H H0. +assert (Hk : ~ a / b == 0). +{ contradict H. + transitivity (b * (a / b)). + - now rewrite rdiv_simpl. + - rewrite H. apply rmul_0_r. } +apply rmul_reg_l with (a / b); trivial. +rewrite (rmul_comm (a / b)), rinv_l; trivial. +rewrite !rdiv_def. +transitivity (/ a * a * (/ b * b)); [ | ring ]. +now rewrite !rinv_l, rmul_1_l. +Qed. + +Theorem rdiv4 a b c d : + ~ b == 0 -> + ~ d == 0 -> + (a / b) * (c / d) == (a * c) / (b * d). +Proof. +intros H H0. +assert (~ b * d == 0) by now apply field_is_integral_domain. +apply rmul_reg_l with (b * d); trivial. +rewrite rdiv_simpl; trivial. +transitivity (b * (a / b) * (d * (c / d))); [ ring | ]. +rewrite !rdiv_simpl; trivial. +Qed. -Theorem rdiv7: - forall r1 r2 r3 r4, - ~ r2 == 0 -> - ~ r3 == 0 -> - ~ r4 == 0 -> - (r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3). +Theorem rdiv4b a b c d e f : + ~ b * e == 0 -> + ~ d * f == 0 -> + ((a * f) / (b * e)) * ((c * e) / (d * f)) == (a * c) / (b * d). +Proof. +intros H H0. +assert (~ b == 0) by (contradict H; rewrite H; ring). +assert (~ e == 0) by (contradict H; rewrite H; ring). +assert (~ d == 0) by (contradict H0; rewrite H0; ring). +assert (~ f == 0) by (contradict H0; rewrite H0; ring). +assert (~ b*d == 0) by now apply field_is_integral_domain. +assert (~ e*f == 0) by now apply field_is_integral_domain. +rewrite rdiv4; trivial. +transitivity ((e * f) * (a * c) / ((e * f) * (b * d))). +- apply rdiv_ext; ring. +- rewrite <- rdiv4, rdiv_r_r; trivial. +Qed. + +Theorem rdiv7 a b c d : + ~ b == 0 -> + ~ c == 0 -> + ~ d == 0 -> + (a / b) / (c / d) == (a * d) / (b * c). Proof. intros. -rewrite (rdiv_def (r1 / r2)). +rewrite (rdiv_def (a / b)). rewrite rdiv6; trivial. apply rdiv4; trivial. Qed. -Theorem rdiv7b: - forall r1 r2 r3 r4 r5 r6, - ~ r2 * r6 == 0 -> - ~ r3 * r5 == 0 -> - ~ r4 * r6 == 0 -> - ((r1 * r5) / (r2 * r6)) / ((r3 * r5) / (r4 * r6)) == (r1 * r4) / (r2 * r3). +Theorem rdiv7b a b c d e f : + ~ b * f == 0 -> + ~ c * e == 0 -> + ~ d * f == 0 -> + ((a * e) / (b * f)) / ((c * e) / (d * f)) == (a * d) / (b * c). +Proof. +intros Hbf Hce Hdf. +assert (~ c==0) by (contradict Hce; rewrite Hce; ring). +assert (~ e==0) by (contradict Hce; rewrite Hce; ring). +assert (~ b==0) by (contradict Hbf; rewrite Hbf; ring). +assert (~ f==0) by (contradict Hbf; rewrite Hbf; ring). +assert (~ b*c==0) by now apply field_is_integral_domain. +assert (~ e*f==0) by now apply field_is_integral_domain. +rewrite rdiv7; trivial. +transitivity ((e * f) * (a * d) / ((e * f) * (b * c))). +- apply rdiv_ext; ring. +- now rewrite <- rdiv4, rdiv_r_r. +Qed. + +Theorem rinv_nz a : ~ a == 0 -> ~ /a == 0. +Proof. +intros H H0. apply rI_neq_rO. +rewrite <- (rdiv_r_r H), rdiv_def, H0. apply rmul_0_r. +Qed. + +Theorem rdiv8 a b : ~ b == 0 -> a == 0 -> a / b == 0. +Proof. +intros H H0. +now rewrite rdiv_def, H0, rmul_0_l. +Qed. + +Theorem cross_product_eq a b c d : + ~ b == 0 -> ~ d == 0 -> a * d == c * b -> a / b == c / d. Proof. intros. -rewrite rdiv7; auto. -transitivity ((r5 * r6) * (r1 * r4) / ((r5 * r6) * (r2 * r3))). -apply SRdiv_ext; ring. -assert (HH: ~ r5*r6 == 0). - apply field_is_integral_domain. - intros H2; case H0; rewrite H2; ring. - intros H2; case H1; rewrite H2; ring. -rewrite <- rdiv4 ; auto. -rewrite rdiv_r_r; auto. - apply field_is_integral_domain. - intros H2; case H; rewrite H2; ring. - intros H2; case H0; rewrite H2; ring. +transitivity (a / b * (d / d)). +- now rewrite rdiv_r_r, rmul_1_r. +- now rewrite rdiv4, H1, (rmul_comm b d), <- rdiv4, rdiv_r_r. Qed. +(* Results about [pow_pos] and [pow_N] *) -Theorem rdiv8: forall r1 r2, ~ r2 == 0 -> r1 == 0 -> r1 / r2 == 0. -intros r1 r2 H H0. -transitivity (r1 * / r2); auto. -transitivity (0 * / r2); auto. +Instance pow_ext : Proper (req ==> eq ==> req) (pow_pos rmul). +Proof. +intros x y H p p' <-. +induction p as [p IH| p IH|];simpl; trivial; now rewrite !IH, ?H. Qed. +Instance pow_N_ext : Proper (req ==> eq ==> req) (pow_N rI rmul). +Proof. +intros x y H n n' <-. destruct n; simpl; trivial. now apply pow_ext. +Qed. -Theorem cross_product_eq : forall r1 r2 r3 r4, - ~ r2 == 0 -> ~ r4 == 0 -> r1 * r4 == r3 * r2 -> r1 / r2 == r3 / r4. -intros. -transitivity (r1 / r2 * (r4 / r4)). - rewrite rdiv_r_r; trivial. - symmetry . - apply (ARmul_1_r Rsth ARth). - rewrite rdiv4; trivial. - rewrite H1. - rewrite (ARmul_comm ARth r2 r4). - rewrite <- rdiv4; trivial. - rewrite rdiv_r_r by trivial. - apply (ARmul_1_r Rsth ARth). +Lemma pow_pos_0 p : pow_pos rmul 0 p == 0. +Proof. +induction p;simpl;trivial; now rewrite !IHp. Qed. +Lemma pow_pos_1 p : pow_pos rmul 1 p == 1. +Proof. +induction p;simpl;trivial; ring [IHp]. +Qed. + +Lemma pow_pos_cst c p : pow_pos rmul [c] p == [pow_pos cmul c p]. +Proof. +induction p;simpl;trivial; now rewrite !CRmorph.(morph_mul), !IHp. +Qed. + +Lemma pow_pos_mul_l x y p : + pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p. +Proof. +induction p;simpl;trivial; ring [IHp]. +Qed. + +Lemma pow_pos_add_r x p1 p2 : + pow_pos rmul x (p1+p2) == pow_pos rmul x p1 * pow_pos rmul x p2. +Proof. + exact (Ring_theory.pow_pos_add Rsth rmul_ext rmul_assoc x p1 p2). +Qed. + +Lemma pow_pos_mul_r x p1 p2 : + pow_pos rmul x (p1*p2) == pow_pos rmul (pow_pos rmul x p1) p2. +Proof. +induction p1;simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r; + simpl; trivial; ring [IHp1]. +Qed. + +Lemma pow_pos_nz x p : ~x==0 -> ~pow_pos rmul x p == 0. +Proof. + intros Hx. induction p;simpl;trivial; + repeat (apply field_is_integral_domain; trivial). +Qed. + +Lemma pow_pos_div a b p : ~ b == 0 -> + pow_pos rmul (a / b) p == pow_pos rmul a p / pow_pos rmul b p. +Proof. + intros. + induction p; simpl; trivial. + - rewrite IHp. + assert (nz := pow_pos_nz p H). + rewrite !rdiv4; trivial. + apply field_is_integral_domain; trivial. + - rewrite IHp. + assert (nz := pow_pos_nz p H). + rewrite !rdiv4; trivial. +Qed. + +(* === is a morphism *) + +Instance PEadd_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEadd C). +Proof. intros ? ? E ? ? E' l. simpl. now rewrite E, E'. Qed. +Instance PEsub_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEsub C). +Proof. intros ? ? E ? ? E' l. simpl. now rewrite E, E'. Qed. +Instance PEmul_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEmul C). +Proof. intros ? ? E ? ? E' l. simpl. now rewrite E, E'. Qed. +Instance PEopp_ext : Proper (NPEequiv ==> NPEequiv) (@PEopp C). +Proof. intros ? ? E l. simpl. now rewrite E. Qed. +Instance PEpow_ext : Proper (NPEequiv ==> eq ==> NPEequiv) (@PEpow C). +Proof. + intros ? ? E ? ? <- l. simpl. rewrite !rpow_pow. apply pow_N_ext; trivial. +Qed. + +Lemma PE_1_l (e : PExpr C) : (1 * e === e)%poly. +Proof. + intros l. simpl. rewrite phi_1. apply rmul_1_l. +Qed. + +Lemma PE_1_r (e : PExpr C) : (e * 1 === e)%poly. +Proof. + intros l. simpl. rewrite phi_1. apply rmul_1_r. +Qed. + +Lemma PEpow_0_r (e : PExpr C) : (e ^ 0 === 1)%poly. +Proof. + intros l. simpl. now rewrite !rpow_pow. +Qed. + +Lemma PEpow_1_r (e : PExpr C) : (e ^ 1 === e)%poly. +Proof. + intros l. simpl. now rewrite !rpow_pow. +Qed. + +Lemma PEpow_1_l n : (1 ^ n === 1)%poly. +Proof. + intros l. simpl. rewrite rpow_pow. destruct n; simpl. + - now rewrite phi_1. + - now rewrite phi_1, pow_pos_1. +Qed. + +Lemma PEpow_add_r (e : PExpr C) n n' : + (e ^ (n+n') === e ^ n * e ^ n')%poly. +Proof. + intros l. simpl. rewrite !rpow_pow. + destruct n; simpl. + - rewrite rmul_1_l. trivial. + - destruct n'; simpl. + + rewrite rmul_1_r. trivial. + + apply pow_pos_add_r. +Qed. + +Lemma PEpow_mul_l (e e' : PExpr C) n : + ((e * e') ^ n === e ^ n * e' ^ n)%poly. +Proof. + intros l. simpl. rewrite !rpow_pow. destruct n; simpl; trivial. + - symmetry; apply rmul_1_l. + - apply pow_pos_mul_l. +Qed. + +Lemma PEpow_mul_r (e : PExpr C) n n' : + (e ^ (n * n') === (e ^ n) ^ n')%poly. +Proof. + intros l. simpl. rewrite !rpow_pow. + destruct n, n'; simpl; trivial. + - now rewrite pow_pos_1. + - apply pow_pos_mul_r. +Qed. + +Lemma PEpow_nz l e n : ~ e @ l == 0 -> ~ (e^n) @ l == 0. +Proof. + intros. simpl. rewrite rpow_pow. destruct n; simpl. + - apply rI_neq_rO. + - now apply pow_pos_nz. +Qed. + + (*************************************************************************** Some equality test ***************************************************************************) +Local Notation "a &&& b" := (if a then b else false) + (at level 40, left associativity). + (* equality test *) -Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := - match e1, e2 with - PEc c1, PEc c2 => ceqb c1 c2 - | PEX p1, PEX p2 => Pos.eqb p1 p2 - | PEadd e3 e5, PEadd e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false - | PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false - | PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false - | PEopp e3, PEopp e4 => PExpr_eq e3 e4 - | PEpow e3 n3, PEpow e4 n4 => if N.eqb n3 n4 then PExpr_eq e3 e4 else false +Fixpoint PExpr_eq (e e' : PExpr C) {struct e} : bool := + match e, e' with + | PEc c, PEc c' => ceqb c c' + | PEX _ p, PEX _ p' => Pos.eqb p p' + | e1 + e2, e1' + e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2' + | e1 - e2, e1' - e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2' + | e1 * e2, e1' * e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2' + | - e, - e' => PExpr_eq e e' + | e ^ n, e' ^ n' => N.eqb n n' &&& PExpr_eq e e' | _, _ => false - end. - -Add Morphism (pow_pos rmul) with signature req ==> eq ==> req as pow_morph. -intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH]. -Qed. - -Add Morphism (pow_N rI rmul) with signature req ==> eq ==> req as pow_N_morph. -intros x y H [|p];simpl;auto. apply pow_morph;trivial. -Qed. - -Theorem PExpr_eq_semi_correct: - forall l e1 e2, PExpr_eq e1 e2 = true -> NPEeval l e1 == NPEeval l e2. -intros l e1; elim e1. -intros c1; intros e2; elim e2; simpl; (try (intros; discriminate)). -intros c2; apply (morph_eq CRmorph). -intros p1; intros e2; elim e2; simpl; (try (intros; discriminate)). -intros p2; case Pos.eqb_spec; intros; now subst. -intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)). -intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4); - (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6); - (try (intros; discriminate)); auto. -intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)). -intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4); - (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6); - (try (intros; discriminate)); auto. -intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)). -intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4); - (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6); - (try (intros; discriminate)); auto. -intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))). -intros e4; generalize (rec e4); case (PExpr_eq e3 e4); - (try (intros; discriminate)); auto. -intros e3 rec n3 e2;(case e2;simpl;(try (intros;discriminate))). -intros e4 n4; case N.eqb_spec; try discriminate; intros EQ H; subst. -repeat rewrite pow_th.(rpow_pow_N). rewrite (rec _ H);auto. -Qed. - -(* add *) -Definition NPEadd e1 e2 := - match e1, e2 with - PEc c1, PEc c2 => PEc (cadd c1 c2) - | PEc c, _ => if ceqb c cO then e2 else PEadd e1 e2 - | _, PEc c => if ceqb c cO then e1 else PEadd e1 e2 - (* Peut t'on factoriser ici ??? *) - | _, _ => PEadd e1 e2 - end. + end%poly. -Theorem NPEadd_correct: - forall l e1 e2, NPEeval l (NPEadd e1 e2) == NPEeval l (PEadd e1 e2). +Lemma if_true (a b : bool) : a &&& b = true -> a = true /\ b = true. Proof. -intros l e1 e2. -destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect; - try (intro eq_c; rewrite eq_c); simpl;try apply eq_refl; - try (ring [(morph0 CRmorph)]). - apply (morph_add CRmorph). + destruct a, b; split; trivial. Qed. -Definition NPEpow x n := - match n with - | N0 => PEc cI - | Npos p => - if Pos.eqb p xH then x else - match x with - | PEc c => - if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (pow_pos cmul c p) - | _ => PEpow x n - end - end. - -Theorem NPEpow_correct : forall l e n, - NPEeval l (NPEpow e n) == NPEeval l (PEpow e n). +Theorem PExpr_eq_semi_ok e e' : + PExpr_eq e e' = true -> (e === e')%poly. +Proof. +revert e'; induction e; destruct e'; simpl; try discriminate. +- intros H l. now apply (morph_eq CRmorph). +- case Pos.eqb_spec; intros; now subst. +- intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. +- intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. +- intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. +- intros H. now rewrite IHe. +- intros H. destruct (if_true _ _ H). + apply N.eqb_eq in H0. now rewrite IHe, H0. +Qed. + +Lemma PExpr_eq_spec e e' : BoolSpec (e === e')%poly True (PExpr_eq e e'). Proof. - destruct n;simpl. - rewrite pow_th.(rpow_pow_N);simpl;auto. - fold (p =? 1)%positive. - case Pos.eqb_spec; intros H; (rewrite H || clear H). - now rewrite pow_th.(rpow_pow_N). - destruct e;simpl;auto. - repeat apply ceqb_rect;simpl;intros;rewrite pow_th.(rpow_pow_N);simpl. - symmetry;induction p;simpl;trivial; ring [IHp H CRmorph.(morph1)]. - symmetry; induction p;simpl;trivial;ring [IHp CRmorph.(morph0)]. - induction p;simpl;auto;repeat rewrite CRmorph.(morph_mul);ring [IHp]. + assert (H := PExpr_eq_semi_ok e e'). + destruct PExpr_eq; constructor; intros; trivial. now apply H. Qed. -(* mul *) -Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C := - match x, y with - PEc c1, PEc c2 => PEc (cmul c1 c2) - | PEc c, _ => - if ceqb c cI then y else if ceqb c cO then PEc cO else PEmul x y - | _, PEc c => - if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y - | PEpow e1 n1, PEpow e2 n2 => - if N.eqb n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y - | _, _ => PEmul x y - end. +(** Smart constructors for polynomial expression, + with reduction of constants *) -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. +Definition NPEadd e1 e2 := + match e1, e2 with + | PEc c1, PEc c2 => PEc (c1 + c2) + | PEc c, _ => if (c =? 0)%coef then e2 else e1 + e2 + | _, PEc c => if (c =? 0)%coef then e1 else e1 + e2 + (* Peut t'on factoriser ici ??? *) + | _, _ => (e1 + e2) + end%poly. +Infix "++" := NPEadd (at level 60, right associativity). -Theorem NPEmul_correct : forall l e1 e2, - NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2). -induction e1;destruct e2; simpl;try reflexivity; - repeat apply ceqb_rect; - try (intro eq_c; rewrite eq_c); simpl; try reflexivity; - try ring [(morph0 CRmorph) (morph1 CRmorph)]. - apply (morph_mul CRmorph). -case N.eqb_spec; intros H; try rewrite <- H; clear H. -rewrite NPEpow_correct. simpl. -repeat rewrite pow_th.(rpow_pow_N). -rewrite IHe1; destruct n;simpl;try ring. -apply pow_pos_mul. -simpl;auto. +Theorem NPEadd_ok e1 e2 : (e1 ++ e2 === e1 + e2)%poly. +Proof. +intros l. +destruct e1, e2; simpl; try reflexivity; try (case ceqb_spec); +try intro H; try rewrite H; simpl; +try apply eq_refl; try (ring [phi_0]). +apply (morph_add CRmorph). Qed. -(* sub *) Definition NPEsub e1 e2 := match e1, e2 with - PEc c1, PEc c2 => PEc (csub c1 c2) - | PEc c, _ => if ceqb c cO then PEopp e2 else PEsub e1 e2 - | _, PEc c => if ceqb c cO then e1 else PEsub e1 e2 + | PEc c1, PEc c2 => PEc (c1 - c2) + | PEc c, _ => if (c =? 0)%coef then - e2 else e1 - e2 + | _, PEc c => if (c =? 0)%coef then e1 else e1 - e2 (* Peut-on factoriser ici *) - | _, _ => PEsub e1 e2 - end. + | _, _ => e1 - e2 + end%poly. +Infix "--" := NPEsub (at level 50, left associativity). -Theorem NPEsub_correct: - forall l e1 e2, NPEeval l (NPEsub e1 e2) == NPEeval l (PEsub e1 e2). -intros l e1 e2. -destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect; - try (intro eq_c; rewrite eq_c); simpl; - try rewrite (morph0 CRmorph); try reflexivity; +Theorem NPEsub_ok e1 e2: (e1 -- e2 === e1 - e2)%poly. +Proof. +intros l. +destruct e1, e2; simpl; try reflexivity; try case ceqb_spec; + try intro H; try rewrite H; simpl; + try rewrite phi_0; try reflexivity; 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. + match e1 with PEc c1 => PEc (- c1) | _ => - e1 end%poly. + +Theorem NPEopp_ok e : (NPEopp e === -e)%poly. +Proof. +intros l. destruct e; simpl; trivial. apply (morph_opp CRmorph). +Qed. + +Definition NPEpow x n := + match n with + | N0 => 1 + | Npos p => + if (p =? 1)%positive then x else + match x with + | PEc c => + if (c =? 1)%coef then 1 + else if (c =? 0)%coef then 0 + else PEc (pow_pos cmul c p) + | _ => x ^ n + end + end%poly. +Infix "^^" := NPEpow (at level 35, right associativity). -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). +Theorem NPEpow_ok e n : (e ^^ n === e ^ n)%poly. +Proof. + intros l. unfold NPEpow; destruct n. + - simpl; now rewrite rpow_pow. + - case Pos.eqb_spec; [intro; subst | intros _]. + + simpl. now rewrite rpow_pow. + + destruct e;simpl;trivial. + repeat case ceqb_spec; intros; rewrite ?rpow_pow, ?H; simpl. + * now rewrite phi_1, pow_pos_1. + * now rewrite phi_0, pow_pos_0. + * now rewrite pow_pos_cst. +Qed. + +Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C := + match x, y with + | PEc c1, PEc c2 => PEc (c1 * c2) + | PEc c, _ => if (c =? 1)%coef then y else if (c =? 0)%coef then 0 else x * y + | _, PEc c => if (c =? 1)%coef then x else if (c =? 0)%coef then 0 else x * y + | e1 ^ n1, e2 ^ n2 => if (n1 =? n2)%N then (NPEmul e1 e2)^^n1 else x * y + | _, _ => x * y + end%poly. +Infix "**" := NPEmul (at level 40, left associativity). + +Theorem NPEmul_ok e1 e2 : (e1 ** e2 === e1 * e2)%poly. +Proof. +intros l. +revert e2; induction e1;destruct e2; simpl;try reflexivity; + repeat (case ceqb_spec; intro H; try rewrite H; clear H); + simpl; try reflexivity; try ring [phi_0 phi_1]. + apply (morph_mul CRmorph). +case N.eqb_spec; [intros <- | reflexivity]. +rewrite NPEpow_ok. simpl. +rewrite !rpow_pow. rewrite IHe1. +destruct n; simpl; [ ring | apply pow_pos_mul_l ]. Qed. (* simplification *) -Fixpoint PExpr_simp (e : PExpr C) : PExpr C := +Fixpoint PEsimp (e : PExpr C) : PExpr C := match e with - PEadd e1 e2 => NPEadd (PExpr_simp e1) (PExpr_simp e2) - | PEmul e1 e2 => NPEmul (PExpr_simp e1) (PExpr_simp e2) - | PEsub e1 e2 => NPEsub (PExpr_simp e1) (PExpr_simp e2) - | PEopp e1 => NPEopp (PExpr_simp e1) - | PEpow e1 n1 => NPEpow (PExpr_simp e1) n1 + | e1 + e2 => (PEsimp e1) ++ (PEsimp e2) + | e1 * e2 => (PEsimp e1) ** (PEsimp e2) + | e1 - e2 => (PEsimp e1) -- (PEsimp e2) + | - e1 => NPEopp (PEsimp e1) + | e1 ^ n1 => (PEsimp e1) ^^ n1 | _ => e - end. + end%poly. -Theorem PExpr_simp_correct: - forall l e, NPEeval l (PExpr_simp e) == NPEeval l e. -intros l e; elim e; simpl; auto. -intros e1 He1 e2 He2. -transitivity (NPEeval l (PEadd (PExpr_simp e1) (PExpr_simp e2))); auto. -apply NPEadd_correct. -simpl; auto. -intros e1 He1 e2 He2. -transitivity (NPEeval l (PEsub (PExpr_simp e1) (PExpr_simp e2))); auto. -apply NPEsub_correct. -simpl; auto. -intros e1 He1 e2 He2. -transitivity (NPEeval l (PEmul (PExpr_simp e1) (PExpr_simp e2))); auto. -apply NPEmul_correct. -simpl; auto. -intros e1 He1. -transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto. -apply NPEopp_correct. -simpl; auto. -intros e1 He1 n;simpl. -rewrite NPEpow_correct;simpl. -repeat rewrite pow_th.(rpow_pow_N). -rewrite He1;auto. +Theorem PEsimp_ok e : (PEsimp e === e)%poly. +Proof. +induction e; simpl. +- reflexivity. +- reflexivity. +- intro l; trivial. +- intro l; trivial. +- rewrite NPEadd_ok. now f_equiv. +- rewrite NPEsub_ok. now f_equiv. +- rewrite NPEmul_ok. now f_equiv. +- rewrite NPEopp_ok. now f_equiv. +- rewrite NPEpow_ok. now f_equiv. Qed. @@ -592,7 +721,9 @@ Qed. (* The input: syntax of a field expression *) Inductive FExpr : Type := - FEc: C -> FExpr + | FEO : FExpr + | FEI : FExpr + | FEc: C -> FExpr | FEX: positive -> FExpr | FEadd: FExpr -> FExpr -> FExpr | FEsub: FExpr -> FExpr -> FExpr @@ -604,6 +735,8 @@ Inductive FExpr : Type := Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := match pe with + | FEO => rO + | FEI => rI | FEc c => phi c | FEX x => BinList.nth 0 x l | FEadd x y => FEeval l x + FEeval l y @@ -633,44 +766,46 @@ Record linear : Type := mk_linear { Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop := match le with | nil => True - | e1 :: nil => ~ req (NPEeval l e1) rO - | e1 :: l1 => ~ req (NPEeval l e1) rO /\ PCond l l1 + | e1 :: nil => ~ req (e1 @ l) rO + | e1 :: l1 => ~ req (e1 @ l) rO /\ PCond l l1 end. -Theorem PCond_cons_inv_l : - forall l a l1, PCond l (a::l1) -> ~ NPEeval l a == 0. -intros l a l1 H. -destruct l1; simpl in H |- *; trivial. -destruct H; trivial. +Theorem PCond_cons l a l1 : + PCond l (a :: l1) <-> ~ a @ l == 0 /\ PCond l l1. +Proof. +destruct l1. +- simpl. split; [split|destruct 1]; trivial. +- reflexivity. 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. -destruct H; trivial. +Theorem PCond_cons_inv_l l a l1 : PCond l (a::l1) -> ~ a @ l == 0. +Proof. +rewrite PCond_cons. now destruct 1. Qed. -Theorem PCond_app_inv_l: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l1. -intros l l1 l2; elim l1; simpl app. - simpl; auto. - destruct l0; simpl in *. - destruct l2; firstorder. - firstorder. +Theorem PCond_cons_inv_r l a l1 : PCond l (a :: l1) -> PCond l l1. +Proof. +rewrite PCond_cons. now destruct 1. 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 ). +Theorem PCond_app l l1 l2 : + PCond l (l1 ++ l2) <-> PCond l l1 /\ PCond l l2. +Proof. +induction l1. +- simpl. split; [split|destruct 1]; trivial. +- simpl app. rewrite !PCond_cons, IHl1. symmetry; apply and_assoc. Qed. + (* An unsatisfiable condition: issued when a division by zero is detected *) -Definition absurd_PCond := cons (PEc cO) nil. +Definition absurd_PCond := cons 0%poly nil. Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond. +Proof. unfold absurd_PCond; simpl. red; intros. apply H. -apply (morph0 CRmorph). +apply phi_0. Qed. (*************************************************************************** @@ -679,167 +814,124 @@ Qed. ***************************************************************************) -Fixpoint isIn (e1:PExpr C) (p1:positive) - (e2:PExpr C) (p2:positive) {struct e2}: option (N * PExpr C) := +Definition default_isIn e1 p1 e2 p2 := + if PExpr_eq e1 e2 then + match Z.pos_sub p1 p2 with + | Zpos p => Some (Npos p, 1%poly) + | Z0 => Some (N0, 1%poly) + | Zneg p => Some (N0, e2 ^^ Npos p) + end + else None. + +Fixpoint isIn e1 p1 e2 p2 {struct e2}: option (N * PExpr C) := match e2 with - | PEmul e3 e4 => + | e3 * e4 => match isIn e1 p1 e3 p2 with - | Some (N0, e5) => Some (N0, NPEmul e5 (NPEpow e4 (Npos p2))) + | Some (N0, e5) => Some (N0, e5 ** (e4 ^^ Npos p2)) | 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))) + | Some (n, e6) => Some (n, e5 ** e6) + | None => Some (Npos p, e5 ** (e4 ^^ Npos p2)) end | None => match isIn e1 p1 e4 p2 with - | Some (n, e5) => Some (n,NPEmul (NPEpow e3 (Npos p2)) e5) + | Some (n, e5) => Some (n, (e3 ^^ Npos p2) ** e5) | None => None end end - | PEpow e3 N0 => None - | PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pos.mul p3 p2) - | _ => - if PExpr_eq e1 e2 then - match Z.pos_sub p1 p2 with - | Zpos p => Some (Npos p, PEc cI) - | Z0 => Some (N0, PEc cI) - | Zneg p => Some (N0, NPEpow e2 (Npos p)) - end - else None - end. + | e3 ^ N0 => None + | e3 ^ Npos p3 => isIn e1 p1 e3 (Pos.mul p3 p2) + | _ => default_isIn e1 p1 e2 p2 + end%poly. 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_add := - (Ring_theory.pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)). - Lemma Z_pos_sub_gt p q : (p > q)%positive -> Z.pos_sub p q = Zpos (p - q). Proof. intros; now apply Z.pos_sub_gt, Pos.gt_lt. Qed. Ltac simpl_pos_sub := rewrite ?Z_pos_sub_gt in * by assumption. - Lemma isIn_correct_aux : forall l e1 e2 p1 p2, - match - (if PExpr_eq e1 e2 then - match Z.sub (Zpos p1) (Zpos p2) with - | Zpos p => Some (Npos p, PEc cI) - | Z0 => Some (N0, PEc cI) - | Zneg p => Some (N0, NPEpow e2 (Npos p)) - end - else None) - with + Lemma default_isIn_ok e1 e2 p1 p2 : + match default_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 + let n' := ZtoN (Zpos p1 - NtoZ n) in + (e2 ^ N.pos p2 === e1 ^ n' * e3)%poly + /\ (Zpos p1 > NtoZ n)%Z + | _ => True end. Proof. - intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2); - case (PExpr_eq e1 e2); simpl; auto; intros H. + unfold default_isIn. + case PExpr_eq_spec; trivial. intros EQ. rewrite Z.pos_sub_spec. - case Pos.compare_spec;intros;simpl. - - repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:reflexivity. - subst. rewrite H by trivial. ring [ (morph1 CRmorph)]. - - fold (p2 - p1 =? 1)%positive. - fold (NPEpow e2 (Npos (p2 - p1))). - rewrite NPEpow_correct;simpl. - repeat rewrite pow_th.(rpow_pow_N);simpl. - rewrite H;trivial. split. 2:reflexivity. - rewrite <- pow_pos_add. now rewrite Pos.add_comm, Pos.sub_add. - - repeat rewrite pow_th.(rpow_pow_N);simpl. - rewrite H;trivial. - rewrite Z.pos_sub_gt by now apply Pos.sub_decr. - replace (p1 - (p1 - p2))%positive with p2; - [| rewrite Pos.sub_sub_distr, Pos.add_comm; - auto using Pos.add_sub, Pos.sub_decr ]. - split. - simpl. ring [ (morph1 CRmorph)]. - now apply Z.lt_gt, Pos.sub_decr. -Qed. - -Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2). -induction p1;simpl;intros;repeat rewrite pow_pos_mul;repeat rewrite pow_pos_add;simpl. -ring [(IHp1 p2)]. ring [(IHp1 p2)]. auto. -Qed. - - -Theorem isIn_correct: forall l e1 p1 e2 p2, + case Pos.compare_spec;intros H; split; try reflexivity. + - simpl. now rewrite PE_1_r, H, EQ. + - rewrite NPEpow_ok, EQ, <- PEpow_add_r. f_equiv. + simpl. f_equiv. now rewrite Pos.add_comm, Pos.sub_add. + - simpl. rewrite PE_1_r, EQ. f_equiv. + rewrite Z.pos_sub_gt by now apply Pos.sub_decr. simpl. f_equiv. + rewrite Pos.sub_sub_distr, Pos.add_comm; trivial. + rewrite Pos.add_sub; trivial. + apply Pos.sub_decr; trivial. + - simpl. now apply Z.lt_gt, Pos.sub_decr. +Qed. + +Ltac npe_simpl := rewrite ?NPEmul_ok, ?NPEpow_ok, ?PEpow_mul_l. +Ltac npe_ring := intro l; simpl; ring. + +Theorem isIn_ok e1 p1 e2 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 + let n' := ZtoN (Zpos p1 - NtoZ n) in + (e2 ^ N.pos p2 === e1 ^ n' * e3)%poly + /\ (Zpos p1 > NtoZ n)%Z | _ => True end. Proof. 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. - 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]. - generalize (H0 p4 p2);clear H0;destruct (isIn e1 p4 p0 p2). destruct p5. - destruct n;simpl. - rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl. - intros (H1,H2) (H3,H4). - simpl_pos_sub. simpl in H3. - rewrite pow_pos_mul. rewrite H1;rewrite H3. - assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 * - (pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) == - pow_pos rmul (NPEeval l e1) p4 * pow_pos rmul (NPEeval l e1) (p1 - p4) * - NPEeval l p3 *NPEeval l p5) by ring. rewrite H;clear H. - rewrite <- pow_pos_add. - rewrite Pos.add_comm, Pos.sub_add by (now apply Z.gt_lt in H4). - split. symmetry;apply ARth.(ARmul_assoc). reflexivity. - repeat rewrite pow_th.(rpow_pow_N);simpl. - intros (H1,H2) (H3,H4). - simpl_pos_sub. simpl in H1, H3. - assert (Zpos p1 > Zpos p6)%Z. - apply Zgt_trans with (Zpos p4). exact H4. exact H2. - simpl_pos_sub. - split. 2:exact H. - rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3. - assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 * - (pow_pos rmul (NPEeval l e1) (p4 - p6) * NPEeval l p5) == - pow_pos rmul (NPEeval l e1) (p1 - p4) * pow_pos rmul (NPEeval l e1) (p4 - p6) * - NPEeval l p3 * NPEeval l p5) by ring. rewrite H0;clear H0. - rewrite <- pow_pos_add. - replace (p1 - p4 + (p4 - p6))%positive with (p1 - p6)%positive. - rewrite NPEmul_correct. simpl;ring. - assert - (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z. - change ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z). - rewrite <- Z.add_assoc. rewrite (Z.add_assoc (- Zpos p4)). - simpl. rewrite Z.pos_sub_diag. simpl. reflexivity. - unfold Z.sub, Z.opp in H0. simpl in H0. - simpl_pos_sub. inversion H0; trivial. - simpl. repeat rewrite pow_th.(rpow_pow_N). - intros H1 (H2,H3). simpl_pos_sub. - rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. - simpl in H2. rewrite pow_th.(rpow_pow_N);simpl. - rewrite pow_pos_mul. split. ring [H2]. exact H3. - generalize (H0 p1 p2);clear H0;destruct (isIn e1 p1 p0 p2). destruct p3. - destruct n;simpl. rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. - repeat rewrite pow_th.(rpow_pow_N);simpl. - intros (H1,H2);split;trivial. rewrite pow_pos_mul;ring [H1]. - rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. - repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul. - intros (H1, H2);rewrite H1;split. - simpl_pos_sub. simpl in H1;ring [H1]. trivial. - trivial. - destruct n. trivial. - generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3. - destruct n;simpl. repeat rewrite pow_th.(rpow_pow_N). simpl. - intros (H1,H2);split. rewrite pow_pos_pow_pos. trivial. trivial. - repeat rewrite pow_th.(rpow_pow_N). simpl. - intros (H1,H2);split;trivial. - rewrite pow_pos_pow_pos;trivial. - trivial. +revert p1 p2. +induction e2; intros p1 p2; + try refine (default_isIn_ok e1 _ p1 p2); simpl isIn. +- specialize (IHe2_1 p1 p2). + destruct isIn as [([|p],e)|]. + + split; [|reflexivity]. + clear IHe2_2. + destruct IHe2_1 as (IH,_). + npe_simpl. rewrite IH. npe_ring. + + specialize (IHe2_2 p p2). + destruct isIn as [([|p'],e')|]. + * destruct IHe2_1 as (IH1,GT1). + destruct IHe2_2 as (IH2,GT2). + split; [|simpl; apply Zgt_trans with (Z.pos p); trivial]. + npe_simpl. rewrite IH1, IH2. simpl. simpl_pos_sub. simpl. + replace (N.pos p1) with (N.pos p + N.pos (p1 - p))%N. + rewrite PEpow_add_r; npe_ring. + { simpl. f_equal. rewrite Pos.add_comm, Pos.sub_add. trivial. + now apply Pos.gt_lt. } + * destruct IHe2_1 as (IH1,GT1). + destruct IHe2_2 as (IH2,GT2). + assert (Z.pos p1 > Z.pos p')%Z by (now apply Zgt_trans with (Zpos p)). + split; [|simpl; trivial]. + npe_simpl. rewrite IH1, IH2. simpl. simpl_pos_sub. simpl. + replace (N.pos (p1 - p')) with (N.pos (p1 - p) + N.pos (p - p'))%N. + rewrite PEpow_add_r; npe_ring. + { simpl. f_equal. rewrite Pos.add_sub_assoc, Pos.sub_add; trivial. + now apply Pos.gt_lt. + now apply Pos.gt_lt. } + * destruct IHe2_1 as (IH,GT). split; trivial. + npe_simpl. rewrite IH. npe_ring. + + specialize (IHe2_2 p1 p2). + destruct isIn as [(n,e)|]; trivial. + destruct IHe2_2 as (IH,GT). split; trivial. + set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d. + npe_simpl. rewrite IH. npe_ring. +- destruct n; trivial. + specialize (IHe2 p1 (p * p2)%positive). + destruct isIn as [(n,e)|]; trivial. + destruct IHe2 as (IH,GT). split; trivial. + set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d. + now rewrite <- PEpow_mul_r. Qed. Record rsplit : Type := mk_rsplit { @@ -852,121 +944,122 @@ Notation left := rsplit_left. Notation right := rsplit_right. Notation common := rsplit_common. -Fixpoint split_aux (e1: PExpr C) (p:positive) (e2:PExpr C) {struct e1}: rsplit := +Fixpoint split_aux e1 p e2 {struct e1}: rsplit := match e1 with - | PEmul e3 e4 => + | e3 * e4 => let r1 := split_aux e3 p e2 in let r2 := split_aux e4 p (right r1) in - mk_rsplit (NPEmul (left r1) (left r2)) - (NPEmul (common r1) (common r2)) - (right r2) - | PEpow e3 N0 => mk_rsplit (PEc cI) (PEc cI) e2 - | PEpow e3 (Npos p3) => split_aux e3 (Pos.mul p3 p) e2 + mk_rsplit (left r1 ** left r2) + (common r1 ** common r2) + (right r2) + | e3 ^ N0 => mk_rsplit 1 1 e2 + | e3 ^ Npos p3 => split_aux e3 (Pos.mul p3 p) e2 | _ => - match isIn e1 p e2 xH with - | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3 - | 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 + match isIn e1 p e2 1 with + | Some (N0,e3) => mk_rsplit 1 (e1 ^^ Npos p) e3 + | Some (Npos q, e3) => mk_rsplit (e1 ^^ Npos q) (e1 ^^ Npos (p - q)) e3 + | None => mk_rsplit (e1 ^^ Npos p) 1 e2 end - end. + end%poly. -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 (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 - NPEeval l (PEpow e1 (Npos p)) == NPEeval l (NPEmul (left res) (common res)) - /\ - NPEeval l e2 == NPEeval l (NPEmul (right res) (common res)). -Proof. - intros. unfold res;clear res; generalize (isIn_correct l e1 p e2 xH). - destruct (isIn e1 p e2 1). destruct p0. +Lemma split_aux_ok1 e1 p e2 : + (let res := match isIn e1 p e2 1 with + | Some (N0,e3) => mk_rsplit 1 (e1 ^^ Npos p) e3 + | Some (Npos q, e3) => mk_rsplit (e1 ^^ Npos q) (e1 ^^ Npos (p - q)) e3 + | None => mk_rsplit (e1 ^^ Npos p) 1 e2 + end + in + e1 ^ Npos p === left res * common res + /\ e2 === right res * common res)%poly. +Proof. Opaque NPEpow NPEmul. - destruct n;simpl; - (repeat rewrite NPEmul_correct;simpl; - repeat rewrite NPEpow_correct;simpl; - repeat rewrite pow_th.(rpow_pow_N);simpl). - intros (H, Hgt);split;try ring [H CRmorph.(morph1)]. - intros (H, Hgt). simpl_pos_sub. simpl in H;split;try ring [H]. - apply Z.gt_lt in Hgt. - now rewrite <- pow_pos_add, Pos.add_comm, Pos.sub_add. - simpl;intros. repeat rewrite NPEmul_correct;simpl. - rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)]. -Qed. - -Theorem split_aux_correct: forall l e1 p e2, - 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)) - (common (split_aux 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. -simpl. repeat (rewrite NPEmul_correct;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. -destruct n;simpl. -split. repeat rewrite pow_th.(rpow_pow_N);simpl. -rewrite NPEmul_correct. simpl. - induction k;simpl;try ring [CRmorph.(morph1)]; ring [IHk CRmorph.(morph1)]. - rewrite NPEmul_correct;simpl. ring [CRmorph.(morph1)]. -generalize (IHe1 (p*k)%positive e2);clear IHe1;simpl. -repeat rewrite NPEmul_correct;simpl. -repeat rewrite pow_th.(rpow_pow_N);simpl. -rewrite pow_pos_pow_pos. intros [H1 H2];split;ring [H1 H2]. + intros. unfold res;clear res; generalize (isIn_ok e1 p e2 xH). + destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl. + - intros (H1,H2); split; npe_simpl. + + now rewrite PE_1_l. + + rewrite PEpow_1_r in H1. rewrite H1. npe_ring. + - intros (H1,H2); split; npe_simpl. + + rewrite <- PEpow_add_r. f_equiv. simpl. f_equal. + rewrite Pos.add_comm, Pos.sub_add; trivial. + now apply Z.gt_lt in H2. + + rewrite PEpow_1_r in H1. rewrite H1. simpl_pos_sub. simpl. npe_ring. + - intros _; split; npe_simpl; now rewrite PE_1_r. +Qed. + +Theorem split_aux_ok: forall e1 p e2, + (e1 ^ Npos p === left (split_aux e1 p e2) * common (split_aux e1 p e2) + /\ e2 === right (split_aux e1 p e2) * common (split_aux e1 p e2))%poly. +Proof. +induction e1;intros k e2; try refine (split_aux_ok1 _ k e2);simpl. +destruct (IHe1_1 k e2) as (H1,H2). +destruct (IHe1_2 k (right (split_aux e1_1 k e2))) as (H3,H4). +clear IHe1_1 IHe1_2. +- npe_simpl; split. + * rewrite H1, H3. npe_ring. + * rewrite H2 at 1. rewrite H4 at 1. npe_ring. +- destruct n; simpl. + + rewrite PEpow_0_r, PEpow_1_l, !PE_1_r. now split. + + rewrite <- PEpow_mul_r. simpl. apply IHe1. 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))). +Theorem split_ok_l e1 e2 : + (e1 === left (split e1 e2) * common (split e1 e2))%poly. +Proof. +destruct (split_aux_ok e1 xH e2) as (H,_). now rewrite <- H, PEpow_1_r. +Qed. + +Theorem split_ok_r e1 e2 : + (e2 === right (split e1 e2) * common (split e1 e2))%poly. Proof. -intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl. -rewrite pow_th.(rpow_pow_N);simpl;auto. +destruct (split_aux_ok e1 xH e2) as (_,H). trivial. Qed. -Theorem split_correct_r: forall l e1 e2, - NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2)) - (common (split e1 e2))). +Lemma split_nz_l l e1 e2 : + ~ e1 @ l == 0 -> ~ left (split e1 e2) @ l == 0. Proof. -intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl;auto. + intros H. contradict H. rewrite (split_ok_l e1 e2); simpl. + now rewrite H, rmul_0_l. +Qed. + +Lemma split_nz_r l e1 e2 : + ~ e2 @ l == 0 -> ~ right (split e1 e2) @ l == 0. +Proof. + intros H. contradict H. rewrite (split_ok_r e1 e2); simpl. + now rewrite H, rmul_0_l. Qed. 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 + | FEO => mk_linear 0 1 nil + | FEI => mk_linear 1 1 nil + | FEc c => mk_linear (PEc c) 1 nil + | FEX x => mk_linear (PEX C x) 1 nil | FEadd e1 e2 => let x := Fnorm e1 in let y := Fnorm e2 in let s := split (denum x) (denum y) in mk_linear - (NPEadd (NPEmul (num x) (right s)) (NPEmul (num y) (left s))) - (NPEmul (left s) (NPEmul (right s) (common s))) - (condition x ++ condition y) - + ((num x ** right s) ++ (num y ** left s)) + (left s ** (right s ** common s)) + (condition x ++ condition y)%list | FEsub e1 e2 => let x := Fnorm e1 in let y := Fnorm e2 in let s := split (denum x) (denum y) in mk_linear - (NPEsub (NPEmul (num x) (right s)) (NPEmul (num y) (left s))) - (NPEmul (left s) (NPEmul (right s) (common s))) - (condition x ++ condition y) + ((num x ** right s) -- (num y ** left s)) + (left s ** (right s ** common s)) + (condition x ++ condition y)%list | FEmul e1 e2 => let x := Fnorm e1 in let y := Fnorm e2 in let s1 := split (num x) (denum y) in let s2 := split (num y) (denum x) in - mk_linear (NPEmul (left s1) (left s2)) - (NPEmul (right s2) (right s1)) - (condition x ++ condition y) + mk_linear (left s1 ** left s2) + (right s2 ** right s1) + (condition x ++ condition y)%list | FEopp e1 => let x := Fnorm e1 in mk_linear (NPEopp (num x)) (denum x) (condition x) @@ -978,15 +1071,14 @@ Fixpoint Fnorm (e : FExpr) : linear := let y := Fnorm e2 in let s1 := split (num x) (num y) in let s2 := split (denum x) (denum y) in - mk_linear (NPEmul (left s1) (right s2)) - (NPEmul (left s2) (right s1)) - (num y :: condition x ++ condition y) + mk_linear (left s1 ** right s2) + (left s2 ** right s1) + (num y :: condition x ++ condition y)%list | FEpow e1 n => let x := Fnorm e1 in - mk_linear (NPEpow (num x) n) (NPEpow (denum x) n) (condition x) + mk_linear ((num x)^^n) ((denum x)^^n) (condition x) end. - (* Example *) (* Eval compute @@ -996,93 +1088,31 @@ Eval compute (FEadd (FEinv (FEX xH%positive)) (FEinv (FEX (xO xH)%positive))))). *) - Lemma pow_pos_not_0 : forall x, ~x==0 -> forall p, ~pow_pos rmul x p == 0. +Theorem Pcond_Fnorm l e : + PCond l (condition (Fnorm e)) -> ~ (denum (Fnorm e))@l == 0. 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). - reflexivity. - 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. -intros l e; elim e. - simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO. - simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO. - intros e1 Hrec1 e2 Hrec2 Hcond. - simpl condition in Hcond. - simpl denum. - rewrite NPEmul_correct. - simpl. - apply field_is_integral_domain. - intros HH; case Hrec1; auto. - apply PCond_app_inv_l with (1 := Hcond). - rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))). - rewrite NPEmul_correct; simpl; rewrite HH; ring. - intros HH; case Hrec2; auto. - apply PCond_app_inv_r with (1 := Hcond). - rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto. - intros e1 Hrec1 e2 Hrec2 Hcond. - simpl condition in Hcond. - simpl denum. - rewrite NPEmul_correct. - simpl. - apply field_is_integral_domain. - intros HH; case Hrec1; auto. - apply PCond_app_inv_l with (1 := Hcond). - rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))). - rewrite NPEmul_correct; simpl; rewrite HH; ring. - intros HH; case Hrec2; auto. - apply PCond_app_inv_r with (1 := Hcond). - rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto. - intros e1 Hrec1 e2 Hrec2 Hcond. - simpl condition in Hcond. - simpl denum. - rewrite NPEmul_correct. - simpl. - apply field_is_integral_domain. - intros HH; apply Hrec1. - apply PCond_app_inv_l with (1 := Hcond). - rewrite (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))). - rewrite NPEmul_correct; simpl; rewrite HH; ring. - intros HH; apply Hrec2. - apply PCond_app_inv_r with (1 := Hcond). - rewrite (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2))). - rewrite NPEmul_correct; simpl; rewrite HH; ring. - intros e1 Hrec1 Hcond. - simpl condition in Hcond. - simpl denum. - auto. - intros e1 Hrec1 Hcond. - simpl condition in Hcond. - simpl denum. - apply PCond_cons_inv_l with (1:=Hcond). - intros e1 Hrec1 e2 Hrec2 Hcond. - simpl condition in Hcond. - simpl denum. - rewrite NPEmul_correct. - simpl. - apply field_is_integral_domain. - intros HH; apply Hrec1. - specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1. - apply PCond_app_inv_l with (1 := Hcond1). - rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))). - rewrite NPEmul_correct; simpl; rewrite HH; ring. - intros HH; apply PCond_cons_inv_l with (1:=Hcond). - rewrite (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2))). - rewrite NPEmul_correct; simpl; rewrite HH; ring. - simpl;intros e1 Hrec1 n Hcond. - rewrite NPEpow_correct. - simpl;rewrite pow_th.(rpow_pow_N). - destruct n;simpl;intros. - apply AFth.(AF_1_neq_0). apply pow_pos_not_0;auto. -Qed. -Hint Resolve Pcond_Fnorm. +induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app; + simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok. +- simpl. rewrite phi_1; exact rI_neq_rO. +- simpl. rewrite phi_1; exact rI_neq_rO. +- simpl; intros. rewrite phi_1; exact rI_neq_rO. +- simpl; intros. rewrite phi_1; exact rI_neq_rO. +- rewrite <- split_ok_r. simpl. apply field_is_integral_domain. + + apply split_nz_l, IHe1, Hc1. + + apply IHe2, Hc2. +- rewrite <- split_ok_r. simpl. apply field_is_integral_domain. + + apply split_nz_l, IHe1, Hc1. + + apply IHe2, Hc2. +- simpl. apply field_is_integral_domain. + + apply split_nz_r, IHe1, Hc1. + + apply split_nz_r, IHe2, Hc2. +- now apply IHe. +- trivial. +- destruct Hc2 as (Hc2,_). simpl. apply field_is_integral_domain. + + apply split_nz_l, IHe1, Hc2. + + apply split_nz_r, Hc1. +- rewrite NPEpow_ok. apply PEpow_nz, IHe, Hc. +Qed. (*************************************************************************** @@ -1091,154 +1121,106 @@ Hint Resolve Pcond_Fnorm. ***************************************************************************) -Theorem Fnorm_FEeval_PEeval: - forall l fe, +Ltac uneval := + repeat match goal with + | |- context [ ?x @ ?l * ?y @ ?l ] => change (x@l * y@l) with ((x*y)@l) + | |- context [ ?x @ ?l + ?y @ ?l ] => change (x@l + y@l) with ((x+y)@l) + end. + +Theorem Fnorm_FEeval_PEeval l fe: PCond l (condition (Fnorm fe)) -> - FEeval l fe == NPEeval l (num (Fnorm fe)) / NPEeval l (denum (Fnorm fe)). -Proof. -intros l fe; elim fe; simpl. -intros c H; rewrite CRmorph.(morph1); apply rdiv1. -intros p H; rewrite CRmorph.(morph1); apply rdiv1. -intros e1 He1 e2 He2 HH. -assert (HH1: PCond l (condition (Fnorm e1))). -apply PCond_app_inv_l with ( 1 := HH ). -assert (HH2: PCond l (condition (Fnorm e2))). -apply PCond_app_inv_r with ( 1 := HH ). -rewrite (He1 HH1); rewrite (He2 HH2). -rewrite NPEadd_correct; simpl. -repeat rewrite NPEmul_correct; simpl. -generalize (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))) - (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))). -repeat rewrite NPEmul_correct; simpl. -intros U1 U2; rewrite U1; rewrite U2. -apply rdiv2b; auto. - rewrite <- U1; auto. - rewrite <- U2; auto. - -intros e1 He1 e2 He2 HH. -assert (HH1: PCond l (condition (Fnorm e1))). -apply PCond_app_inv_l with ( 1 := HH ). -assert (HH2: PCond l (condition (Fnorm e2))). -apply PCond_app_inv_r with ( 1 := HH ). -rewrite (He1 HH1); rewrite (He2 HH2). -rewrite NPEsub_correct; simpl. -repeat rewrite NPEmul_correct; simpl. -generalize (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))) - (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))). -repeat rewrite NPEmul_correct; simpl. -intros U1 U2; rewrite U1; rewrite U2. -apply rdiv3b; auto. - rewrite <- U1; auto. - rewrite <- U2; auto. - -intros e1 He1 e2 He2 HH. -assert (HH1: PCond l (condition (Fnorm e1))). -apply PCond_app_inv_l with ( 1 := HH ). -assert (HH2: PCond l (condition (Fnorm e2))). -apply PCond_app_inv_r with ( 1 := HH ). -rewrite (He1 HH1); rewrite (He2 HH2). -repeat rewrite NPEmul_correct; simpl. -generalize (split_correct_l l (num (Fnorm e1)) (denum (Fnorm e2))) - (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2))) - (split_correct_l l (num (Fnorm e2)) (denum (Fnorm e1))) - (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))). -repeat rewrite NPEmul_correct; simpl. -intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3; - rewrite U4; simpl. -apply rdiv4b; auto. - rewrite <- U4; auto. - rewrite <- U2; auto. - -intros e1 He1 HH. -rewrite NPEopp_correct; simpl; rewrite (He1 HH); apply rdiv5; auto. - -intros e1 He1 HH. -assert (HH1: PCond l (condition (Fnorm e1))). -apply PCond_cons_inv_r with ( 1 := HH ). -rewrite (He1 HH1); apply rdiv6; auto. -apply PCond_cons_inv_l with ( 1 := HH ). - -intros e1 He1 e2 He2 HH. -assert (HH1: PCond l (condition (Fnorm e1))). -apply PCond_app_inv_l with (condition (Fnorm e2)). -apply PCond_cons_inv_r with ( 1 := HH ). -assert (HH2: PCond l (condition (Fnorm e2))). -apply PCond_app_inv_r with (condition (Fnorm e1)). -apply PCond_cons_inv_r with ( 1 := HH ). -rewrite (He1 HH1); rewrite (He2 HH2). -repeat rewrite NPEmul_correct;simpl. -generalize (split_correct_l l (num (Fnorm e1)) (num (Fnorm e2))) - (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2))) - (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))) - (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))). -repeat rewrite NPEmul_correct; simpl. -intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3; - rewrite U4; simpl. -apply rdiv7b; auto. - rewrite <- U3; auto. - rewrite <- U2; auto. -apply PCond_cons_inv_l with ( 1 := HH ). - rewrite <- U4; auto. - -intros e1 He1 n Hcond;assert (He1' := He1 Hcond);clear He1. -repeat rewrite NPEpow_correct;simpl;repeat rewrite pow_th.(rpow_pow_N). -rewrite He1';clear He1'. -destruct n;simpl. apply rdiv1. -generalize (NPEeval l (num (Fnorm e1))) (NPEeval l (denum (Fnorm e1))) - (Pcond_Fnorm _ _ Hcond). -intros r r0 Hdiff;induction p;simpl. -repeat (rewrite <- rdiv4;trivial). -rewrite IHp. reflexivity. -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. -rewrite IHp;reflexivity. -apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial. -reflexivity. -Qed. - -Theorem Fnorm_crossproduct: - forall l fe1 fe2, + FEeval l fe == (num (Fnorm fe)) @ l / (denum (Fnorm fe)) @ l. +Proof. +induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl; + intros (Hc1,Hc2) || intros Hc; + try (specialize (IHfe1 Hc1);apply Pcond_Fnorm in Hc1); + try (specialize (IHfe2 Hc2);apply Pcond_Fnorm in Hc2); + try set (F1 := Fnorm fe1) in *; try set (F2 := Fnorm fe2) in *. + +- now rewrite phi_1, phi_0, rdiv_def. +- now rewrite phi_1; apply rdiv1. +- rewrite phi_1; apply rdiv1. +- rewrite phi_1; apply rdiv1. +- rewrite NPEadd_ok, !NPEmul_ok. simpl. + rewrite <- rdiv2b; uneval; rewrite <- ?split_ok_l, <- ?split_ok_r; trivial. + now f_equiv. + +- rewrite NPEsub_ok, !NPEmul_ok. simpl. + rewrite <- rdiv3b; uneval; rewrite <- ?split_ok_l, <- ?split_ok_r; trivial. + now f_equiv. + +- rewrite !NPEmul_ok. simpl. + rewrite IHfe1, IHfe2. + rewrite (split_ok_l (num F1) (denum F2) l), + (split_ok_r (num F1) (denum F2) l), + (split_ok_l (num F2) (denum F1) l), + (split_ok_r (num F2) (denum F1) l) in *. + apply rdiv4b; trivial. + +- rewrite NPEopp_ok; simpl; rewrite (IHfe Hc); apply rdiv5. + +- rewrite (IHfe Hc2); apply rdiv6; trivial; + apply Pcond_Fnorm; trivial. + +- destruct Hc2 as (Hc2,Hc3). + rewrite !NPEmul_ok. simpl. + assert (U1 := split_ok_l (num F1) (num F2) l). + assert (U2 := split_ok_r (num F1) (num F2) l). + assert (U3 := split_ok_l (denum F1) (denum F2) l). + assert (U4 := split_ok_r (denum F1) (denum F2) l). + rewrite (IHfe1 Hc2), (IHfe2 Hc3), U1, U2, U3, U4. + simpl in U2, U3, U4. apply rdiv7b; + rewrite <- ?U2, <- ?U3, <- ?U4; try apply Pcond_Fnorm; trivial. + +- rewrite !NPEpow_ok. simpl. rewrite !rpow_pow, (IHfe Hc). + destruct n; simpl. + + apply rdiv1. + + apply pow_pos_div. apply Pcond_Fnorm; trivial. +Qed. + +Theorem Fnorm_crossproduct l fe1 fe2 : let nfe1 := Fnorm fe1 in let nfe2 := Fnorm fe2 in - NPEeval l (PEmul (num nfe1) (denum nfe2)) == - NPEeval l (PEmul (num nfe2) (denum nfe1)) -> + (num nfe1 * denum nfe2) @ l == (num nfe2 * denum nfe1) @ l -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. -intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2. -rewrite Fnorm_FEeval_PEeval by - apply PCond_app_inv_l with (1 := Hcond). - rewrite Fnorm_FEeval_PEeval by - apply PCond_app_inv_r with (1 := Hcond). - apply cross_product_eq; trivial. - apply Pcond_Fnorm. - apply PCond_app_inv_l with (1 := Hcond). - apply Pcond_Fnorm. - apply PCond_app_inv_r with (1 := Hcond). +Proof. +simpl. rewrite PCond_app. intros Hcrossprod (Hc1,Hc2). +rewrite !Fnorm_FEeval_PEeval; trivial. +apply cross_product_eq; trivial; + apply Pcond_Fnorm; trivial. Qed. (* Correctness lemmas of reflexive tactics *) -Notation Ninterp_PElist := (interp_PElist rO radd rmul rsub ropp req phi Cp_phi rpow). -Notation Nmk_monpol_list := (mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv). +Notation Ninterp_PElist := + (interp_PElist rO rI radd rmul rsub ropp req phi Cp_phi rpow). +Notation Nmk_monpol_list := + (mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv). -Theorem Fnorm_correct: +Theorem Fnorm_ok: forall n l lpe fe, Ninterp_PElist l lpe -> Peq ceqb (Nnorm n (Nmk_monpol_list lpe) (num (Fnorm fe))) (Pc cO) = true -> PCond l (condition (Fnorm fe)) -> FEeval l fe == 0. -intros n l lpe fe Hlpe H H1; - apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1). -apply rdiv8; auto. -transitivity (NPEeval l (PEc cO)); auto. -rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th cdiv_th n l lpe);auto. -change (NPEeval l (PEc cO)) with (Pphi 0 radd rmul phi l (Pc cO)). -apply (Peq_ok Rsth Reqe CRmorph);auto. -simpl. apply (morph0 CRmorph); auto. +Proof. +intros n l lpe fe Hlpe H H1. +rewrite (Fnorm_FEeval_PEeval l fe H1). +apply rdiv8. apply Pcond_Fnorm; trivial. +transitivity (0@l); trivial. +rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th cdiv_th n l lpe); trivial. +change (0 @ l) with (Pphi 0 radd rmul phi l (Pc cO)). +apply (Peq_ok Rsth Reqe CRmorph); trivial. Qed. +Notation ring_rw_correct := + (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec). + +Notation ring_rw_pow_correct := + (ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec). + +Notation ring_correct := + (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th). + (* simplify a field expression into a fraction *) (* TODO: simplify when den is constant... *) Definition display_linear l num den := @@ -1247,71 +1229,54 @@ Definition display_linear l num den := Definition display_pow_linear l num den := NPphi_pow l num / NPphi_pow l den. -Theorem Field_rw_correct : - forall n lpe l, +Theorem Field_rw_correct n lpe l : Ninterp_PElist l lpe -> forall lmp, Nmk_monpol_list lpe = lmp -> forall fe nfe, Fnorm fe = nfe -> PCond l (condition nfe) -> - FEeval l fe == display_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)). + FEeval l fe == + display_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)). Proof. - intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. - apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H). - unfold display_linear; apply SRdiv_ext; - eapply (ring_rw_correct Rsth Reqe ARth CRmorph);eauto. + intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. + rewrite (Fnorm_FEeval_PEeval _ _ H). + unfold display_linear; apply rdiv_ext; + eapply ring_rw_correct; eauto. Qed. -Theorem Field_rw_pow_correct : - forall n lpe l, +Theorem Field_rw_pow_correct n lpe l : Ninterp_PElist l lpe -> forall lmp, Nmk_monpol_list lpe = lmp -> forall fe nfe, Fnorm fe = nfe -> PCond l (condition nfe) -> - FEeval l fe == display_pow_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)). + FEeval l fe == + display_pow_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)). Proof. - intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. - apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H). - unfold display_pow_linear; apply SRdiv_ext; - eapply (ring_rw_pow_correct Rsth Reqe ARth CRmorph);eauto. + intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. + rewrite (Fnorm_FEeval_PEeval _ _ H). + unfold display_pow_linear; apply rdiv_ext; + eapply ring_rw_pow_correct;eauto. Qed. -Theorem Field_correct : - forall n l lpe fe1 fe2, Ninterp_PElist l lpe -> +Theorem Field_correct n l lpe fe1 fe2 : + Ninterp_PElist l lpe -> forall lmp, Nmk_monpol_list lpe = lmp -> forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> - Peq ceqb (Nnorm n lmp (PEmul (num nfe1) (denum nfe2))) - (Nnorm n lmp (PEmul (num nfe2) (denum nfe1))) = true -> + Peq ceqb (Nnorm n lmp (num nfe1 * denum nfe2)) + (Nnorm n lmp (num nfe2 * denum nfe1)) = true -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. Proof. -intros n l lpe fe1 fe2 Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp. +intros Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp. apply Fnorm_crossproduct; trivial. -eapply (ring_correct Rsth Reqe ARth CRmorph); eauto. +eapply ring_correct; eauto. Qed. (* simplify a field equation : generate the crossproduct and simplify polynomials *) -Theorem Field_simplify_eq_old_correct : - forall l fe1 fe2 nfe1 nfe2, - Fnorm fe1 = nfe1 -> - Fnorm fe2 = nfe2 -> - NPphi_dev l (Nnorm O nil (PEmul (num nfe1) (denum nfe2))) == - NPphi_dev l (Nnorm O nil (PEmul (num nfe2) (denum nfe1))) -> - PCond l (condition nfe1 ++ condition nfe2) -> - FEeval l fe1 == FEeval l fe2. -Proof. -intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond; subst nfe1 nfe2. -apply Fnorm_crossproduct; trivial. -match goal with - [ |- NPEeval l ?x == NPEeval l ?y] => - rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec - O nil l I Logic.eq_refl x Logic.eq_refl); - rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec - O nil l I Logic.eq_refl y Logic.eq_refl) - end. -trivial. -Qed. + +(** This allows rewriting modulo the simplification of PEeval on PMul *) +Declare Equivalent Keys PEeval rmul. Theorem Field_simplify_eq_correct : forall n l lpe fe1 fe2, @@ -1320,37 +1285,23 @@ Theorem Field_simplify_eq_correct : forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> 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))) -> + NPphi_dev l (Nnorm n lmp (num nfe1 * right den)) == + NPphi_dev l (Nnorm n lmp (num nfe2 * left den)) -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. Proof. -intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; - subst nfe1 nfe2 den lmp. -apply Fnorm_crossproduct; trivial. +intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond. +apply Fnorm_crossproduct; rewrite ?eq1, ?eq2; trivial. simpl. -rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). -rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))). -rewrite NPEmul_correct. -rewrite NPEmul_correct. +rewrite (split_ok_l (denum nfe1) (denum nfe2) l), eq3. +rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3. simpl. -repeat rewrite (ARmul_assoc ARth). -rewrite <-( - let x := PEmul (num (Fnorm fe1)) - (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in -ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l - Hlpe Logic.eq_refl - x Logic.eq_refl) in Hcrossprod. -rewrite <-( - let x := (PEmul (num (Fnorm fe2)) - (rsplit_left - (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in - ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l - Hlpe Logic.eq_refl - x Logic.eq_refl) in Hcrossprod. -simpl in Hcrossprod. -rewrite Hcrossprod. -reflexivity. +rewrite !rmul_assoc. +apply rmul_ext; trivial. +rewrite (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl), + (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl). +rewrite Hlmp. +apply Hcrossprod. Qed. Theorem Field_simplify_eq_pow_correct : @@ -1360,37 +1311,55 @@ Theorem Field_simplify_eq_pow_correct : forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> 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))) -> + NPphi_pow l (Nnorm n lmp (num nfe1 * right den)) == + NPphi_pow l (Nnorm n lmp (num nfe2 * left den)) -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. Proof. -intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; - subst nfe1 nfe2 den lmp. -apply Fnorm_crossproduct; trivial. +intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond. +apply Fnorm_crossproduct; rewrite ?eq1, ?eq2; trivial. simpl. -rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). -rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))). -rewrite NPEmul_correct. -rewrite NPEmul_correct. +rewrite (split_ok_l (denum nfe1) (denum nfe2) l), eq3. +rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3. simpl. -repeat rewrite (ARmul_assoc ARth). -rewrite <-( - let x := PEmul (num (Fnorm fe1)) - (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in -ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l - Hlpe Logic.eq_refl - x Logic.eq_refl) in Hcrossprod. -rewrite <-( - let x := (PEmul (num (Fnorm fe2)) - (rsplit_left - (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in - ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l - Hlpe Logic.eq_refl - x Logic.eq_refl) in Hcrossprod. -simpl in Hcrossprod. -rewrite Hcrossprod. -reflexivity. +rewrite !rmul_assoc. +apply rmul_ext; trivial. +rewrite + (ring_rw_pow_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl), + (ring_rw_pow_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl). +rewrite Hlmp. +apply Hcrossprod. +Qed. + +Theorem Field_simplify_aux_ok l fe1 fe2 den : + FEeval l fe1 == FEeval l fe2 -> + split (denum (Fnorm fe1)) (denum (Fnorm fe2)) = den -> + PCond l (condition (Fnorm fe1) ++ condition (Fnorm fe2)) -> + (num (Fnorm fe1) * right den) @ l == (num (Fnorm fe2) * left den) @ l. +Proof. + rewrite PCond_app; intros Hfe Hden (Hc1,Hc2); simpl. + assert (Hc1' := Pcond_Fnorm _ _ Hc1). + assert (Hc2' := Pcond_Fnorm _ _ Hc2). + set (N1 := num (Fnorm fe1)) in *. set (N2 := num (Fnorm fe2)) in *. + set (D1 := denum (Fnorm fe1)) in *. set (D2 := denum (Fnorm fe2)) in *. + assert (~ (common den) @ l == 0). + { intro H. apply Hc1'. + rewrite (split_ok_l D1 D2 l). + rewrite Hden. simpl. ring [H]. } + apply (@rmul_reg_l ((common den) @ l)); trivial. + rewrite !(rmul_comm ((common den) @ l)), <- !rmul_assoc. + change + (N1@l * (right den * common den) @ l == + N2@l * (left den * common den) @ l). + rewrite <- Hden, <- split_ok_l, <- split_ok_r. + apply (@rmul_reg_l (/ D2@l)). { apply rinv_nz; trivial. } + rewrite (rmul_comm (/ D2 @ l)), <- !rmul_assoc. + rewrite <- rdiv_def, rdiv_r_r, rmul_1_r by trivial. + apply (@rmul_reg_l (/ (D1@l))). { apply rinv_nz; trivial. } + rewrite !(rmul_comm (/ D1@l)), <- !rmul_assoc. + rewrite <- !rdiv_def, rdiv_r_r, rmul_1_r by trivial. + rewrite (rmul_comm (/ D2@l)), <- rdiv_def. + unfold N1,N2,D1,D2; rewrite <- !Fnorm_FEeval_PEeval; trivial. Qed. Theorem Field_simplify_eq_pow_in_correct : @@ -1400,47 +1369,17 @@ Theorem Field_simplify_eq_pow_in_correct : forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> 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 -> + forall np1, Nnorm n lmp (num nfe1 * right den) = np1 -> + forall np2, Nnorm n lmp (num nfe2 * left den) = np2 -> FEeval l fe1 == FEeval l fe2 -> - PCond l (condition nfe1 ++ condition nfe2) -> + PCond l (condition nfe1 ++ condition nfe2) -> NPphi_pow l np1 == NPphi_pow l np2. Proof. intros. subst nfe1 nfe2 lmp np1 np2. - repeat rewrite (Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec). - 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))). - intro Heq;apply N1. - rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). - rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq]. - repeat rewrite (ARth.(ARmul_comm) (NPEeval l (rsplit_common den))). - repeat rewrite <- ARth.(ARmul_assoc). - change (NPEeval l (rsplit_right den) * NPEeval l (rsplit_common den)) with - (NPEeval l (PEmul (rsplit_right den) (rsplit_common den))). - change (NPEeval l (rsplit_left den) * NPEeval l (rsplit_common den)) with - (NPEeval l (PEmul (rsplit_left den) (rsplit_common den))). - repeat rewrite <- NPEmul_correct. rewrite <- H3. rewrite <- split_correct_l. - rewrite <- split_correct_r. - apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe2)))). - intro Heq; apply AFth.(AF_1_neq_0). - rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial. - ring [Heq]. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))). - repeat rewrite <- (ARth.(ARmul_assoc)). - rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. - apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))). - intro Heq; apply AFth.(AF_1_neq_0). - rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial. - ring [Heq]. repeat rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe1)))). - repeat rewrite <- (ARth.(ARmul_assoc)). - repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. - rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp. - 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). + rewrite !(Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec). + repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). + simpl. apply Field_simplify_aux_ok; trivial. Qed. Theorem Field_simplify_eq_in_correct : @@ -1450,47 +1389,16 @@ forall n l lpe fe1 fe2, forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> 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 -> + forall np1, Nnorm n lmp (num nfe1 * right den) = np1 -> + forall np2, Nnorm n lmp (num nfe2 * left den) = np2 -> FEeval l fe1 == FEeval l fe2 -> - PCond l (condition nfe1 ++ condition nfe2) -> - NPphi_dev l np1 == - NPphi_dev l np2. + PCond l (condition nfe1 ++ condition nfe2) -> + NPphi_dev l np1 == NPphi_dev l np2. Proof. intros. subst nfe1 nfe2 lmp np1 np2. - repeat rewrite (Pphi_dev_ok Rsth Reqe ARth CRmorph get_sign_spec). - 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))). - intro Heq;apply N1. - rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). - rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq]. - repeat rewrite (ARth.(ARmul_comm) (NPEeval l (rsplit_common den))). - repeat rewrite <- ARth.(ARmul_assoc). - change (NPEeval l (rsplit_right den) * NPEeval l (rsplit_common den)) with - (NPEeval l (PEmul (rsplit_right den) (rsplit_common den))). - change (NPEeval l (rsplit_left den) * NPEeval l (rsplit_common den)) with - (NPEeval l (PEmul (rsplit_left den) (rsplit_common den))). - repeat rewrite <- NPEmul_correct;rewrite <- H3. rewrite <- split_correct_l. - rewrite <- split_correct_r. - apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe2)))). - intro Heq; apply AFth.(AF_1_neq_0). - rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial. - ring [Heq]. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))). - repeat rewrite <- (ARth.(ARmul_assoc)). - rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. - apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))). - intro Heq; apply AFth.(AF_1_neq_0). - rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial. - ring [Heq]. repeat rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe1)))). - repeat rewrite <- (ARth.(ARmul_assoc)). - repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. - rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp. - 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). + rewrite !(Pphi_dev_ok Rsth Reqe ARth CRmorph get_sign_spec). + repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). + apply Field_simplify_aux_ok; trivial. Qed. @@ -1499,7 +1407,7 @@ Section Fcons_impl. Variable Fcons : PExpr C -> list (PExpr C) -> list (PExpr C). Hypothesis PCond_fcons_inv : forall l a l1, - PCond l (Fcons a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. + PCond l (Fcons a l1) -> ~ a @ l == 0 /\ PCond l l1. Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) := match l with @@ -1507,15 +1415,15 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) := | cons a l1 => Fcons a (Fapp l1 m) end. - Lemma fcons_correct : forall l l1, +Lemma fcons_ok : forall l l1, (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1. - Proof. - intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1. - induction l1; simpl; intros. - trivial. - elim PCond_fcons_inv with (1 := H); intros. - destruct l1; trivial. split; trivial. apply IHl1; trivial. - Qed. +Proof. +intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1. +induction l1; simpl; intros. + trivial. + elim PCond_fcons_inv with (1 := H); intros. + destruct l1; trivial. split; trivial. apply IHl1; trivial. +Qed. End Fcons_impl. @@ -1531,21 +1439,15 @@ Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := 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. -simpl; auto. -intros a0 l0. -generalize (PExpr_eq_semi_correct l a a0); case (PExpr_eq a a0). -intros H H0 H1; split; auto. -rewrite H; auto. -generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. -intros H H0 H1; - assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)). -split. -generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. -apply H0. -generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto. -generalize Hp; case l0; simpl; intuition. + forall l a l1, PCond l (Fcons a l1) -> ~ a @ l == 0 /\ PCond l l1. +Proof. +induction l1 as [|e l1]; simpl Fcons. +- simpl; now split. +- case PExpr_eq_spec; intros H; rewrite !PCond_cons; intros (H1,H2); + repeat split; trivial. + + now rewrite H. + + now apply IHl1. + + now apply IHl1. Qed. (* equality of normal forms rather than syntactic equality *) @@ -1558,23 +1460,16 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := 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. -simpl; auto. -intros a0 l0. -generalize (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th O l nil a a0). simpl. - case (Peq ceqb (Nnorm O nil a) (Nnorm O nil a0)). -intros H H0 H1; split; auto. -rewrite H; auto. -generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. -intros H H0 H1; - assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)). -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. -generalize Hp; case l0; simpl; intuition. + forall l a l1, PCond l (Fcons0 a l1) -> ~ a @ l == 0 /\ PCond l l1. +Proof. +induction l1 as [|e l1]; simpl Fcons0. +- simpl; now split. +- generalize (ring_correct O l nil a e). lazy zeta; simpl Peq. + case Peq; intros H; rewrite !PCond_cons; intros (H1,H2); + repeat split; trivial. + + now rewrite H. + + now apply IHl1. + + now apply IHl1. Qed. (* split factorized denominators *) @@ -1586,95 +1481,83 @@ Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := end. Theorem PFcons00_fcons_inv: - forall l a l1, PCond l (Fcons00 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. -intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). - intros p H p0 H0 l1 H1. - simpl in H1. - case (H _ H1); intros H2 H3. - case (H0 _ H3); intros H4 H5; split; auto. - simpl. - apply field_is_integral_domain; trivial. - simpl;intros. rewrite pow_th.(rpow_pow_N). - destruct (H _ H0);split;auto. - destruct n;simpl. apply AFth.(AF_1_neq_0). - apply pow_pos_not_0;trivial. + forall l a l1, PCond l (Fcons00 a l1) -> ~ a @ l == 0 /\ PCond l l1. +Proof. +intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail). +- intros p H p0 H0 l1 H1. + simpl in H1. + destruct (H _ H1) as (H2,H3). + destruct (H0 _ H3) as (H4,H5). split; trivial. + simpl. + apply field_is_integral_domain; trivial. +- intros. destruct (H _ H0). split; trivial. + apply PEpow_nz; trivial. Qed. Definition Pcond_simpl_gen := - fcons_correct _ PFcons00_fcons_inv. + fcons_ok _ PFcons00_fcons_inv. (* Specific case when the equality test of coefs is complete w.r.t. the field equality: non-zero coefs can be eliminated, and opposite can be simplified (if -1 <> 0) *) -Hypothesis ceqb_complete : forall c1 c2, phi c1 == phi c2 -> ceqb c1 c2 = true. +Hypothesis ceqb_complete : forall c1 c2, [c1] == [c2] -> ceqb c1 c2 = true. -Lemma ceqb_rect_complete : forall c1 c2 (A:Type) (x y:A) (P:A->Type), - (phi c1 == phi c2 -> P x) -> - (~ phi c1 == phi c2 -> P y) -> - P (if ceqb c1 c2 then x else y). +Lemma ceqb_spec' c1 c2 : Bool.reflect ([c1] == [c2]) (ceqb c1 c2). Proof. -intros. -generalize (fun h => X (morph_eq CRmorph c1 c2 h)). -generalize (@ceqb_complete c1 c2). -case (c1 ?=! c2); auto; intros. -apply X0. -red; intro. -absurd (false = true); auto; discriminate. +assert (H := morph_eq CRmorph c1 c2). +assert (H' := @ceqb_complete c1 c2). +destruct (ceqb c1 c2); constructor. +- now apply H. +- intro E. specialize (H' E). discriminate. 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) + | PEmul e1 e2 => Fcons1 e1 (Fcons1 e2 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 + | PEopp e => if (-(1) =? 0)%coef then absurd_PCond else Fcons1 e l + | PEc c => if (c =? 0)%coef then absurd_PCond else l | _ => Fcons0 e l end. Theorem PFcons1_fcons_inv: - forall l a l1, PCond l (Fcons1 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. -intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). - simpl; intros c l1. - apply ceqb_rect_complete; intros. - elim (@absurd_PCond_bottom l H0). - split; trivial. - rewrite <- (morph0 CRmorph); trivial. - intros p H p0 H0 l1 H1. - simpl in H1. - case (H _ H1); intros H2 H3. - case (H0 _ H3); intros H4 H5; split; auto. - simpl. - apply field_is_integral_domain; trivial. - simpl; intros p H l1. - apply ceqb_rect_complete; intros. - elim (@absurd_PCond_bottom l H1). - destruct (H _ H1). + forall l a l1, PCond l (Fcons1 a l1) -> ~ a @ l == 0 /\ PCond l l1. +Proof. +intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail). +- simpl; intros c l1. + case ceqb_spec'; intros H H0. + + elim (@absurd_PCond_bottom l H0). + + split; trivial. rewrite <- phi_0; trivial. +- intros p H p0 H0 l1 H1. simpl in H1. + destruct (H _ H1) as (H2,H3). + destruct (H0 _ H3) as (H4,H5). + split; trivial. simpl. apply field_is_integral_domain; trivial. +- simpl; intros p H l1. + case ceqb_spec'; intros H0 H1. + + elim (@absurd_PCond_bottom l H1). + + destruct (H _ H1). split; trivial. apply ropp_neq_0; trivial. - rewrite (morph_opp CRmorph) in H0. - rewrite (morph1 CRmorph) in H0. - rewrite (morph0 CRmorph) in H0. - trivial. - intros;simpl. destruct (H _ H0);split;trivial. - rewrite pow_th.(rpow_pow_N). destruct n;simpl. - apply AFth.(AF_1_neq_0). apply pow_pos_not_0;trivial. + rewrite (morph_opp CRmorph), phi_0, phi_1 in H0. trivial. +- intros. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial. Qed. -Definition Fcons2 e l := Fcons1 (PExpr_simp e) l. +Definition Fcons2 e l := Fcons1 (PEsimp e) l. Theorem PFcons2_fcons_inv: - forall l a l1, PCond l (Fcons2 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. + forall l a l1, PCond l (Fcons2 a l1) -> ~ a @ l == 0 /\ PCond l l1. +Proof. unfold Fcons2; intros l a l1 H; split; - case (PFcons1_fcons_inv l (PExpr_simp a) l1); auto. + case (PFcons1_fcons_inv l (PEsimp a) l1); trivial. intros H1 H2 H3; case H1. -transitivity (NPEeval l a); trivial. -apply PExpr_simp_correct. +transitivity (a@l); trivial. +apply PEsimp_ok. Qed. Definition Pcond_simpl_complete := - fcons_correct _ PFcons2_fcons_inv. + fcons_ok _ PFcons2_fcons_inv. End Fcons_simpl. @@ -1742,22 +1625,22 @@ Hypothesis S_inj : forall x y, 1+x==1+y -> x==y. Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0. -Lemma add_inj_r : forall p x y, +Lemma add_inj_r p x y : gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y. -intros p x y. +Proof. elim p using Pos.peano_ind; simpl; intros. apply S_inj; trivial. apply H. apply S_inj. - repeat rewrite (ARadd_assoc ARth). + rewrite !(ARadd_assoc ARth). rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth); trivial. Qed. -Lemma gen_phiPOS_inj : forall x y, +Lemma gen_phiPOS_inj x y : gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y -> x = y. -intros x y. -repeat rewrite <- (same_gen Rsth Reqe ARth). +Proof. +rewrite <- !(same_gen Rsth Reqe ARth). case (Pos.compare_spec x y). intros. trivial. @@ -1777,9 +1660,10 @@ case (Pos.compare_spec x y). Qed. -Lemma gen_phiN_inj : forall x y, +Lemma gen_phiN_inj x y : gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> x = y. +Proof. destruct x; destruct y; simpl; intros; trivial. elim gen_phiPOS_not_0 with p. symmetry . @@ -1789,7 +1673,7 @@ destruct x; destruct y; simpl; intros; trivial. rewrite gen_phiPOS_inj with (1 := H); trivial. Qed. -Lemma gen_phiN_complete : forall x y, +Lemma gen_phiN_complete x y : gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> N.eqb x y = true. Proof. @@ -1808,31 +1692,22 @@ Section Field. Let AFth := F2AF Rsth Reqe Fth. Let ARth := Rth_ARth Rsth Reqe Rth. -Lemma ring_S_inj : forall x y, 1+x==1+y -> x==y. +Lemma ring_S_inj x y : 1+x==1+y -> x==y. +Proof. intros. -transitivity (x + (1 + - (1))). - rewrite (Ropp_def Rth). - symmetry . - apply (ARadd_0_r Rsth ARth). - transitivity (y + (1 + - (1))). - repeat rewrite <- (ARplus_assoc ARth). - repeat rewrite (ARadd_assoc ARth). - apply (Radd_ext Reqe). - repeat rewrite <- (ARadd_comm ARth 1). - trivial. - reflexivity. - rewrite (Ropp_def Rth). - apply (ARadd_0_r Rsth ARth). +rewrite <- (ARadd_0_l ARth x), <- (ARadd_0_l ARth y). +rewrite <- (Ropp_def Rth 1), (ARadd_comm ARth 1). +rewrite <- !(ARadd_assoc ARth). now apply (Radd_ext Reqe). Qed. - - Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0. +Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0. Let gen_phiPOS_inject := gen_phiPOS_inj AFth ring_S_inj gen_phiPOS_not_0. -Lemma gen_phiPOS_discr_sgn : forall x y, +Lemma gen_phiPOS_discr_sgn x y : ~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y. +Proof. red; intros. apply gen_phiPOS_not_0 with (y + x)%positive. rewrite (ARgen_phiPOS_add Rsth Reqe ARth). @@ -1845,9 +1720,10 @@ transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y). apply (Ropp_def Rth). Qed. -Lemma gen_phiZ_inj : forall x y, +Lemma gen_phiZ_inj x y : gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> x = y. +Proof. destruct x; destruct y; simpl; intros. trivial. elim gen_phiPOS_not_0 with p. @@ -1878,9 +1754,10 @@ destruct x; destruct y; simpl; intros. reflexivity. Qed. -Lemma gen_phiZ_complete : forall x y, +Lemma gen_phiZ_complete x y : gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> Zeq_bool x y = true. +Proof. intros. replace y with x. unfold Zeq_bool. @@ -1891,3 +1768,6 @@ Qed. End Field. End Complete. + +Arguments FEO [C]. +Arguments FEI [C]. diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index e106d5b5..b92b847b 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import ZArith_base. -Require Import Zpow_def. +Require Import Zbool. Require Import BinInt. Require Import BinNat. Require Import Setoid. @@ -16,6 +15,7 @@ Require Import Ring_polynom. Import List. Set Implicit Arguments. +(* Set Universe Polymorphism. *) Import RingSyntax. @@ -815,7 +815,7 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk := fun f => f arth ext_r morph lemma1 lemma2 | _ => fail 4 "ring: bad sign specification" end - | _ => fail 3 "ring: bad coefficiant division specification" + | _ => fail 3 "ring: bad coefficient division specification" end | _ => fail 2 "ring: bad power specification" end diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v index cfd00521..a10eeecc 100644 --- a/plugins/setoid_ring/NArithRing.v +++ b/plugins/setoid_ring/NArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v index 95d7deee..2dc3197d 100644 --- a/plugins/setoid_ring/Ncring.v +++ b/plugins/setoid_ring/Ncring.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 516a993e..c40e0ffb 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -192,6 +192,7 @@ Lemma gen_phiZ_opp : forall x, [- x] == - [x]. Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y]. Proof. intros;subst;reflexivity. Qed. +Declare Equivalent Keys bracket gen_phiZ. (*proof that [.] satisfies morphism specifications*) Global Instance gen_phiZ_morph : (@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*) diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index eefc9428..5845b629 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -103,7 +103,7 @@ Variable P:Pol. (* Xi^n * P + Q les variables de tete de Q ne sont pas forcement < i -mais Q est normalisé : variables de tete decroissantes *) +mais Q est normalisé : variables de tete decroissantes *) Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:= match Q with @@ -216,8 +216,8 @@ Definition Psub(P P':Pol):= P ++ (--P'). intros l P i n Q;unfold mkPX. destruct P;try (simpl;reflexivity). assert (Hh := ring_morphism_eq c 0). -simpl; case_eq (Ceqb c 0);simpl;try reflexivity. -intros. + simpl; case_eq (Ceqb c 0);simpl;try reflexivity. + intros. rewrite Hh. rewrite ring_morphism0. rsimpl. apply Ceqb_eq. trivial. destruct (Pos.compare_spec i p). @@ -416,10 +416,13 @@ Qed. Variable pow_th : power_theory Cp_phi rpow. (** evaluation of polynomial expressions towards R *) + Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R := match pe with + | PEO => 0 + | PEI => 1 | PEc c => [c] - | PEX j => nth 0 j l + | PEX _ j => nth 0 j l | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2) | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2) @@ -500,8 +503,10 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) := Fixpoint norm_aux (pe:PExpr C) : Pol := match pe with + | PEO => Pc cO + | PEI => Pc cI | PEc c => Pc c - | PEX j => mk_X j + | PEX _ j => mk_X j | PEadd pe1 (PEopp pe2) => Psub (norm_aux pe1) (norm_aux pe2) | PEadd pe1 pe2 => Padd (norm_aux pe1) (norm_aux pe2) @@ -520,28 +525,30 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) := Proof. intros. induction pe. -Esimpl3. Esimpl3. simpl. - rewrite IHpe1;rewrite IHpe2. - destruct pe2; Esimpl3. -unfold Psub. -destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity. -simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2. -destruct pe1. destruct pe2; rewrite Padd_ok; rewrite Popp_ok; try reflexivity. -Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. - Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. -simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity. -simpl. rewrite IHpe; Esimpl3. -simpl. - rewrite Ppow_N_ok; (intros;try reflexivity). - rewrite rpow_pow_N. Esimpl3. - induction n;simpl. Esimpl3. induction p; simpl. - try rewrite IHp;try rewrite IHpe; - repeat rewrite Pms_ok; - repeat rewrite Pmul_ok;reflexivity. -rewrite Pmul_ok. try rewrite IHp;try rewrite IHpe; - repeat rewrite Pms_ok; - repeat rewrite Pmul_ok;reflexivity. trivial. -exact pow_th. + - now simpl; rewrite <- ring_morphism0. + - now simpl; rewrite <- ring_morphism1. + - Esimpl3. + - Esimpl3. + - simpl. + rewrite IHpe1;rewrite IHpe2. + destruct pe2; Esimpl3. + unfold Psub. + destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity. + - simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2. + now destruct pe1; + [destruct pe2; rewrite Padd_ok; rewrite Popp_ok; Esimpl3 | Esimpl3..]. + - simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity. + - now simpl; rewrite IHpe; Esimpl3. + - simpl. + rewrite Ppow_N_ok; (intros;try reflexivity). + rewrite rpow_pow_N; [| now apply pow_th]. + induction n;simpl; [now Esimpl3|]. + induction p; simpl; trivial. + + try rewrite IHp;try rewrite IHpe; + repeat rewrite Pms_ok; repeat rewrite Pmul_ok;reflexivity. + + rewrite Pmul_ok. + try rewrite IHp;try rewrite IHpe; repeat rewrite Pms_ok; + repeat rewrite Pmul_ok;reflexivity. Qed. Lemma norm_subst_spec : diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v index 4fb02909..31c9e54d 100644 --- a/plugins/setoid_ring/Ncring_tac.v +++ b/plugins/setoid_ring/Ncring_tac.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -76,11 +76,11 @@ Instance reify_mul (R:Type) : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10. Instance reify_mul_ext (R:Type) `{Ring R} - lvar z e2 t2 + lvar (z:Z) e2 t2 `{Ring (T:=R)} {_:reify e2 lvar t2} : reify (PEmul (PEc z) e2) lvar - (@multiplication Z _ _ z t2)|9. + (@multiplication Z _ _ z t2)|9. Instance reify_sub (R:Type) e1 lvar t1 e2 t2 op @@ -127,7 +127,6 @@ Definition list_reifyl (R:Type) lexpr lvar lterm Unset Implicit Arguments. - Ltac lterm_goal g := match g with | ?t1 == ?t2 => constr:(t1::t2::nil) @@ -138,6 +137,7 @@ Ltac lterm_goal g := Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y. intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed. + Ltac reify_goal lvar lexpr lterm:= (*idtac lvar; idtac lexpr; idtac lterm;*) match lexpr with diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v index 98150d35..b2417db6 100644 --- a/plugins/setoid_ring/Ring.v +++ b/plugins/setoid_ring/Ring.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v index b64023ea..9508b8e7 100644 --- a/plugins/setoid_ring/Ring_base.v +++ b/plugins/setoid_ring/Ring_base.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/setoid_ring/Ring_equiv.v b/plugins/setoid_ring/Ring_equiv.v deleted file mode 100644 index 945f6c68..00000000 --- a/plugins/setoid_ring/Ring_equiv.v +++ /dev/null @@ -1,74 +0,0 @@ -Require Import Setoid_ring_theory. -Require Import LegacyRing_theory. -Require Import Ring_theory. - -Set Implicit Arguments. - -Section Old2New. - -Variable A : Type. - -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. -Variable R : Ring_Theory Aplus Amult Aone Azero Aopp Aeq. - -Let Aminus := fun x y => Aplus x (Aopp y). - -Lemma ring_equiv1 : - ring_theory Azero Aone Aplus Amult Aminus Aopp (eq (A:=A)). -Proof. -destruct R. -split; eauto. -Qed. - -End Old2New. - -Section New2OldRing. - Variable R : Type. - Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). - Variable Rth : ring_theory rO rI radd rmul rsub ropp (eq (A:=R)). - - Variable reqb : R -> R -> bool. - Variable reqb_ok : forall x y, reqb x y = true -> x = y. - - Lemma ring_equiv2 : - Ring_Theory radd rmul rI rO ropp reqb. -Proof. -elim Rth; intros; constructor; eauto. -intros. -apply reqb_ok. -destruct (reqb x y); trivial; intros. -elim H. -Qed. - - Definition default_eqb : R -> R -> bool := fun x y => false. - Lemma default_eqb_ok : forall x y, default_eqb x y = true -> x = y. -Proof. -discriminate 1. -Qed. - -End New2OldRing. - -Section New2OldSemiRing. - Variable R : Type. - Variable (rO rI : R) (radd rmul: R->R->R). - Variable SRth : semi_ring_theory rO rI radd rmul (eq (A:=R)). - - Variable reqb : R -> R -> bool. - Variable reqb_ok : forall x y, reqb x y = true -> x = y. - - Lemma sring_equiv2 : - Semi_Ring_Theory radd rmul rI rO reqb. -Proof. -elim SRth; intros; constructor; eauto. -intros. -apply reqb_ok. -destruct (reqb x y); trivial; intros. -elim H. -Qed. - -End New2OldSemiRing. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 21d3099c..2d2756b1 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -1,17 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) + Set Implicit Arguments. -Require Import Setoid Morphisms BinList BinPos BinNat BinInt. +Require Import Setoid Morphisms. +Require Import BinList BinPos BinNat BinInt. Require Export Ring_theory. - Local Open Scope positive_scope. Import RingSyntax. +(* Set Universe Polymorphism. *) Section MakeRingPol. @@ -372,17 +374,6 @@ Section MakeRingPol. Infix "**" := Pmul. - Fixpoint Psquare (P:Pol) : Pol := - match P with - | Pc c => Pc (c *! c) - | Pinj j Q => Pinj j (Psquare 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 - mkPX (mkPX P2 i P0 ++ twoPQ) i Q2 - end. - (** Monomial **) (** A monomial is X1^k1...Xi^ki. Its representation @@ -511,6 +502,29 @@ Section MakeRingPol. Reserved Notation "P @ l " (at level 10, no associativity). Notation "P @ l " := (Pphi l P). + Definition Pequiv (P Q : Pol) := forall l, P@l == Q@l. + Infix "===" := Pequiv (at level 70, no associativity). + + Instance Pequiv_eq : Equivalence Pequiv. + Proof. + unfold Pequiv; split; red; intros; [reflexivity|now symmetry|now etransitivity]. + Qed. + + Instance Pphi_ext : Proper (eq ==> Pequiv ==> req) Pphi. + Proof. + now intros l l' <- P Q H. + Qed. + + Instance Pinj_ext : Proper (eq ==> Pequiv ==> Pequiv) Pinj. + Proof. + intros i j <- P P' HP l. simpl. now rewrite HP. + Qed. + + Instance PX_ext : Proper (Pequiv ==> eq ==> Pequiv ==> Pequiv) PX. + Proof. + intros P P' HP p p' <- Q Q' HQ l. simpl. now rewrite HP, HQ. + Qed. + (** Evaluation of a monomial towards R *) Fixpoint Mphi(l:list R) (M: Mon) : R := @@ -532,8 +546,9 @@ Section MakeRingPol. Lemma jump_add' i j (l:list R) : jump (i + j) l = jump j (jump i l). Proof. rewrite Pos.add_comm. apply jump_add. Qed. - Lemma Peq_ok P P' : (P ?== P') = true -> forall l, P@l == P'@ l. + Lemma Peq_ok P P' : (P ?== P') = true -> P === P'. Proof. + unfold Pequiv. revert P';induction P;destruct P';simpl; intros H l; try easy. - now apply (morph_eq CRmorph). - destruct (Pos.compare_spec p p0); [ subst | easy | easy ]. @@ -545,8 +560,7 @@ Section MakeRingPol. now rewrite IHP1, IHP2. Qed. - Lemma Peq_spec P P' : - BoolSpec (forall l, P@l == P'@l) True (P ?== P'). + Lemma Peq_spec P P' : BoolSpec (P === P') True (P ?== P'). Proof. generalize (Peq_ok P P'). destruct (P ?== P'); auto. Qed. @@ -567,6 +581,11 @@ Section MakeRingPol. now rewrite jump_add'. Qed. + Instance mkPinj_ext : Proper (eq ==> Pequiv ==> Pequiv) mkPinj. + Proof. + intros i j <- P Q H l. now rewrite !mkPinj_ok. + Qed. + Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j. Proof. rewrite Pos.add_comm. @@ -590,6 +609,11 @@ Section MakeRingPol. rewrite H, Pphi0, Pos.add_comm, pow_pos_add; rsimpl. Qed. + Instance mkPX_ext : Proper (Pequiv ==> eq ==> Pequiv ==> Pequiv) mkPX. + Proof. + intros P P' HP i i' <- Q Q' HQ l. now rewrite !mkPX_ok, HP, HQ. + Qed. + Hint Rewrite Pphi0 Pphi1 @@ -656,7 +680,7 @@ Section MakeRingPol. - add_permut. - destruct p; simpl; rewrite ?jump_pred_double; add_permut. - - destr_pos_sub; intros ->;Esimpl. + - destr_pos_sub; intros ->; Esimpl. + rewrite IHP';rsimpl. add_permut. + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut. + rewrite IHP1, pow_pos_add;rsimpl. add_permut. @@ -689,47 +713,23 @@ Section MakeRingPol. rewrite IHP'2, pow_pos_add; rsimpl. add_permut. Qed. - Lemma PsubX_ok P' P k l : - (forall P l, (P--P')@l == P@l - P'@l) -> - (PsubX Psub P' k P) @ l == P@l - P'@l * (hd l)^k. + Lemma Psub_opp P' P : P -- P' === P ++ (--P'). Proof. - intros IHP'. - revert k l. induction P;simpl;intros. - - rewrite Popp_ok;rsimpl; add_permut. - - destruct p; simpl; - rewrite Popp_ok;rsimpl; - rewrite ?jump_pred_double; add_permut. - - destr_pos_sub; intros ->; Esimpl. - + rewrite IHP';rsimpl. add_permut. - + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut. - + rewrite IHP1, pow_pos_add;rsimpl. add_permut. + revert P; induction P'; simpl; intros. + - intro l; Esimpl. + - revert p; induction P; simpl; intros; try reflexivity. + + destr_pos_sub; intros ->; now apply mkPinj_ext. + + destruct p0; now apply PX_ext. + - destruct P; simpl; try reflexivity. + + destruct p0; now apply PX_ext. + + destr_pos_sub; intros ->; apply mkPX_ext; auto. + revert p1. induction P2; simpl; intros; try reflexivity. + destr_pos_sub; intros ->; now apply mkPX_ext. Qed. Lemma Psub_ok P' P l : (P -- P')@l == P@l - P'@l. Proof. - revert P l; induction P';simpl;intros;Esimpl. - - revert p l; induction P;simpl;intros. - + Esimpl; add_permut. - + destr_pos_sub; intros ->;Esimpl. - * rewrite IHP';rsimpl. - * rewrite IHP';Esimpl. now rewrite jump_add'. - * rewrite IHP. now rewrite jump_add'. - + destruct p0;simpl. - * rewrite IHP2;simpl. rsimpl. - * rewrite IHP2;simpl. rewrite jump_pred_double. rsimpl. - * rewrite IHP'. rsimpl. - - destruct P;simpl. - + Esimpl; add_permut. - + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl. - * rsimpl. add_permut. - * rewrite jump_pred_double. rsimpl. add_permut. - * rsimpl. add_permut. - + destr_pos_sub; intros ->; Esimpl. - * rewrite IHP'1, IHP'2;rsimpl. add_permut. - * rewrite IHP'1, IHP'2;simpl;Esimpl. - rewrite pow_pos_add;rsimpl. add_permut. - * rewrite PsubX_ok by trivial;rsimpl. - rewrite IHP'2, pow_pos_add;rsimpl. add_permut. + rewrite Psub_opp, Padd_ok, Popp_ok. rsimpl. Qed. Lemma PmulI_ok P' : @@ -764,15 +764,6 @@ Section MakeRingPol. add_permut; f_equiv; mul_permut. Qed. - Lemma Psquare_ok P l : (Psquare P)@l == P@l * P@l. - Proof. - revert l;induction P;simpl;intros;Esimpl. - - apply IHP. - - rewrite Padd_ok, Pmul_ok;Esimpl. - rewrite IHP1, IHP2. - mul_push ((hd l)^p). now mul_push (P2@l). - Qed. - Lemma mkZmon_ok M j l : (mkZmon j M) @@ l == (zmon j M) @@ l. Proof. @@ -807,9 +798,9 @@ Section MakeRingPol. P@l == Q@l + [c] * R@l. Proof. revert l. - induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl. - - assert (H := div_th.(div_eucl_th) c0 c). - destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. + induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl. + - assert (H := div_th.(div_eucl_th) c0 c). + destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. - destr_factor. Esimpl. - destr_factor. Esimpl. add_permut. Qed. @@ -818,11 +809,12 @@ Section MakeRingPol. let (c,M) := cM in let (Q,R) := MFactor P c M in P@l == Q@l + [c] * M@@l * R@l. - Proof. + Proof. destruct cM as (c,M). revert M l. - induction P; destruct M; intros l; simpl; auto; + induction P; destruct M; intros l; simpl; auto; try (case ceqb_spec; intro He); - try (case Pos.compare_spec; intros He); rewrite ?He; + try (case Pos.compare_spec; intros He); + rewrite ?He; destr_factor; simpl; Esimpl. - assert (H := div_th.(div_eucl_th) c0 c). destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. @@ -880,9 +872,9 @@ Section MakeRingPol. Lemma PSubstL1_ok n LM1 P1 l : MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l. Proof. - revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros. - - reflexivity. - - rewrite <- IH by intuition. now apply PNSubst1_ok. + revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros. + - reflexivity. + - rewrite <- IH by intuition; now apply PNSubst1_ok. Qed. Lemma PSubstL_ok n LM1 P1 P2 l : @@ -907,6 +899,8 @@ Section MakeRingPol. (** Definition of polynomial expressions *) Inductive PExpr : Type := + | PEO : PExpr + | PEI : PExpr | PEc : C -> PExpr | PEX : positive -> PExpr | PEadd : PExpr -> PExpr -> PExpr @@ -915,6 +909,7 @@ Section MakeRingPol. | PEopp : PExpr -> PExpr | PEpow : PExpr -> N -> PExpr. + (** evaluation of polynomial expressions towards R *) Definition mk_X j := mkPinj_pred j mkX. @@ -922,6 +917,8 @@ Section MakeRingPol. Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R := match pe with + | PEO => rO + | PEI => rI | PEc c => phi c | PEX j => nth 0 j l | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) @@ -985,11 +982,13 @@ Section POWER. Variable n : nat. Variable lmp:list (C*Mon*Pol). Let subst_l P := PNSubstL P lmp n n. - Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2). + Let Pmul_subst P1 P2 := subst_l (P1 ** P2). Let Ppow_subst := Ppow_N subst_l. Fixpoint norm_aux (pe:PExpr) : Pol := match pe with + | PEO => Pc cO + | PEI => Pc cI | PEc c => Pc c | PEX j => mk_X j | PEadd (PEopp pe1) pe2 => (norm_aux pe2) -- (norm_aux pe1) @@ -1021,7 +1020,7 @@ Section POWER. end. Proof. simpl (norm_aux (PEadd _ _)). - destruct pe1; [ | | | | | reflexivity | ]; + destruct pe1; [ | | | | | | | reflexivity | ]; destruct pe2; simpl get_PEopp; reflexivity. Qed. @@ -1034,22 +1033,26 @@ Section POWER. now destruct pe. Qed. + Arguments norm_aux !pe : simpl nomatch. + Lemma norm_aux_spec l pe : PEeval l pe == (norm_aux pe)@l. Proof. intros. - induction pe. + induction pe; cbn. + - now rewrite (morph0 CRmorph). + - now rewrite (morph1 CRmorph). - reflexivity. - apply mkX_ok. - - simpl PEeval. rewrite IHpe1, IHpe2. + - rewrite IHpe1, IHpe2. assert (H1 := norm_aux_PEopp pe1). assert (H2 := norm_aux_PEopp pe2). rewrite norm_aux_PEadd. do 2 destruct get_PEopp; rewrite ?H1, ?H2; Esimpl; add_permut. - - simpl. rewrite IHpe1, IHpe2. Esimpl. - - simpl. rewrite IHpe1, IHpe2. now rewrite Pmul_ok. - - simpl. rewrite IHpe. Esimpl. - - simpl. rewrite Ppow_N_ok by reflexivity. + - rewrite IHpe1, IHpe2. Esimpl. + - rewrite IHpe1, IHpe2. now rewrite Pmul_ok. + - rewrite IHpe. Esimpl. + - rewrite Ppow_N_ok by reflexivity. rewrite pow_th.(rpow_pow_N). destruct n0; simpl; Esimpl. induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok. Qed. @@ -1483,3 +1486,6 @@ Qed. Qed. End MakeRingPol. + +Arguments PEO [C]. +Arguments PEI [C]. diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index 7a7ffcfd..77863edc 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -196,12 +196,17 @@ Ltac get_MonPol lemma := (********************************************************) (* Building the atom list of a ring expression *) -Ltac FV Cst CstPow add mul sub opp pow t fv := +(* We do not assume that Cst recognizes the rO and rI terms as constants, as *) +(* the tactic could be used to discriminate occurrences of an opaque *) +(* constant phi, with (phi 0) not convertible to 0 for instance *) +Ltac FV Cst CstPow rO rI add mul sub opp pow t fv := let rec TFV t fv := let f := match Cst t with | NotConstant => match t with + | rO => fun _ => fv + | rI => fun _ => fv | (add ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv) | (mul ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv) | (sub ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv) @@ -219,32 +224,39 @@ 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 := + (* We do not assume that Cst recognizes the rO and rI terms as constants, as *) + (* the tactic could be used to discriminate occurrences of an opaque *) + (* constant phi, with (phi 0) not convertible to 0 for instance *) +Ltac mkPolexpr C Cst CstPow rO rI radd rmul rsub ropp rpow t fv := let rec mkP t := let f := match Cst t with | InitialRing.NotConstant => match t with + | rO => + fun _ => constr:(@PEO C) + | rI => + fun _ => constr:(@PEI C) | (radd ?t1 ?t2) => fun _ => let e1 := mkP t1 in - let e2 := mkP t2 in constr:(PEadd e1 e2) + let e2 := mkP t2 in constr:(@PEadd C e1 e2) | (rmul ?t1 ?t2) => fun _ => let e1 := mkP t1 in - let e2 := mkP t2 in constr:(PEmul e1 e2) + let e2 := mkP t2 in constr:(@PEmul C e1 e2) | (rsub ?t1 ?t2) => fun _ => let e1 := mkP t1 in - let e2 := mkP t2 in constr:(PEsub e1 e2) + let e2 := mkP t2 in constr:(@PEsub C e1 e2) | (ropp ?t1) => fun _ => - let e1 := mkP t1 in constr:(PEopp e1) + let e1 := mkP t1 in constr:(@PEopp C e1) | (rpow ?t1 ?n) => match CstPow n with | 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) + | ?c => fun _ => let e1 := mkP t1 in constr:(@PEpow C e1 c) end | _ => fun _ => let p := Find_at t fv in constr:(PEX C p) @@ -260,58 +272,58 @@ Ltac PackRing F req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post := let RNG := match type of lemma1 with | context - [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] => + [@PEeval ?R ?r0 ?r1 ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] => (fun proj => proj cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2) + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2) | _ => fail 1 "field anomaly: bad correctness lemma (parse)" end in F RNG. Ltac get_Carrier RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => R). Ltac get_Eq RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => req). Ltac get_Pre RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => pre). Ltac get_Post RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => post). Ltac get_NormLemma RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => lemma1). Ltac get_SimplifyLemma RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => lemma2). Ltac get_RingFV RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => - FV cst_tac pow_tac add mul sub opp pow). + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => + FV cst_tac pow_tac r0 r1 add mul sub opp pow). Ltac get_RingMeta RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => - mkPolexpr C cst_tac pow_tac add mul sub opp pow). + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => + mkPolexpr C cst_tac pow_tac r0 r1 add mul sub opp pow). Ltac get_RingHypTac RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => - let mkPol := mkPolexpr C cst_tac pow_tac add mul sub opp pow in + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => + let mkPol := mkPolexpr C cst_tac pow_tac r0 r1 add mul sub opp pow in fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH). (* ring tactics *) @@ -338,8 +350,8 @@ Ltac Ring RNG lemma lH := (apply (lemma vfv vlpe pe1 pe2) || fail "typing error while applying ring"); [ ((let prh := proofHyp_tac lH in exact prh) - || idtac "can not automatically proof hypothesis :"; - idtac " maybe a left member of a hypothesis is not a monomial") + || idtac "can not automatically prove hypothesis :"; + [> idtac " maybe a left member of a hypothesis is not a monomial"..]) | vm_compute; (exact (eq_refl true) || fail "not a valid ring equation")]). diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index af43b0ab..4f05f0d4 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -28,6 +28,8 @@ Reserved Notation "x == y" (at level 70, no associativity). End RingSyntax. Import RingSyntax. +(* Set Universe Polymorphism. *) + Section Power. Variable R:Type. Variable rI : R. @@ -252,6 +254,7 @@ Section ALMOST_RING. Section SEMI_RING. Variable SReqe : sring_eq_ext radd rmul req. + Add Morphism radd : radd_ext1. exact (SRadd_ext SReqe). Qed. Add Morphism rmul : rmul_ext1. exact (SRmul_ext SReqe). Qed. Variable SRth : semi_ring_theory 0 1 radd rmul req. @@ -503,7 +506,6 @@ Qed. End ALMOST_RING. - Section AddRing. (* Variable R : Type. @@ -528,7 +530,6 @@ Inductive ring_kind : Type := (_ : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi). - End AddRing. diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v index 58a4d7ea..605a23a9 100644 --- a/plugins/setoid_ring/Rings_Z.v +++ b/plugins/setoid_ring/Rings_Z.v @@ -1,6 +1,7 @@ Require Export Cring. Require Export Integral_domain. Require Export Ncring_initial. +Require Export Omega. Instance Zcri: (Cring (Rr:=Zr)). red. exact Z.mul_comm. Defined. diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v index 1177688d..848e06a7 100644 --- a/plugins/setoid_ring/ZArithRing.v +++ b/plugins/setoid_ring/ZArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -48,8 +48,8 @@ Ltac Zpower_neg := Add Ring Zr : Zth (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Z.succ], power_tac Zpower_theory [Zpow_tac], - (* The two following option are not needed, it is the default chose when the set of - coefficiant is usual ring Z *) + (* The following two options are not needed; they are the default choice + when the set of coefficient is the 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 d1a5c0ab..2f9e8509 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -1,30 +1,27 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp +open Errors open Util open Names open Term +open Vars open Closure open Environ open Libnames -open Tactics +open Globnames open Glob_term open Tacticals open Tacexpr -open Pcoq -open Tactic -open Constr -open Proof_type open Coqlib -open Tacmach open Mod_subst open Tacinterp open Libobject @@ -32,14 +29,20 @@ open Printer open Declare open Decl_kinds open Entries +open Misctypes + +DECLARE PLUGIN "newring_plugin" (****************************************************************************) (* controlled reduction *) -let mark_arg i c = mkEvar(i,[|c|]) +(** ppedrot: something dubious here, we're obviously using evars the wrong + way. FIXME! *) + +let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|]) let unmark_arg f c = match destEvar c with - | (i,[|c|]) -> f i c + | (i,[|c|]) -> f (Evar.repr i) c | _ -> assert false type protect_flag = Eval|Prot|Rec @@ -48,10 +51,19 @@ let tag_arg tag_rec map subs i c = match map i with Eval -> mk_clos subs c | Prot -> mk_atom c - | Rec -> if i = -1 then mk_clos subs c else tag_rec c + | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c + +let global_head_of_constr c = + let f, args = decompose_app c in + try global_of_constr f + with Not_found -> anomaly (str "global_head_of_constr") + +let global_of_constr_nofail c = + try global_of_constr c + with Not_found -> VarRef (Id.of_string "dummy") let rec mk_clos_but f_map subs t = - match f_map t with + match f_map (global_of_constr_nofail t) with | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t | None -> (match kind_of_term t with @@ -62,9 +74,9 @@ let rec mk_clos_but f_map subs t = and mk_clos_app_but f_map subs f args n = if n >= Array.length args then mk_atom(mkApp(f, args)) else - let fargs, args' = array_chop n args in + let fargs, args' = Array.chop n args in let f' = mkApp(f,fargs) in - match f_map f' with + match f_map (global_of_constr_nofail f') with Some map -> mk_clos_deep (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s')) @@ -72,24 +84,13 @@ and mk_clos_app_but f_map subs f args n = (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) | None -> mk_clos_app_but f_map subs f args (n+1) - -let interp_map l c = - try - let (im,am) = List.assoc c l in - Some(fun i -> - if List.mem i im then Eval - else if List.mem i am then Prot - else if i = -1 then Eval - else Rec) - with Not_found -> None - let interp_map l t = - try Some(list_assoc_f eq_constr t l) with Not_found -> None + try Some(List.assoc_f eq_gr t l) with Not_found -> None -let protect_maps = ref Stringmap.empty -let add_map s m = protect_maps := Stringmap.add s m !protect_maps +let protect_maps = ref String.Map.empty +let add_map s m = protect_maps := String.Map.add s m !protect_maps let lookup_map map = - try Stringmap.find map !protect_maps + try String.Map.find map !protect_maps with Not_found -> errorlabstrm"lookup_map"(str"map "++qs map++str"not found") @@ -101,112 +102,120 @@ let protect_tac map = Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Termops.InHyp));; + Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));; TACTIC EXTEND protect_fv [ "protect_fv" string(map) "in" ident(id) ] -> - [ protect_tac_in map id ] + [ Proofview.V82.tactic (protect_tac_in map id) ] | [ "protect_fv" string(map) ] -> - [ protect_tac map ] + [ Proofview.V82.tactic (protect_tac map) ] END;; (****************************************************************************) let closed_term t l = - let l = List.map constr_of_global l in + let l = List.map Universes.constr_of_global l in let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt()) ;; TACTIC EXTEND closed_term [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> - [ closed_term t l ] + [ Proofview.V82.tactic (closed_term t l) ] END ;; -TACTIC EXTEND echo +(* TACTIC EXTEND echo | [ "echo" constr(t) ] -> [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] -END;; +END;;*) (* let closed_term_ast l = - TacFun([Some(id_of_string"t")], - TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term", - [Genarg.in_gen Genarg.wit_constr (mkVar(id_of_string"t")); - Genarg.in_gen (Genarg.wit_list1 Genarg.wit_ref) l]))) + TacFun([Some(Id.of_string"t")], + TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", + [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t")); + Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l]))) *) let closed_term_ast l = - let l = List.map (fun gr -> ArgArg(dummy_loc,gr)) l in - TacFun([Some(id_of_string"t")], - TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term", - [Genarg.in_gen Genarg.globwit_constr (GVar(dummy_loc,id_of_string"t"),None); - Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l]))) + let tacname = { + mltac_plugin = "newring_plugin"; + mltac_tactic = "closed_term"; + } in + let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in + TacFun([Some(Id.of_string"t")], + TacML(Loc.ghost,tacname, + [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None); + Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l])) (* -let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term" +let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) (****************************************************************************) let ic c = let env = Global.env() and sigma = Evd.empty in - Constrintern.interp_constr sigma env c + Constrintern.interp_open_constr env sigma c + +let ic_unsafe c = (*FIXME remove *) + let env = Global.env() and sigma = Evd.empty in + fst (Constrintern.interp_constr env sigma 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 - { const_entry_body = c; - const_entry_secctx = None; - const_entry_type = None; - const_entry_opaque = true }, - IsProof Lemma)) +let decl_constant na ctx c = + let vars = Universes.universes_of_constr c in + let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in + mkConst(declare_constant (Id.of_string na) + (DefinitionEntry (definition_entry ~opaque:true + ~univs:(Univ.ContextSet.to_context ctx) c), + IsProof Lemma)) (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = - TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) + TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args)) (* Calling a locally bound tactic *) let ltac_lcall tac args = - TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) + TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args)) let ltac_letin (x, e1) e2 = - TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2) + TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2) let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) = Tacinterp.eval_tactic (ltac_letin ("F", Tacexp f) (ltac_lcall "F" args)) let ltac_record flds = - TacFun([Some(id_of_string"proj")], ltac_lcall "proj" flds) + TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds) -let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c) +let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c) -let dummy_goal env = +let dummy_goal env sigma = let (gl,_,sigma) = - Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Store.empty in - {Evd.it = gl; - Evd.sigma = sigma} + Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in + {Evd.it = gl; Evd.sigma = sigma} -let exec_tactic env n f args = - let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in +let constr_of v = match Value.to_constr v with + | Some c -> c + | None -> failwith "Ring.exec_tactic: anomaly" + +let exec_tactic env evd n f args = + let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let res = ref [||] in let get_res ist = - let l = List.map (fun id -> List.assoc id ist.lfun) lid in + let l = List.map (fun id -> Id.Map.find id ist.lfun) lid in res := Array.of_list l; TacId[] in let getter = Tacexp(TacFun(List.map(fun id -> Some id) lid, - glob_tactic(tacticIn get_res))) in - let _ = - Tacinterp.eval_tactic(ltac_call f (args@[getter])) (dummy_goal env) in - !res - -let constr_of = function - | VConstr ([],c) -> c - | _ -> failwith "Ring.exec_tactic: anomaly" + Tacintern.glob_tactic(tacticIn get_res))) in + let gl = dummy_goal env evd in + let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in + let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in + Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd let stdlib_modules = [["Coq";"Setoids";"Setoid"]; @@ -217,16 +226,23 @@ let stdlib_modules = let coq_constant c = lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c) +let coq_reference c = + lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c) let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" -let coq_cons = coq_constant "cons" -let coq_nil = coq_constant "nil" -let coq_None = coq_constant "None" -let coq_Some = coq_constant "Some" +let coq_None = coq_reference "None" +let coq_Some = coq_reference "Some" let coq_eq = coq_constant "eq" +let coq_cons = coq_reference "cons" +let coq_nil = coq_reference "nil" + let lapp f args = mkApp(Lazy.force f,args) +let plapp evd f args = + let fc = Evarutil.e_new_global evd (Lazy.force f) in + mkApp(fc,args) + let dest_rel0 t = match kind_of_term t with | App(f,args) when Array.length args >= 2 -> @@ -255,17 +271,19 @@ let plugin_modules = let my_constant c = lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c) +let my_reference c = + lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) let new_ring_path = - make_dirpath (List.map id_of_string ["Ring_tac";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) let ltac s = - lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s)) + lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s)) let znew_ring_path = - make_dirpath (List.map id_of_string ["InitialRing";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = - lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s)) + lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s)) -let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);; +let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);; let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; (* Ring theory *) @@ -274,9 +292,9 @@ let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; let coq_almost_ring_theory = my_constant "almost_ring_theory" (* setoid and morphism utilities *) -let coq_eq_setoid = my_constant "Eqsth" -let coq_eq_morph = my_constant "Eq_ext" -let coq_eq_smorph = my_constant "Eq_s_ext" +let coq_eq_setoid = my_reference "Eqsth" +let coq_eq_morph = my_reference "Eq_ext" +let coq_eq_smorph = my_reference "Eq_s_ext" (* ring -> almost_ring utilities *) let coq_ring_theory = my_constant "ring_theory" @@ -303,16 +321,19 @@ let ltac_inv_morph_nothing = zltac"inv_morph_nothing" let coq_pow_N_pow_N = my_constant "pow_N_pow_N" (* hypothesis *) -let coq_mkhypo = my_constant "mkhypo" -let coq_hypo = my_constant "hypo" +let coq_mkhypo = my_reference "mkhypo" +let coq_hypo = my_reference "hypo" (* Equality: do not evaluate but make recursive call on both sides *) let map_with_eq arg_map c = let (req,_,_) = dest_rel c in interp_map - ((req,(function -1->Prot|_->Rec)):: + ((global_head_of_constr req,(function -1->Prot|_->Rec)):: List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) +let map_without_eq arg_map _ = + interp_map (List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) + let _ = add_map "ring" (map_with_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); @@ -343,15 +364,12 @@ type ring_info = ring_pre_tac : glob_tactic_expr; ring_post_tac : glob_tactic_expr } -module Cmap = Map.Make(struct type t = constr let compare = constr_ord end) +module Cmap = Map.Make(Constr) -let from_carrier = ref Cmap.empty -let from_relation = ref Cmap.empty -let from_name = ref Spmap.empty +let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" +let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table" let ring_for_carrier r = Cmap.find r !from_carrier -let ring_for_relation rel = Cmap.find rel !from_relation - let find_ring_structure env sigma l = match l with @@ -370,32 +388,9 @@ let find_ring_structure env sigma l = (str"cannot find a declared ring structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false -(* - let (req,_,_) = dest_rel cl in - (try ring_for_relation req - with Not_found -> - errorlabstrm "ring" - (str"cannot find a declared ring structure for equality"++ - spc()++str"\""++pr_constr req++str"\"")) *) - -let _ = - Summary.declare_summary "tactic-new-ring-table" - { Summary.freeze_function = - (fun () -> !from_carrier,!from_relation,!from_name); - Summary.unfreeze_function = - (fun (ct,rt,nt) -> - from_carrier := ct; from_relation := rt; from_name := nt); - Summary.init_function = - (fun () -> - from_carrier := Cmap.empty; from_relation := Cmap.empty; - from_name := Spmap.empty) } let add_entry (sp,_kn) e = -(* let _ = ty e.ring_lemma1 in - let _ = ty e.ring_lemma2 in -*) 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 @@ -408,10 +403,10 @@ let subst_th (subst,th) = let th' = subst_mps subst th.ring_th in let thm1' = subst_mps subst th.ring_lemma1 in let thm2' = subst_mps subst th.ring_lemma2 in - let tac'= subst_tactic subst th.ring_cst_tac in - let pow_tac'= subst_tactic subst th.ring_pow_tac in - let pretac'= subst_tactic subst th.ring_pre_tac in - let posttac'= subst_tactic subst th.ring_post_tac in + let tac'= Tacsubst.subst_tactic subst th.ring_cst_tac in + let pow_tac'= Tacsubst.subst_tactic subst th.ring_pow_tac in + let pretac'= Tacsubst.subst_tactic subst th.ring_pre_tac in + let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in if c' == th.ring_carrier && eq' == th.ring_req && eq_constr set' th.ring_setoid && @@ -443,20 +438,20 @@ let theory_to_obj : ring_info -> obj = let cache_th (name,th) = add_entry name th in declare_object {(default_object "tactic-new-ring-theory") with - open_function = (fun i o -> if i=1 then cache_th o); + open_function = (fun i o -> if Int.equal i 1 then cache_th o); cache_function = cache_th; subst_function = subst_th; classify_function = (fun x -> Substitute x)} -let setoid_of_relation env a r = - let evm = Evd.empty in +let setoid_of_relation env evd a r = try - lapp coq_mk_Setoid - [|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 |] + let evm = !evd in + let evm, refl = Rewrite.get_reflexive_proof env evm a r in + let evm, sym = Rewrite.get_symmetric_proof env evm a r in + let evm, trans = Rewrite.get_transitive_proof env evm a r in + evd := evm; + lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |] with Not_found -> error "cannot find setoid relation" @@ -469,7 +464,7 @@ let op_smorph r add mul req m1 m2 = (* let default_ring_equality (r,add,mul,opp,req) = *) (* let is_setoid = function *) (* {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *) -(* eq_constr req rel (\* Qu: use conversion ? *\) *) +(* eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *) (* | _ -> false in *) (* match default_relation_for_carrier ~filter:is_setoid r with *) (* Leibniz _ -> *) @@ -484,7 +479,7 @@ let op_smorph r add mul req m1 m2 = (* let is_endomorphism = function *) (* { args=args } -> List.for_all *) (* (function (var,Relation rel) -> *) -(* var=None && eq_constr req rel *) +(* var=None && eq_constr_nounivs req rel *) (* | _ -> false) args in *) (* let add_m = *) (* try default_morphism ~filter:is_endomorphism add *) @@ -519,17 +514,19 @@ let op_smorph r add mul req m1 m2 = (* op_smorph r add mul req add_m.lem mul_m.lem) in *) (* (setoid,op_morph) *) -let ring_equality (r,add,mul,opp,req) = +let ring_equality env evd (r,add,mul,opp,req) = match kind_of_term req with - | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) -> - let setoid = lapp coq_eq_setoid [|r|] in + | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) -> + let setoid = plapp evd coq_eq_setoid [|r|] in let op_morph = match opp with - Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] - | None -> lapp coq_eq_smorph [|r;add;mul|] in + Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|] + | None -> plapp evd coq_eq_smorph [|r;add;mul|] in + let setoid = Typing.solve_evars env evd setoid in + let op_morph = Typing.solve_evars env evd op_morph in (setoid,op_morph) | _ -> - let setoid = setoid_of_relation (Global.env ()) r req in + let setoid = setoid_of_relation (Global.env ()) evd r req in let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in let add_m, add_m_lem = try Rewrite.default_morphism signature add @@ -549,7 +546,7 @@ let ring_equality (r,add,mul,opp,req) = let op_morph = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in Flags.if_verbose - msgnl + msg_info (str"Using setoid \""++pr_constr req++str"\""++spc()++ str"and morphisms \""++pr_constr add_m_lem ++ str"\","++spc()++ str"\""++pr_constr mul_m_lem++ @@ -558,7 +555,7 @@ let ring_equality (r,add,mul,opp,req) = op_morph) | None -> (Flags.if_verbose - msgnl + msg_info (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ str"and morphisms \""++pr_constr add_m_lem ++ str"\""++spc()++str"and \""++ @@ -566,22 +563,22 @@ let ring_equality (r,add,mul,opp,req) = 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 = +let build_setoid_params env evd r add mul opp req eqth = match eqth with Some th -> th - | None -> ring_equality (r,add,mul,opp,req) + | None -> ring_equality env evd (r,add,mul,opp,req) let dest_ring env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in match kind_of_term th_typ with App(f,[|r;zero;one;add;mul;sub;opp;req|]) - when eq_constr f (Lazy.force coq_almost_ring_theory) -> + when eq_constr_nounivs f (Lazy.force coq_almost_ring_theory) -> (None,r,zero,one,add,mul,Some sub,Some opp,req) | App(f,[|r;zero;one;add;mul;req|]) - when eq_constr f (Lazy.force coq_semi_ring_theory) -> + when eq_constr_nounivs f (Lazy.force coq_semi_ring_theory) -> (Some true,r,zero,one,add,mul,None,None,req) | App(f,[|r;zero;one;add;mul;sub;opp;req|]) - when eq_constr f (Lazy.force coq_ring_theory) -> + when eq_constr_nounivs f (Lazy.force coq_ring_theory) -> (Some false,r,zero,one,add,mul,Some sub,Some opp,req) | _ -> error "bad ring structure" @@ -591,18 +588,18 @@ let dest_morph env sigma m_spec = match kind_of_term m_typ with App(f,[|r;zero;one;add;mul;sub;opp;req; c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) - when eq_constr f (Lazy.force coq_ring_morph) -> + when eq_constr_nounivs f (Lazy.force coq_ring_morph) -> (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi) | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) - when eq_constr f (Lazy.force coq_semi_morph) -> + when eq_constr_nounivs f (Lazy.force coq_semi_morph) -> (c,czero,cone,cadd,cmul,None,None,ceqb,phi) | _ -> error "bad morphism structure" -type coeff_spec = - Computational of constr (* equality test *) +type 'constr coeff_spec = + Computational of 'constr (* equality test *) | Abstract (* coeffs = Z *) - | Morphism of constr (* general morphism *) + | Morphism of 'constr (* general morphism *) let reflect_coeff rkind = @@ -618,101 +615,89 @@ type cst_tac_spec = let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = match cst_tac with - Some (CstTac t) -> Tacinterp.glob_tactic t + Some (CstTac t) -> Tacintern.glob_tactic t | Some (Closed lc) -> closed_term_ast (List.map Smartlocate.global_with_alias lc) | None -> - (match rk, opp, kind with - Abstract, None, _ -> - let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in - TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) - | Abstract, Some opp, Some _ -> - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in - TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) - | Abstract, Some opp, None -> - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in - TacArg - (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) - | Computational _,_,_ -> - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in - TacArg - (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one])) - | Morphism mth,_,_ -> - let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in - TacArg - (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone]))) - -let make_hyp env c = - let t = Retyping.get_type_of env Evd.empty c in - lapp coq_mkhypo [|t;c|] - -let make_hyp_list env lH = - let carrier = Lazy.force coq_hypo in - 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 carrier = Lazy.force coq_hypo in + let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in + TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])) + +let make_hyp env evd c = + let t = Retyping.get_type_of env !evd c in + plapp evd coq_mkhypo [|t;c|] + +let make_hyp_list env evd lH = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in + let l = + List.fold_right + (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH + (plapp evd coq_nil [|carrier|]) + in + let l' = Typing.solve_evars env evd l in + Evarutil.nf_evars_universes !evd l' + +let interp_power env evd pow = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in match pow with | None -> - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in - (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) + let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in + (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with - | CstTac t -> Tacinterp.glob_tactic t + | CstTac t -> Tacintern.glob_tactic t | Closed lc -> closed_term_ast (List.map Smartlocate.global_with_alias lc) in - let spec = make_hyp env (ic spec) in - (tac, lapp coq_Some [|carrier; spec|]) + let spec = make_hyp env evd (ic_unsafe spec) in + (tac, plapp evd coq_Some [|carrier; spec|]) -let interp_sign env sign = - let carrier = Lazy.force coq_hypo in +let interp_sign env evd sign = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in match sign with - | None -> lapp coq_None [|carrier|] + | None -> plapp evd coq_None [|carrier|] | Some spec -> - let spec = make_hyp env (ic spec) in - lapp coq_Some [|carrier;spec|] + let spec = make_hyp env evd (ic_unsafe spec) in + plapp evd coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let interp_div env div = - let carrier = Lazy.force coq_hypo in +let interp_div env evd div = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in match div with - | None -> lapp coq_None [|carrier|] + | None -> plapp evd coq_None [|carrier|] | Some spec -> - let spec = make_hyp env (ic spec) in - lapp coq_Some [|carrier;spec|] + let spec = make_hyp env evd (ic_unsafe spec) in + plapp evd coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let add_theory name rth eqth morphth cst_tac (pre,post) power sign div = +let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = check_required_library (cdir@["Ring_base"]); let env = Global.env() in - 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 sspec = interp_sign env sign in - let dspec = interp_div env div in + let evd = ref sigma in + let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in + let (pow_tac, pspec) = interp_power env evd power in + let sspec = interp_sign env evd sign in + let dspec = interp_div env evd div in let rk = reflect_coeff morphth in - let params = - exec_tactic env 5 (zltac "ring_lemmas") + let params,ctx = + exec_tactic env !evd 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 + let lemma1 = params.(3) in + let lemma2 = params.(4) in - let lemma1 = decl_constant (string_of_id name^"_ring_lemma1") lemma1 in - let lemma2 = decl_constant (string_of_id name^"_ring_lemma2") lemma2 in + let lemma1 = + decl_constant (Id.to_string name^"_ring_lemma1") ctx lemma1 in + let lemma2 = + decl_constant (Id.to_string name^"_ring_lemma2") ctx lemma2 in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = match pre with - Some t -> Tacinterp.glob_tactic t + Some t -> Tacintern.glob_tactic t | _ -> TacId [] in let posttac = match post with - Some t -> Tacinterp.glob_tactic t + Some t -> Tacintern.glob_tactic t | _ -> TacId [] in let _ = Lib.add_leaf name @@ -720,9 +705,9 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div = { ring_carrier = r; ring_req = req; ring_setoid = sth; - ring_ext = constr_of params.(1); - ring_morph = constr_of params.(2); - ring_th = constr_of params.(0); + ring_ext = params.(1); + ring_morph = params.(2); + ring_th = params.(0); ring_cst_tac = cst_tac; ring_pow_tac = pow_tac; ring_lemma1 = lemma1; @@ -731,22 +716,28 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div = ring_post_tac = posttac }) in () -type ring_mod = - Ring_kind of coeff_spec +type 'constr ring_mod = + Ring_kind of 'constr coeff_spec | Const_tac of cst_tac_spec | Pre_tac of raw_tactic_expr | Post_tac of raw_tactic_expr - | Setoid of Topconstr.constr_expr * Topconstr.constr_expr - | Pow_spec of cst_tac_spec * Topconstr.constr_expr + | Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr + | Pow_spec of cst_tac_spec * Constrexpr.constr_expr (* Syntaxification tactic , correctness lemma *) - | Sign_spec of Topconstr.constr_expr - | Div_spec of Topconstr.constr_expr + | Sign_spec of Constrexpr.constr_expr + | Div_spec of Constrexpr.constr_expr + + +let ic_coeff_spec = function + | Computational t -> Computational (ic_unsafe t) + | Morphism t -> Morphism (ic_unsafe t) + | Abstract -> Abstract VERNAC ARGUMENT EXTEND ring_mod - | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic eq_test)) ] + | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] | [ "abstract" ] -> [ Ring_kind Abstract ] - | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic morph)) ] + | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ] | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ] | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] @@ -761,7 +752,7 @@ VERNAC ARGUMENT EXTEND ring_mod END let set_once s r v = - if !r = None then r := Some v else error (s^" cannot be set twice") + if Option.is_empty !r then r := Some v else error (s^" cannot be set twice") let process_ring_mods l = let kind = ref None in @@ -773,21 +764,29 @@ let process_ring_mods l = let power = ref None in let div = ref None in List.iter(function - Ring_kind k -> set_once "ring kind" kind k + Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k) | 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_unsafe sth,ic_unsafe 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; let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !cst_tac, !pre, !post, !power, !sign, !div) -VERNAC COMMAND EXTEND AddSetoidRing +VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in add_theory id (ic t) set k cst (pre,post) power sign div] + | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ + msg_notice (strbrk "The following ring structures have been declared:"); + Spmap.iter (fun fn fi -> + msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr fi.ring_req)) + ) !from_name ] END (*****************************************************************************) @@ -799,10 +798,11 @@ let make_args_list rl t = | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2] | _ -> rl -let make_term_list carrier rl = - List.fold_right - (fun x l -> lapp coq_cons [|carrier;x;l|]) rl - (lapp coq_nil [|carrier|]) +let make_term_list env evd carrier rl = + let l = List.fold_right + (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl + (plapp evd coq_nil [|carrier|]) + in Typing.solve_evars env evd l let ltac_ring_structure e = let req = carg e.ring_req in @@ -819,19 +819,24 @@ let ltac_ring_structure e = [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] -let ring_lookup (f:glob_tactic_expr) lH rl t gl = - let env = pf_env gl in - let sigma = project gl in - let rl = make_args_list rl t in - let e = find_ring_structure env sigma rl in - let rl = carg (make_term_list e.ring_carrier rl) in - let lH = carg (make_hyp_list env lH) in - let ring = ltac_ring_structure e in - ltac_apply f (ring@[lH;rl]) gl +let ring_lookup (f:glob_tactic_expr) lH rl t = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + try (* find_ring_strucure can raise an exception *) + let evdref = ref sigma in + let rl = make_args_list rl t in + let e = find_ring_structure env sigma rl in + let rl = carg (make_term_list env evdref e.ring_carrier rl) in + let lH = carg (make_hyp_list env evdref lH) in + let ring = ltac_ring_structure e in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end TACTIC EXTEND ring_lookup | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> - [ let (t,lr) = list_sep_last lrt in ring_lookup f lH lr t] + [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] END @@ -839,10 +844,10 @@ END (***********************************************************************) let new_field_path = - make_dirpath (List.map id_of_string ["Field_tac";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) let field_ltac s = - lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s)) + lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s)) let _ = add_map "field" @@ -851,9 +856,9 @@ let _ = add_map "field" coq_nil, (function -1->Eval|_ -> Prot); (* display_linear: evaluate polynomials and coef operations, protect field operations and make recursive call on the var map *) - my_constant "display_linear", + my_reference "display_linear", (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); - my_constant "display_pow_linear", + my_reference "display_pow_linear", (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) @@ -865,16 +870,16 @@ let _ = add_map "field" pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot); (* 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)]);; + my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; let _ = add_map "field_cond" - (map_with_eq + (map_without_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); (* PCond: evaluate morphism and denum list, protect ring operations and make recursive call on the var map *) - my_constant "PCond", (function -1|8|10|13->Eval|12->Rec|_->Prot)]);; -(* (function -1|8|10->Eval|9->Rec|_->Prot)]);;*) + my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);; +(* (function -1|9|11->Eval|10->Rec|_->Prot)]);;*) let _ = Redexpr.declare_reduction "simpl_field_expr" @@ -882,29 +887,29 @@ let _ = Redexpr.declare_reduction "simpl_field_expr" -let afield_theory = my_constant "almost_field_theory" -let field_theory = my_constant "field_theory" -let sfield_theory = my_constant "semi_field_theory" -let af_ar = my_constant"AF_AR" -let f_r = my_constant"F_R" -let sf_sr = my_constant"SF_SR" -let dest_field env sigma th_spec = - let th_typ = Retyping.get_type_of env sigma th_spec in +let afield_theory = my_reference "almost_field_theory" +let field_theory = my_reference "field_theory" +let sfield_theory = my_reference "semi_field_theory" +let af_ar = my_reference"AF_AR" +let f_r = my_reference"F_R" +let sf_sr = my_reference"SF_SR" +let dest_field env evd th_spec = + let th_typ = Retyping.get_type_of env !evd th_spec in match kind_of_term th_typ with | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when eq_constr f (Lazy.force afield_theory) -> - let rth = lapp af_ar + when is_global (Lazy.force afield_theory) f -> + let rth = plapp evd af_ar [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when eq_constr f (Lazy.force field_theory) -> + when is_global (Lazy.force field_theory) f -> let rth = - lapp f_r + plapp evd f_r [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;div;inv;req|]) - when eq_constr f (Lazy.force sfield_theory) -> - let rth = lapp sf_sr + when is_global (Lazy.force sfield_theory) f -> + let rth = plapp evd sf_sr [|r;zero;one;add;mul;div;inv;req;th_spec|] in (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) | _ -> error "bad field structure" @@ -922,13 +927,10 @@ type field_info = field_pre_tac : glob_tactic_expr; field_post_tac : glob_tactic_expr } -let field_from_carrier = ref Cmap.empty -let field_from_relation = ref Cmap.empty -let field_from_name = ref Spmap.empty - +let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table" +let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table" let field_for_carrier r = Cmap.find r !field_from_carrier -let field_for_relation rel = Cmap.find rel !field_from_relation let find_field_structure env sigma l = check_required_library (cdir@["Field_tac"]); @@ -948,35 +950,9 @@ let find_field_structure env sigma l = (str"cannot find a declared field structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false -(* let (req,_,_) = dest_rel cl in - (try field_for_relation req - with Not_found -> - errorlabstrm "field" - (str"cannot find a declared field structure for equality"++ - spc()++str"\""++pr_constr req++str"\"")) *) - -let _ = - Summary.declare_summary "tactic-new-field-table" - { Summary.freeze_function = - (fun () -> !field_from_carrier,!field_from_relation,!field_from_name); - Summary.unfreeze_function = - (fun (ct,rt,nt) -> - field_from_carrier := ct; field_from_relation := rt; - field_from_name := nt); - Summary.init_function = - (fun () -> - field_from_carrier := Cmap.empty; field_from_relation := Cmap.empty; - field_from_name := Spmap.empty) } let add_field_entry (sp,_kn) e = -(* - let _ = ty e.field_ok in - let _ = ty e.field_simpl_eq_ok in - let _ = ty e.field_simpl_ok in - let _ = ty e.field_cond in -*) 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 let subst_th (subst,th) = @@ -987,10 +963,10 @@ let subst_th (subst,th) = let thm3' = subst_mps subst th.field_simpl_ok in let thm4' = subst_mps subst th.field_simpl_eq_in_ok in let thm5' = subst_mps subst th.field_cond in - let tac'= subst_tactic subst th.field_cst_tac in - let pow_tac' = subst_tactic subst th.field_pow_tac in - let pretac'= subst_tactic subst th.field_pre_tac in - let posttac'= subst_tactic subst th.field_post_tac in + let tac'= Tacsubst.subst_tactic subst th.field_cst_tac in + let pow_tac' = Tacsubst.subst_tactic subst th.field_pow_tac in + let pretac'= Tacsubst.subst_tactic subst th.field_pre_tac in + let posttac'= Tacsubst.subst_tactic subst th.field_post_tac in if c' == th.field_carrier && eq' == th.field_req && thm1' == th.field_ok && @@ -1019,17 +995,17 @@ let ftheory_to_obj : field_info -> obj = let cache_th (name,th) = add_field_entry name th in declare_object {(default_object "tactic-new-field-theory") with - open_function = (fun i o -> if i=1 then cache_th o); + open_function = (fun i o -> if Int.equal i 1 then cache_th o); cache_function = cache_th; subst_function = subst_th; classify_function = (fun x -> Substitute x) } -let field_equality r inv req = +let field_equality evd r inv req = match kind_of_term req with - | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) -> - mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) + | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) -> + mkApp(Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) | _ -> - let _setoid = setoid_of_relation (Global.env ()) r req in + let _setoid = setoid_of_relation (Global.env ()) evd r req in let signature = [Some (r,Some req)],Some(r,Some req) in let inv_m, inv_m_lem = try Rewrite.default_morphism signature inv @@ -1037,45 +1013,50 @@ let field_equality r inv req = 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 = +let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power sign odiv = check_required_library (cdir@["Field_tac"]); let env = Global.env() in - let sigma = Evd.empty in + let evd = ref sigma in let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) = - dest_field env sigma fth in - let (sth,ext) = build_setoid_params r add mul opp req eqth in + dest_field env evd fth in + let (sth,ext) = build_setoid_params env evd 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 sspec = interp_sign env sign in - let dspec = interp_div env odiv in - let inv_m = field_equality r inv req in + let _ = add_theory name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in + let (pow_tac, pspec) = interp_power env evd power in + let sspec = interp_sign env evd sign in + let dspec = interp_div env evd odiv in + let inv_m = field_equality evd r inv req in let rk = reflect_coeff morphth in - let params = - exec_tactic env 9 (field_ltac"field_lemmas") + let params,ctx = + exec_tactic env !evd 9 (field_ltac"field_lemmas") (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in - let lemma1 = constr_of params.(3) in - let lemma2 = constr_of params.(4) in - let lemma3 = constr_of params.(5) in - let lemma4 = constr_of params.(6) in + let lemma1 = params.(3) in + let lemma2 = params.(4) in + let lemma3 = params.(5) in + let lemma4 = params.(6) in let cond_lemma = match inj with - | Some thm -> mkApp(constr_of params.(8),[|thm|]) - | None -> constr_of params.(7) in - let lemma1 = decl_constant (string_of_id name^"_field_lemma1") lemma1 in - let lemma2 = decl_constant (string_of_id name^"_field_lemma2") lemma2 in - let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in - let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in - let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in + | Some thm -> mkApp(params.(8),[|thm|]) + | None -> params.(7) in + let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") + ctx lemma1 in + let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") + ctx lemma2 in + let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") + ctx lemma3 in + let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") + ctx lemma4 in + let cond_lemma = decl_constant (Id.to_string name^"_lemma5") + ctx cond_lemma in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = match pre with - Some t -> Tacinterp.glob_tactic t + Some t -> Tacintern.glob_tactic t | _ -> TacId [] in let posttac = match post with - Some t -> Tacinterp.glob_tactic t + Some t -> Tacintern.glob_tactic t | _ -> TacId [] in let _ = Lib.add_leaf name @@ -1092,9 +1073,9 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi field_pre_tac = pretac; field_post_tac = posttac }) in () -type field_mod = - Ring_mod of ring_mod - | Inject of Topconstr.constr_expr +type 'constr field_mod = + Ring_mod of 'constr ring_mod + | Inject of Constrexpr.constr_expr VERNAC ARGUMENT EXTEND field_mod | [ ring_mod(m) ] -> [ Ring_mod m ] @@ -1112,23 +1093,31 @@ let process_field_mods l = let power = ref None in let div = ref None in List.iter(function - Ring_mod(Ring_kind k) -> set_once "field kind" kind k + Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k) | Ring_mod(Const_tac t) -> set_once "tactic recognizing constants" cst_tac t | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t - | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic sth,ic ext) + | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext) | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec) | Ring_mod(Sign_spec t) -> set_once "sign" sign t | Ring_mod(Div_spec t) -> set_once "div" div t - | Inject i -> set_once "infinite property" inj (ic i)) l; + | Inject i -> set_once "infinite property" inj (ic_unsafe i)) l; let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) -VERNAC COMMAND EXTEND AddSetoidField +VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "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] +| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ + msg_notice (strbrk "The following field structures have been declared:"); + Spmap.iter (fun fn fi -> + msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr fi.field_req)) + ) !field_from_name ] END @@ -1146,18 +1135,23 @@ let ltac_field_structure e = [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac] -let field_lookup (f:glob_tactic_expr) lH rl t gl = - let env = pf_env gl in - let sigma = project gl in - let rl = make_args_list rl t in - let e = find_field_structure env sigma rl in - let rl = carg (make_term_list e.field_carrier rl) in - let lH = carg (make_hyp_list env lH) in - let field = ltac_field_structure e in - ltac_apply f (field@[lH;rl]) gl +let field_lookup (f:glob_tactic_expr) lH rl t = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + try + let evdref = ref sigma in + let rl = make_args_list rl t in + let e = find_field_structure env sigma rl in + let rl = carg (make_term_list env evdref e.field_carrier rl) in + let lH = carg (make_hyp_list env evdref lH) in + let field = ltac_field_structure e in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end TACTIC EXTEND field_lookup | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> - [ let (t,l) = list_sep_last lt in field_lookup f lH l t ] + [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] END diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget index 580df9b5..595ba55e 100644 --- a/plugins/setoid_ring/vo.itarget +++ b/plugins/setoid_ring/vo.itarget @@ -7,7 +7,6 @@ InitialRing.vo NArithRing.vo RealField.vo Ring_base.vo -Ring_equiv.vo Ring_polynom.vo Ring_tac.vo Ring_theory.vo |