diff options
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 4 | ||||
| -rw-r--r-- | plugins/setoid_ring/Cring.v | 5 | ||||
| -rw-r--r-- | plugins/setoid_ring/Field_tac.v | 62 | ||||
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 21 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ncring_polynom.v | 51 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ncring_tac.v | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_polynom.v | 14 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 46 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 26 |
9 files changed, 137 insertions, 94 deletions
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 21a94afca..2a287556b 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -98,7 +98,7 @@ Definition PhiR : list R -> PolZ -> R := (InitialRing.gen_phiZ ring0 ring1 add mul opp)). Definition PEevalR : list R -> PEZ -> R := - PEeval ring0 add mul sub opp + PEeval ring0 ring1 add mul sub opp (gen_phiZ ring0 ring1 add mul opp) N.to_nat pow. @@ -241,6 +241,8 @@ Fixpoint interpret3 t fv {struct t}: R := | (PEpow t1 t2) => let v1 := interpret3 t1 fv in pow v1 (N.to_nat t2) | (PEc t1) => (IZR1 t1) + | PEO => 0 + | PEI => 1 | (PEX _ n) => List.nth (pred (Pos.to_nat n)) fv 0 end. diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index 02194d4f1..cb2e78e42 100644 --- a/plugins/setoid_ring/Cring.v +++ b/plugins/setoid_ring/Cring.v @@ -21,6 +21,7 @@ Require Export Ncring_tac. Class Cring {R:Type}`{Rr:Ring R} := cring_mul_comm: forall x y:R, x * y == y * x. + Ltac reify_goal lvar lexpr lterm:= (*idtac lvar; idtac lexpr; idtac lterm;*) match lexpr with @@ -30,10 +31,10 @@ Ltac reify_goal lvar lexpr lterm:= |- (?op ?u1 ?u2) => change (op (@Ring_polynom.PEeval - _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) + _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e1) (@Ring_polynom.PEeval - _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) + _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e2)) end end. diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index dda1edbe1..1b52be14b 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -10,12 +10,19 @@ Require Import Ring_tac BinList Ring_polynom InitialRing. Require Export Field_theory. (* syntaxification *) - Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv := + (* We do not assume that Cst recognizes the rO and rI terms as constants, as *) + (* the tactic could be used to discriminate occurrences of an opaque *) + (* constant phi, with (phi 0) not convertible to 0 for instance *) + Ltac mkFieldexpr C Cst CstPow rO rI radd rmul rsub ropp rdiv rinv rpow t fv := let rec mkP t := let f := match Cst t with | InitialRing.NotConstant => match t with + | rO => + fun _ => constr:(@FEO C) + | rI => + fun _ => constr:(@FEI C) | (radd ?t1 ?t2) => fun _ => let e1 := mkP t1 in @@ -54,11 +61,16 @@ Require Export Field_theory. f () in mkP t. -Ltac FFV Cst CstPow add mul sub opp div inv pow t fv := + (* We do not assume that Cst recognizes the rO and rI terms as constants, as *) + (* the tactic could be used to discriminate occurrences of an opaque *) + (* constant phi, with (phi 0) not convertible to 0 for instance *) +Ltac FFV Cst CstPow rO rI add mul sub opp div inv pow t fv := let rec TFV t fv := match Cst t with | InitialRing.NotConstant => match t with + | rO => fv + | rI => fv | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) @@ -83,60 +95,60 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv := Ltac PackField F req Cst_tac Pow_tac L1 L2 L3 L4 cond_ok pre post := let FLD := match type of L1 with - | context [req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv + | context [req (@FEeval ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] => (fun proj => proj Cst_tac Pow_tac pre post - req radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok) + req rO rI radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok) | _ => fail 1 "field anomaly: bad correctness lemma (parse)" end in F FLD. Ltac get_FldPre FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => pre). Ltac get_FldPost FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => post). Ltac get_L1 FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => L1). Ltac get_SimplifyEqLemma FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => L2). Ltac get_SimplifyLemma FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => L3). Ltac get_L4 FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => L4). Ltac get_CondLemma FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => cond_ok). Ltac get_FldEq FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => req). @@ -146,33 +158,33 @@ Ltac get_FldCarrier FLD := Ltac get_RingFV FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => - FV Cst_tac Pow_tac radd rmul rsub ropp rpow). + FV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow). Ltac get_FFV FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => - FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow). + FFV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow). Ltac get_RingMeta FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => - mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow). + mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow). Ltac get_Meta FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => - mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow). + mkFieldexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow). Ltac get_Hyp_tac FLD := FLD ltac: - (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C + (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok => - let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow in fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH). Ltac get_FEeval FLD := @@ -180,8 +192,8 @@ Ltac get_FEeval FLD := match type of L1 with | context [(@FEeval - ?R ?r0 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] => - constr:(@FEeval R r0 add mul sub opp div inv C phi Cpow powphi pow) + ?R ?r0 ?r1 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] => + constr:(@FEeval R r0 r1 add mul sub opp div inv C phi Cpow powphi pow) | _ => fail 1 "field anomaly: bad correctness lemma (get_FEeval)" end. @@ -560,7 +572,7 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk := (fun f => f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in cond1_ok cond2_ok) - | _ => fail 4 "field: bad coefficiant division specification" + | _ => fail 4 "field: bad coefficient division specification" end | _ => fail 3 "field: bad sign specification" end diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index bc947d54e..4c9b34b6a 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -135,7 +135,7 @@ Let rpow_pow := pow_th.(rpow_pow_N). Bind Scope PE_scope with PExpr. Delimit Scope PE_scope with poly. -Notation NPEeval := (PEeval rO radd rmul rsub ropp phi Cp_phi rpow). +Notation NPEeval := (PEeval rO rI radd rmul rsub ropp phi Cp_phi rpow). Notation "P @ l" := (NPEeval l P) (at level 10, no associativity). Infix "+" := PEadd : PE_scope. @@ -698,6 +698,8 @@ Fixpoint PEsimp (e : PExpr C) : PExpr C := Theorem PEsimp_ok e : (PEsimp e === e)%poly. Proof. induction e; simpl. +- reflexivity. +- reflexivity. - intro l; trivial. - intro l; trivial. - rewrite NPEadd_ok. now f_equiv. @@ -717,7 +719,9 @@ Qed. (* The input: syntax of a field expression *) Inductive FExpr : Type := - FEc: C -> FExpr + | FEO : FExpr + | FEI : FExpr + | FEc: C -> FExpr | FEX: positive -> FExpr | FEadd: FExpr -> FExpr -> FExpr | FEsub: FExpr -> FExpr -> FExpr @@ -729,6 +733,8 @@ Inductive FExpr : Type := Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := match pe with + | FEO => rO + | FEI => rI | FEc c => phi c | FEX x => BinList.nth 0 x l | FEadd x y => FEeval l x + FEeval l y @@ -1024,6 +1030,8 @@ Qed. Fixpoint Fnorm (e : FExpr) : linear := match e with + | FEO => mk_linear (PEc cO) (PEc cI) nil + | FEI => mk_linear (PEc cI) (PEc cI) nil | FEc c => mk_linear (PEc c) (PEc cI) nil | FEX x => mk_linear (PEX C x) (PEc cI) nil | FEadd e1 e2 => @@ -1083,6 +1091,8 @@ Theorem Pcond_Fnorm l e : Proof. induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok. +- simpl. rewrite phi_1; exact rI_neq_rO. +- simpl. rewrite phi_1; exact rI_neq_rO. - simpl; intros. rewrite phi_1; exact rI_neq_rO. - simpl; intros. rewrite phi_1; exact rI_neq_rO. - rewrite <- split_ok_r. simpl. apply field_is_integral_domain. @@ -1125,6 +1135,8 @@ induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl; try (specialize (IHfe2 Hc2);apply Pcond_Fnorm in Hc2); try set (F1 := Fnorm fe1) in *; try set (F2 := Fnorm fe2) in *. +- now rewrite phi_1, phi_0, rdiv_def. +- now rewrite phi_1; apply rdiv1. - rewrite phi_1; apply rdiv1. - rewrite phi_1; apply rdiv1. - rewrite NPEadd_ok, !NPEmul_ok. simpl. @@ -1177,7 +1189,7 @@ apply cross_product_eq; trivial; Qed. (* Correctness lemmas of reflexive tactics *) -Notation Ninterp_PElist := (interp_PElist rO radd rmul rsub ropp req phi Cp_phi rpow). +Notation Ninterp_PElist := (interp_PElist rO rI radd rmul rsub ropp req phi Cp_phi rpow). Notation Nmk_monpol_list := (mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv). Theorem Fnorm_ok: @@ -1747,3 +1759,6 @@ Qed. End Field. End Complete. + +Arguments FEO [C]. +Arguments FEI [C].
\ No newline at end of file diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 7ffe98e29..32824838b 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -416,8 +416,11 @@ Qed. Variable pow_th : power_theory Cp_phi rpow. (** evaluation of polynomial expressions towards R *) + Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R := match pe with + | PEO => 0 + | PEI => 1 | PEc c => [c] | PEX _ j => nth 0 j l | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) @@ -500,6 +503,8 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) := Fixpoint norm_aux (pe:PExpr C) : Pol := match pe with + | PEO => Pc cO + | PEI => Pc cI | PEc c => Pc c | PEX _ j => mk_X j | PEadd pe1 (PEopp pe2) => @@ -520,28 +525,30 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) := Proof. intros. induction pe. -Esimpl3. Esimpl3. simpl. - rewrite IHpe1;rewrite IHpe2. - destruct pe2; Esimpl3. -unfold Psub. -destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity. -simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2. -destruct pe1. destruct pe2; rewrite Padd_ok; rewrite Popp_ok; try reflexivity. -Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. - Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. -simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity. -simpl. rewrite IHpe; Esimpl3. -simpl. - rewrite Ppow_N_ok; (intros;try reflexivity). - rewrite rpow_pow_N. Esimpl3. - induction n;simpl. Esimpl3. induction p; simpl. - try rewrite IHp;try rewrite IHpe; - repeat rewrite Pms_ok; - repeat rewrite Pmul_ok;reflexivity. -rewrite Pmul_ok. try rewrite IHp;try rewrite IHpe; - repeat rewrite Pms_ok; - repeat rewrite Pmul_ok;reflexivity. trivial. -exact pow_th. + - now simpl; rewrite <- ring_morphism0. + - now simpl; rewrite <- ring_morphism1. + - Esimpl3. + - Esimpl3. + - simpl. + rewrite IHpe1;rewrite IHpe2. + destruct pe2; Esimpl3. + unfold Psub. + destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity. + - simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2. + now destruct pe1; + [destruct pe2; rewrite Padd_ok; rewrite Popp_ok; Esimpl3 | Esimpl3..]. + - simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity. + - now simpl; rewrite IHpe; Esimpl3. + - simpl. + rewrite Ppow_N_ok; (intros;try reflexivity). + rewrite rpow_pow_N; [| now apply pow_th]. + induction n;simpl; [now Esimpl3|]. + induction p; simpl; trivial. + + try rewrite IHp;try rewrite IHpe; + repeat rewrite Pms_ok; repeat rewrite Pmul_ok;reflexivity. + + rewrite Pmul_ok. + try rewrite IHp;try rewrite IHpe; repeat rewrite Pms_ok; + repeat rewrite Pmul_ok;reflexivity. Qed. Lemma norm_subst_spec : diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v index 804c62d58..53fd202ef 100644 --- a/plugins/setoid_ring/Ncring_tac.v +++ b/plugins/setoid_ring/Ncring_tac.v @@ -127,7 +127,6 @@ Definition list_reifyl (R:Type) lexpr lvar lterm Unset Implicit Arguments. - Ltac lterm_goal g := match g with | ?t1 == ?t2 => constr:(t1::t2::nil) @@ -138,6 +137,7 @@ Ltac lterm_goal g := Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y. intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed. + Ltac reify_goal lvar lexpr lterm:= (*idtac lvar; idtac lexpr; idtac lterm;*) match lexpr with diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index eeae7077d..6ffa54866 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -896,6 +896,8 @@ Section MakeRingPol. (** Definition of polynomial expressions *) Inductive PExpr : Type := + | PEO : PExpr + | PEI : PExpr | PEc : C -> PExpr | PEX : positive -> PExpr | PEadd : PExpr -> PExpr -> PExpr @@ -904,6 +906,7 @@ Section MakeRingPol. | PEopp : PExpr -> PExpr | PEpow : PExpr -> N -> PExpr. + (** evaluation of polynomial expressions towards R *) Definition mk_X j := mkPinj_pred j mkX. @@ -911,6 +914,8 @@ Section MakeRingPol. Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R := match pe with + | PEO => rO + | PEI => rI | PEc c => phi c | PEX j => nth 0 j l | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) @@ -979,6 +984,8 @@ Section POWER. Fixpoint norm_aux (pe:PExpr) : Pol := match pe with + | PEO => Pc cO + | PEI => Pc cI | PEc c => Pc c | PEX j => mk_X j | PEadd (PEopp pe1) pe2 => (norm_aux pe2) -- (norm_aux pe1) @@ -1010,7 +1017,7 @@ Section POWER. end. Proof. simpl (norm_aux (PEadd _ _)). - destruct pe1; [ | | | | | reflexivity | ]; + destruct pe1; [ | | | | | | | reflexivity | ]; destruct pe2; simpl get_PEopp; reflexivity. Qed. @@ -1028,6 +1035,8 @@ Section POWER. Proof. intros. induction pe. + - now rewrite (morph0 CRmorph). + - now rewrite (morph1 CRmorph). - reflexivity. - apply mkX_ok. - simpl PEeval. rewrite IHpe1, IHpe2. @@ -1472,3 +1481,6 @@ Qed. Qed. End MakeRingPol. + +Arguments PEO [C]. +Arguments PEI [C].
\ No newline at end of file diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index 7a7ffcfdc..1d958d09b 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -196,12 +196,17 @@ Ltac get_MonPol lemma := (********************************************************) (* Building the atom list of a ring expression *) -Ltac FV Cst CstPow add mul sub opp pow t fv := +(* We do not assume that Cst recognizes the rO and rI terms as constants, as *) +(* the tactic could be used to discriminate occurrences of an opaque *) +(* constant phi, with (phi 0) not convertible to 0 for instance *) +Ltac FV Cst CstPow rO rI add mul sub opp pow t fv := let rec TFV t fv := let f := match Cst t with | NotConstant => match t with + | rO => fun _ => fv + | rI => fun _ => fv | (add ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv) | (mul ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv) | (sub ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv) @@ -219,12 +224,19 @@ Ltac FV Cst CstPow add mul sub opp pow t fv := in TFV t fv. (* syntaxification of ring expressions *) -Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := + (* We do not assume that Cst recognizes the rO and rI terms as constants, as *) + (* the tactic could be used to discriminate occurrences of an opaque *) + (* constant phi, with (phi 0) not convertible to 0 for instance *) +Ltac mkPolexpr C Cst CstPow rO rI radd rmul rsub ropp rpow t fv := let rec mkP t := let f := match Cst t with | InitialRing.NotConstant => match t with + | rO => + fun _ => constr:(@PEO C) + | rI => + fun _ => constr:(@PEI C) | (radd ?t1 ?t2) => fun _ => let e1 := mkP t1 in @@ -260,58 +272,58 @@ Ltac PackRing F req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post := let RNG := match type of lemma1 with | context - [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] => + [@PEeval ?R ?r0 ?r1 ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] => (fun proj => proj cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2) + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2) | _ => fail 1 "field anomaly: bad correctness lemma (parse)" end in F RNG. Ltac get_Carrier RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => R). Ltac get_Eq RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => req). Ltac get_Pre RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => pre). Ltac get_Post RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => post). Ltac get_NormLemma RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => lemma1). Ltac get_SimplifyLemma RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => lemma2). Ltac get_RingFV RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => - FV cst_tac pow_tac add mul sub opp pow). + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => + FV cst_tac pow_tac r0 r1 add mul sub opp pow). Ltac get_RingMeta RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => - mkPolexpr C cst_tac pow_tac add mul sub opp pow). + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => + mkPolexpr C cst_tac pow_tac r0 r1 add mul sub opp pow). Ltac get_RingHypTac RNG := RNG ltac:(fun cst_tac pow_tac pre post - R req add mul sub opp C Cpow powphi pow lemma1 lemma2 => - let mkPol := mkPolexpr C cst_tac pow_tac add mul sub opp pow in + R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 => + let mkPol := mkPolexpr C cst_tac pow_tac r0 r1 add mul sub opp pow in fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH). (* ring tactics *) @@ -338,7 +350,7 @@ Ltac Ring RNG lemma lH := (apply (lemma vfv vlpe pe1 pe2) || fail "typing error while applying ring"); [ ((let prh := proofHyp_tac lH in exact prh) - || idtac "can not automatically proof hypothesis :"; + || idtac "can not automatically prove hypothesis :"; idtac " maybe a left member of a hypothesis is not a monomial") | vm_compute; (exact (eq_refl true) || fail "not a valid ring equation")]). diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 7e4fc7277..f618c54b0 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -599,26 +599,8 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = | Some (Closed lc) -> closed_term_ast (List.map Smartlocate.global_with_alias lc) | None -> - (match rk, opp, kind with - Abstract, None, _ -> - let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morphN) in - TacArg(Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul])) - | Abstract, Some opp, Some _ -> - let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morphZ) in - TacArg(Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul;opp])) - | Abstract, Some opp, None -> - let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morphNword) in - TacArg - (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul;opp])) - | Computational _,_,_ -> - let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_gen) in - TacArg - (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;zero;one])) - | Morphism mth,_,_ -> - let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in - let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_gen) in - TacArg - (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;czero;cone]))) + let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in + TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])) let make_hyp env c = let t = Retyping.get_type_of env Evd.empty c in @@ -857,8 +839,8 @@ let _ = add_map "field_cond" coq_nil, (function -1->Eval|_ -> Prot); (* PCond: evaluate morphism and denum list, protect ring operations and make recursive call on the var map *) - my_constant "PCond", (function -1|8|10|13->Eval|12->Rec|_->Prot)]);; -(* (function -1|8|10->Eval|9->Rec|_->Prot)]);;*) + my_constant "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);; +(* (function -1|9|11->Eval|10->Rec|_->Prot)]);;*) let _ = Redexpr.declare_reduction "simpl_field_expr" |