diff options
Diffstat (limited to 'contrib/setoid_ring')
| -rw-r--r-- | contrib/setoid_ring/ArithRing.v | 70 | ||||
| -rw-r--r-- | contrib/setoid_ring/BinList.v | 58 | ||||
| -rw-r--r-- | contrib/setoid_ring/Field.v | 10 | ||||
| -rw-r--r-- | contrib/setoid_ring/Field_tac.v | 200 | ||||
| -rw-r--r-- | contrib/setoid_ring/Field_theory.v | 1460 | ||||
| -rw-r--r-- | contrib/setoid_ring/InitialRing.v (renamed from contrib/setoid_ring/ZRing_th.v) | 451 | ||||
| -rw-r--r-- | contrib/setoid_ring/NArithRing.v | 31 | ||||
| -rw-r--r-- | contrib/setoid_ring/RealField.v | 105 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring.v | 43 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_base.v | 16 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_equiv.v | 74 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_polynom.v (renamed from contrib/setoid_ring/Pol.v) | 697 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_tac.v | 794 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_theory.v (renamed from contrib/setoid_ring/Ring_th.v) | 120 | ||||
| -rw-r--r-- | contrib/setoid_ring/ZArithRing.v | 33 | ||||
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 1009 |
16 files changed, 3413 insertions, 1758 deletions
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v new file mode 100644 index 00000000..5060bc69 --- /dev/null +++ b/contrib/setoid_ring/ArithRing.v @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Mult. +Require Export Ring. +Set Implicit Arguments. + +Ltac isnatcst t := + let t := eval hnf in t in + match t with + O => true + | S ?p => isnatcst p + | _ => false + end. +Ltac natcst t := + match isnatcst t with + true => t + | _ => NotConstant + end. + +Ltac Ss_to_add f acc := + match f with + | S ?f1 => Ss_to_add f1 (S acc) + | _ => constr:(acc + f)%nat + end. + +Ltac natprering := + match goal with + |- context C [S ?p] => + match p with + O => fail 1 (* avoid replacing 1 with 1+0 ! *) + | p => match isnatcst p with + | true => fail 1 + | false => let v := Ss_to_add p (S 0) in + fold v; natprering + end + end + | _ => idtac + end. + + Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat). + Proof. + constructor. exact plus_0_l. exact plus_comm. exact plus_assoc. + exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc. + exact mult_plus_distr_r. + Qed. + + +Unboxed Fixpoint nateq (n m:nat) {struct m} : bool := + match n, m with + | O, O => true + | S n', S m' => nateq n' m' + | _, _ => false + end. + +Lemma nateq_ok : forall n m:nat, nateq n m = true -> n = m. +Proof. + simple induction n; simple induction m; simpl; intros; try discriminate. + trivial. + rewrite (H n1 H1). + trivial. +Qed. + +Add Ring natr : natSRth + (decidable nateq_ok, constants [natcst], preprocess [natprering]). diff --git a/contrib/setoid_ring/BinList.v b/contrib/setoid_ring/BinList.v index 0def087f..0d0fe5a4 100644 --- a/contrib/setoid_ring/BinList.v +++ b/contrib/setoid_ring/BinList.v @@ -1,46 +1,36 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + Set Implicit Arguments. Require Import BinPos. +Require Export List. +Require Export ListTactics. Open Scope positive_scope. +Section MakeBinList. + Variable A : Type. + Variable default : A. -Section LIST. - - Variable A:Type. - Variable default:A. - - Inductive list : Type := - | nil : list - | cons : A -> list -> list. - - Infix "::" := cons (at level 60, right associativity). - - Definition hd l := match l with hd :: _ => hd | _ => default end. - - Definition tl l := match l with _ :: tl => tl | _ => nil end. - - Fixpoint jump (p:positive) (l:list) {struct p} : list := + Fixpoint jump (p:positive) (l:list A) {struct p} : list A := match p with - | xH => tl l + | xH => tail l | xO p => jump p (jump p l) - | xI p => jump p (jump p (tl l)) + | xI p => jump p (jump p (tail l)) end. - Fixpoint nth (p:positive) (l:list) {struct p} : A:= + Fixpoint nth (p:positive) (l:list A) {struct p} : A:= match p with - | xH => hd l + | xH => hd default l | xO p => nth p (jump p l) - | xI p => nth p (jump p (tl l)) + | xI p => nth p (jump p (tail l)) end. - Fixpoint rev_append (rev l : list) {struct l} : list := - match l with - | nil => rev - | (cons h t) => rev_append (cons h rev) t - end. - - Definition rev l : list := rev_append nil l. - - Lemma jump_tl : forall j l, tl (jump j l) = jump j (tl l). + Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l). Proof. induction j;simpl;intros. repeat rewrite IHj;trivial. @@ -71,7 +61,7 @@ Section LIST. Qed. Lemma jump_Pdouble_minus_one : forall i l, - (jump (Pdouble_minus_one i) (tl l)) = (jump i (jump i l)). + (jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)). Proof. induction i;intros;simpl. repeat rewrite jump_tl;trivial. @@ -80,7 +70,7 @@ Section LIST. Qed. - Lemma nth_jump : forall p l, nth p (tl l) = hd (jump p l). + Lemma nth_jump : forall p l, nth p (tail l) = hd default (jump p l). Proof. induction p;simpl;intros. rewrite <-jump_tl;rewrite IHp;trivial. @@ -89,7 +79,7 @@ Section LIST. Qed. Lemma nth_Pdouble_minus_one : - forall p l, nth (Pdouble_minus_one p) (tl l) = nth p (jump p l). + forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l). Proof. induction p;simpl;intros. repeat rewrite jump_tl;trivial. @@ -98,4 +88,4 @@ Section LIST. trivial. Qed. -End LIST. +End MakeBinList. diff --git a/contrib/setoid_ring/Field.v b/contrib/setoid_ring/Field.v new file mode 100644 index 00000000..a944ba5f --- /dev/null +++ b/contrib/setoid_ring/Field.v @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Export Field_theory. +Require Export Field_tac. diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v new file mode 100644 index 00000000..786654ab --- /dev/null +++ b/contrib/setoid_ring/Field_tac.v @@ -0,0 +1,200 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Ring_tac BinList Ring_polynom InitialRing. +Require Export Field_theory. + + (* syntaxification *) + Ltac mkFieldexpr C Cst radd rmul rsub ropp rdiv rinv t fv := + let rec mkP t := + match Cst t with + | Ring_tac.NotConstant => + match t with + | (radd ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEadd e1 e2) + | (rmul ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEmul e1 e2) + | (rsub ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEsub e1 e2) + | (ropp ?t1) => + let e1 := mkP t1 in constr:(FEopp e1) + | (rdiv ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEdiv e1 e2) + | (rinv ?t1) => + let e1 := mkP t1 in constr:(FEinv e1) + | _ => + let p := Find_at t fv in constr:(@FEX C p) + end + | ?c => constr:(FEc c) + end + in mkP t. + +Ltac FFV Cst add mul sub opp div inv t fv := + let rec TFV t fv := + match Cst t with + | Ring_tac.NotConstant => + match t with + | (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) + | (opp ?t1) => TFV t1 fv + | (div ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) + | (inv ?t1) => TFV t1 fv + | _ => AddFvTail t fv + end + | _ => fv + end + in TFV t fv. + +Ltac ParseFieldComponents lemma req := + match type of lemma with + | context [@FEeval ?R ?rO ?add ?mul ?sub ?opp ?div ?inv ?C ?phi _ _] => + (fun f => f add mul sub opp div inv C) + | _ => fail 1 "field anomaly: bad correctness lemma (parse)" + end. + +(* simplifying the non-zero condition... *) + +Ltac fold_field_cond req := + let rec fold_concl t := + match t with + ?x /\ ?y => + let fx := fold_concl x in let fy := fold_concl y in constr:(fx/\fy) + | req ?x ?y -> False => constr:(~ req x y) + | _ => t + end in + match goal with + |- ?t => let ft := fold_concl t in change ft + end. + +Ltac simpl_PCond req := + protect_fv "field_cond"; + try (exact I); + fold_field_cond req. + +(* Rewriting (field_simplify) *) +Ltac Field_simplify lemma Cond_lemma req Cst_tac := + let Make_tac := + match type of lemma with + | forall l fe nfe, + _ = nfe -> + PCond _ _ _ _ _ _ _ _ _ -> + req (FEeval ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv (C:=?C) ?phi l fe) + _ => + let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in + let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in + let simpl_field H := protect_fv "field" in H in + fun f rl => f mkFV mkFE simpl_field lemma req rl; + try (apply Cond_lemma; simpl_PCond req) + | _ => fail 1 "field anomaly: bad correctness lemma (rewr)" + end in + Make_tac ReflexiveRewriteTactic. +(* Pb: second rewrite are applied to non-zero condition of first rewrite... *) + +Tactic Notation (at level 0) "field_simplify" constr_list(rl) := + field_lookup + (fun req cst_tac _ _ field_simplify_ok cond_ok pre post rl => + pre(); Field_simplify field_simplify_ok cond_ok req cst_tac rl; post()). + + +(* Generic form of field tactics *) +Ltac Field_Scheme FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req := + let R := match type of req with ?R -> _ => R end in + let rec ParseExpr ilemma := + match type of ilemma with + forall nfe, ?fe = nfe -> _ => + (fun t => + let x := fresh "fld_expr" in + let H := fresh "norm_fld_expr" in + compute_assertion H x fe; + ParseExpr (ilemma x H) t; + try clear x H) + | _ => (fun t => t ilemma) + end in + let Main r1 r2 := + let fv := FV_tac r1 (@List.nil R) in + let fv := FV_tac r2 fv in + let fe1 := SYN_tac r1 fv in + let fe2 := SYN_tac r2 fv in + ParseExpr (lemma fv fe1 fe2) + ltac:(fun ilemma => + apply ilemma || fail "field anomaly: failed in applying lemma"; + [ SIMPL_tac | apply Cond_lemma; simpl_PCond req]) in + OnEquation req Main. + +(* solve completely a field equation, leaving non-zero conditions to be + proved (field) *) +Ltac Field lemma Cond_lemma req Cst_tac := + let Main radd rmul rsub ropp rdiv rinv C := + let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in + let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in + let Simpl := + vm_compute; reflexivity || fail "not a valid field equation" in + Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in + ParseFieldComponents lemma req Main. + +Tactic Notation (at level 0) "field" := + field_lookup + (fun req cst_tac field_ok _ _ cond_ok pre post rl => + pre(); Field field_ok cond_ok req cst_tac; post()). + +(* transforms a field equation to an equivalent (simplified) ring equation, + and leaves non-zero conditions to be proved (field_simplify_eq) *) +Ltac Field_simplify_eq lemma Cond_lemma req Cst_tac := + let Main radd rmul rsub ropp rdiv rinv C := + let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in + let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in + let Simpl := (protect_fv "field") in + Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in + ParseFieldComponents lemma req Main. + +Tactic Notation (at level 0) "field_simplify_eq" := + field_lookup + (fun req cst_tac _ field_simplify_eq_ok _ cond_ok pre post rl => + pre(); Field_simplify_eq field_simplify_eq_ok cond_ok req cst_tac; + post()). + +(* Adding a new field *) + +Ltac ring_of_field f := + match type of f with + | almost_field_theory _ _ _ _ _ _ _ _ _ => constr:(AF_AR f) + | field_theory _ _ _ _ _ _ _ _ _ => constr:(F_R f) + | semi_field_theory _ _ _ _ _ _ _ => constr:(SF_SR f) + end. + +Ltac coerce_to_almost_field set ext f := + match type of f with + | almost_field_theory _ _ _ _ _ _ _ _ _ => f + | field_theory _ _ _ _ _ _ _ _ _ => constr:(F2AF set ext f) + | semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f) + end. + +Ltac field_elements set ext fspec rk := + let afth := coerce_to_almost_field set ext fspec in + let rspec := ring_of_field fspec in + ring_elements set ext rspec rk + ltac:(fun arth ext_r morph f => f afth ext_r morph). + + +Ltac field_lemmas set ext inv_m fspec rk := + field_elements set ext fspec rk + ltac:(fun afth ext_r morph => + let field_ok := constr:(Field_correct set ext_r inv_m afth morph) in + let field_simpl_ok := + constr:(Pphi_dev_div_ok set ext_r inv_m afth morph) in + let field_simpl_eq_ok := + constr:(Field_simplify_eq_correct set ext_r inv_m afth morph) in + let cond1_ok := constr:(Pcond_simpl_gen set ext_r afth morph) in + let cond2_ok := constr:(Pcond_simpl_complete set ext_r afth morph) in + (fun f => f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok + cond1_ok cond2_ok)). diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v new file mode 100644 index 00000000..f810859c --- /dev/null +++ b/contrib/setoid_ring/Field_theory.v @@ -0,0 +1,1460 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Ring. +Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List. +Require Import ZArith_base. +Set Implicit Arguments. + +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 : Setoid_Theory R req. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Variable SRinv_ext : forall p q, p == q -> / p == / q. + + (* Field properties *) + Record almost_field_theory : Prop := mk_afield { + AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req; + 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). + + (* 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. + + Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req + cO cI cadd cmul csub copp ceqb phi. + +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). +Proof. +intros. +generalize (fun h => X (morph_eq CRmorph c1 c2 h)). +case (ceqb c1 c2); auto. +Qed. + + + (* 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). + + + (* Usefull tactics *) + Add Setoid R req Rsth as R_set1. + Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. + Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism rinv : rinv_ext. exact SRinv_ext. Qed. + +Let eq_trans := Setoid.Seq_trans _ _ Rsth. +Let eq_sym := Setoid.Seq_sym _ _ Rsth. +Let eq_refl := Setoid.Seq_refl _ _ Rsth. + +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) . + +Notation NPEeval := (PEeval rO radd rmul rsub ropp phi). +Notation Nnorm := (norm cO cI cadd cmul csub copp ceqb). +Notation NPphi_dev := (Pphi_dev rO rI radd rmul cO cI ceqb phi). + +(* add abstract semi-ring to help with some proofs *) +Add Ring Rring : (ARth_SRth ARth). + + +(* additional ring properties *) + +Lemma rsub_0_l : forall r, 0 - r == - r. +intros; rewrite (ARsub_def ARth) in |- *; ring. +Qed. + +Lemma rsub_0_r : forall r, r - 0 == r. +intros; rewrite (ARsub_def ARth) in |- *. +rewrite (ARopp_zero Rsth Reqe ARth) in |- *; ring. +Qed. + +(*************************************************************************** + + Properties of division + + ***************************************************************************) + +Theorem rdiv_simpl: forall p q, ~ q == 0 -> q * (p / q) == p. +intros p q H. +rewrite rdiv_def in |- *. +transitivity (/ q * q * p); [ ring | idtac ]. +rewrite rinv_l in |- *; auto. +Qed. +Hint Resolve rdiv_simpl . + +Theorem SRdiv_ext: + forall p1 p2, p1 == p2 -> forall q1 q2, q1 == q2 -> p1 / q1 == p2 / q2. +intros p1 p2 H q1 q2 H0. +transitivity (p1 * / q1); auto. +transitivity (p2 * / q2); auto. +Qed. +Hint Resolve SRdiv_ext . + + Add Morphism rdiv : rdiv_ext. exact SRdiv_ext. Qed. + +Lemma rmul_reg_l : forall p q1 q2, + ~ p == 0 -> p * q1 == p * q2 -> q1 == q2. +intros. +rewrite <- (@rdiv_simpl q1 p) in |- *; trivial. +rewrite <- (@rdiv_simpl q2 p) in |- *; trivial. +repeat rewrite rdiv_def in |- *. +repeat rewrite (ARmul_assoc ARth) in |- *. +auto. +Qed. + +Theorem field_is_integral_domain : forall r1 r2, + ~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0. +Proof. +red in |- *; intros. +apply H0. +transitivity (1 * r2); auto. +transitivity (/ r1 * r1 * r2); auto. +rewrite <- (ARmul_assoc ARth) in |- *. +rewrite H1 in |- *. +apply ARmul_0_r with (1 := Rsth) (2 := ARth). +Qed. + +Theorem ropp_neq_0 : forall r, + ~ -(1) == 0 -> ~ r == 0 -> ~ -r == 0. +intros. +setoid_replace (- r) with (- (1) * r). + apply field_is_integral_domain; trivial. + rewrite <- (ARopp_mul_l ARth) in |- *. + rewrite (ARmul_1_l ARth) in |- *. + reflexivity. +Qed. + +Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1. +intros. +rewrite (AFdiv_def AFth) in |- *. +rewrite (ARmul_comm ARth) in |- *. +apply (AFinv_l AFth). +trivial. +Qed. + +Theorem rdiv1: forall r, r == r / 1. +intros r; transitivity (1 * (r / 1)); auto. +Qed. + +Theorem rdiv2: + forall r1 r2 r3 r4, + ~ r2 == 0 -> + ~ r4 == 0 -> + r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4). +Proof. +intros r1 r2 r3 r4 H H0. +assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). +apply rmul_reg_l with (r2 * r4); trivial. +rewrite rdiv_simpl in |- *; trivial. +rewrite (ARdistr_r Rsth Reqe ARth) in |- *. +apply (Radd_ext Reqe). + transitivity (r2 * (r1 / r2) * r4); [ ring | auto ]. + transitivity (r2 * (r4 * (r3 / r4))); auto. + transitivity (r2 * r3); auto. +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)). +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) + by complete (repeat apply field_is_integral_domain; trivial). +apply rmul_reg_l with (r2 * (r4 * r5)); trivial. +rewrite rdiv_simpl in |- *; trivial. +rewrite (ARdistr_r Rsth Reqe ARth) in |- *. +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. +intros r1 r2. +transitivity (- (r1 * / r2)); auto. +transitivity (- r1 * / r2); auto. +Qed. +Hint Resolve rdiv5 . + +Theorem rdiv3: + forall r1 r2 r3 r4, + ~ r2 == 0 -> + ~ r4 == 0 -> + r1 / r2 - r3 / r4 == (r1 * r4 - r3 * r2) / (r2 * r4). +intros r1 r2 r3 r4 H H0. +assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). +transitivity (r1 / r2 + - (r3 / r4)); auto. +transitivity (r1 / r2 + - r3 / r4); auto. +transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)); auto. +apply rdiv2; auto. +apply SRdiv_ext; auto. +transitivity (r1 * r4 + - (r3 * r2)); symmetry; 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 in |- *; ring. + apply rmul_reg_l with (r1 / r2); auto. + transitivity (/ (r1 / r2) * (r1 / r2)); auto. + transitivity 1; auto. + repeat rewrite rdiv_def in |- *. + transitivity (/ r1 * r1 * (/ r2 * r2)); [ idtac | ring ]. + repeat rewrite rinv_l in |- *; 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 complete (apply field_is_integral_domain; trivial). +apply rmul_reg_l with (r2 * r4); trivial. +rewrite rdiv_simpl in |- *; trivial. +transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ]. +repeat rewrite rdiv_simpl in |- *; trivial. +Qed. + + Theorem rdiv7: + forall r1 r2 r3 r4, + ~ r2 == 0 -> + ~ r3 == 0 -> + ~ r4 == 0 -> + (r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3). +Proof. +intros. +rewrite (rdiv_def (r1 / r2)) in |- *. +rewrite rdiv6 in |- *; trivial. +apply rdiv4; trivial. +Qed. + +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. +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 in |- *; trivial. + symmetry in |- *. + apply (ARmul_1_r Rsth ARth). + rewrite rdiv4 in |- *; trivial. + rewrite H1 in |- *. + rewrite (ARmul_comm ARth r2 r4) in |- *. + rewrite <- rdiv4 in |- *; trivial. + rewrite rdiv_r_r in |- *. + trivial. + apply (ARmul_1_r Rsth ARth). +Qed. + +(*************************************************************************** + + Some equality test + + ***************************************************************************) + +Fixpoint positive_eq (p1 p2 : positive) {struct p1} : bool := + match p1, p2 with + xH, xH => true + | xO p3, xO p4 => positive_eq p3 p4 + | xI p3, xI p4 => positive_eq p3 p4 + | _, _ => false + end. + +Theorem positive_eq_correct: + forall p1 p2, if positive_eq p1 p2 then p1 = p2 else p1 <> p2. +intros p1; elim p1; + (try (intros p2; case p2; simpl; auto; intros; discriminate)). +intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4. +generalize (rec p4); case (positive_eq p3 p4); auto. +intros H1; apply f_equal with ( f := xI ); auto. +intros H1 H2; case H1; injection H2; auto. +intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4. +generalize (rec p4); case (positive_eq p3 p4); auto. +intros H1; apply f_equal with ( f := xO ); auto. +intros H1 H2; case H1; injection H2; auto. +Qed. + +(* equality test *) +Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := + match e1, e2 with + PEc c1, PEc c2 => ceqb c1 c2 + | PEX p1, PEX p2 => positive_eq p1 p2 + | 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 + | _, _ => false + end. + +Theorem PExpr_eq_semi_correct: + forall l e1 e2, PExpr_eq e1 e2 = true -> NPEeval l e1 == NPEeval l e2. +intros l e1; elim e1. +intros c1; intros e2; elim e2; simpl; (try (intros; discriminate)). +intros c2; apply (morph_eq CRmorph). +intros p1; intros e2; elim e2; simpl; (try (intros; discriminate)). +intros p2; generalize (positive_eq_correct p1 p2); case (positive_eq p1 p2); + (try (intros; discriminate)); intros H; rewrite H; auto. +intros 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. +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 + | _, _ => PEadd e1 e2 + end. + +Theorem NPEadd_correct: + forall l e1 e2, NPEeval l (NPEadd e1 e2) == NPEeval l (PEadd e1 e2). +Proof. +intros l e1 e2. +destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; + try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; + try rewrite (morph0 CRmorph) in |- *; try ring. +apply (morph_add CRmorph). +Qed. + +(* mul *) +Definition NPEmul x y := + 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 + | _, _ => PEmul x y + end. + +Theorem NPEmul_correct : forall l e1 e2, + NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2). +intros l e1 e2. +destruct e1; destruct e2; simpl in |- *; try reflexivity; + repeat apply ceqb_rect; + try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; + try rewrite (morph0 CRmorph) in |- *; + try rewrite (morph1 CRmorph) in |- *; + try ring. +apply (morph_mul 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 + | _, _ => PEsub e1 e2 + end. + +Theorem NPEsub_correct: + forall l e1 e2, NPEeval l (NPEsub e1 e2) == NPEeval l (PEsub e1 e2). +intros l e1 e2. +destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; + try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; + try rewrite (morph0 CRmorph) in |- *; try reflexivity; + try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r). +apply (morph_sub CRmorph). +Qed. + +(* opp *) +Definition NPEopp e1 := + match e1 with PEc c1 => PEc (copp c1) | _ => PEopp e1 end. + +Theorem NPEopp_correct: + forall l e1, NPEeval l (NPEopp e1) == NPEeval l (PEopp e1). +intros l e1; case e1; simpl; auto. +intros; apply (morph_opp CRmorph). +Qed. + +(* simplification *) +Fixpoint PExpr_simp (e : PExpr C) : PExpr C := + match e with + 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) + | _ => e + end. + +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. +Qed. + + +(**************************************************************************** + + Datastructure + + ***************************************************************************) + +(* The input: syntax of a field expression *) + +Inductive FExpr : Type := + FEc: C -> FExpr + | FEX: positive -> FExpr + | FEadd: FExpr -> FExpr -> FExpr + | FEsub: FExpr -> FExpr -> FExpr + | FEmul: FExpr -> FExpr -> FExpr + | FEopp: FExpr -> FExpr + | FEinv: FExpr -> FExpr + | FEdiv: FExpr -> FExpr -> FExpr . + +Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := + match pe with + | FEc c => phi c + | FEX x => BinList.nth 0 x l + | FEadd x y => FEeval l x + FEeval l y + | FEsub x y => FEeval l x - FEeval l y + | FEmul x y => FEeval l x * FEeval l y + | FEopp x => - FEeval l x + | FEinv x => / FEeval l x + | FEdiv x y => FEeval l x / FEeval l y + end. + +(* The result of the normalisation *) + +Record linear : Type := mk_linear { + num : PExpr C; + denum : PExpr C; + condition : list (PExpr C) }. + +(*************************************************************************** + + Semantics and properties of side condition + + ***************************************************************************) + +Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop := + match le with + | nil => True + | e1 :: nil => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO + | e1 :: l1 => ~ req (PEeval rO radd rmul rsub ropp phi l e1) 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. +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. +Qed. + +Theorem PCond_app_inv_l: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l1. +intros l l1 l2; elim l1; simpl app in |- *. + simpl in |- *; auto. + destruct l0; simpl in *. + destruct l2; firstorder. + firstorder. +Qed. + +Theorem PCond_app_inv_r: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l2. +intros l l1 l2; elim l1; simpl app; auto. +intros a l0 H H0; apply H; apply PCond_cons_inv_r with ( 1 := H0 ). +Qed. + +(* An unsatisfiable condition: issued when a division by zero is detected *) +Definition absurd_PCond := cons (PEc cO) nil. + +Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond. +unfold absurd_PCond in |- *; simpl in |- *. +red in |- *; intros. +apply H. +apply (morph0 CRmorph). +Qed. + +(*************************************************************************** + + Normalisation + + ***************************************************************************) + + +Fixpoint isIn (e1 e2: PExpr C) {struct e2}: option (PExpr C) := + match e2 with + | PEmul e3 e4 => + match isIn e1 e3 with + Some e5 => Some (NPEmul e5 e4) + | None => match isIn e1 e4 with + | Some e5 => Some (NPEmul e3 e5) + | None => None + end + end + | _ => + if PExpr_eq e1 e2 then Some (PEc cI) else None + end. + +Theorem isIn_correct: forall l e1 e2, + match isIn e1 e2 with + (Some e3) => NPEeval l e2 == NPEeval l (NPEmul e1 e3) + | _ => True + end. +Proof. +intros l e1 e2; elim e2; simpl; auto. + intros c; + generalize (PExpr_eq_semi_correct l e1 (PEc c)); + case (PExpr_eq e1 (PEc c)); simpl; auto; intros H. + rewrite NPEmul_correct; simpl; auto. + rewrite H; auto; simpl. + rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. + intros p; + generalize (PExpr_eq_semi_correct l e1 (PEX C p)); + case (PExpr_eq e1 (PEX C p)); simpl; auto; intros H. + rewrite NPEmul_correct; simpl; auto. + rewrite H; auto; simpl. + rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. + intros p Hrec p1 Hrec1. + generalize (PExpr_eq_semi_correct l e1 (PEadd p p1)); + case (PExpr_eq e1 (PEadd p p1)); simpl; auto; intros H. + rewrite NPEmul_correct; simpl; auto. + rewrite H; auto; simpl. + rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. + intros p Hrec p1 Hrec1. + generalize (PExpr_eq_semi_correct l e1 (PEsub p p1)); + case (PExpr_eq e1 (PEsub p p1)); simpl; auto; intros H. + rewrite NPEmul_correct; simpl; auto. + rewrite H; auto; simpl. + rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. + intros p; case (isIn e1 p). + intros p2 Hrec p1 Hrec1. + rewrite Hrec; auto; simpl. + repeat (rewrite NPEmul_correct; simpl; auto). + intros _ p1; case (isIn e1 p1); auto. + intros p2 H; rewrite H. + repeat (rewrite NPEmul_correct; simpl; auto). + ring. + intros p; + generalize (PExpr_eq_semi_correct l e1 (PEopp p)); + case (PExpr_eq e1 (PEopp p)); simpl; auto; intros H. + rewrite NPEmul_correct; simpl; auto. + rewrite H; auto; simpl. + rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. +Qed. + +Record rsplit : Type := mk_rsplit { + rsplit_left : PExpr C; + rsplit_common : PExpr C; + rsplit_right : PExpr C}. + +(* Stupid name clash *) +Let left := rsplit_left. +Let right := rsplit_right. +Let common := rsplit_common. + +Fixpoint split (e1 e2: PExpr C) {struct e1}: rsplit := + match e1 with + | PEmul e3 e4 => + let r1 := split e3 e2 in + let r2 := split e4 (right r1) in + mk_rsplit (NPEmul (left r1) (left r2)) + (NPEmul (common r1) (common r2)) + (right r2) + | _ => + match isIn e1 e2 with + Some e3 => mk_rsplit (PEc cI) e1 e3 + | None => mk_rsplit e1 (PEc cI) e2 + end + end. + +Theorem split_correct: forall l e1 e2, + NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2)) + (common (split e1 e2))) +/\ + NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2)) + (common (split e1 e2))). +Proof. +intros l e1; elim e1; simpl; auto. + intros c e2; generalize (isIn_correct l (PEc c) e2); + case (isIn (PEc c) e2); auto; intros p; + [intros Hp1; rewrite Hp1 | idtac]; + simpl left; simpl common; simpl right; auto; + repeat rewrite NPEmul_correct; simpl; split; + try rewrite (morph1 CRmorph); ring. + intros p e2; generalize (isIn_correct l (PEX C p) e2); + case (isIn (PEX C p) e2); auto; intros p1; + [intros Hp1; rewrite Hp1 | idtac]; + simpl left; simpl common; simpl right; auto; + repeat rewrite NPEmul_correct; simpl; split; + try rewrite (morph1 CRmorph); ring. + intros p1 _ p2 _ e2; generalize (isIn_correct l (PEadd p1 p2) e2); + case (isIn (PEadd p1 p2) e2); auto; intros p; + [intros Hp1; rewrite Hp1 | idtac]; + simpl left; simpl common; simpl right; auto; + repeat rewrite NPEmul_correct; simpl; split; + try rewrite (morph1 CRmorph); ring. + intros p1 _ p2 _ e2; generalize (isIn_correct l (PEsub p1 p2) e2); + case (isIn (PEsub p1 p2) e2); auto; intros p; + [intros Hp1; rewrite Hp1 | idtac]; + simpl left; simpl common; simpl right; auto; + repeat rewrite NPEmul_correct; simpl; split; + try rewrite (morph1 CRmorph); ring. + intros p1 Hp1 p2 Hp2 e2. + repeat rewrite NPEmul_correct; simpl; split. + case (Hp1 e2); case (Hp2 (right (split p1 e2))). + intros tmp1 _ tmp2 _; rewrite tmp1; rewrite tmp2. + repeat rewrite NPEmul_correct; simpl. + ring. + case (Hp1 e2); case (Hp2 (right (split p1 e2))). + intros _ tmp1 _ tmp2; rewrite tmp2; + repeat rewrite NPEmul_correct; simpl. + rewrite tmp1. + repeat rewrite NPEmul_correct; simpl. + ring. + intros p _ e2; generalize (isIn_correct l (PEopp p) e2); + case (isIn (PEopp p) e2); auto; intros p1; + [intros Hp1; rewrite Hp1 | idtac]; + simpl left; simpl common; simpl right; auto; + repeat rewrite NPEmul_correct; simpl; split; + try rewrite (morph1 CRmorph); ring. +Qed. + + +Theorem split_correct_l: forall l e1 e2, + NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2)) + (common (split e1 e2))). +Proof. +intros l e1 e2; case (split_correct l e1 e2); auto. +Qed. + +Theorem split_correct_r: forall l e1 e2, + NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2)) + (common (split e1 e2))). +Proof. +intros l e1 e2; case (split_correct l e1 e2); auto. +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 + | 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) + + | 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) + | FEmul e1 e2 => + let x := Fnorm e1 in + let y := Fnorm e2 in + mk_linear (NPEmul (num x) (num y)) + (NPEmul (denum x) (denum y)) + (condition x ++ condition y) + | FEopp e1 => + let x := Fnorm e1 in + mk_linear (NPEopp (num x)) (denum x) (condition x) + | FEinv e1 => + let x := Fnorm e1 in + mk_linear (denum x) (num x) (num x :: condition x) + | FEdiv e1 e2 => + let x := Fnorm e1 in + let y := Fnorm e2 in + mk_linear (NPEmul (num x) (denum y)) + (NPEmul (denum x) (num y)) + (num y :: condition x ++ condition y) + end. + + +(* Example *) +(* +Eval compute + in (Fnorm + (FEdiv + (FEc cI) + (FEadd (FEinv (FEX xH%positive)) (FEinv (FEX (xO xH)%positive))))). +*) + +Theorem Pcond_Fnorm: + forall l e, + PCond l (condition (Fnorm e)) -> ~ NPEeval l (denum (Fnorm e)) == 0. +intros l e; elim e. + simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO. + simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO. + intros e1 Hrec1 e2 Hrec2 Hcond. + simpl condition in Hcond. + simpl denum in |- *. + rewrite NPEmul_correct in |- *. + simpl in |- *. + 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 in |- *. + rewrite NPEmul_correct in |- *. + simpl in |- *. + 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 in |- *. + rewrite NPEmul_correct in |- *. + simpl in |- *. + apply field_is_integral_domain. + apply Hrec1. + apply PCond_app_inv_l with (1 := Hcond). + apply Hrec2. + apply PCond_app_inv_r with (1 := Hcond). + intros e1 Hrec1 Hcond. + simpl condition in Hcond. + simpl denum in |- *. + auto. + intros e1 Hrec1 Hcond. + simpl condition in Hcond. + simpl denum in |- *. + apply PCond_cons_inv_l with (1:=Hcond). + intros e1 Hrec1 e2 Hrec2 Hcond. + simpl condition in Hcond. + simpl denum in |- *. + rewrite NPEmul_correct in |- *. + simpl in |- *. + apply field_is_integral_domain. + apply Hrec1. + specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1. + apply PCond_app_inv_l with (1 := Hcond1). + apply PCond_cons_inv_l with (1:=Hcond). +Qed. +Hint Resolve Pcond_Fnorm. + + +(*************************************************************************** + + Main theorem + + ***************************************************************************) + +Theorem Fnorm_FEeval_PEeval: + forall 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. +apply rdiv4; 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. +apply rdiv7; auto. +apply PCond_cons_inv_l with ( 1 := HH ). +Qed. + +Theorem Fnorm_crossproduct: + forall 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)) -> + PCond l (condition nfe1 ++ condition nfe2) -> + FEeval l fe1 == FEeval l fe2. +intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2. +rewrite Fnorm_FEeval_PEeval in |- *. + apply PCond_app_inv_l with (1 := Hcond). + rewrite Fnorm_FEeval_PEeval in |- *. + 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). +Qed. + +(* Correctness lemmas of reflexive tactics *) + +Theorem Fnorm_correct: + forall l fe, + Peq ceqb (Nnorm (num (Fnorm fe))) (Pc cO) = true -> + PCond l (condition (Fnorm fe)) -> FEeval l fe == 0. +intros l fe H H1; + apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1). +apply rdiv8; auto. +transitivity (NPEeval l (PEc cO)); auto. +apply (ring_correct Rsth Reqe ARth CRmorph); auto. +simpl; apply (morph0 CRmorph); auto. +Qed. + +(* simplify a field expression into a fraction *) +(* TODO: simplify when den is constant... *) +Definition display_linear l num den := + NPphi_dev l num / NPphi_dev l den. + +Theorem Pphi_dev_div_ok: + forall l fe nfe, + Fnorm fe = nfe -> + PCond l (condition nfe) -> + FEeval l fe == display_linear l (Nnorm (num nfe)) (Nnorm (denum nfe)). +Proof. + intros l fe nfe eq_nfe H; subst nfe. + apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H). + unfold display_linear; apply SRdiv_ext; + apply (Pphi_dev_ok Rsth Reqe ARth CRmorph); reflexivity. +Qed. + +(* solving a field equation *) +Theorem Field_correct : + forall l fe1 fe2, + forall nfe1, Fnorm fe1 = nfe1 -> + forall nfe2, Fnorm fe2 = nfe2 -> + Peq ceqb (Nnorm (PEmul (num nfe1) (denum nfe2))) + (Nnorm (PEmul (num nfe2) (denum nfe1))) = true -> + PCond l (condition nfe1 ++ condition nfe2) -> + FEeval l fe1 == FEeval l fe2. +Proof. +intros l fe1 fe2 nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2. +apply Fnorm_crossproduct; trivial. +apply (ring_correct Rsth Reqe ARth CRmorph); trivial. +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 (PEmul (num nfe1) (denum nfe2))) == + NPphi_dev l (Nnorm (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. +rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *. +rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *. +trivial. +Qed. + +Theorem Field_simplify_eq_correct : + forall l fe1 fe2, + forall nfe1, Fnorm fe1 = nfe1 -> + forall nfe2, Fnorm fe2 = nfe2 -> + forall den, split (denum nfe1) (denum nfe2) = den -> + NPphi_dev l (Nnorm (PEmul (num nfe1) (right den))) == + NPphi_dev l (Nnorm (PEmul (num nfe2) (left den))) -> + PCond l (condition nfe1 ++ condition nfe2) -> + FEeval l fe1 == FEeval l fe2. +Proof. +intros l fe1 fe2 nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; + subst nfe1 nfe2 den. +apply Fnorm_crossproduct; trivial. +simpl in |- *. +elim (split_correct l (denum (Fnorm fe1)) (denum (Fnorm fe2))); intros. +rewrite H in |- *. +rewrite H0 in |- *. +clear H H0. +rewrite NPEmul_correct in |- *. +rewrite NPEmul_correct in |- *. +simpl in |- *. +repeat rewrite (ARmul_assoc ARth) in |- *. +rewrite <- (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in Hcrossprod. +rewrite <- (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in Hcrossprod. +simpl in Hcrossprod. +rewrite Hcrossprod in |- *. +reflexivity. +Qed. + +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. + +Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) := + match l with + | nil => m + | cons a l1 => Fcons a (Fapp l1 m) + end. + +Lemma fcons_correct : forall l l1, + PCond l (Fapp l1 nil) -> PCond l l1. +induction l1; simpl in |- *; intros. + trivial. + elim PCond_fcons_inv with (1 := H); intros. + destruct l1; auto. +Qed. + +End Fcons_impl. + +Section Fcons_simpl. + +(* Some general simpifications of the condition: eliminate duplicates, + split multiplications *) + +Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := + match l with + nil => cons e nil + | cons a l1 => if PExpr_eq e a then l else cons a (Fcons e l1) + end. + +Theorem PFcons_fcons_inv: + forall l a l1, PCond l (Fcons a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. +intros l a l1; elim l1; simpl Fcons; auto. +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. +Qed. + +(* equality of normal forms rather than syntactic equality *) +Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := + match l with + nil => cons e nil + | cons a l1 => + if Peq ceqb (Nnorm e) (Nnorm a) then l else cons a (Fcons0 e l1) + end. + +Theorem PFcons0_fcons_inv: + forall l a l1, PCond l (Fcons0 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. +intros l a l1; elim l1; simpl Fcons0; auto. +simpl; auto. +intros a0 l0. +generalize (ring_correct Rsth Reqe ARth CRmorph l a a0); + case (Peq ceqb (Nnorm a) (Nnorm 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. +Qed. + +Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := + match e with + PEmul e1 e2 => Fcons00 e1 (Fcons00 e2 l) + | _ => Fcons0 e l + 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 in |- *. + apply field_is_integral_domain; trivial. +Qed. + + +Definition Pcond_simpl_gen := + fcons_correct _ 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. + +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). +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 in |- *; intro. +absurd (false = true); auto; 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) + | PEopp e => if ceqb (copp cI) cO then absurd_PCond else Fcons1 e l + | PEc c => if ceqb c cO then absurd_PCond else l + | _ => Fcons0 e l + 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 in |- *; intros c l1. + apply ceqb_rect_complete; intros. + elim (@absurd_PCond_bottom l H0). + split; trivial. + rewrite <- (morph0 CRmorph) in |- *; trivial. + intros p H p0 H0 l1 H1. + simpl in H1. + case (H _ H1); intros H2 H3. + case (H0 _ H3); intros H4 H5; split; auto. + simpl in |- *. + apply field_is_integral_domain; trivial. + simpl in |- *; intros p H l1. + apply ceqb_rect_complete; intros. + 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. +Qed. + +Definition Fcons2 e l := Fcons1 (PExpr_simp e) l. + +Theorem PFcons2_fcons_inv: + forall l a l1, PCond l (Fcons2 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. +unfold Fcons2 in |- *; intros l a l1 H; split; + case (PFcons1_fcons_inv l (PExpr_simp a) l1); auto. +intros H1 H2 H3; case H1. +transitivity (NPEeval l a); trivial. +apply PExpr_simp_correct. +Qed. + +Definition Pcond_simpl_complete := + fcons_correct _ PFcons2_fcons_inv. + +End Fcons_simpl. + +Let Mpc := MPcond_map cO cI cadd cmul csub copp ceqb. +Let Mp := MPcond_dev rO rI radd rmul req cO cI ceqb phi. +Let Subst := PNSubstL cO cI cadd cmul ceqb. + +(* simplification + rewriting *) +Theorem Field_subst_correct : +forall l ul fe m n, + PCond l (Fapp Fcons00 (condition (Fnorm fe)) nil) -> + Mp (Mpc ul) l -> + Peq ceqb (Subst (Nnorm (num (Fnorm fe))) (Mpc ul) m n) (Pc cO) = true -> + FEeval l fe == 0. +intros l ul fe m n H H1 H2. +assert (H3 := (Pcond_simpl_gen _ _ H)). +apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe + (Pcond_simpl_gen _ _ H)). +apply rdiv8; auto. +rewrite (PNSubstL_dev_ok Rsth Reqe ARth CRmorph m n + _ (num (Fnorm fe)) l H1). +rewrite <-(Ring_polynom.Pphi_Pphi_dev Rsth Reqe ARth CRmorph). +rewrite (fun x => Peq_ok Rsth Reqe CRmorph x (Pc cO)); auto. +simpl; apply (morph0 CRmorph); auto. +Qed. + + +End AlmostField. + +Section FieldAndSemiField. + + Record field_theory : Prop := mk_field { + F_R : ring_theory rO rI radd rmul rsub ropp req; + F_1_neq_0 : ~ 1 == 0; + Fdiv_def : forall p q, p / q == p * / q; + Finv_l : forall p, ~ p == 0 -> / p * p == 1 + }. + + Definition F2AF f := + mk_afield + (Rth_ARth Rsth Reqe f.(F_R)) f.(F_1_neq_0) f.(Fdiv_def) f.(Finv_l). + + Record semi_field_theory : Prop := mk_sfield { + SF_SR : semi_ring_theory rO rI radd rmul req; + SF_1_neq_0 : ~ 1 == 0; + SFdiv_def : forall p q, p / q == p * / q; + SFinv_l : forall p, ~ p == 0 -> / p * p == 1 + }. + +End FieldAndSemiField. + +End MakeFieldPol. + + Definition SF2AF R (rO rI:R) radd rmul rdiv rinv req Rsth + (sf:semi_field_theory rO rI radd rmul rdiv rinv req) := + mk_afield _ _ + (SRth_ARth Rsth sf.(SF_SR)) + sf.(SF_1_neq_0) + sf.(SFdiv_def) + sf.(SFinv_l). + + +Section Complete. + 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" := (ropp x). + Notation "x / y " := (rdiv x y). Notation "/ x" := (rinv x). + Notation "x == y" := (req x y) (at level 70, no associativity). + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid3. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed. + +Section AlmostField. + + Variable AFth : almost_field_theory rO rI radd rmul rsub ropp rdiv rinv req. + 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). + +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, + gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y. +intros p x y. +elim p using Pind; simpl in |- *; intros. + apply S_inj; trivial. + apply H. + apply S_inj. + repeat rewrite (ARadd_assoc ARth) in |- *. + rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *; trivial. +Qed. + +Lemma gen_phiPOS_inj : forall x y, + gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y -> + x = y. +intros x y. +repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *. +ElimPcompare x y; intro. + intros. + apply Pcompare_Eq_eq; trivial. + intro. + elim gen_phiPOS_not_0 with (y - x)%positive. + apply add_inj_r with x. + symmetry in |- *. + rewrite (ARadd_0_r Rsth ARth) in |- *. + rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. + rewrite Pplus_minus in |- *; trivial. + change Eq with (CompOpp Eq) in |- *. + rewrite <- Pcompare_antisym in |- *; trivial. + rewrite H in |- *; trivial. + intro. + elim gen_phiPOS_not_0 with (x - y)%positive. + apply add_inj_r with y. + rewrite (ARadd_0_r Rsth ARth) in |- *. + rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. + rewrite Pplus_minus in |- *; trivial. +Qed. + + +Lemma gen_phiN_inj : forall x y, + gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> + x = y. +destruct x; destruct y; simpl in |- *; intros; trivial. + elim gen_phiPOS_not_0 with p. + symmetry in |- *. + rewrite (same_gen Rsth Reqe ARth) in |- *; trivial. + elim gen_phiPOS_not_0 with p. + rewrite (same_gen Rsth Reqe ARth) in |- *; trivial. + rewrite gen_phiPOS_inj with (1 := H) in |- *; trivial. +Qed. + +Lemma gen_phiN_complete : forall x y, + gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> + Neq_bool x y = true. +intros. + replace y with x. + unfold Neq_bool in |- *. + rewrite Ncompare_refl in |- *; trivial. + apply gen_phiN_inj; trivial. +Qed. + +End AlmostField. + +Section Field. + + Variable Fth : field_theory rO rI radd rmul rsub ropp rdiv rinv req. + Let Rth := Fth.(F_R). + Let rI_neq_rO := Fth.(F_1_neq_0). + Let rdiv_def := Fth.(Fdiv_def). + Let rinv_l := Fth.(Finv_l). + 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. +intros. +transitivity (x + (1 + - (1))). + rewrite (Ropp_def Rth) in |- *. + symmetry in |- *. + apply (ARadd_0_r Rsth ARth). + transitivity (y + (1 + - (1))). + repeat rewrite <- (ARplus_assoc ARth) in |- *. + repeat rewrite (ARadd_assoc ARth) in |- *. + apply (Radd_ext Reqe). + repeat rewrite <- (ARadd_comm ARth 1) in |- *. + trivial. + reflexivity. + rewrite (Ropp_def Rth) in |- *. + apply (ARadd_0_r Rsth ARth). +Qed. + + + 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, + ~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y. +red in |- *; intros. +apply gen_phiPOS_not_0 with (y + x)%positive. +rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. +transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y). + apply (Radd_ext Reqe); trivial. + reflexivity. + rewrite (same_gen Rsth Reqe ARth) in |- *. + rewrite (same_gen Rsth Reqe ARth) in |- *. + trivial. + apply (Ropp_def Rth). +Qed. + +Lemma gen_phiZ_inj : forall x y, + gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> + x = y. +destruct x; destruct y; simpl in |- *; intros. + trivial. + elim gen_phiPOS_not_0 with p. + rewrite (same_gen Rsth Reqe ARth) in |- *. + symmetry in |- *; trivial. + elim gen_phiPOS_not_0 with p. + rewrite (same_gen Rsth Reqe ARth) in |- *. + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *. + rewrite <- H in |- *. + apply (ARopp_zero Rsth Reqe ARth). + elim gen_phiPOS_not_0 with p. + rewrite (same_gen Rsth Reqe ARth) in |- *. + trivial. + rewrite gen_phiPOS_inject with (1 := H) in |- *; trivial. + elim gen_phiPOS_discr_sgn with (1 := H). + elim gen_phiPOS_not_0 with p. + rewrite (same_gen Rsth Reqe ARth) in |- *. + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *. + rewrite H in |- *. + apply (ARopp_zero Rsth Reqe ARth). + elim gen_phiPOS_discr_sgn with p0 p. + symmetry in |- *; trivial. + replace p0 with p; trivial. + apply gen_phiPOS_inject. + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *. + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)) in |- *. + rewrite H in |- *; trivial. + reflexivity. +Qed. + +Lemma gen_phiZ_complete : forall x y, + gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> + Zeq_bool x y = true. +intros. + replace y with x. + unfold Zeq_bool in |- *. + rewrite Zcompare_refl in |- *; trivial. + apply gen_phiZ_inj; trivial. +Qed. + +End Field. + +End Complete. + diff --git a/contrib/setoid_ring/ZRing_th.v b/contrib/setoid_ring/InitialRing.v index 9060428b..7df68cc0 100644 --- a/contrib/setoid_ring/ZRing_th.v +++ b/contrib/setoid_ring/InitialRing.v @@ -1,11 +1,21 @@ -Require Import Ring_th. -Require Import Pol. -Require Import Ring_tac. +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + Require Import ZArith_base. Require Import BinInt. Require Import BinNat. Require Import Setoid. - Set Implicit Arguments. +Require Import Ring_theory. +Require Import Ring_tac. +Require Import Ring_polynom. +Set Implicit Arguments. + +Import RingSyntax. (** Z is a ring and a setoid*) @@ -187,7 +197,7 @@ Section ZMORPHISM. replace Eq with (CompOpp Eq);trivial. rewrite <- Pcompare_antisym;simpl. rewrite match_compOpp. - rewrite (Radd_sym Rth). + rewrite (Radd_comm Rth). apply gen_phiZ1_add_pos_neg. rewrite (ARgen_phiPOS_add ARth); norm. Qed. @@ -255,6 +265,14 @@ Lemma Neq_bool_ok : forall x y, Neq_bool x y = true -> x = y. rewrite H;trivial. Qed. +Lemma Neq_bool_complete : forall x y, Neq_bool x y = true -> x = y. + Proof. + intros x y;unfold Neq_bool. + assert (H:=Ncompare_Eq_eq x y); + destruct (Ncompare x y);intros;try discriminate. + rewrite H;trivial. + Qed. + (**Same as above : definition of two,extensionaly equal, generic morphisms *) (**from N to any semi-ring*) Section NMORPHISM. @@ -326,271 +344,9 @@ Section NMORPHISM. Qed. End NMORPHISM. -(* -Section NNMORPHISM. -Variable R : Type. - Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). - Variable req : R -> R -> Prop. - Notation "0" := rO. Notation "1" := rI. - Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). - Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). - Notation "x == y" := (req x y). - Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid5. - Ltac rrefl := gen_reflexivity Rsth. - Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext5. exact Reqe.(Radd_ext). Qed. - Add Morphism rmul : rmul_ext5. exact Reqe.(Rmul_ext). Qed. - Add Morphism ropp : ropp_ext5. exact Reqe.(Ropp_ext). Qed. - - Lemma SReqe : sring_eq_ext radd rmul req. - case Reqe; constructor; trivial. - Qed. - - Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. - Add Morphism rsub : rsub_ext6. exact (ARsub_ext Rsth Reqe ARth). Qed. - Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. - Ltac add_push := gen_add_push radd Rsth Reqe ARth. - - Lemma SRth : semi_ring_theory 0 1 radd rmul req. - case ARth; constructor; trivial. - Qed. - - Definition NN := prod N N. - Definition gen_phiNN (x:NN) := - rsub (gen_phiN rO rI radd rmul (fst x)) (gen_phiN rO rI radd rmul (snd x)). - Notation "[ x ]" := (gen_phiNN x). - - Definition NNadd (x y : NN) : NN := - (fst x + fst y, snd x + snd y)%N. - Definition NNmul (x y : NN) : NN := - (fst x * fst y + snd x * snd y, fst y * snd x + fst x * snd y)%N. - Definition NNopp (x:NN) : NN := (snd x, fst x)%N. - Definition NNsub (x y:NN) : NN := (fst x + snd y, fst y + snd x)%N. - - - Lemma gen_phiNN_add : forall x y, [NNadd x y] == [x] + [y]. - Proof. -intros. -unfold NNadd, gen_phiNN in |- *; simpl in |- *. -repeat rewrite (gen_phiN_add Rsth SReqe SRth). -norm. -add_push (- gen_phiN 0 1 radd rmul (snd x)). -rrefl. -Qed. - - Hypothesis ropp_involutive : forall x, - - x == x. - - - Lemma gen_phiNN_mult : forall x y, [NNmul x y] == [x] * [y]. - Proof. -intros. -unfold NNmul, gen_phiNN in |- *; simpl in |- *. -repeat rewrite (gen_phiN_add Rsth SReqe SRth). -repeat rewrite (gen_phiN_mult Rsth SReqe SRth). -norm. -rewrite ropp_involutive. -add_push (- (gen_phiN 0 1 radd rmul (fst y) * gen_phiN 0 1 radd rmul (snd x))). -add_push ( gen_phiN 0 1 radd rmul (snd x) * gen_phiN 0 1 radd rmul (snd y)). -rewrite (ARmul_sym ARth (gen_phiN 0 1 radd rmul (fst y)) - (gen_phiN 0 1 radd rmul (snd x))). -rrefl. -Qed. - - Lemma gen_phiNN_sub : forall x y, [NNsub x y] == [x] - [y]. -intros. -unfold NNsub, gen_phiNN; simpl. -repeat rewrite (gen_phiN_add Rsth SReqe SRth). -repeat rewrite (ARsub_def ARth). -repeat rewrite (ARopp_add ARth). -repeat rewrite (ARadd_assoc ARth). -rewrite ropp_involutive. -add_push (- gen_phiN 0 1 radd rmul (fst y)). -add_push ( - gen_phiN 0 1 radd rmul (snd x)). -rrefl. -Qed. - - -Definition NNeqbool (x y: NN) := - andb (Neq_bool (fst x) (fst y)) (Neq_bool (snd x) (snd y)). - -Lemma NNeqbool_ok0 : forall x y, - NNeqbool x y = true -> x = y. -unfold NNeqbool in |- *. -intros. -assert (Neq_bool (fst x) (fst y) = true). - generalize H. - case (Neq_bool (fst x) (fst y)); simpl in |- *; trivial. - assert (Neq_bool (snd x) (snd y) = true). - rewrite H0 in H; simpl in |- *; trivial. - generalize H0 H1. - destruct x; destruct y; simpl in |- *. - intros. - replace n with n1. - replace n2 with n0; trivial. - apply Neq_bool_ok; trivial. - symmetry in |- *. - apply Neq_bool_ok; trivial. -Qed. - - -(*gen_phiN satisfies morphism specifications*) - Lemma gen_phiNN_morph : ring_morph 0 1 radd rmul rsub ropp req - (N0,N0) (Npos xH,N0) NNadd NNmul NNsub NNopp NNeqbool gen_phiNN. - Proof. - constructor;intros;simpl; try rrefl. - apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult. - rewrite (Neq_bool_ok x y);trivial. rrefl. - Qed. - -End NNMORPHISM. - -Section NSTARMORPHISM. -Variable R : Type. - Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). - Variable req : R -> R -> Prop. - Notation "0" := rO. Notation "1" := rI. - Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). - Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). - Notation "x == y" := (req x y). - Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid3. - Ltac rrefl := gen_reflexivity Rsth. - Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext3. exact Reqe.(Radd_ext). Qed. - Add Morphism rmul : rmul_ext3. exact Reqe.(Rmul_ext). Qed. - Add Morphism ropp : ropp_ext3. exact Reqe.(Ropp_ext). Qed. - - Lemma SReqe : sring_eq_ext radd rmul req. - case Reqe; constructor; trivial. - Qed. - - Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. - Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed. - Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. - Ltac add_push := gen_add_push radd Rsth Reqe ARth. - - Lemma SRth : semi_ring_theory 0 1 radd rmul req. - case ARth; constructor; trivial. - Qed. - - Inductive Nword : Set := - Nlast (p:positive) - | Ndigit (n:N) (w:Nword). - - Fixpoint opp_iter (n:nat) (t:R) {struct n} : R := - match n with - O => t - | S k => ropp (opp_iter k t) - end. - - Fixpoint gen_phiNword (x:Nword) (n:nat) {struct x} : R := - match x with - Nlast p => opp_iter n (gen_phi_pos p) - | Ndigit N0 w => gen_phiNword w (S n) - | Ndigit m w => radd (opp_iter n (gen_phiN m)) (gen_phiNword w (S n)) - end. - Notation "[ x ]" := (gen_phiNword x). - - Fixpoint Nwadd (x y : Nword) {struct x} : Nword := - match x, y with - Nlast p1, Nlast p2 => Nlast (p1+p2)%positive - | Nlast p1, Ndigit n w => Ndigit (Npos p1 + n)%N w - | Ndigit n w, Nlast p1 => Ndigit (n + Npos p1)%N w - | Ndigit n1 w1, Ndigit n2 w2 => Ndigit (n1+n2)%N (Nwadd w1 w2) - end. - Fixpoint Nwmulp (x:positive) (y:Nword) {struct y} : Nword := - match y with - Nlast p => Nlast (x*p)%positive - | Ndigit n w => Ndigit (Npos x * n)%N (Nwmulp x w) - end. - Definition Nwmul (x y : Nword) {struct x} : Nword := - match x with - Nlast k => Nmulp k y - | Ndigit N0 w => Ndigit N0 (Nwmul w y) - | Ndigit (Npos k) w => - Nwadd (Nwmulp k y) (Ndigit N0 (Nwmul w y)) - end. - - Definition Nwopp (x:Nword) : Nword := Ndigit N0 x. - Definition Nwsub (x y:NN) : NN := (Nwadd x (Ndigit N0 y)). - - - Lemma gen_phiNN_add : forall x y, [NNadd x y] == [x] + [y]. - Proof. -intros. -unfold NNadd, gen_phiNN in |- *; simpl in |- *. -repeat rewrite (gen_phiN_add Rsth SReqe SRth). -norm. -add_push (- gen_phiN 0 1 radd rmul (snd x)). -rrefl. -Qed. - - Lemma gen_phiNN_mult : forall x y, [NNmul x y] == [x] * [y]. - Proof. -intros. -unfold NNmul, gen_phiNN in |- *; simpl in |- *. -repeat rewrite (gen_phiN_add Rsth SReqe SRth). -repeat rewrite (gen_phiN_mult Rsth SReqe SRth). -norm. -rewrite ropp_involutive. -add_push (- (gen_phiN 0 1 radd rmul (fst y) * gen_phiN 0 1 radd rmul (snd x))). -add_push ( gen_phiN 0 1 radd rmul (snd x) * gen_phiN 0 1 radd rmul (snd y)). -rewrite (ARmul_sym ARth (gen_phiN 0 1 radd rmul (fst y)) - (gen_phiN 0 1 radd rmul (snd x))). -rrefl. -Qed. - Lemma gen_phiNN_sub : forall x y, [NNsub x y] == [x] - [y]. -intros. -unfold NNsub, gen_phiNN; simpl. -repeat rewrite (gen_phiN_add Rsth SReqe SRth). -repeat rewrite (ARsub_def ARth). -repeat rewrite (ARopp_add ARth). -repeat rewrite (ARadd_assoc ARth). -rewrite ropp_involutive. -add_push (- gen_phiN 0 1 radd rmul (fst y)). -add_push ( - gen_phiN 0 1 radd rmul (snd x)). -rrefl. -Qed. - - -Definition NNeqbool (x y: NN) := - andb (Neq_bool (fst x) (fst y)) (Neq_bool (snd x) (snd y)). - -Lemma NNeqbool_ok0 : forall x y, - NNeqbool x y = true -> x = y. -unfold NNeqbool in |- *. -intros. -assert (Neq_bool (fst x) (fst y) = true). - generalize H. - case (Neq_bool (fst x) (fst y)); simpl in |- *; trivial. - assert (Neq_bool (snd x) (snd y) = true). - rewrite H0 in H; simpl in |- *; trivial. - generalize H0 H1. - destruct x; destruct y; simpl in |- *. - intros. - replace n with n1. - replace n2 with n0; trivial. - apply Neq_bool_ok; trivial. - symmetry in |- *. - apply Neq_bool_ok; trivial. -Qed. - - -(*gen_phiN satisfies morphism specifications*) - Lemma gen_phiNN_morph : ring_morph 0 1 radd rmul rsub ropp req - (N0,N0) (Npos xH,N0) NNadd NNmul NNsub NNopp NNeqbool gen_phiNN. - Proof. - constructor;intros;simpl; try rrefl. - apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult. - rewrite (Neq_bool_ok x y);trivial. rrefl. - Qed. - -End NSTARMORPHISM. -*) - - (* syntaxification of constants in an abstract ring *) + (* syntaxification of constants in an abstract ring: + the inverse of gen_phiPOS *) Ltac inv_gen_phi_pos rI add mul t := let rec inv_cst t := match t with @@ -600,7 +356,7 @@ End NSTARMORPHISM. | (mul (add rI rI) ?p) => (* 2p *) match inv_cst p with NotConstant => NotConstant - | 1%positive => NotConstant + | 1%positive => NotConstant (* 2*1 is not convertible to 2 *) | ?p => constr:(xO p) end | (add rI (mul (add rI rI) ?p)) => (* 1+2p *) @@ -613,6 +369,7 @@ End NSTARMORPHISM. end in inv_cst t. +(* The inverse of gen_phiN *) Ltac inv_gen_phiN rO rI add mul t := match t with rO => constr:0%N @@ -623,6 +380,7 @@ End NSTARMORPHISM. end end. +(* The inverse of gen_phiZ *) Ltac inv_gen_phiZ rO rI add mul opp t := match t with rO => constr:0%Z @@ -637,6 +395,7 @@ End NSTARMORPHISM. | ?p => constr:(Zpos p) end end. + (* coefs = Z (abstract ring) *) Module Zpol. @@ -646,23 +405,15 @@ Definition ring_gen_correct (Rth_ARth rSet req_th Rth) Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool (@gen_phiZ R rO rI radd rmul ropp) - (@gen_phiZ_morph R rO rI radd rmul rsub ropp req rSet req_th Rth). + (gen_phiZ_morph rSet req_th Rth). Definition ring_rw_gen_correct R rO rI radd rmul rsub ropp req rSet req_th Rth := - @Pphi_dev_ok R rO rI radd rmul rsub ropp req rSet req_th - (Rth_ARth rSet req_th Rth) - Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool - (@gen_phiZ R rO rI radd rmul ropp) - (@gen_phiZ_morph R rO rI radd rmul rsub ropp req rSet req_th Rth). - -Definition ring_rw_gen_correct' - R rO rI radd rmul rsub ropp req rSet req_th Rth := - @Pphi_dev_ok' R rO rI radd rmul rsub ropp req rSet req_th + @Pphi_dev_ok R rO rI radd rmul rsub ropp req rSet req_th (Rth_ARth rSet req_th Rth) Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool (@gen_phiZ R rO rI radd rmul ropp) - (@gen_phiZ_morph R rO rI radd rmul rsub ropp req rSet req_th Rth). + (gen_phiZ_morph rSet req_th Rth). Definition ring_gen_eq_correct R rO rI radd rmul rsub ropp Rth := @ring_gen_correct @@ -672,10 +423,6 @@ Definition ring_rw_gen_eq_correct R rO rI radd rmul rsub ropp Rth := @ring_rw_gen_correct R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth. -Definition ring_rw_gen_eq_correct' R rO rI radd rmul rsub ropp Rth := - @ring_rw_gen_correct' - R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth. - End Zpol. (* coefs = N (abstract semi-ring) *) @@ -688,115 +435,77 @@ Definition ring_gen_correct (SRth_ARth rSet SRth) N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool (@gen_phiN R rO rI radd rmul) - (@gen_phiN_morph R rO rI radd rmul req rSet req_th SRth). + (gen_phiN_morph rSet req_th SRth). Definition ring_rw_gen_correct R rO rI radd rmul req rSet req_th SRth := - @Pphi_dev_ok R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet - (SReqe_Reqe req_th) - (SRth_ARth rSet SRth) - N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool - (@gen_phiN R rO rI radd rmul) - (@gen_phiN_morph R rO rI radd rmul req rSet req_th SRth). - -Definition ring_rw_gen_correct' - R rO rI radd rmul req rSet req_th SRth := - @Pphi_dev_ok' R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet + @Pphi_dev_ok R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet (SReqe_Reqe req_th) (SRth_ARth rSet SRth) N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool (@gen_phiN R rO rI radd rmul) - (@gen_phiN_morph R rO rI radd rmul req rSet req_th SRth). + (gen_phiN_morph rSet req_th SRth). Definition ring_gen_eq_correct R rO rI radd rmul SRth := @ring_gen_correct R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth. -Definition ring_rw_gen_eq_correct R rO rI radd rmul SRth := - @ring_rw_gen_correct - R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth. - Definition ring_rw_gen_eq_correct' R rO rI radd rmul SRth := - @ring_rw_gen_correct' + @ring_rw_gen_correct R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth. End Npol. -(* Z *) - -Ltac isZcst t := - match t with - Z0 => constr:true - | Zpos ?p => isZcst p - | Zneg ?p => isZcst p - | xI ?p => isZcst p - | xO ?p => isZcst p - | xH => constr:true - | _ => constr:false - end. -Ltac Zcst t := - match isZcst t with - true => t - | _ => NotConstant - end. - -Add New Ring Zr : Zth Computational Zeqb_ok Constant Zcst. -(* N *) - -Ltac isNcst t := - match t with - N0 => constr:true - | Npos ?p => isNcst p - | xI ?p => isNcst p - | xO ?p => isNcst p - | xH => constr:true - | _ => constr:false - end. -Ltac Ncst t := - match isNcst t with - true => t - | _ => NotConstant +Ltac coerce_to_almost_ring set ext rspec := + match type of rspec with + | ring_theory _ _ _ _ _ _ _ => constr:(Rth_ARth set ext rspec) + | semi_ring_theory _ _ _ _ _ => constr:(SRth_ARth set rspec) + | almost_ring_theory _ _ _ _ _ _ _ => rspec + | _ => fail 1 "not a valid ring theory" end. -Add New Ring Nr : Nth Computational Neq_bool_ok Constant Ncst. - -(* nat *) - -Ltac isnatcst t := - match t with - O => true - | S ?p => isnatcst p - | _ => false - end. -Ltac natcst t := - match isnatcst t with - true => t - | _ => NotConstant +Ltac coerce_to_ring_ext ext := + match type of ext with + | ring_eq_ext _ _ _ _ => ext + | sring_eq_ext _ _ _ => constr:(SReqe_Reqe ext) + | _ => fail 1 "not a valid ring_eq_ext theory" end. - Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat). - Proof. - constructor. exact plus_0_l. exact plus_comm. exact plus_assoc. - exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc. - exact mult_plus_distr_r. - Qed. - - -Unboxed Fixpoint nateq (n m:nat) {struct m} : bool := - match n, m with - | O, O => true - | S n', S m' => nateq n' m' - | _, _ => false +Ltac abstract_ring_morphism set ext rspec := + match type of rspec with + | ring_theory _ _ _ _ _ _ _ => constr:(gen_phiZ_morph set ext rspec) + | semi_ring_theory _ _ _ _ _ => constr:(gen_phiN_morph set ext rspec) + | almost_ring_theory _ _ _ _ _ _ _ => + fail 1 "an almost ring cannot be abstract" + | _ => fail 1 "bad ring structure" end. -Lemma nateq_ok : forall n m:nat, nateq n m = true -> n = m. -Proof. - simple induction n; simple induction m; simpl; intros; try discriminate. - trivial. - rewrite (H n1 H1). - trivial. -Qed. +Ltac ring_elements set ext rspec rk := + let arth := coerce_to_almost_ring set ext rspec in + let ext_r := coerce_to_ring_ext ext in + let morph := + match rk with + | Abstract => abstract_ring_morphism set ext rspec + | @Computational ?reqb_ok => + match type of arth with + | almost_ring_theory ?rO ?rI ?add ?mul ?sub ?opp _ => + constr:(IDmorph rO rI add mul sub opp set _ reqb_ok) + | _ => fail 2 "ring anomaly" + end + | @Morphism ?m => m + | _ => fail 1 "ill-formed ring kind" + end in + fun f => f arth ext_r morph. + +(* Given a ring structure and the kind of morphism, + returns 2 lemmas (one for ring, and one for ring_simplify). *) + +Ltac ring_lemmas set ext rspec rk := + ring_elements set ext rspec rk + ltac:(fun arth ext_r morph => + let lemma1 := constr:(ring_correct set ext_r arth morph) in + let lemma2 := constr:(Pphi_dev_ok set ext_r arth morph) in + fun f => f arth ext_r morph lemma1 lemma2). -Add New Ring natr : natSRth Computational nateq_ok Constant natcst. diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v new file mode 100644 index 00000000..33e3cb4e --- /dev/null +++ b/contrib/setoid_ring/NArithRing.v @@ -0,0 +1,31 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Export Ring. +Require Import BinPos BinNat. +Import InitialRing. + +Set Implicit Arguments. + +Ltac isNcst t := + let t := eval hnf in t in + match t with + N0 => constr:true + | Npos ?p => isNcst p + | xI ?p => isNcst p + | xO ?p => isNcst p + | xH => constr:true + | _ => constr:false + end. +Ltac Ncst t := + match isNcst t with + true => t + | _ => NotConstant + end. + +Add Ring Nr : Nth (decidable Neq_bool_ok, constants [Ncst]). diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v new file mode 100644 index 00000000..13896123 --- /dev/null +++ b/contrib/setoid_ring/RealField.v @@ -0,0 +1,105 @@ +Require Import Raxioms. +Require Import Rdefinitions. +Require Export Ring Field. + +Open Local Scope R_scope. + +Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)). +Proof. +constructor. + intro; apply Rplus_0_l. + exact Rplus_comm. + symmetry in |- *; apply Rplus_assoc. + intro; apply Rmult_1_l. + exact Rmult_comm. + symmetry in |- *; apply Rmult_assoc. + intros m n p. + rewrite Rmult_comm in |- *. + rewrite (Rmult_comm n p) in |- *. + rewrite (Rmult_comm m p) in |- *. + apply Rmult_plus_distr_l. + reflexivity. + exact Rplus_opp_r. +Qed. + +Lemma Rfield : field_theory 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)). +Proof. +constructor. + exact RTheory. + exact R1_neq_R0. + reflexivity. + exact Rinv_l. +Qed. + +Lemma Rlt_n_Sn : forall x, x < x + 1. +Proof. +intro. +elim archimed with x; intros. +destruct H0. + apply Rlt_trans with (IZR (up x)); trivial. + replace (IZR (up x)) with (x + (IZR (up x) - x))%R. + apply Rplus_lt_compat_l; trivial. + unfold Rminus in |- *. + rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *. + rewrite <- Rplus_assoc in |- *. + rewrite Rplus_opp_r in |- *. + apply Rplus_0_l. + elim H0. + unfold Rminus in |- *. + rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *. + rewrite <- Rplus_assoc in |- *. + rewrite Rplus_opp_r in |- *. + rewrite Rplus_0_l in |- *; trivial. +Qed. + +Notation Rset := (Eqsth R). +Notation Rext := (Eq_ext Rplus Rmult Ropp). + +Lemma Rlt_0_2 : 0 < 2. +apply Rlt_trans with (0 + 1). + apply Rlt_n_Sn. + rewrite Rplus_comm in |- *. + apply Rplus_lt_compat_l. + replace 1 with (0 + 1). + apply Rlt_n_Sn. + apply Rplus_0_l. +Qed. + +Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0. +unfold Rgt in |- *. +induction x; simpl in |- *; intros. + apply Rlt_trans with (1 + 0). + rewrite Rplus_comm in |- *. + apply Rlt_n_Sn. + apply Rplus_lt_compat_l. + rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *. + rewrite Rmult_comm in |- *. + apply Rmult_lt_compat_l. + apply Rlt_0_2. + trivial. + rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *. + rewrite Rmult_comm in |- *. + apply Rmult_lt_compat_l. + apply Rlt_0_2. + trivial. + replace 1 with (0 + 1). + apply Rlt_n_Sn. + apply Rplus_0_l. +Qed. + + +Lemma Rgen_phiPOS_not_0 : + forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0. +red in |- *; intros. +specialize (Rgen_phiPOS x). +rewrite H in |- *; intro. +apply (Rlt_asym 0 0); trivial. +Qed. + +Lemma Zeq_bool_complete : forall x y, + InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x = + InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y -> + Zeq_bool x y = true. +Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0. + +Add Field RField : Rfield (infinite Zeq_bool_complete). diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v new file mode 100644 index 00000000..167e026f --- /dev/null +++ b/contrib/setoid_ring/Ring.v @@ -0,0 +1,43 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Bool. +Require Export Ring_theory. +Require Export Ring_base. +Require Export Ring_tac. + +Lemma BoolTheory : + ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)). +split; simpl in |- *. +destruct x; reflexivity. +destruct x; destruct y; reflexivity. +destruct x; destruct y; destruct z; reflexivity. +reflexivity. +destruct x; destruct y; reflexivity. +destruct x; destruct y; reflexivity. +destruct x; destruct y; destruct z; reflexivity. +reflexivity. +destruct x; reflexivity. +Qed. + +Unboxed Definition bool_eq (b1 b2:bool) := + if b1 then b2 else negb b2. + +Lemma bool_eq_ok : forall b1 b2, bool_eq b1 b2 = true -> b1 = b2. +destruct b1; destruct b2; auto. +Qed. + +Ltac bool_cst t := + let t := eval hnf in t in + match t with + true => constr:true + | false => constr:false + | _ => NotConstant + end. + +Add Ring bool_ring : BoolTheory (decidable bool_eq_ok, constants [bool_cst]). diff --git a/contrib/setoid_ring/Ring_base.v b/contrib/setoid_ring/Ring_base.v new file mode 100644 index 00000000..95b037e3 --- /dev/null +++ b/contrib/setoid_ring/Ring_base.v @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This module gathers the necessary base to build an instance of the + ring tactic. Abstract rings need more theory, depending on + ZArith_base. *) + +Declare ML Module "newring". +Require Export Ring_theory. +Require Export Ring_tac. +Require Import InitialRing. diff --git a/contrib/setoid_ring/Ring_equiv.v b/contrib/setoid_ring/Ring_equiv.v new file mode 100644 index 00000000..945f6c68 --- /dev/null +++ b/contrib/setoid_ring/Ring_equiv.v @@ -0,0 +1,74 @@ +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/contrib/setoid_ring/Pol.v b/contrib/setoid_ring/Ring_polynom.v index 2bf2574f..7317ab21 100644 --- a/contrib/setoid_ring/Pol.v +++ b/contrib/setoid_ring/Ring_polynom.v @@ -1,9 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + Set Implicit Arguments. Require Import Setoid. -Require Export BinList. +Require Import BinList. Require Import BinPos. Require Import BinInt. -Require Export Ring_th. +Require Export Ring_theory. + +Import RingSyntax. Section MakeRingPol. @@ -313,7 +323,13 @@ Section MakeRingPol. end. Notation "P ** P'" := (Pmul P P'). - (** Evaluation of a polynomial towards R *) + + (** Monomial **) + + Inductive Mon: Set := + mon0: Mon + | zmon: positive -> Mon -> Mon + | vmon: positive -> Mon -> Mon. Fixpoint pow (x:R) (i:positive) {struct i}: R := match i with @@ -322,6 +338,96 @@ Section MakeRingPol. | xI i => let p := pow x i in x * p * p end. + Fixpoint Mphi(l:list R) (M: Mon) {struct M} : R := + match M with + mon0 => rI + | zmon j M1 => Mphi (jump j l) M1 + | vmon i M1 => + let x := hd 0 l in + let xi := pow x i in + (Mphi (tail l) M1) * xi + end. + + Definition zmon_pred j M := + match j with xH => M | _ => zmon (Ppred j) M end. + + Definition mkZmon j M := + match M with mon0 => mon0 | _ => zmon j M end. + + Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol := + match P, M with + _, mon0 => (Pc cO, P) + | Pc _, _ => (P, Pc cO) + | Pinj j1 P1, zmon j2 M1 => + match (j1 ?= j2) Eq with + Eq => let (R,S) := MFactor P1 M1 in + (mkPinj j1 R, mkPinj j1 S) + | Lt => let (R,S) := MFactor P1 (zmon (j2 - j1) M1) in + (mkPinj j1 R, mkPinj j1 S) + | Gt => (P, Pc cO) + end + | Pinj _ _, vmon _ _ => (P, Pc cO) + | PX P1 i Q1, zmon j M1 => + let M2 := zmon_pred j M1 in + let (R1, S1) := MFactor P1 M in + let (R2, S2) := MFactor Q1 M2 in + (mkPX R1 i R2, mkPX S1 i S2) + | PX P1 i Q1, vmon j M1 => + match (i ?= j) Eq with + Eq => let (R1,S1) := MFactor P1 (mkZmon xH M1) in + (mkPX R1 i Q1, S1) + | Lt => let (R1,S1) := MFactor P1 (vmon (j - i) M1) in + (mkPX R1 i Q1, S1) + | Gt => let (R1,S1) := MFactor P1 (mkZmon xH M1) in + (mkPX R1 i Q1, mkPX S1 (i-j) (Pc cO)) + end + end. + + Definition POneSubst (P1: Pol) (M1: Mon) (P2: Pol): option Pol := + let (Q1,R1) := MFactor P1 M1 in + match R1 with + (Pc c) => if c ?=! cO then None + else Some (Padd Q1 (Pmul P2 R1)) + | _ => Some (Padd Q1 (Pmul P2 R1)) + end. + + Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) {struct n}: Pol := + match POneSubst P1 M1 P2 with + Some P3 => match n with S n1 => PNSubst1 P3 M1 P2 n1 | _ => P3 end + | _ => P1 + end. + + Definition PNSubst (P1: Pol) (M1: Mon) (P2: Pol) (n: nat): option Pol := + match POneSubst P1 M1 P2 with + Some P3 => match n with S n1 => Some (PNSubst1 P3 M1 P2 n1) | _ => None end + | _ => None + end. + + Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: + Pol := + match LM1 with + cons (M1,P2) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n + | _ => P1 + end. + + Fixpoint PSubstL (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: option Pol := + match LM1 with + cons (M1,P2) LM2 => + match PNSubst P1 M1 P2 n with + Some P3 => Some (PSubstL1 P3 LM2 n) + | None => PSubstL P1 LM2 n + end + | _ => None + end. + + Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) {struct m}: Pol := + match PSubstL P1 LM1 n with + Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end + | _ => P1 + end. + + (** Evaluation of a polynomial towards R *) + Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R := match P with | Pc c => [c] @@ -329,7 +435,7 @@ Section MakeRingPol. | PX P i Q => let x := hd 0 l in let xi := pow x i in - (Pphi l P) * xi + (Pphi (tl l) Q) + (Pphi l P) * xi + (Pphi (tail l) Q) end. Reserved Notation "P @ l " (at level 10, no associativity). @@ -418,7 +524,7 @@ Section MakeRingPol. Qed. Lemma mkPX_ok : forall l P i Q, - (mkPX P i Q)@l == P@l*(pow (hd 0 l) i) + Q@(tl l). + (mkPX P i Q)@l == P@l*(pow (hd 0 l) i) + Q@(tail l). Proof. intros l P i Q;unfold mkPX. destruct P;try (simpl;rrefl). @@ -500,7 +606,7 @@ Section MakeRingPol. induction P';simpl;intros;Esimpl2. generalize P p l;clear P p l. induction P;simpl;intros. - Esimpl2;apply (ARadd_sym ARth). + Esimpl2;apply (ARadd_comm ARth). assert (H := ZPminus_spec p p0);destruct (ZPminus p p0). rewrite H;Esimpl. rewrite IHP';rrefl. rewrite H;Esimpl. rewrite IHP';Esimpl. @@ -519,33 +625,33 @@ Section MakeRingPol. rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl. rewrite IHP'2;simpl. rewrite jump_Pdouble_minus_one;rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl. - rewrite IHP'2;rsimpl. add_push (P @ (tl l));rrefl. + rewrite IHP'2;rsimpl. add_push (P @ (tail l));rrefl. assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. rewrite IHP'1;rewrite IHP'2;rsimpl. - add_push (P3 @ (tl l));rewrite H;rrefl. + add_push (P3 @ (tail l));rewrite H;rrefl. rewrite IHP'1;rewrite IHP'2;simpl;Esimpl. rewrite H;rewrite Pplus_comm. rewrite pow_Pplus;rsimpl. - add_push (P3 @ (tl l));rrefl. + add_push (P3 @ (tail l));rrefl. assert (forall P k l, (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow (hd 0 l) k). - induction P;simpl;intros;try apply (ARadd_sym ARth). - destruct p2;simpl;try apply (ARadd_sym ARth). - rewrite jump_Pdouble_minus_one;apply (ARadd_sym ARth). + induction P;simpl;intros;try apply (ARadd_comm ARth). + destruct p2;simpl;try apply (ARadd_comm ARth). + rewrite jump_Pdouble_minus_one;apply (ARadd_comm ARth). assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2. - rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tl l0));rrefl. + rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl. rewrite IHP'1;simpl;Esimpl. rewrite H1;rewrite Pplus_comm. rewrite pow_Pplus;simpl;Esimpl. - add_push (P5 @ (tl l0));rrefl. + add_push (P5 @ (tail l0));rrefl. rewrite IHP1;rewrite H1;rewrite Pplus_comm. rewrite pow_Pplus;simpl;rsimpl. - add_push (P5 @ (tl l0));rrefl. + add_push (P5 @ (tail l0));rrefl. rewrite H0;rsimpl. - add_push (P3 @ (tl l)). + add_push (P3 @ (tail l)). rewrite H;rewrite Pplus_comm. rewrite IHP'2;rewrite pow_Pplus;rsimpl. - add_push (P3 @ (tl l));rrefl. + add_push (P3 @ (tail l));rrefl. Qed. Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l. @@ -553,7 +659,7 @@ Section MakeRingPol. induction P';simpl;intros;Esimpl2;trivial. generalize P p l;clear P p l. induction P;simpl;intros. - Esimpl2;apply (ARadd_sym ARth). + Esimpl2;apply (ARadd_comm ARth). assert (H := ZPminus_spec p p0);destruct (ZPminus p p0). rewrite H;Esimpl. rewrite IHP';rsimpl. rewrite H;Esimpl. rewrite IHP';Esimpl. @@ -569,35 +675,35 @@ Section MakeRingPol. repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try rrefl. destruct p0;simpl;Esimpl2. rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow (hd 0 l) p));trivial. - add_push (P @ (jump p0 (jump p0 (tl l))));rrefl. + add_push (P @ (jump p0 (jump p0 (tail l))));rrefl. rewrite IHP'2;simpl;rewrite jump_Pdouble_minus_one;rsimpl. add_push (- (P'1 @ l * pow (hd 0 l) p));rrefl. - rewrite IHP'2;rsimpl;add_push (P @ (tl l));rrefl. + rewrite IHP'2;rsimpl;add_push (P @ (tail l));rrefl. assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. rewrite IHP'1; rewrite IHP'2;rsimpl. - add_push (P3 @ (tl l));rewrite H;rrefl. + add_push (P3 @ (tail l));rewrite H;rrefl. rewrite IHP'1; rewrite IHP'2;rsimpl;simpl;Esimpl. rewrite H;rewrite Pplus_comm. rewrite pow_Pplus;rsimpl. - add_push (P3 @ (tl l));rrefl. + add_push (P3 @ (tail l));rrefl. assert (forall P k l, (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow (hd 0 l) k). induction P;simpl;intros. - rewrite Popp_ok;rsimpl;apply (ARadd_sym ARth);trivial. + rewrite Popp_ok;rsimpl;apply (ARadd_comm ARth);trivial. destruct p2;simpl;rewrite Popp_ok;rsimpl. - apply (ARadd_sym ARth);trivial. - rewrite jump_Pdouble_minus_one;apply (ARadd_sym ARth);trivial. - apply (ARadd_sym ARth);trivial. + apply (ARadd_comm ARth);trivial. + rewrite jump_Pdouble_minus_one;apply (ARadd_comm ARth);trivial. + apply (ARadd_comm ARth);trivial. assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl. - rewrite IHP'1;rsimpl;add_push (P5 @ (tl l0));rewrite H1;rrefl. + rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;rrefl. rewrite IHP'1;rewrite H1;rewrite Pplus_comm. rewrite pow_Pplus;simpl;Esimpl. - add_push (P5 @ (tl l0));rrefl. + add_push (P5 @ (tail l0));rrefl. rewrite IHP1;rewrite H1;rewrite Pplus_comm. rewrite pow_Pplus;simpl;rsimpl. - add_push (P5 @ (tl l0));rrefl. + add_push (P5 @ (tail l0));rrefl. rewrite H0;rsimpl. - rewrite IHP'2;rsimpl;add_push (P3 @ (tl l)). + rewrite IHP'2;rsimpl;add_push (P3 @ (tail l)). rewrite H;rewrite Pplus_comm. rewrite pow_Pplus;rsimpl. Qed. @@ -609,7 +715,7 @@ Section MakeRingPol. (PmulI Pmul_aux P' p P) @ l == P @ l * P' @ (jump p l). Proof. induction P;simpl;intros. - Esimpl2;apply (ARmul_sym ARth). + Esimpl2;apply (ARmul_comm ARth). assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2. rewrite H1; rewrite H;rrefl. rewrite H1; rewrite H. @@ -639,13 +745,198 @@ Section MakeRingPol. Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. Proof. destruct P;simpl;intros. - Esimpl2;apply (ARmul_sym ARth). + Esimpl2;apply (ARmul_comm ARth). rewrite (PmulI_ok P (Pmul_aux_ok P)). - apply (ARmul_sym ARth). + apply (ARmul_comm ARth). rewrite Padd_ok; Esimpl2. rewrite (PmulI_ok P3 (Pmul_aux_ok P3));trivial. rewrite Pmul_aux_ok;mul_push (P' @ l). - rewrite (ARmul_sym ARth (P' @ l));rrefl. + rewrite (ARmul_comm ARth (P' @ l));rrefl. + Qed. + + + Lemma mkZmon_ok: forall M j l, + Mphi l (mkZmon j M) == Mphi l (zmon j M). + intros M j l; case M; simpl; intros; rsimpl. + Qed. + + Lemma Mphi_ok: forall P M l, + let (Q,R) := MFactor P M in + P@l == Q@l + (Mphi l M) * (R@l). + Proof. + intros P; elim P; simpl; auto; clear P. + intros c M l; case M; simpl; auto; try intro p; try intro m; + try rewrite (morph0 CRmorph); rsimpl. + + intros i P Hrec M l; case M; simpl; clear M. + rewrite (morph0 CRmorph); rsimpl. + intros j M. + case_eq ((i ?= j) Eq); intros He; simpl. + rewrite (Pcompare_Eq_eq _ _ He). + generalize (Hrec M (jump j l)); case (MFactor P M); + simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto. + generalize (Hrec (zmon (j -i) M) (jump i l)); + case (MFactor P (zmon (j -i) M)); simpl. + intros P2 Q2 H; repeat rewrite mkPinj_ok; auto. + rewrite <- (Pplus_minus _ _ (ZC2 _ _ He)). + rewrite Pplus_comm; rewrite jump_Pplus; auto. + rewrite (morph0 CRmorph); rsimpl. + intros P2 m; rewrite (morph0 CRmorph); rsimpl. + + intros P2 Hrec1 i Q2 Hrec2 M l; case M; simpl; auto. + rewrite (morph0 CRmorph); rsimpl. + intros j M1. + generalize (Hrec1 (zmon j M1) l); + case (MFactor P2 (zmon j M1)). + intros R1 S1 H1. + generalize (Hrec2 (zmon_pred j M1) (List.tail l)); + case (MFactor Q2 (zmon_pred j M1)); simpl. + intros R2 S2 H2; rewrite H1; rewrite H2. + repeat rewrite mkPX_ok; simpl. + rsimpl. + apply radd_ext; rsimpl. + rewrite (ARadd_comm ARth); rsimpl. + apply radd_ext; rsimpl. + rewrite (ARadd_comm ARth); rsimpl. + case j; simpl; auto; try intros j1; rsimpl. + rewrite jump_Pdouble_minus_one; rsimpl. + intros j M1. + case_eq ((i ?= j) Eq); intros He; simpl. + rewrite (Pcompare_Eq_eq _ _ He). + generalize (Hrec1 (mkZmon xH M1) l); case (MFactor P2 (mkZmon xH M1)); + simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. + rewrite H; rewrite mkPX_ok; rsimpl. + repeat (rewrite <-(ARadd_assoc ARth)). + apply radd_ext; rsimpl. + rewrite (ARadd_comm ARth); rsimpl. + apply radd_ext; rsimpl. + repeat (rewrite <-(ARmul_assoc ARth)). + rewrite mkZmon_ok. + apply rmul_ext; rsimpl. + rewrite (ARmul_comm ARth); rsimpl. + generalize (Hrec1 (vmon (j - i) M1) l); + case (MFactor P2 (vmon (j - i) M1)); + simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. + rewrite H; rsimpl; repeat rewrite mkPinj_ok; auto. + rewrite mkPX_ok; rsimpl. + repeat (rewrite <-(ARadd_assoc ARth)). + apply radd_ext; rsimpl. + rewrite (ARadd_comm ARth); rsimpl. + apply radd_ext; rsimpl. + repeat (rewrite <-(ARmul_assoc ARth)). + apply rmul_ext; rsimpl. + rewrite (ARmul_comm ARth); rsimpl. + apply rmul_ext; rsimpl. + rewrite <- pow_Pplus. + rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl. + generalize (Hrec1 (mkZmon 1 M1) l); + case (MFactor P2 (mkZmon 1 M1)); + simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. + rewrite H; rsimpl. + rewrite mkPX_ok; rsimpl. + repeat (rewrite <-(ARadd_assoc ARth)). + apply radd_ext; rsimpl. + rewrite (ARadd_comm ARth); rsimpl. + apply radd_ext; rsimpl. + rewrite mkZmon_ok. + repeat (rewrite <-(ARmul_assoc ARth)). + apply rmul_ext; rsimpl. + rewrite (ARmul_comm ARth); rsimpl. + rewrite mkPX_ok; simpl; rsimpl. + rewrite (morph0 CRmorph); rsimpl. + repeat (rewrite <-(ARmul_assoc ARth)). + rewrite (ARmul_comm ARth (Q3@l)); rsimpl. + apply rmul_ext; rsimpl. + rewrite <- pow_Pplus. + rewrite (Pplus_minus _ _ He); rsimpl. + Qed. + + + Lemma POneSubst_ok: forall P1 M1 P2 P3 l, + POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l. + intros P2 M1 P3 P4 l; unfold POneSubst. + generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto. + intros Q1 R1; case R1. + intros c H; rewrite H. + generalize (morph_eq CRmorph c cO); + case (c ?=! cO); simpl; auto. + intros H1 H2; rewrite H1; auto; rsimpl. + discriminate. + intros _ H1 H2; injection H1; intros; subst. + rewrite H2; rsimpl. + rewrite Padd_ok; rewrite Pmul_ok; rsimpl. + intros i P5 H; rewrite H. + intros HH H1; injection HH; intros; subst; rsimpl. + rewrite Padd_ok; rewrite Pmul_ok; rewrite H1; rsimpl. + intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3. + injection H2; intros; subst; rsimpl. + rewrite Padd_ok; rewrite Pmul_ok; rsimpl. + Qed. + + + Lemma PNSubst1_ok: forall n P1 M1 P2 l, + Mphi l M1 == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l. + Proof. + intros n; elim n; simpl; auto. + intros P2 M1 P3 l H. + generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); + case (POneSubst P2 M1 P3); [idtac | intros; rsimpl]. + intros P4 Hrec; rewrite (Hrec P4); auto; rsimpl. + intros n1 Hrec P2 M1 P3 l H. + generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); + case (POneSubst P2 M1 P3); [idtac | intros; rsimpl]. + intros P4 Hrec1; rewrite (Hrec1 P4); auto; rsimpl. + Qed. + + Lemma PNSubst_ok: forall n P1 M1 P2 l P3, + PNSubst P1 M1 P2 n = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l. + Proof. + intros n P2 M1 P3 l P4; unfold PNSubst. + generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); + case (POneSubst P2 M1 P3); [idtac | intros; discriminate]. + intros P5 H1; case n; try (intros; discriminate). + intros n1 H2; injection H2; intros; subst. + rewrite <- PNSubst1_ok; auto. + Qed. + + Fixpoint MPcond (LM1: list (Mon * Pol)) (l: list R) {struct LM1} : Prop := + match LM1 with + cons (M1,P2) LM2 => (Mphi l M1 == P2@l) /\ (MPcond LM2 l) + | _ => True + end. + + Lemma PSubstL1_ok: forall n LM1 P1 l, + MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l. + Proof. + intros n LM1; elim LM1; simpl; auto. + intros; rsimpl. + intros (M2,P2) LM2 Hrec P3 l [H H1]. + rewrite <- Hrec; auto. + apply PNSubst1_ok; auto. + Qed. + + Lemma PSubstL_ok: forall n LM1 P1 P2 l, + PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l. + Proof. + intros n LM1; elim LM1; simpl; auto. + intros; discriminate. + intros (M2,P2) LM2 Hrec P3 P4 l. + generalize (PNSubst_ok n P3 M2 P2); case (PNSubst P3 M2 P2 n). + intros P5 H0 H1 [H2 H3]; injection H1; intros; subst. + rewrite <- PSubstL1_ok; auto. + intros l1 H [H1 H2]; auto. + Qed. + + Lemma PNSubstL_ok: forall m n LM1 P1 l, + MPcond LM1 l -> P1@l == (PNSubstL P1 LM1 m n)@l. + Proof. + intros m; elim m; simpl; auto. + intros n LM1 P2 l H; generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l); + case (PSubstL P2 LM1 n); intros; rsimpl; auto. + intros m1 Hrec n LM1 P2 l H. + generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l); + case (PSubstL P2 LM1 n); intros; rsimpl; auto. + rewrite <- Hrec; auto. Qed. (** Definition of polynomial expressions *) @@ -714,7 +1005,7 @@ Section MakeRingPol. | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P2 P1 l) | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l) | |- context [(norm (PEopp ?pe))@?l] => rewrite (norm_PEopp l pe) - end;Esimpl2;try rrefl;try apply (ARadd_sym ARth). + end;Esimpl2;try rrefl;try apply (ARadd_comm ARth). Lemma norm_ok : forall l pe, PEeval l pe == (norm pe)@l. Proof. @@ -757,12 +1048,12 @@ Section MakeRingPol. Fixpoint add_mult_dev (rP:R) (P:Pol) (fv lm:list R) {struct P} : R := (* rP + P@l * lm *) match P with - | Pc c => if c ?=! cI then mkadd_mult rP (rev lm) - else mkadd_mult rP (cons [c] (rev lm)) + | Pc c => if c ?=! cI then mkadd_mult rP (rev' lm) + else mkadd_mult rP (cons [c] (rev' lm)) | Pinj j Q => add_mult_dev rP Q (jump j fv) lm | PX P i Q => let rP := add_mult_dev rP P fv (powl i (hd 0 fv) lm) in - if Q ?== P0 then rP else add_mult_dev rP Q (tl fv) lm + if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) lm end. Definition mkmult1 lm := @@ -774,14 +1065,14 @@ Section MakeRingPol. Fixpoint mult_dev (P:Pol) (fv lm : list R) {struct P} : R := (* P@l * lm *) match P with - | Pc c => if c ?=! cI then mkmult1 (rev lm) else mkmult [c] (rev lm) + | Pc c => if c ?=! cI then mkmult1 (rev' lm) else mkmult [c] (rev' lm) | Pinj j Q => mult_dev Q (jump j fv) lm | PX P i Q => let rP := mult_dev P fv (powl i (hd 0 fv) lm) in - if Q ?== P0 then rP else add_mult_dev rP Q (tl fv) lm + if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) lm end. - Definition Pphi_dev fv P := mult_dev P fv (nil R). + Definition Pphi_dev fv P := mult_dev P fv nil. Add Morphism mkmult : mkmult_ext. intros r r0 eqr l;generalize l r r0 eqr;clear l r r0 eqr; @@ -808,21 +1099,21 @@ Section MakeRingPol. Qed. Lemma mkmult_rev_append : forall lm l r, - mkmult r (rev_append l lm) == mkmult (mkmult r l) lm. + mkmult r (rev_append lm l) == mkmult (mkmult r l) lm. Proof. induction lm; simpl in |- *; intros. rrefl. rewrite IHlm; simpl in |- *. - repeat rewrite <- (ARmul_sym ARth a); rewrite <- mul_mkmult. + repeat rewrite <- (ARmul_comm ARth a); rewrite <- mul_mkmult. rrefl. Qed. Lemma powl_mkmult_rev : forall p r x lm, - mkmult r (rev (powl p x lm)) == mkmult (pow x p * r) (rev lm). + mkmult r (rev' (powl p x lm)) == mkmult (pow x p * r) (rev' lm). Proof. induction p;simpl;intros. repeat rewrite IHp. - unfold rev;simpl. + unfold rev';simpl. repeat rewrite mkmult_rev_append. simpl. setoid_replace (pow x p * (pow x p * r) * x) @@ -831,18 +1122,18 @@ Section MakeRingPol. repeat rewrite IHp. setoid_replace (pow x p * (pow x p * r) ) with (pow x p * pow x p * r);Esimpl. - unfold rev;simpl. repeat rewrite mkmult_rev_append;simpl. - rewrite (ARmul_sym ARth);rrefl. + unfold rev';simpl. repeat rewrite mkmult_rev_append;simpl. + rewrite (ARmul_comm ARth);rrefl. Qed. Lemma Pphi_add_mult_dev : forall P rP fv lm, - rP + P@fv * mkmult1 (rev lm) == add_mult_dev rP P fv lm. + rP + P@fv * mkmult1 (rev' lm) == add_mult_dev rP P fv lm. Proof. induction P;simpl;intros. assert (H := (morph_eq CRmorph) c cI). destruct (c ?=! cI). rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl. - destruct (rev lm);Esimpl;rrefl. + destruct (rev' lm);Esimpl;rrefl. rewrite mkmult1_mkmult;rrefl. apply IHP. replace (match P3 with @@ -865,7 +1156,7 @@ Section MakeRingPol. Qed. Lemma Pphi_mult_dev : forall P fv lm, - P@fv * mkmult1 (rev lm) == mult_dev P fv lm. + P@fv * mkmult1 (rev' lm) == mult_dev P fv lm. Proof. induction P;simpl;intros. assert (H := (morph_eq CRmorph) c cI). @@ -898,298 +1189,44 @@ Section MakeRingPol. rewrite <- Pphi_mult_dev;simpl;Esimpl. Qed. - Lemma Pphi_dev_ok : forall l pe, PEeval l pe == Pphi_dev l (norm pe). + Lemma Pphi_dev_gen_ok : forall l pe, PEeval l pe == Pphi_dev l (norm pe). Proof. intros l pe;rewrite <- Pphi_Pphi_dev;apply norm_ok. Qed. - Lemma Pphi_dev_ok' : + Lemma Pphi_dev_ok : forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe. Proof. - intros l pe npe npe_eq; subst npe; apply Pphi_dev_ok. - Qed. - -(* The same but building a PExpr *) -(* - Fixpoint Pmkmult (r:PExpr) (lm:list PExpr) {struct lm}: PExpr := - match lm with - | nil => r - | cons h t => Pmkmult (PEmul r h) t - end. - - Definition Pmkadd_mult rP lm := - match lm with - | nil => PEadd rP (PEc cI) - | cons h t => PEadd rP (Pmkmult h t) - end. - - Fixpoint Ppowl (i:positive) (x:PExpr) (l:list PExpr) {struct i}: list PExpr := - match i with - | xH => cons x l - | xO i => Ppowl i x (Ppowl i x l) - | xI i => Ppowl i x (Ppowl i x (cons x l)) - end. - - Fixpoint Padd_mult_dev - (rP:PExpr) (P:Pol) (fv lm:list PExpr) {struct P} : PExpr := - (* rP + P@l * lm *) - match P with - | Pc c => if c ?=! cI then Pmkadd_mult rP (rev lm) - else Pmkadd_mult rP (cons [PEc c] (rev lm)) - | Pinj j Q => Padd_mult_dev rP Q (jump j fv) lm - | PX P i Q => - let rP := Padd_mult_dev rP P fv (Ppowl i (hd P0 fv) lm) in - if Q ?== P0 then rP else Padd_mult_dev rP Q (tl fv) lm - end. - - Definition Pmkmult1 lm := - match lm with - | nil => PEc cI - | cons h t => Pmkmult h t - end. - - Fixpoint Pmult_dev (P:Pol) (fv lm : list PExpr) {struct P} : PExpr := - (* P@l * lm *) - match P with - | Pc c => if c ?=! cI then Pmkmult1 (rev lm) else Pmkmult [PEc c] (rev lm) - | Pinj j Q => Pmult_dev Q (jump j fv) lm - | PX P i Q => - let rP := Pmult_dev P fv (Ppowl i (hd (PEc r0) fv) lm) in - if Q ?== P0 then rP else Padd_mult_dev rP Q (tl fv) lm - end. - - Definition Pphi_dev2 fv P := Pmult_dev P fv (nil PExpr). - -... -*) - (************************************************) - (* avec des parentheses mais un peu plus efficace *) - - - (************************************************** - - Fixpoint pow_mult (i:positive) (x r:R){struct i}:R := - match i with - | xH => r * x - | xO i => pow_mult i x (pow_mult i x r) - | xI i => pow_mult i x (pow_mult i x (r * x)) - end. - - Definition pow_dev i x := - match i with - | xH => x - | xO i => pow_mult (Pdouble_minus_one i) x x - | xI i => pow_mult (xO i) x x - end. - - Lemma pow_mult_pow : forall i x r, pow_mult i x r == pow x i * r. - Proof. - induction i;simpl;intros. - rewrite (IHi x (pow_mult i x (r * x)));rewrite (IHi x (r*x));rsimpl. - mul_push x;rrefl. - rewrite (IHi x (pow_mult i x r));rewrite (IHi x r);rsimpl. - apply ARth.(ARmul_sym). - Qed. - - Lemma pow_dev_pow : forall p x, pow_dev p x == pow x p. - Proof. - destruct p;simpl;intros. - rewrite (pow_mult_pow p x (pow_mult p x x)). - rewrite (pow_mult_pow p x x);rsimpl;mul_push x;rrefl. - rewrite (pow_mult_pow (Pdouble_minus_one p) x x). - rewrite (ARth.(ARmul_sym) (pow x (Pdouble_minus_one p)) x). - rewrite <- (pow_Psucc x (Pdouble_minus_one p)). - rewrite Psucc_o_double_minus_one_eq_xO;simpl; rrefl. - rrefl. - Qed. - - Fixpoint Pphi_dev (fv:list R) (P:Pol) {struct P} : R := - match P with - | Pc c => [c] - | Pinj j Q => Pphi_dev (jump j fv) Q - | PX P i Q => - let rP := mult_dev P fv (pow_dev i (hd 0 fv)) in - add_dev rP Q (tl fv) - end + intros l pe npe npe_eq; subst npe; apply Pphi_dev_gen_ok. + Qed. - with add_dev (ra:R) (P:Pol) (fv:list R) {struct P} : R := - match P with - | Pc c => if c ?=! cO then ra else ra + [c] - | Pinj j Q => add_dev ra Q (jump j fv) - | PX P i Q => - let ra := add_mult_dev ra P fv (pow_dev i (hd 0 fv)) in - add_dev ra Q (tl fv) - end - - with mult_dev (P:Pol) (fv:list R) (rm:R) {struct P} : R := - match P with - | Pc c => if c ?=! cI then rm else [c]*rm - | Pinj j Q => mult_dev Q (jump j fv) rm - | PX P i Q => - let ra := mult_dev P fv (pow_mult i (hd 0 fv) rm) in - add_mult_dev ra Q (tl fv) rm - end - - with add_mult_dev (ra:R) (P:Pol) (fv:list R) (rm:R) {struct P} : R := - match P with - | Pc c => if c ?=! cO then ra else ra + [c]*rm - | Pinj j Q => add_mult_dev ra Q (jump j fv) rm - | PX P i Q => - let rmP := pow_mult i (hd 0 fv) rm in - let raP := add_mult_dev ra P fv rmP in - add_mult_dev raP Q (tl fv) rm - end. - - Lemma Pphi_add_mult_dev : forall P ra fv rm, - add_mult_dev ra P fv rm == ra + P@fv * rm. - Proof. - induction P;simpl;intros. - assert (H := CRmorph.(morph_eq) c cO). - destruct (c ?=! cO). - rewrite (H (refl_equal true));rewrite CRmorph.(morph0);Esimpl. - rrefl. - apply IHP. - rewrite (IHP2 (add_mult_dev ra P2 fv (pow_mult p (hd 0 fv) rm)) (tl fv) rm). - rewrite (IHP1 ra fv (pow_mult p (hd 0 fv) rm)). - rewrite (pow_mult_pow p (hd 0 fv) rm);rsimpl. - Qed. - - Lemma Pphi_add_dev : forall P ra fv, add_dev ra P fv == ra + P@fv. - Proof. - induction P;simpl;intros. - assert (H := CRmorph.(morph_eq) c cO). - destruct (c ?=! cO). - rewrite (H (refl_equal true));rewrite CRmorph.(morph0);Esimpl. - rrefl. - apply IHP. - rewrite (IHP2 (add_mult_dev ra P2 fv (pow_dev p (hd 0 fv))) (tl fv)). - rewrite (Pphi_add_mult_dev P2 ra fv (pow_dev p (hd 0 fv))). - rewrite (pow_dev_pow p (hd 0 fv));rsimpl. - Qed. + Fixpoint MPcond_dev (LM1: list (Mon * Pol)) (l: list R) {struct LM1} : Prop := + match LM1 with + cons (M1,P2) LM2 => (Mphi l M1 == Pphi_dev l P2) /\ (MPcond_dev LM2 l) + | _ => True + end. - Lemma Pphi_mult_dev : forall P fv rm, mult_dev P fv rm == P@fv * rm. - Proof. - induction P;simpl;intros. - assert (H := CRmorph.(morph_eq) c cI). - destruct (c ?=! cI). - rewrite (H (refl_equal true));rewrite CRmorph.(morph1);Esimpl. - rrefl. - apply IHP. - rewrite (Pphi_add_mult_dev P3 - (mult_dev P2 fv (pow_mult p (hd 0 fv) rm)) (tl fv) rm). - rewrite (IHP1 fv (pow_mult p (hd 0 fv) rm)). - rewrite (pow_mult_pow p (hd 0 fv) rm);rsimpl. - Qed. + Fixpoint MPcond_map (LM1: list (Mon * PExpr)): list (Mon * Pol) := + match LM1 with + cons (M1,P2) LM2 => cons (M1, norm P2) (MPcond_map LM2) + | _ => nil + end. - Lemma Pphi_Pphi_dev : forall P fv, P@fv == Pphi_dev fv P. + Lemma MP_cond_dev_imp_MP_cond: forall LM1 l, + MPcond_dev LM1 l -> MPcond LM1 l. Proof. - induction P;simpl;intros. - rrefl. trivial. - rewrite (Pphi_add_dev P3 (mult_dev P2 fv (pow_dev p (hd 0 fv))) (tl fv)). - rewrite (Pphi_mult_dev P2 fv (pow_dev p (hd 0 fv))). - rewrite (pow_dev_pow p (hd 0 fv));rsimpl. + intros LM1; elim LM1; simpl; auto. + intros (M2,P2) LM2 Hrec l [H1 H2]; split; auto. + rewrite H1; rewrite Pphi_Pphi_dev; rsimpl. Qed. - Lemma Pphi_dev_ok : forall l pe, PEeval l pe == Pphi_dev l (norm pe). - Proof. - intros l pe;rewrite <- (Pphi_Pphi_dev (norm pe) l);apply norm_ok. + Lemma PNSubstL_dev_ok: forall m n lm pe l, + let LM := MPcond_map lm in + MPcond_dev LM l -> PEeval l pe == Pphi_dev l (PNSubstL (norm pe) LM m n). + intros m n lm p3 l LM H. + rewrite <- Pphi_Pphi_dev; rewrite <- PNSubstL_ok; auto. + apply MP_cond_dev_imp_MP_cond; auto. + rewrite Pphi_Pphi_dev; apply Pphi_dev_ok; auto. Qed. - Ltac Trev l := - let rec rev_append rev l := - match l with - | (nil _) => constr:(rev) - | (cons ?h ?t) => let rev := constr:(cons h rev) in rev_append rev t - end in - rev_append (nil R) l. - - Ltac TPphi_dev add mul := - let tl l := match l with (cons ?h ?t) => constr:(t) end in - let rec jump j l := - match j with - | xH => tl l - | (xO ?j) => let l := jump j l in jump j l - | (xI ?j) => let t := tl l in let l := jump j l in jump j l - end in - let rec pow_mult i x r := - match i with - | xH => constr:(mul r x) - | (xO ?i) => let r := pow_mult i x r in pow_mult i x r - | (xI ?i) => - let r := constr:(mul r x) in - let r := pow_mult i x r in - pow_mult i x r - end in - let pow_dev i x := - match i with - | xH => x - | (xO ?i) => - let i := eval compute in (Pdouble_minus_one i) in pow_mult i x x - | (xI ?i) => pow_mult (xO i) x x - end in - let rec add_mult_dev ra P fv rm := - match P with - | (Pc ?c) => - match eval compute in (c ?=! cO) with - | true => constr:ra - | _ => let rc := eval compute in [c] in constr:(add ra (mul rc rm)) - end - | (Pinj ?j ?Q) => - let fv := jump j fv in add_mult_dev ra Q fv rm - | (PX ?P ?i ?Q) => - match fv with - | (cons ?hd ?tl) => - let rmP := pow_mult i hd rm in - let raP := add_mult_dev ra P fv rmP in - add_mult_dev raP Q tl rm - end - end in - let rec mult_dev P fv rm := - match P with - | (Pc ?c) => - match eval compute in (c ?=! cI) with - | true => constr:rm - | false => let rc := eval compute in [c] in constr:(mul rc rm) - end - | (Pinj ?j ?Q) => let fv := jump j fv in mult_dev Q fv rm - | (PX ?P ?i ?Q) => - match fv with - | (cons ?hd ?tl) => - let rmP := pow_mult i hd rm in - let ra := mult_dev P fv rmP in - add_mult_dev ra Q tl rm - end - end in - let rec add_dev ra P fv := - match P with - | (Pc ?c) => - match eval compute in (c ?=! cO) with - | true => ra - | false => let rc := eval compute in [c] in constr:(add ra rc) - end - | (Pinj ?j ?Q) => let fv := jump j fv in add_dev ra Q fv - | (PX ?P ?i ?Q) => - match fv with - | (cons ?hd ?tl) => - let rmP := pow_dev i hd in - let ra := add_mult_dev ra P fv rmP in - add_dev ra Q tl - end - end in - let rec Pphi_dev fv P := - match P with - | (Pc ?c) => eval compute in [c] - | (Pinj ?j ?Q) => let fv := jump j fv in Pphi_dev fv Q - | (PX ?P ?i ?Q) => - match fv with - | (cons ?hd ?tl) => - let rm := pow_dev i hd in - let rP := mult_dev P fv rm in - add_dev rP Q tl - end - end in - Pphi_dev. - - **************************************************************) - End MakeRingPol. diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index 6c3f87a5..95efde7f 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -1,76 +1,73 @@ Set Implicit Arguments. Require Import Setoid. -Require Import BinList. Require Import BinPos. -Require Import Pol. +Require Import Ring_polynom. +Require Import BinList. Declare ML Module "newring". -(* Some Tactics *) - -Ltac compute_assertion id t := - let t' := eval compute in t in - (assert (id : t = t'); [exact_no_check (refl_equal t')|idtac]). -Ltac compute_assertion' id id' t := - let t' := eval compute in t in +(* adds a definition id' on the normal form of t and an hypothesis id + stating that t = id' (tries to produces a proof as small as possible) *) +Ltac compute_assertion id id' t := + let t' := eval vm_compute in t in (pose (id' := t'); assert (id : t = id'); [exact_no_check (refl_equal id')|idtac]). -Ltac compute_replace' id t := - let t' := eval compute in t in - (replace t with t' in id; [idtac|exact_no_check (refl_equal t')]). +(********************************************************************) +(* Tacticals to build reflexive tactics *) -Ltac bin_list_fold_right fcons fnil l := - match l with - | (cons ?x ?tl) => fcons x ltac:(bin_list_fold_right fcons fnil tl) - | (nil _) => fnil +Ltac OnEquation req := + match goal with + | |- req ?lhs ?rhs => (fun f => f lhs rhs) + | _ => fail 1 "Goal is not an equation (of expected equality)" end. -Ltac bin_list_fold_left fcons fnil l := - match l with - | (cons ?x ?tl) => bin_list_fold_left fcons ltac:(fcons x fnil) tl - | (nil _) => fnil - end. -Ltac bin_list_iter f l := - match l with - | (cons ?x ?tl) => f x; bin_list_iter f tl - | (nil _) => idtac +Ltac OnMainSubgoal H ty := + match ty with + | _ -> ?ty' => + let subtac := OnMainSubgoal H ty' in + fun tac => lapply H; [clear H; intro H; subtac tac | idtac] + | _ => (fun tac => tac) end. - -(** A tactic that reverses a list *) -Ltac Trev R l := - let rec rev_append rev l := - match l with - | (nil _) => constr:(rev) - | (cons ?h ?t) => let rev := constr:(cons h rev) in rev_append rev t - end in - rev_append (nil R) l. -(* to avoid conflicts with Coq booleans*) +Ltac ApplyLemmaAndSimpl tac lemma pe:= + let npe := fresh "ast_nf" in + let H := fresh "eq_nf" in + let Heq := fresh "thm" in + let npe_spec := + match type of (lemma pe) with + forall npe, ?npe_spec = npe -> _ => npe_spec + | _ => fail 1 "ApplyLemmaAndSimpl: cannot find norm expression" + end in + (compute_assertion H npe npe_spec; + (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma"); + clear H; + OnMainSubgoal Heq ltac:(type of Heq) + ltac:(tac Heq; rewrite Heq; clear Heq npe)). + +(* General scheme of reflexive tactics using of correctness lemma + that involves normalisation of one expression *) +Ltac ReflexiveRewriteTactic FV_tac SYN_tac SIMPL_tac lemma2 req rl := + let R := match type of req with ?R -> _ => R end in + (* build the atom list *) + let fv := list_fold_left FV_tac (@List.nil R) rl in + (* some type-checking to avoid late errors *) + (check_fv fv; + (* rewrite steps *) + list_iter + ltac:(fun r => + let ast := SYN_tac r fv in + try ApplyLemmaAndSimpl SIMPL_tac (lemma2 fv) ast) + rl). + +(********************************************************) + +(* An object to return when an expression is not recognized as a constant *) Definition NotConstant := false. - -Ltac IN a l := - match l with - | (cons a ?l) => true - | (cons _ ?l) => IN a l - | (nil _) => false - end. - -Ltac AddFv a l := - match (IN a l) with - | true => l - | _ => constr:(cons a l) - end. - -Ltac Find_at a l := - match l with - | (nil _) => fail 1 "ring anomaly" - | (cons a _) => constr:1%positive - | (cons _ ?l) => let p := Find_at a l in eval compute in (Psucc p) - end. +(* Building the atom list of a ring expression *) Ltac FV Cst add mul sub opp t fv := let rec TFV t fv := match Cst t with @@ -80,13 +77,13 @@ Ltac FV Cst add mul sub opp t fv := | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (opp ?t1) => TFV t1 fv - | _ => AddFv t fv + | _ => AddFvTail t fv end | _ => fv - end + end in TFV t fv. - (* syntaxification *) + (* syntaxification of ring expressions *) Ltac mkPolexpr C Cst radd rmul rsub ropp t fv := let rec mkP t := match Cst t with @@ -111,644 +108,53 @@ Ltac FV Cst add mul sub opp t fv := in mkP t. (* ring tactics *) -Ltac Make_ring_rewrite_step lemma pe:= - let npe := fresh "npe" in - let H := fresh "eq_npe" in - let Heq := fresh "ring_thm" in - let npe_spec := - match type of (lemma pe) with - forall (npe:_), ?npe_spec = npe -> _ => npe_spec - | _ => fail 1 "cannot find norm expression" - end in - (compute_assertion' H npe npe_spec; - assert (Heq:=lemma _ _ H); clear H; - protect_fv in Heq; - (rewrite Heq; clear Heq npe) || clear npe). - - -Ltac Make_ring_rw_list Cst_tac lemma req rl := - match type of lemma with - forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C), - _ = npe -> - req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ => - let mkFV := FV Cst_tac add mul sub opp in - let mkPol := mkPolexpr C Cst_tac add mul sub opp in - (* build the atom list *) - let rfv := bin_list_fold_left mkFV (nil R) rl in - let fv := Trev R rfv in - (* rewrite *) - bin_list_iter - ltac:(fun r => - let pe := mkPol r fv in - Make_ring_rewrite_step (lemma fv) pe) - rl - | _ => fail 1 "bad lemma" - end. - -Ltac Make_ring_rw Cst_tac lemma req r := - Make_ring_rw_list Cst_tac lemma req (cons r (nil _)). - - (* Building the generic tactic *) - - Ltac Make_ring_tac Cst_tac lemma1 lemma2 req := - match type of lemma2 with - forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C), - _ = npe -> - req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ => - match goal with - | |- req ?r1 ?r2 => - let mkFV := FV Cst_tac add mul sub opp in - let mkPol := mkPolexpr C Cst_tac add mul sub opp in - let rfv := mkFV (add r1 r2) (nil R) in - let fv := Trev R rfv in - let pe1 := mkPol r1 fv in - let pe2 := mkPol r2 fv in - ((apply (lemma1 fv pe1 pe2); - vm_compute; - exact (refl_equal true)) || - (Make_ring_rewrite_step (lemma2 fv) pe1; - Make_ring_rewrite_step (lemma2 fv) pe2)) - | _ => fail 1 "goal is not an equality from a declared ring" - end - end. - - -(* coefs belong to the same type as the target ring (concrete ring) *) -Definition ring_id_correct - R rO rI radd rmul rsub ropp req rSet req_th ARth reqb reqb_ok := - @ring_correct R rO rI radd rmul rsub ropp req rSet req_th ARth - R rO rI radd rmul rsub ropp reqb - (@IDphi R) - (@IDmorph R rO rI radd rmul rsub ropp req rSet reqb reqb_ok). - -Definition ring_rw_id_correct - R rO rI radd rmul rsub ropp req rSet req_th ARth reqb reqb_ok := - @Pphi_dev_ok R rO rI radd rmul rsub ropp req rSet req_th ARth - R rO rI radd rmul rsub ropp reqb - (@IDphi R) - (@IDmorph R rO rI radd rmul rsub ropp req rSet reqb reqb_ok). - -Definition ring_rw_id_correct' - R rO rI radd rmul rsub ropp req rSet req_th ARth reqb reqb_ok := - @Pphi_dev_ok' R rO rI radd rmul rsub ropp req rSet req_th ARth - R rO rI radd rmul rsub ropp reqb - (@IDphi R) - (@IDmorph R rO rI radd rmul rsub ropp req rSet reqb reqb_ok). - -Definition ring_id_eq_correct R rO rI radd rmul rsub ropp ARth reqb reqb_ok := - @ring_id_correct R rO rI radd rmul rsub ropp (@eq R) - (Eqsth R) (Eq_ext _ _ _) ARth reqb reqb_ok. - -Definition ring_rw_id_eq_correct - R rO rI radd rmul rsub ropp ARth reqb reqb_ok := - @ring_rw_id_correct R rO rI radd rmul rsub ropp (@eq R) - (Eqsth R) (Eq_ext _ _ _) ARth reqb reqb_ok. - -Definition ring_rw_id_eq_correct' - R rO rI radd rmul rsub ropp ARth reqb reqb_ok := - @ring_rw_id_correct' R rO rI radd rmul rsub ropp (@eq R) - (Eqsth R) (Eq_ext _ _ _) ARth reqb reqb_ok. - -(* -Require Import ZArith. -Require Import Setoid. -Require Import Ring_tac. -Import BinList. -Import Ring_th. -Open Scope Z_scope. - -Add New Ring Zr : (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) - Computational Zeqb_ok - Constant Zcst. - -Goal forall a b, (a+b*2)*(a+b*2)=1. -intros. - setoid ring ((a + b * 2) * (a + b * 2)). - - Make_ring_rw_list Zcst - (ring_rw_id_correct' (Eqsth Z) (Eq_ext _ _ _) - (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) - (eq (A:=Z)) - (cons ((a+b)*(a+b)) (nil _)). - - -Goal forall a b, (a+b)*(a+b)=1. -intros. -Ltac zringl := - Make_ring_rw3_list ltac:(inv_gen_phiZ 0 1 Zplus Zmult Zopp) - (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) - (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) - (eq (A:=Z)) -(BinList.cons ((a+b)*(a+b)) (BinList.nil _)). - -Open Scope Z_scope. - -let Cst_tac := inv_gen_phiZ 0 1 Zplus Zmult Zopp in -let lemma := - constr:(ring_rw_id_correct' (Eqsth Z) (Eq_ext _ _ _) - (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) in -let req := constr:(eq (A:=Z)) in -let rl := constr:(cons ((a+b)*(a+b)) (nil _)) in -Make_ring_rw_list Cst_tac lemma req rl. - -let fv := constr:(cons a (cons b (nil _))) in -let pe := - constr:(PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))) in -Make_ring_rewrite_step (lemma fv) pe. - - - - -OK - -Lemma L0 : - forall (l : list Z) (pe : PExpr Z) pe', - pe' = norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe -> - PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe = - Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe'. -intros; subst pe'. -apply - (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) - (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok). -Qed. -Lemma L0' : - forall (l : list Z) (pe : PExpr Z) pe', - norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe = pe' -> - PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe = - Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe'. -intros; subst pe'. -apply - (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) - (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok). -Qed. - -pose (pe:=PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))). -compute_assertion ipattern:H (norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe). -let fv := constr:(cons a (cons b (nil _))) in -assert (Heq := L0 fv _ (sym_equal H)); clear H. - protect_fv' in Heq. - rewrite Heq; clear Heq; clear pe. - - -MIEUX (mais taille preuve = taille de pe + taille de nf(pe)... ): - - -Lemma L : - forall (l : list Z) (pe : PExpr Z) pe' (x y :Z), - pe' = norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe -> - x = PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe -> - y = Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe' -> - x=y. -intros; subst x y pe'. -apply - (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) - (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok). -Qed. -Lemma L' : - forall (l : list Z) (pe : PExpr Z) pe' (x y :Z), - Peq Zeq_bool pe' (norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe) = true -> - x = PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe -> - y = Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe' -> - forall (P:Z->Type), P y -> P x. -intros. - rewrite L with (2:=H0) (3:=H1); trivial. -apply (Peq_ok (Eqsth Z) (Eq_ext _ _ _) - (IDmorph 0 1 Zplus Zminus Zmult Zopp (Eqsth Z) Zeq_bool Zeqb_ok) ). - - (IDmorph (Eqsth Z) (Eq_ext _ _ _) Zeqb_ok). - - - (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth)). -Qed. - -eapply L' - with (x:=(a+b)*(a+b)) - (pe:=PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))) - (l:=cons a (cons b (nil Z)));[compute;reflexivity|reflexivity|idtac|idtac];norm_evars;[protect_fv';reflexivity|idtac];norm_evars. - - - - - -set (x:=a). -set (x0:=b). -set (fv:=cons x (cons x0 (nil Z))). -let fv:=constr:(cons a (cons b (nil Z))) in -let lemma := constr : (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) - (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) in -let pe := - constr : (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))) in -assert (Heq := lemma fv pe). -set (npe:=norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool - (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2)))). -fold npe in Heq. -move npe after fv. -let fv' := eval red in fv in -compute in npe. -subst npe. -let fv' := eval red in fv in -compute_without_globals_of (fv',Zplus,0,1,Zmult,Zopp,Zminus) in Heq. -rewrite Heq. -clear Heq fv; subst x x0. - - -simpl in Heq. -unfold Pphi_dev in Heq. -unfold mult_dev in Heq. -unfold P0, Peq in *. -unfold Zeq_bool at 3, Zcompare, Pcompare in Heq. -unfold fv, hd, tl in Heq. -unfold powl, rev, rev_append in Heq. -unfold mkmult1 in Heq. -unfold mkmult in Heq. -unfold add_mult_dev in |- *. -unfold add_mult_dev at 2 in Heq. -unfold P0, Peq at 1 in Heq. -unfold Zeq_bool at 2 3 4 5 6, Zcompare, Pcompare in Heq. -unfold hd, powl, rev, rev_append in Heq. -unfold mkadd_mult in Heq. -unfold mkmult in Heq. -unfold add_mult_dev in Heq. -unfold P0, Peq in Heq. -unfold Zeq_bool, Zcompare, Pcompare in Heq. -unfold hd,powl, rev,rev_append in Heq. -unfold mkadd_mult in Heq. -unfold mkmult in Heq. -unfold IDphi in Heq. - - fv := cons x (cons x0 (nil Z)) - PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2)) - Heq : PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) fv - (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))) = - Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) fv - (norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool - (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2)))) - - -let Cst_tac := inv_gen_phiZ 0 1 Zplus Zmult Zopp in -let lemma := - constr:(ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _) - (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) in -let req := constr:(eq (A:=Z)) in -let rl := constr:(BinList.cons ((a+b)*(a+b)) (BinList.nil _)) in - match type of lemma with - forall (l:list ?R) (pe:PExpr ?C), - req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ => - Constant natcst. - - -Require Import Setoid. -Open Scope nat_scope. - -Require Import Ring_th. -Require Import Arith. - -Add New Ring natr : (SRth_ARth (Eqsth nat) natSRth) - Computational nateq_ok - Constant natcst. - - -Require Import Rbase. -Open Scope R_scope. - - Lemma Rth : ring_theory 0 1 Rplus Rmult Rminus Ropp (@eq R). - Proof. - constructor. exact Rplus_0_l. exact Rplus_comm. - intros;symmetry;apply Rplus_assoc. - exact Rmult_1_l. exact Rmult_comm. - intros;symmetry;apply Rmult_assoc. - exact Rmult_plus_distr_r. trivial. exact Rplus_opp_r. - Qed. - -Add New Ring Rr : Rth Abstract. - -Goal forall a b, (a+b*10)*(a+b*10)=1. -intros. - -Module Zring. - Import Zpol. - Import BinPos. - Import BinInt. - -Ltac is_PCst p := - match p with - | xH => true - | (xO ?p') => is_PCst p' - | (xI ?p') => is_PCst p' - | _ => false - end. - -Ltac ZCst t := - match t with - | Z0 => constr:t - | (Zpos ?p) => - match (is_PCst p) with - | false => NotConstant - | _ => constr:t - end - | (Zneg ?p) => - match (is_PCst p) with - | false => NotConstant - | _ => constr:t - end - | _ => NotConstant - end. - -Ltac zring := - Make_ring_tac ZCst - (Zpol.ring_gen_eq_correct Zth) (Zpol.ring_rw_gen_eq_correct Zth) (@eq Z). - -Ltac zrewrite := - Make_ring_rw3 ZCst (Zpol.ring_rw_gen_eq_correct Zth) (@eq Z). - -Ltac zrewrite_list := - Make_ring_rw3_list ZCst (Zpol.ring_rw_gen_eq_correct Zth) (@eq Z). - -End Zring. -*) - - - -(* -(*** Intanciation for Z*) -Require Import ZArith. -Open Scope Z_scope. - -Module Zring. - Let R := Z. - Let rO := 0. - Let rI := 1. - Let radd := Zplus. - Let rmul := Zmult. - Let rsub := Zminus. - Let ropp := Zopp. - Let Rth := Zth. - Let reqb := Zeq_bool. - Let req_morph := Zeqb_ok. - - (* CE_Entries *) - Let C := R. - Let cO := rO. - Let cI := rI. - Let cadd := radd. - Let cmul := rmul. - Let csub := rsub. - Let copp := ropp. - Let req := (@eq R). - Let ceqb := reqb. - Let phi := @IDphi R. - Let Rsth : Setoid_Theory R req := Eqsth R. - Let Reqe : ring_eq_ext radd rmul ropp req := - (@Eq_ext R radd rmul ropp). - Let ARth : almost_ring_theory rO rI radd rmul rsub ropp req := - (@Rth_ARth R rO rI radd rmul rsub ropp req Rsth Reqe Rth). - Let CRmorph : ring_morph rO rI radd rmul rsub ropp req - cO cI cadd cmul csub copp ceqb phi := - (@IDmorph R rO rI radd rmul rsub ropp req Rsth reqb req_morph). - - Definition Peq := Eval red in (Pol.Peq ceqb). - Definition mkPinj := Eval red in (@Pol.mkPinj C). - Definition mkPX := - Eval red; - change (Pol.Peq ceqb) with Peq; - change (@Pol.mkPinj Z) with mkPinj in - (Pol.mkPX cO ceqb). - - Definition P0 := Eval red in (Pol.P0 cO). - Definition P1 := Eval red in (Pol.P1 cI). - - Definition X := - Eval red; change (Pol.P0 cO) with P0; change (Pol.P1 cI) with P1 in - (Pol.X cO cI). - - Definition mkX := - Eval red; change (Pol.X cO cI) with X in - (mkX cO cI). - - Definition PaddC - Definition PaddI - Definition PaddX - - Definition Padd := - Eval red in - - (Pol.Padd cO cadd ceqb) - - Definition PmulC - Definition PmulI - Definition Pmul_aux - Definition Pmul - - Definition PsubC - Definition PsubI - Definition PsubX - Definition Psub - - - - Definition norm := - Eval red; - change (Pol.Padd cO cadd ceqb) with Padd; - change (Pol.Pmul cO cI cadd cmul ceqb) with Pmul; - change (Pol.Psub cO cadd csub copp ceqb) with Psub; - change (Pol.Popp copp) with Psub; - - in - (Pol.norm cO cI cadd cmul csub copp ceqb). - - - -End Zring. - -Ltac is_PCst p := - match p with - | xH => true - | (xO ?p') => is_PCst p' - | (xI ?p') => is_PCst p' - | _ => false - end. - -Ltac ZCst t := - match t with - | Z0 => constr:t - | (Zpos ?p) => - match (is_PCst p) with - | false => NotConstant - | _ => t - end - | (Zneg ?p) => - match (is_PCst p) with - | false => NotConstant - | _ => t - end - | _ => NotConstant - end. - -Ltac zring := - Zring.Make_ring_tac Zplus Zmult Zminus Zopp (@eq Z) ZCst. - -Ltac zrewrite := - Zring.Make_ring_rw3 Zplus Zmult Zminus Zopp ZCst. -*) - -(* -(* Instanciation for Bool *) -Require Import Bool. - -Module BCE. - Definition R := bool. - Definition rO := false. - Definition rI := true. - Definition radd := xorb. - Definition rmul := andb. - Definition rsub := xorb. - Definition ropp b:bool := b. - Lemma Rth : ring_theory rO rI radd rmul rsub ropp (@eq bool). - Proof. - constructor. - exact false_xorb. - exact xorb_comm. - intros; symmetry in |- *; apply xorb_assoc. - exact andb_true_b. - exact andb_comm. - exact andb_assoc. - destruct x; destruct y; destruct z; reflexivity. - intros; reflexivity. - exact xorb_nilpotent. - Qed. - - Definition reqb := eqb. - Definition req_morph := eqb_prop. -End BCE. - -Module BEntries := CE_Entries BCE. - -Module Bring := MakeRingPol BEntries. - -Ltac BCst t := - match t with - | true => true - | false => false - | _ => NotConstant - end. - -Ltac bring := - Bring.Make_ring_tac xorb andb xorb (fun b:bool => b) (@eq bool) BCst. - -Ltac brewrite := - Zring.Make_ring_rw3 Zplus Zmult Zminus Zopp ZCst. -*) - -(*Module Rring. - -(* Instanciation for R *) -Require Import Rbase. -Open Scope R_scope. - - Lemma Rth : ring_theory 0 1 Rplus Rmult Rminus Ropp (@eq R). - Proof. - constructor. exact Rplus_0_l. exact Rplus_comm. - intros;symmetry;apply Rplus_assoc. - exact Rmult_1_l. exact Rmult_comm. - intros;symmetry;apply Rmult_assoc. - exact Rmult_plus_distr_r. trivial. exact Rplus_opp_r. - Qed. - -Ltac RCst := inv_gen_phiZ 0 1 Rplus Rmul Ropp. - -Ltac rring := - Make_ring_tac RCst - (Zpol.ring_gen_eq_correct Rth) (Zpol.ring_rw_gen_eq_correct Rth) (@eq R). - -Ltac rrewrite := - Make_ring_rw3 RCst (Zpol.ring_rw_gen_eq_correct Rth) (@eq R). - -Ltac rrewrite_list := - Make_ring_rw3_list RCst (Zpol.ring_rw_gen_eq_correct Rth) (@eq R). - -End Rring. -*) -(************************) -(* -(* Instanciation for N *) -Require Import NArith. -Open Scope N_scope. - -Module NCSE. - Definition R := N. - Definition rO := 0. - Definition rI := 1. - Definition radd := Nplus. - Definition rmul := Nmult. - Definition SRth := Nth. - Definition reqb := Neq_bool. - Definition req_morph := Neq_bool_ok. -End NCSE. - -Module NEntries := CSE_Entries NCSE. - -Module Nring := MakeRingPol NEntries. - -Ltac NCst := inv_gen_phiN 0 1 Nplus Nmult. - -Ltac nring := - Nring.Make_ring_tac Nplus Nmult (@SRsub N Nplus) (@SRopp N) (@eq N) NCst. - -Ltac nrewrite := - Nring.Make_ring_rw3 Nplus Nmult (@SRsub N Nplus) (@SRopp N) NCst. - -(* Instanciation for nat *) -Open Scope nat_scope. - -Module NatASE. - Definition R := nat. - Definition rO := 0. - Definition rI := 1. - Definition radd := plus. - Definition rmul := mult. - Lemma SRth : semi_ring_theory O (S O) plus mult (@eq nat). - Proof. - constructor. exact plus_0_l. exact plus_comm. exact plus_assoc. - exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc. - exact mult_plus_distr_r. - Qed. -End NatASE. - -Module NatEntries := ASE_Entries NatASE. + Ltac Ring Cst_tac lemma1 req := + let Make_tac := + match type of lemma1 with + | forall (l:list ?R) (pe1 pe2:PExpr ?C), + _ = true -> + req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe1) _ => + let mkFV := FV Cst_tac add mul sub opp in + let mkPol := mkPolexpr C Cst_tac add mul sub opp in + fun f => f R mkFV mkPol + | _ => fail 1 "ring anomaly: bad correctness lemma" + end in + let Main r1 r2 R mkFV mkPol := + let fv := mkFV r1 (@List.nil R) in + let fv := mkFV r2 fv in + check_fv fv; + (let pe1 := mkPol r1 fv in + let pe2 := mkPol r2 fv in + apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring"; + vm_compute; + exact (refl_equal true) || fail "not a valid ring equation") in + Make_tac ltac:(OnEquation req Main). + +Ltac Ring_simplify Cst_tac lemma2 req rl := + let Make_tac := + match type of lemma2 with + forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C), + _ = npe -> + req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ => + let mkFV := FV Cst_tac add mul sub opp in + let mkPol := mkPolexpr C Cst_tac add mul sub opp in + let simpl_ring H := protect_fv "ring" in H in + (fun tac => tac mkFV mkPol simpl_ring lemma2 req rl) + | _ => fail 1 "ring anomaly: bad correctness lemma" + end in + Make_tac ReflexiveRewriteTactic. -Module Natring := MakeRingPol NatEntries. -Ltac natCst t := - match t with - | O => N0 - | (S ?n) => - match (natCst n) with - | NotConstant => NotConstant - | ?p => constr:(Nsucc p) - end - | _ => NotConstant - end. - -Ltac natring := - Natring.Make_ring_tac plus mult (@SRsub nat plus) (@SRopp nat) (@eq nat) natCst. +Tactic Notation (at level 0) "ring" := + ring_lookup + (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl => + pre(); Ring cst_tac lemma1 req). -Ltac natrewrite := - Natring.Make_ring_rw3 plus mult (@SRsub nat plus) (@SRopp nat) natCst. - -(* Generic tactic, checks the type of the terms and applies the -suitable instanciation*) - -Ltac newring := - match goal with - | |- (?r1 = ?r2) => - match (type of r1) with - | Z => zring - | R => rring - | bool => bring - | N => nring - | nat => natring - end - end. +Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := + ring_lookup + (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl => + pre(); Ring_simplify cst_tac lemma2 req rl; post()) rl. -*) +(* A simple macro tactic to be prefered to ring_simplify *) +Ltac ring_replace t1 t2 := replace t1 with t2 by ring. diff --git a/contrib/setoid_ring/Ring_th.v b/contrib/setoid_ring/Ring_theory.v index 9583dd2d..2f7378eb 100644 --- a/contrib/setoid_ring/Ring_th.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -1,7 +1,15 @@ -Require Import Setoid. - Set Implicit Arguments. +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +Require Import Setoid. +Set Implicit Arguments. +Module RingSyntax. Reserved Notation "x ?=! y" (at level 70, no associativity). Reserved Notation "x +! y " (at level 50, left associativity). Reserved Notation "x -! y" (at level 50, left associativity). @@ -11,14 +19,13 @@ Reserved Notation "-! x" (at level 35, right associativity). Reserved Notation "[ x ]" (at level 1, no associativity). Reserved Notation "x ?== y" (at level 70, no associativity). -Reserved Notation "x ++ y " (at level 50, left associativity). Reserved Notation "x -- y" (at level 50, left associativity). Reserved Notation "x ** y" (at level 40, left associativity). Reserved Notation "-- x" (at level 35, right associativity). Reserved Notation "x == y" (at level 70, no associativity). - - +End RingSyntax. +Import RingSyntax. Section DEFINITIONS. Variable R : Type. @@ -32,24 +39,24 @@ Section DEFINITIONS. (** Semi Ring *) Record semi_ring_theory : Prop := mk_srt { SRadd_0_l : forall n, 0 + n == n; - SRadd_sym : forall n m, n + m == m + n ; + SRadd_comm : forall n m, n + m == m + n ; SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; SRmul_1_l : forall n, 1*n == n; SRmul_0_l : forall n, 0*n == 0; - SRmul_sym : forall n m, n*m == m*n; + SRmul_comm : forall n m, n*m == m*n; SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; SRdistr_l : forall n m p, (n + m)*p == n*p + m*p }. (** Almost Ring *) -(*Almost ring are no ring : Ropp_def is missi**) +(*Almost ring are no ring : Ropp_def is missing **) Record almost_ring_theory : Prop := mk_art { ARadd_0_l : forall x, 0 + x == x; - ARadd_sym : forall x y, x + y == y + x; + ARadd_comm : forall x y, x + y == y + x; ARadd_assoc : forall x y z, x + (y + z) == (x + y) + z; ARmul_1_l : forall x, 1 * x == x; ARmul_0_l : forall x, 0 * x == 0; - ARmul_sym : forall x y, x * y == y * x; + ARmul_comm : forall x y, x * y == y * x; ARmul_assoc : forall x y z, x * (y * z) == (x * y) * z; ARdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); ARopp_mul_l : forall x y, -(x * y) == -x * y; @@ -60,10 +67,10 @@ Section DEFINITIONS. (** Ring *) Record ring_theory : Prop := mk_rt { Radd_0_l : forall x, 0 + x == x; - Radd_sym : forall x y, x + y == y + x; + Radd_comm : forall x y, x + y == y + x; Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; Rmul_1_l : forall x, 1 * x == x; - Rmul_sym : forall x y, x * y == y * x; + Rmul_comm : forall x y, x * y == y * x; Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); Rsub_def : forall x y, x - y == x + -y; @@ -193,9 +200,9 @@ Section ALMOST_RING. Lemma SRth_ARth : almost_ring_theory 0 1 radd rmul SRsub SRopp req. Proof (mk_art 0 1 radd rmul SRsub SRopp req - (SRadd_0_l SRth) (SRadd_sym SRth) (SRadd_assoc SRth) + (SRadd_0_l SRth) (SRadd_comm SRth) (SRadd_assoc SRth) (SRmul_1_l SRth) (SRmul_0_l SRth) - (SRmul_sym SRth) (SRmul_assoc SRth) (SRdistr_l SRth) + (SRmul_comm SRth) (SRmul_assoc SRth) (SRdistr_l SRth) SRopp_mul_l SRopp_add SRsub_def). (** Identity morphism for semi-ring equipped with their almost-ring structure*) @@ -246,17 +253,17 @@ Section ALMOST_RING. rewrite (Rdistr_l Rth);rewrite (Rmul_1_l Rth). rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). - rewrite (Radd_sym Rth); rewrite (Radd_0_l Rth);sreflexivity. + rewrite (Radd_comm Rth); rewrite (Radd_0_l Rth);sreflexivity. Qed. Lemma Ropp_mul_l : forall x y, -(x * y) == -x * y. Proof. intros x y;rewrite <-(Radd_0_l Rth (- x * y)). - rewrite (Radd_sym Rth). + rewrite (Radd_comm Rth). rewrite <-(Ropp_def Rth (x*y)). rewrite (Radd_assoc Rth). rewrite <- (Rdistr_l Rth). - rewrite (Rth.(Radd_sym) (-x));rewrite (Ropp_def Rth). + rewrite (Rth.(Radd_comm) (-x));rewrite (Ropp_def Rth). rewrite Rmul_0_l;rewrite (Radd_0_l Rth);sreflexivity. Qed. @@ -266,17 +273,17 @@ Section ALMOST_RING. rewrite <- ((Ropp_def Rth) x). rewrite <- ((Radd_0_l Rth) (x + - x + - (x + y))). rewrite <- ((Ropp_def Rth) y). - rewrite ((Radd_sym Rth) x). - rewrite ((Radd_sym Rth) y). + rewrite ((Radd_comm Rth) x). + rewrite ((Radd_comm Rth) y). rewrite <- ((Radd_assoc Rth) (-y)). rewrite <- ((Radd_assoc Rth) (- x)). rewrite ((Radd_assoc Rth) y). - rewrite ((Radd_sym Rth) y). + rewrite ((Radd_comm Rth) y). rewrite <- ((Radd_assoc Rth) (- x)). rewrite ((Radd_assoc Rth) y). - rewrite ((Radd_sym Rth) y);rewrite (Ropp_def Rth). - rewrite ((Radd_sym Rth) (-x) 0);rewrite (Radd_0_l Rth). - apply (Radd_sym Rth). + rewrite ((Radd_comm Rth) y);rewrite (Ropp_def Rth). + rewrite ((Radd_comm Rth) (-x) 0);rewrite (Radd_0_l Rth). + apply (Radd_comm Rth). Qed. Lemma Ropp_opp : forall x, - -x == x. @@ -284,13 +291,13 @@ Section ALMOST_RING. intros x; rewrite <- (Radd_0_l Rth (- -x)). rewrite <- (Ropp_def Rth x). rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). - rewrite ((Radd_sym Rth) x);apply (Radd_0_l Rth). + rewrite ((Radd_comm Rth) x);apply (Radd_0_l Rth). Qed. Lemma Rth_ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. Proof - (mk_art 0 1 radd rmul rsub ropp req (Radd_0_l Rth) (Radd_sym Rth) (Radd_assoc Rth) - (Rmul_1_l Rth) Rmul_0_l (Rmul_sym Rth) (Rmul_assoc Rth) (Rdistr_l Rth) + (mk_art 0 1 radd rmul rsub ropp req (Radd_0_l Rth) (Radd_comm Rth) (Radd_assoc Rth) + (Rmul_1_l Rth) Rmul_0_l (Rmul_comm Rth) (Rmul_assoc Rth) (Rdistr_l Rth) Ropp_mul_l Ropp_add (Rsub_def Rth)). (** Every semi morphism between two rings is a morphism*) @@ -315,12 +322,12 @@ Section ALMOST_RING. Proof. intros x;rewrite <- (Rth.(Radd_0_l) [-!x]). rewrite <- ((Ropp_def Rth) [x]). - rewrite ((Radd_sym Rth) [x]). + rewrite ((Radd_comm Rth) [x]). rewrite <- (Radd_assoc Rth). rewrite <- (Smorph_add Smorph). rewrite (Ropp_def Cth). rewrite (Smorph0 Smorph). - rewrite (Radd_sym Rth (-[x])). + rewrite (Radd_comm Rth (-[x])). apply (Radd_0_l Rth);sreflexivity. Qed. @@ -343,6 +350,12 @@ Section ALMOST_RING. (** Usefull lemmas on almost ring *) Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. + Lemma ARth_SRth : semi_ring_theory 0 1 radd rmul req. +Proof. +elim ARth; intros. +constructor; trivial. +Qed. + Lemma ARsub_ext : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2. Proof. @@ -358,15 +371,15 @@ Section ALMOST_RING. Ltac mrewrite := repeat first [ rewrite (ARadd_0_l ARth) - | rewrite <- ((ARadd_sym ARth) 0) + | rewrite <- ((ARadd_comm ARth) 0) | rewrite (ARmul_1_l ARth) - | rewrite <- ((ARmul_sym ARth) 1) + | rewrite <- ((ARmul_comm ARth) 1) | rewrite (ARmul_0_l ARth) - | rewrite <- ((ARmul_sym ARth) 0) + | rewrite <- ((ARmul_comm ARth) 0) | rewrite (ARdistr_l ARth) | sreflexivity | match goal with - | |- context [?z * (?x + ?y)] => rewrite ((ARmul_sym ARth) z (x+y)) + | |- context [?z * (?x + ?y)] => rewrite ((ARmul_comm ARth) z (x+y)) end]. Lemma ARadd_0_r : forall x, (x + 0) == x. @@ -381,37 +394,37 @@ Section ALMOST_RING. Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y. Proof. intros;mrewrite. - repeat rewrite (ARth.(ARmul_sym) z);sreflexivity. + repeat rewrite (ARth.(ARmul_comm) z);sreflexivity. Qed. Lemma ARadd_assoc1 : forall x y z, (x + y) + z == (y + z) + x. Proof. intros;rewrite <-(ARth.(ARadd_assoc) x). - rewrite (ARth.(ARadd_sym) x);sreflexivity. + rewrite (ARth.(ARadd_comm) x);sreflexivity. Qed. Lemma ARadd_assoc2 : forall x y z, (y + x) + z == (y + z) + x. Proof. intros; repeat rewrite <- (ARadd_assoc ARth); - rewrite ((ARadd_sym ARth) x); sreflexivity. + rewrite ((ARadd_comm ARth) x); sreflexivity. Qed. Lemma ARmul_assoc1 : forall x y z, (x * y) * z == (y * z) * x. Proof. intros;rewrite <-((ARmul_assoc ARth) x). - rewrite ((ARmul_sym ARth) x);sreflexivity. + rewrite ((ARmul_comm ARth) x);sreflexivity. Qed. Lemma ARmul_assoc2 : forall x y z, (y * x) * z == (y * z) * x. Proof. intros; repeat rewrite <- (ARmul_assoc ARth); - rewrite ((ARmul_sym ARth) x); sreflexivity. + rewrite ((ARmul_comm ARth) x); sreflexivity. Qed. Lemma ARopp_mul_r : forall x y, - (x * y) == x * -y. Proof. - intros;rewrite ((ARmul_sym ARth) x y); - rewrite (ARopp_mul_l ARth); apply (ARmul_sym ARth). + intros;rewrite ((ARmul_comm ARth) x y); + rewrite (ARopp_mul_l ARth); apply (ARmul_comm ARth). Qed. Lemma ARopp_zero : -0 == 0. @@ -420,8 +433,37 @@ Section ALMOST_RING. repeat rewrite ARmul_0_r; sreflexivity. Qed. + + End ALMOST_RING. +Section AddRing. + + Variable R : Type. + Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + +Inductive ring_kind : Type := +| Abstract +| Computational + (R:Type) + (req : R -> R -> Prop) + (reqb : R -> R -> bool) + (_ : forall x y, (reqb x y) = true -> req x y) +| Morphism + (R : Type) + (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R) + (req : R -> R -> Prop) + (C : Type) + (cO cI : C) (cadd cmul csub : C->C->C) (copp : C->C) + (ceqb : C->C->bool) + phi + (_ : ring_morph rO rI radd rmul rsub ropp req + cO cI cadd cmul csub copp ceqb phi). + +End AddRing. + + (** Some simplification tactics*) Ltac gen_reflexivity Rsth := apply (Seq_refl _ _ Rsth). diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v new file mode 100644 index 00000000..4f47fff0 --- /dev/null +++ b/contrib/setoid_ring/ZArithRing.v @@ -0,0 +1,33 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Export Ring. +Require Import ZArith_base. +Import InitialRing. + +Set Implicit Arguments. + +Ltac isZcst t := + let t := eval hnf in t in + match t with + Z0 => constr:true + | Zpos ?p => isZcst p + | Zneg ?p => isZcst p + | xI ?p => isZcst p + | xO ?p => isZcst p + | xH => constr:true + | _ => constr:false + end. +Ltac Zcst t := + match isZcst t with + true => t + | _ => NotConstant + end. + +Add Ring Zr : Zth + (decidable Zeqb_ok, constants [Zcst], preprocess [unfold Zsucc]). diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index bc2bcb0c..daa2fedb 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: newring.ml4 8878 2006-05-30 16:44:25Z herbelin $ i*) +(*i $Id: newring.ml4 9302 2006-10-27 21:21:17Z barras $ i*) open Pp open Util @@ -16,6 +16,7 @@ open Names open Term open Closure open Environ +open Libnames open Tactics open Rawterm open Tacticals @@ -27,139 +28,53 @@ open Setoid_replace open Proof_type open Coqlib open Tacmach -open Ppconstr open Mod_subst open Tacinterp open Libobject open Printer - -(****************************************************************************) -(* Library linking *) - -let contrib_name = "setoid_ring" - - -let ring_dir = ["Coq";contrib_name] -let setoids_dir = ["Coq";"Setoids"] -let ring_modules = - [ring_dir@["BinList"];ring_dir@["Ring_th"];ring_dir@["Pol"]; - ring_dir@["Ring_tac"];ring_dir@["ZRing_th"]] -let stdlib_modules = [setoids_dir@["Setoid"]] - -let coq_constant c = - lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c) -let ring_constant c = - lazy (Coqlib.gen_constant_in_modules "Ring" ring_modules c) -let ringtac_constant m c = - lazy (Coqlib.gen_constant_in_modules "Ring" [ring_dir@["ZRing_th";m]] c) - -let new_ring_path = - make_dirpath (List.map id_of_string ["Ring_tac";contrib_name;"Coq"]) -let ltac s = - lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s)) -let znew_ring_path = - make_dirpath (List.map id_of_string ["ZRing_th";contrib_name;"Coq"]) -let zltac s = - lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s)) -let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c) - -let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);; -let pol_cst s = mk_cst [contrib_name;"Pol"] s ;; - -let ic c = - let env = Global.env() and sigma = Evd.empty in - Constrintern.interp_constr sigma env c - - -(* Ring theory *) - -(* almost_ring defs *) -let coq_almost_ring_theory = ring_constant "almost_ring_theory" -let coq_ring_lemma1 = ring_constant "ring_correct" -let coq_ring_lemma2 = ring_constant "Pphi_dev_ok'" -let ring_comp1 = ring_constant "ring_id_correct" -let ring_comp2 = ring_constant "ring_rw_id_correct'" -let ring_abs1 = ringtac_constant "Zpol" "ring_gen_correct" -let ring_abs2 = ringtac_constant "Zpol" "ring_rw_gen_correct'" -let sring_abs1 = ringtac_constant "Npol" "ring_gen_correct" -let sring_abs2 = ringtac_constant "Npol" "ring_rw_gen_correct'" - -(* setoid and morphism utilities *) -let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" -let coq_eq_setoid = ring_constant "Eqsth" -let coq_eq_morph = ring_constant "Eq_ext" - -(* ring -> almost_ring utilities *) -let coq_ring_theory = ring_constant "ring_theory" -let coq_ring_morph = ring_constant "ring_morph" -let coq_Rth_ARth = ring_constant "Rth_ARth" -let coq_mk_reqe = ring_constant "mk_reqe" - -(* semi_ring -> almost_ring utilities *) -let coq_semi_ring_theory = ring_constant "semi_ring_theory" -let coq_SRth_ARth = ring_constant "SRth_ARth" -let coq_sring_morph = ring_constant "semi_morph" -let coq_SRmorph_Rmorph = ring_constant "SRmorph_Rmorph" -let coq_mk_seqe = ring_constant "mk_seqe" -let coq_SRsub = ring_constant "SRsub" -let coq_SRopp = ring_constant "SRopp" -let coq_SReqe_Reqe = ring_constant "SReqe_Reqe" - -let ltac_setoid_ring = ltac"Make_ring_tac" -let ltac_setoid_ring_rewrite = ltac"Make_ring_rw_list" -let ltac_inv_morphZ = zltac"inv_gen_phiZ" -let ltac_inv_morphN = zltac"inv_gen_phiN" - -let coq_cons = ring_constant "cons" -let coq_nil = ring_constant "nil" - -let lapp f args = mkApp(Lazy.force f,args) - -let dest_rel t = - match kind_of_term t with - App(f,args) when Array.length args >= 2 -> - mkApp(f,Array.sub args 0 (Array.length args - 2)) - | _ -> failwith "cannot find relation" +open Declare +open Decl_kinds +open Entries (****************************************************************************) (* controlled reduction *) -let mark_arg i c = mkEvar(i,[|c|]);; +let mark_arg i c = mkEvar(i,[|c|]) let unmark_arg f c = match destEvar c with | (i,[|c|]) -> f i c - | _ -> assert false;; + | _ -> assert false -type protect_flag = Eval|Prot|Rec ;; +type protect_flag = Eval|Prot|Rec -let tag_arg tag_rec map i c = +let tag_arg tag_rec map subs i c = match map i with - Eval -> inject c + Eval -> mk_clos subs c | Prot -> mk_atom c - | Rec -> if i = -1 then inject c else tag_rec c + | Rec -> if i = -1 then mk_clos subs c else tag_rec c -let rec mk_clos_but f_map t = +let rec mk_clos_but f_map subs t = match f_map t with - | Some map -> tag_arg (mk_clos_but f_map) map (-1) t + | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t | None -> (match kind_of_term t with - App(f,args) -> mk_clos_app_but f_map f args 0 - (* unspecified constants are evaluated *) - | _ -> inject t) + App(f,args) -> mk_clos_app_but f_map subs f args 0 + | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t + | _ -> mk_atom t) -and mk_clos_app_but f_map f args n = - if n >= Array.length args then inject(mkApp(f, args)) +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 f' = mkApp(f,fargs) in match f_map f' with Some map -> mk_clos_deep - (fun _ -> unmark_arg (tag_arg (mk_clos_but f_map) map)) - (Esubst.ESID 0) + (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s')) + subs (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) - | None -> mk_clos_app_but f_map f args (n+1) -;; + | None -> mk_clos_app_but f_map subs f args (n+1) + let interp_map l c = try @@ -174,98 +89,320 @@ let interp_map l c = let interp_map l t = try Some(List.assoc t l) with Not_found -> None -let arg_map = - [mk_cst [contrib_name;"BinList"] "cons",(function -1->Eval|2->Rec|_->Prot); - mk_cst [contrib_name;"BinList"] "nil", (function -1->Eval|_ -> Prot); - (* Pphi_dev: evaluate polynomial and coef operations, protect - ring operations and make recursive call on morphism and var map *) - pol_cst "Pphi_dev", (function -1|6|7|8|11->Eval|9|10->Rec|_->Prot); - (* PEeval: evaluate polynomial, protect ring operations - and make recursive call on morphism and var map *) - pol_cst "PEeval", (function -1|9->Eval|7|8->Rec|_->Prot); - (* Do not evaluate ring operations... *) - ring_constant "gen_phiZ", (function -1|6->Eval|_->Prot); - ring_constant "gen_phiN", (function -1|5->Eval|_->Prot); -];; +let protect_maps = ref ([]:(string*(constr->'a)) list) +let add_map s m = protect_maps := (s,m) :: !protect_maps +let lookup_map map = + try List.assoc map !protect_maps + with Not_found -> + errorlabstrm"lookup_map"(str"map "++qs map++str"not found") -(* Equality: do not evaluate but make recursive call on both sides *) -let is_ring_thm req = - interp_map - ((req,(function -1->Prot|_->Rec)):: - List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) -;; - -let protect_red env sigma c = - let req = dest_rel c in +let protect_red map env sigma c = kl (create_clos_infos betadeltaiota env) - (mk_clos_but (is_ring_thm req) c);; + (mk_clos_but (lookup_map map c) (Esubst.ESID 0) c);; -let protect_tac = - Tactics.reduct_option (protect_red,DEFAULTcast) None ;; +let protect_tac map = + Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; -let protect_tac_in id = - Tactics.reduct_option (protect_red,DEFAULTcast) (Some(([],id),InHyp));; +let protect_tac_in map id = + Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(([],id),InHyp));; TACTIC EXTEND protect_fv - [ "protect_fv" "in" ident(id) ] -> - [ protect_tac_in id ] -| [ "protect_fv" ] -> - [ protect_tac ] + [ "protect_fv" string(map) "in" ident(id) ] -> + [ protect_tac_in map id ] +| [ "protect_fv" string(map) ] -> + [ protect_tac map ] END;; (****************************************************************************) -(* Ring database *) + +let closed_term t l = + let l = List.map 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 ] +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]))) +*) +let closed_term_ast l = + let l = List.map (fun gr -> ArgArg(dummy_loc,gr)) l in + TacFun([Some(id_of_string"t")], + TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term", + [Genarg.in_gen Genarg.globwit_constr (RVar(dummy_loc,id_of_string"t"),None); + Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l]))) +(* +let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term" +*) + +(****************************************************************************) + +let ic c = + let env = Global.env() and sigma = Evd.empty in + Constrintern.interp_constr sigma env 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_type = None; + const_entry_opaque = true; + const_entry_boxed = true}, + IsProof Lemma)) + +let ltac_call tac args = + TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) + +let ltac_lcall tac args = + TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) + +let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c) + +let dummy_goal env = + {Evd.it= + {Evd.evar_concl=mkProp; + Evd.evar_hyps=named_context_val env; + Evd.evar_body=Evd.Evar_empty; + Evd.evar_extra=None}; + Evd.sigma=Evd.empty} + +let exec_tactic env n f args = + let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in + let res = ref [||] in + let get_res ist = + let l = List.map (fun id -> List.assoc 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" + +let stdlib_modules = + [["Coq";"Setoids";"Setoid"]; + ["Coq";"Lists";"List"] + ] + +let coq_constant c = + lazy (Coqlib.gen_constant_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 lapp f args = mkApp(Lazy.force f,args) + +let rec dest_rel t = + match kind_of_term t with + App(f,args) when Array.length args >= 2 -> + let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in + if closed0 rel then + (rel,args.(Array.length args - 2),args.(Array.length args - 1)) + else error "ring: cannot find relation (not closed)" + | Prod(_,_,c) -> dest_rel c + | _ -> error "ring: cannot find relation" + +(****************************************************************************) +(* Library linking *) + +let contrib_name = "setoid_ring" + +let cdir = ["Coq";contrib_name] +let contrib_modules = + List.map (fun d -> cdir@d) + [["Ring_theory"];["Ring_polynom"]; ["Ring_tac"];["InitialRing"]; + ["Field_tac"]; ["Field_theory"] + ] + +let my_constant c = + lazy (Coqlib.gen_constant_in_modules "Ring" contrib_modules c) + +let new_ring_path = + make_dirpath (List.map id_of_string ["Ring_tac";contrib_name;"Coq"]) +let ltac s = + lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s)) +let znew_ring_path = + make_dirpath (List.map id_of_string ["InitialRing";contrib_name;"Coq"]) +let zltac s = + lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s)) + +let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);; +let pol_cst s = mk_cst [contrib_name;"Ring_polynom"] s ;; + +(* Ring theory *) + +(* almost_ring defs *) +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" + +(* ring -> almost_ring utilities *) +let coq_ring_theory = my_constant "ring_theory" +let coq_mk_reqe = my_constant "mk_reqe" + +(* semi_ring -> almost_ring utilities *) +let coq_semi_ring_theory = my_constant "semi_ring_theory" +let coq_mk_seqe = my_constant "mk_seqe" + +let ltac_inv_morphZ = zltac"inv_gen_phiZ" +let ltac_inv_morphN = zltac"inv_gen_phiN" + +let coq_abstract = my_constant"Abstract" +let coq_comp = my_constant"Computational" +let coq_morph = my_constant"Morphism" + +(* 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)):: + 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); + coq_nil, (function -1->Eval|_ -> Prot); + (* Pphi_dev: evaluate polynomial and coef operations, protect + ring operations and make recursive call on the var map *) + pol_cst "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->Rec|_->Prot); + (* PEeval: evaluate morphism and polynomial, protect ring + operations and make recursive call on the var map *) + pol_cst "PEeval", (function -1|7|9->Eval|8->Rec|_->Prot)]) + +(****************************************************************************) +(* Ring database *) type ring_info = { ring_carrier : types; ring_req : constr; + ring_setoid : constr; + ring_ext : constr; + ring_morph : constr; + ring_th : constr; ring_cst_tac : glob_tactic_expr; ring_lemma1 : constr; - ring_lemma2 : constr } + ring_lemma2 : constr; + ring_pre_tac : glob_tactic_expr; + ring_post_tac : glob_tactic_expr } module Cmap = Map.Make(struct type t = constr let compare = compare end) let from_carrier = ref Cmap.empty let from_relation = ref Cmap.empty +let from_name = ref Spmap.empty + +let ring_for_carrier r = Cmap.find r !from_carrier +let ring_for_relation rel = Cmap.find rel !from_relation +let ring_lookup_by_name ref = + Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) !from_name + + +let find_ring_structure env sigma l cl oname = + match oname, l with + Some rf, _ -> + (try ring_lookup_by_name rf + with Not_found -> + errorlabstrm "ring" + (str "found no ring named "++pr_reference rf)) + | None, t::cl' -> + let ty = Retyping.get_type_of env sigma t in + let check c = + let ty' = Retyping.get_type_of env sigma c in + if not (Reductionops.is_conv env sigma ty ty') then + errorlabstrm "ring" + (str"arguments of ring_simplify do not have all the same type") + in + List.iter check cl'; + (try ring_for_carrier ty + with Not_found -> + errorlabstrm "ring" + (str"cannot find a declared ring structure over"++ + spc()++str"\""++pr_constr ty++str"\"")) + | None, [] -> + 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); + { Summary.freeze_function = + (fun () -> !from_carrier,!from_relation,!from_name); Summary.unfreeze_function = - (fun (ct,rt) -> from_carrier := ct; from_relation := rt); + (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); + (fun () -> + from_carrier := Cmap.empty; from_relation := Cmap.empty; + from_name := Spmap.empty); Summary.survive_module = false; Summary.survive_section = false } -let add_entry _ e = - let _ = ty e.ring_lemma1 in +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_relation := Cmap.add e.ring_req e !from_relation; + from_name := Spmap.add sp e !from_name let subst_th (_,subst,th) = let c' = subst_mps subst th.ring_carrier in let eq' = subst_mps subst th.ring_req in + let set' = subst_mps subst th.ring_setoid in + let ext' = subst_mps subst th.ring_ext in + let morph' = subst_mps subst th.ring_morph in + 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 pretac'= subst_tactic subst th.ring_pre_tac in + let posttac'= subst_tactic subst th.ring_post_tac in if c' == th.ring_carrier && eq' == th.ring_req && + set' = th.ring_setoid && + ext' == th.ring_ext && + morph' == th.ring_morph && + th' == th.ring_th && thm1' == th.ring_lemma1 && thm2' == th.ring_lemma2 && - tac' == th.ring_cst_tac then th + tac' == th.ring_cst_tac && + pretac' == th.ring_pre_tac && + posttac' == th.ring_post_tac then th else { ring_carrier = c'; ring_req = eq'; + ring_setoid = set'; + ring_ext = ext'; + ring_morph = morph'; + ring_th = th'; ring_cst_tac = tac'; ring_lemma1 = thm1'; - ring_lemma2 = thm2' } + ring_lemma2 = thm2'; + ring_pre_tac = pretac'; + ring_post_tac = posttac' } let (theory_to_obj, obj_to_theory) = @@ -280,10 +417,6 @@ let (theory_to_obj, obj_to_theory) = export_function = export_th } -let ring_for_carrier r = Cmap.find r !from_carrier - -let ring_for_relation rel = Cmap.find rel !from_relation - let setoid_of_relation r = lapp coq_mk_Setoid [|r.rel_a; r.rel_aeq; @@ -293,43 +426,19 @@ let op_morph r add mul opp req m1 m2 m3 = lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] let op_smorph r add mul req m1 m2 = - lapp coq_SReqe_Reqe - [| r;add;mul;req;lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]|] - -let sr_sub r add = lapp coq_SRsub [|r;add|] -let sr_opp r = lapp coq_SRopp [|r|] + lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |] -let dest_morphism kind th sth = - let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th in - match kind_of_term th_typ with - App(f,[|_;_;_;_;_;_;_;_;c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) - when f = Lazy.force coq_ring_morph -> - (th,[|c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) - | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) - when f = Lazy.force coq_sring_morph && kind=Some true-> - let th = - lapp coq_SRmorph_Rmorph - [|r;zero;one;add;mul;req;sth;c;czero;cone;cadd;cmul;ceqb;phi;th|]in - (th,[|c;czero;cone;cadd;cmul;cadd;sr_opp c;ceqb;phi|]) - | _ -> failwith "bad ring_morph lemma" - -let dest_eq_test th = - let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th in - match decompose_prod th_typ with - (_,h)::_,_ -> - (match snd(destApplication h) with - [|_;lhs;_|] -> fst(destApplication lhs) - | _ -> failwith "bad lemma for decidability of equality") - | _ -> failwith "bad lemma for decidability of equality" - -let default_ring_equality is_semi (r,add,mul,opp,req) = +let default_ring_equality (r,add,mul,opp,req) = let is_setoid = function {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true | _ -> false in match default_relation_for_carrier ~filter:is_setoid r with Leibniz _ -> let setoid = lapp coq_eq_setoid [|r|] in - let op_morph = lapp coq_eq_morph [|r;add;mul;opp|] 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 (setoid,op_morph) | Relation rel -> let setoid = setoid_of_relation rel in @@ -347,8 +456,12 @@ let default_ring_equality is_semi (r,add,mul,opp,req) = with Not_found -> error "ring multiplication should be declared as a morphism" in let op_morph = - if is_semi <> Some true then - (let opp_m = default_morphism ~filter:is_endomorphism opp in + match opp with + | Some opp -> + (let opp_m = + try default_morphism ~filter:is_endomorphism opp + with Not_found -> + error "ring opposite should be declared as a morphism" in let op_morph = op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in msgnl @@ -358,7 +471,7 @@ let default_ring_equality is_semi (r,add,mul,opp,req) = str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ str"\""); op_morph) - else + | None -> (msgnl (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ str"and morphisms \""++pr_constr add_m.morphism_theory++ @@ -367,159 +480,475 @@ let default_ring_equality is_semi (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 is_semi r add mul opp req eqth = +let build_setoid_params r add mul opp req eqth = match eqth with Some th -> th - | None -> default_ring_equality is_semi (r,add,mul,opp,req) + | None -> default_ring_equality (r,add,mul,opp,req) -let dest_ring th_spec = - let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th_spec in +let dest_ring env sigma th_spec = + let th_typ = Retyping.get_type_of env sigma th_spec in match kind_of_term th_typ with App(f,[|r;zero;one;add;mul;sub;opp;req|]) when f = Lazy.force coq_almost_ring_theory -> - (None,r,zero,one,add,mul,sub,opp,req) + (None,r,zero,one,add,mul,Some sub,Some opp,req) | App(f,[|r;zero;one;add;mul;req|]) when f = Lazy.force coq_semi_ring_theory -> - (Some true,r,zero,one,add,mul,sr_sub r add,sr_opp r,req) + (Some true,r,zero,one,add,mul,None,None,req) | App(f,[|r;zero;one;add;mul;sub;opp;req|]) when f = Lazy.force coq_ring_theory -> - (Some false,r,zero,one,add,mul,sub,opp,req) + (Some false,r,zero,one,add,mul,Some sub,Some opp,req) | _ -> error "bad ring structure" -let build_almost_ring kind r zero one add mul sub opp req sth morph th = - match kind with - None -> th - | Some true -> - lapp coq_SRth_ARth [|r;zero;one;add;mul;req;sth;th|] - | Some false -> - lapp coq_Rth_ARth [|r;zero;one;add;mul;sub;opp;req;sth;morph;th|] - type coeff_spec = Computational of constr (* equality test *) | Abstract (* coeffs = Z *) | Morphism of constr (* general morphism *) + +let reflect_coeff rkind = + (* We build an ill-typed terms on purpose... *) + match rkind with + Abstract -> Lazy.force coq_abstract + | Computational c -> lapp coq_comp [|c|] + | Morphism m -> lapp coq_morph [|m|] + type cst_tac_spec = CstTac of raw_tactic_expr - | Closed of constr list - - -let add_theory name rth eqth morphth cst_tac = - Coqlib.check_required_library ["Coq";"setoid_ring";"Ring_tac"]; - let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring rth in - let (sth,morph) = build_setoid_params kind r add mul opp req eqth in - let args0 = [|r;zero;one;add;mul;sub;opp;req;sth;morph|] in - let (lemma1,lemma2) = - match morphth with - | Computational c -> - let reqb = dest_eq_test c in - let rth = - build_almost_ring - kind r zero one add mul sub opp req sth morph rth in - let args = Array.append args0 [|rth;reqb;c|] in - (lapp ring_comp1 args, lapp ring_comp2 args) - | Morphism m -> - let (m,args1) = dest_morphism kind m sth in - let rth = - build_almost_ring - kind r zero one add mul sub opp req sth morph rth in - let args = Array.concat [args0;[|rth|]; args1; [|m|]] in - (lapp coq_ring_lemma1 args, lapp coq_ring_lemma2 args) - | Abstract -> - Coqlib.check_required_library ["Coq";"setoid_ring";"ZRing_th"]; - let args1 = Array.append args0 [|rth|] in - (match kind with - None -> error "an almost_ring cannot be abstract" - | Some true -> - (lapp sring_abs1 args1, lapp sring_abs2 args1) - | Some false -> - (lapp ring_abs1 args1, lapp ring_abs2 args1)) in - let cst_tac = match cst_tac with + | Closed of reference list + +let interp_cst_tac kind (zero,one,add,mul,opp) cst_tac = + match cst_tac with Some (CstTac t) -> Tacinterp.glob_tactic t - | Some (Closed lc) -> failwith "TODO" + | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc) | None -> - (match kind with - Some true -> + (match opp, kind with + None, _ -> let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) - | Some false -> + | Some opp, Some _ -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) - | _ -> error"a tactic must be specified for an almost_ring") in + | _ -> error"a tactic must be specified for an almost_ring") + +let add_theory name rth eqth morphth cst_tac (pre,post) = + 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 rk = reflect_coeff morphth in + let params = + exec_tactic env 5 (zltac"ring_lemmas") (List.map carg[sth;ext;rth;rk]) in + let lemma1 = constr_of params.(3) in + let lemma2 = constr_of 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 cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in + let pretac = + match pre with + Some t -> Tacinterp.glob_tactic t + | _ -> TacId [] in + let posttac = + match post with + Some t -> Tacinterp.glob_tactic t + | _ -> TacId [] in let _ = Lib.add_leaf name (theory_to_obj { 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_cst_tac = cst_tac; ring_lemma1 = lemma1; - ring_lemma2 = lemma2 }) in + ring_lemma2 = lemma2; + ring_pre_tac = pretac; + ring_post_tac = posttac }) in () -VERNAC ARGUMENT EXTEND ring_coefs -| [ "Computational" constr(c)] -> [ Computational (ic c) ] -| [ "Abstract" ] -> [ Abstract ] -| [ "Coefficients" constr(m)] -> [ Morphism (ic m) ] -| [ ] -> [ Abstract ] +type ring_mod = + Ring_kind of 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 + +VERNAC ARGUMENT EXTEND ring_mod + | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic eq_test)) ] + | [ "abstract" ] -> [ Ring_kind Abstract ] + | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic 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 ] + | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ] + | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] END -VERNAC ARGUMENT EXTEND ring_cst_tac -| [ "Constant" tactic(c)] -> [ Some(CstTac c) ] -| [ "[" ne_constr_list(l) "]" ] -> [ Some(Closed (List.map ic l)) ] -| [ ] -> [ None ] -END +let set_once s r v = + if !r = None then r := Some v else error (s^" cannot be set twice") + +let process_ring_mods l = + let kind = ref None in + let set = ref None in + let cst_tac = ref None in + let pre = ref None in + let post = ref None in + List.iter(function + Ring_kind k -> set_once "ring kind" kind 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)) l; + let k = match !kind with Some k -> k | None -> Abstract in + (k, !set, !cst_tac, !pre, !post) VERNAC COMMAND EXTEND AddSetoidRing -| [ "Add" "New" "Ring" ident(id) ":" constr(t) ring_coefs(c) - "Setoid" constr(e) constr(m) ring_cst_tac(tac) ] -> - [ add_theory id (ic t) (Some (ic e, ic m)) c tac ] -| [ "Add" "New" "Ring" ident(id) ":" constr(t) ring_coefs(c) - ring_cst_tac(tac) ] -> - [ add_theory id (ic t) None c tac ] + | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> + [ let (k,set,cst,pre,post) = process_ring_mods l in + add_theory id (ic t) set k cst (pre,post) ] END - (*****************************************************************************) (* The tactics consist then only in a lookup in the ring database and call the appropriate ltac. *) -let ring gl = - let req = dest_rel (pf_concl gl) in - let e = - 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"\"") in - Tacinterp.eval_tactic - (TacArg(TacCall(dummy_loc, - ArgArg(dummy_loc, Lazy.force ltac_setoid_ring), - Tacexp e.ring_cst_tac:: - List.map carg [e.ring_lemma1;e.ring_lemma2;e.ring_req]))) - gl - -let ring_rewrite rl = - let ty = Retyping.get_type_of (Global.env()) Evd.empty (List.hd rl) in - let e = - try ring_for_carrier ty - with Not_found -> - errorlabstrm "ring" - (str"cannot find a declared ring structure over"++ - spc()++str"\""++pr_constr ty++str"\"") in - let rl = List.fold_right (fun x l -> lapp coq_cons [|ty;x;l|]) rl - (lapp coq_nil [|ty|]) in +let make_term_list carrier rl gl = + let rl = + match rl with + [] -> let (_,t1,t2) = dest_rel (pf_concl gl) in [t1;t2] + | _ -> rl in + List.fold_right + (fun x l -> lapp coq_cons [|carrier;x;l|]) rl + (lapp coq_nil [|carrier|]) + +let ring_lookup (f:glob_tactic_expr) rl gl = + let env = pf_env gl in + let sigma = project gl in + let e = find_ring_structure env sigma rl (pf_concl gl) None in + let rl = carg (make_term_list e.ring_carrier rl gl) in + let req = carg e.ring_req in + let sth = carg e.ring_setoid in + let ext = carg e.ring_ext in + let morph = carg e.ring_morph in + let th = carg e.ring_th in + let cst_tac = Tacexp e.ring_cst_tac in + let lemma1 = carg e.ring_lemma1 in + let lemma2 = carg e.ring_lemma2 in + let pretac = Tacexp(TacFun([None],e.ring_pre_tac)) in + let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in Tacinterp.eval_tactic - (TacArg(TacCall(dummy_loc, - ArgArg(dummy_loc, Lazy.force ltac_setoid_ring_rewrite), - Tacexp e.ring_cst_tac::List.map carg [e.ring_lemma2;e.ring_req;rl]))) + (TacLetIn + ([(dummy_loc,id_of_string"f"),None,Tacexp f], + ltac_lcall "f" + [req;sth;ext;morph;th;cst_tac;lemma1;lemma2;pretac;posttac;rl])) gl + +TACTIC EXTEND ring_lookup +| [ "ring_lookup" tactic(f) constr_list(l) ] -> [ ring_lookup (fst f) l ] +END + +(***********************************************************************) + +let new_field_path = + make_dirpath (List.map id_of_string ["Field_tac";contrib_name;"Coq"]) + +let field_ltac s = + lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s)) + + +let _ = add_map "field" + (map_with_eq + [coq_cons,(function -1->Eval|2->Rec|_->Prot); + 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", + (function -1|7|8|9|10|12|13->Eval|11->Rec|_->Prot); + (* Pphi_dev: evaluate polynomial and coef operations, protect + ring operations and make recursive call on the var map *) + my_constant "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->Rec|_->Prot); + (* PEeval: evaluate morphism and polynomial, protect ring + operations and make recursive call on the var map *) + my_constant "FEeval", (function -1|9|11->Eval|10->Rec|_->Prot)]);; + + +let _ = add_map "field_cond" + (map_with_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->Eval|9->Rec|_->Prot)]);; + + +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 + match kind_of_term th_typ with + | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) + when f = Lazy.force afield_theory -> + let rth = lapp af_ar + [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in + (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) + | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) + when f = Lazy.force field_theory -> + let rth = + lapp f_r + [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in + (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) + | App(f,[|r;zero;one;add;mul;div;inv;req|]) + when f = Lazy.force sfield_theory -> + let rth = lapp sf_sr + [|r;zero;one;add;mul;div;inv;req;th_spec|] in + (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) + | _ -> error "bad field structure" + +type field_info = + { field_carrier : types; + field_req : constr; + field_cst_tac : glob_tactic_expr; + field_ok : constr; + field_simpl_eq_ok : constr; + field_simpl_ok : constr; + field_cond : constr; + 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_for_carrier r = Cmap.find r !field_from_carrier +let field_for_relation rel = Cmap.find rel !field_from_relation +let field_lookup_by_name ref = + Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) + !field_from_name + + +let find_field_structure env sigma l cl oname = + check_required_library (cdir@["Field_tac"]); + match oname, l with + Some rf, _ -> + (try field_lookup_by_name rf + with Not_found -> + errorlabstrm "field" + (str "found no field named "++pr_reference rf)) + | None, t::cl' -> + let ty = Retyping.get_type_of env sigma t in + let check c = + let ty' = Retyping.get_type_of env sigma c in + if not (Reductionops.is_conv env sigma ty ty') then + errorlabstrm "field" + (str"arguments of field_simplify do not have all the same type") + in + List.iter check cl'; + (try field_for_carrier ty + with Not_found -> + errorlabstrm "field" + (str"cannot find a declared field structure over"++ + spc()++str"\""++pr_constr ty++str"\"")) + | None, [] -> + 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); + Summary.survive_module = false; + Summary.survive_section = false } + +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) = + let c' = subst_mps subst th.field_carrier in + let eq' = subst_mps subst th.field_req in + let thm1' = subst_mps subst th.field_ok in + let thm2' = subst_mps subst th.field_simpl_eq_ok in + let thm3' = subst_mps subst th.field_simpl_ok in + let thm4' = subst_mps subst th.field_cond in + let tac'= subst_tactic subst th.field_cst_tac in + let pretac'= subst_tactic subst th.field_pre_tac in + let posttac'= subst_tactic subst th.field_post_tac in + if c' == th.field_carrier && + eq' == th.field_req && + thm1' == th.field_ok && + thm2' == th.field_simpl_eq_ok && + thm3' == th.field_simpl_ok && + thm4' == th.field_cond && + tac' == th.field_cst_tac && + pretac' == th.field_pre_tac && + posttac' == th.field_post_tac then th + else + { field_carrier = c'; + field_req = eq'; + field_cst_tac = tac'; + field_ok = thm1'; + field_simpl_eq_ok = thm2'; + field_simpl_ok = thm3'; + field_cond = thm4'; + field_pre_tac = pretac'; + field_post_tac = posttac' } + +let (ftheory_to_obj, obj_to_ftheory) = + let cache_th (name,th) = add_field_entry name th + and export_th x = Some x in + declare_object + {(default_object "tactic-new-field-theory") with + open_function = (fun i o -> if i=1 then cache_th o); + cache_function = cache_th; + subst_function = subst_th; + classify_function = (fun (_,x) -> Substitute x); + export_function = export_th } -let setoid_ring = function - | [] -> ring - | l -> ring_rewrite l +let default_field_equality r inv req = + let is_setoid = function + {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true + | _ -> false in + match default_relation_for_carrier ~filter:is_setoid r with + Leibniz _ -> + mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) + | Relation rel -> + let is_endomorphism = function + { args=args } -> List.for_all + (function (var,Relation rel) -> + var=None && eq_constr req rel + | _ -> false) args in + let inv_m = + try default_morphism ~filter:is_endomorphism inv + with Not_found -> + error "field inverse should be declared as a morphism" in + inv_m.lem + +let add_field_theory name fth eqth morphth cst_tac inj (pre,post) = + let env = Global.env() in + let sigma = Evd.empty 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 + let eqth = Some(sth,ext) in + let _ = add_theory name rth eqth morphth cst_tac (None,None) in + let inv_m = default_field_equality r inv req in + let rk = reflect_coeff morphth in + let params = + exec_tactic env 8 (field_ltac"field_lemmas") + (List.map carg[sth;ext;inv_m;fth;rk]) in + let lemma1 = constr_of params.(3) in + let lemma2 = constr_of params.(4) in + let lemma3 = constr_of params.(5) in + let cond_lemma = + match inj with + | Some thm -> mkApp(constr_of params.(7),[|thm|]) + | None -> constr_of params.(6) 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 cond_lemma = decl_constant (string_of_id name^"_lemma4") cond_lemma in + let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in + let pretac = + match pre with + Some t -> Tacinterp.glob_tactic t + | _ -> TacId [] in + let posttac = + match post with + Some t -> Tacinterp.glob_tactic t + | _ -> TacId [] in + let _ = + Lib.add_leaf name + (ftheory_to_obj + { field_carrier = r; + field_req = req; + field_cst_tac = cst_tac; + field_ok = lemma1; + field_simpl_eq_ok = lemma2; + field_simpl_ok = lemma3; + field_cond = cond_lemma; + field_pre_tac = pretac; + field_post_tac = posttac }) in () + +type field_mod = + Ring_mod of ring_mod + | Inject of Topconstr.constr_expr + +VERNAC ARGUMENT EXTEND field_mod + | [ ring_mod(m) ] -> [ Ring_mod m ] + | [ "infinite" constr(inj) ] -> [ Inject inj ] +END -TACTIC EXTEND setoid_ring - [ "setoid" "ring" constr_list(l) ] -> [ setoid_ring l ] +let process_field_mods l = + let kind = ref None in + let set = ref None in + let cst_tac = ref None in + let pre = ref None in + let post = ref None in + let inj = ref None in + List.iter(function + Ring_mod(Ring_kind k) -> set_once "field kind" kind 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) + | Inject i -> set_once "infinite property" inj (ic i)) l; + let k = match !kind with Some k -> k | None -> Abstract in + (k, !set, !inj, !cst_tac, !pre, !post) + +VERNAC COMMAND EXTEND AddSetoidField +| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> + [ let (k,set,inj,cst_tac,pre,post) = process_field_mods l in + add_field_theory id (ic t) set k cst_tac inj (pre,post) ] END +let field_lookup (f:glob_tactic_expr) rl gl = + let env = pf_env gl in + let sigma = project gl in + let e = find_field_structure env sigma rl (pf_concl gl) None in + let rl = carg (make_term_list e.field_carrier rl gl) in + let req = carg e.field_req in + let cst_tac = Tacexp e.field_cst_tac in + let field_ok = carg e.field_ok in + let field_simpl_ok = carg e.field_simpl_ok in + let field_simpl_eq_ok = carg e.field_simpl_eq_ok in + let cond_ok = carg e.field_cond in + let pretac = Tacexp(TacFun([None],e.field_pre_tac)) in + let posttac = Tacexp(TacFun([None],e.field_post_tac)) in + Tacinterp.eval_tactic + (TacLetIn + ([(dummy_loc,id_of_string"f"),None,Tacexp f], + ltac_lcall "f" + [req;cst_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;cond_ok; + pretac;posttac;rl])) gl + +TACTIC EXTEND field_lookup +| [ "field_lookup" tactic(f) constr_list(l) ] -> [ field_lookup (fst f) l ] +END |