diff options
author | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
commit | 72b9a7df489ea47b3e5470741fd39f6100d31676 (patch) | |
tree | 60108a573d2a80d2dd4e3833649890e32427ff8d /contrib/setoid_ring | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'contrib/setoid_ring')
-rw-r--r-- | contrib/setoid_ring/InitialRing.v | 263 | ||||
-rw-r--r-- | contrib/setoid_ring/Ring_tac.v | 16 | ||||
-rw-r--r-- | contrib/setoid_ring/newring.ml4 | 54 |
3 files changed, 311 insertions, 22 deletions
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index bbdcd443..f5f845c2 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -13,6 +13,7 @@ Require Import BinNat. Require Import Setoid. Require Import Ring_theory. Require Import Ring_polynom. +Import List. Set Implicit Arguments. @@ -172,7 +173,7 @@ Section ZMORPHISM. Lemma gen_Zeqb_ok : forall x y, Zeq_bool x y = true -> [x] == [y]. Proof. - intros x y H; repeat rewrite same_genZ. + intros x y H. assert (H1 := Zeqb_ok x y H);unfold IDphi in H1. rewrite H1;rrefl. Qed. @@ -365,9 +366,236 @@ Section NMORPHISM. End NMORPHISM. +(* Words on N : initial structure for almost-rings. *) +Definition Nword := list N. +Definition NwO : Nword := nil. +Definition NwI : Nword := 1%N :: nil. + +Definition Nwcons n (w : Nword) : Nword := + match w, n with + | nil, 0%N => nil + | _, _ => n :: w + end. + +Fixpoint Nwadd (w1 w2 : Nword) {struct w1} : Nword := + match w1, w2 with + | n1::w1', n2:: w2' => (n1+n2)%N :: Nwadd w1' w2' + | nil, _ => w2 + | _, nil => w1 + end. + +Definition Nwopp (w:Nword) : Nword := Nwcons 0%N w. + +Definition Nwsub w1 w2 := Nwadd w1 (Nwopp w2). + +Fixpoint Nwscal (n : N) (w : Nword) {struct w} : Nword := + match w with + | m :: w' => (n*m)%N :: Nwscal n w' + | nil => nil + end. + +Fixpoint Nwmul (w1 w2 : Nword) {struct w1} : Nword := + match w1 with + | 0%N::w1' => Nwopp (Nwmul w1' w2) + | n1::w1' => Nwsub (Nwscal n1 w2) (Nwmul w1' w2) + | nil => nil + end. +Fixpoint Nw_is0 (w : Nword) : bool := + match w with + | nil => true + | 0%N :: w' => Nw_is0 w' + | _ => false + end. + +Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool := + match w1, w2 with + | n1::w1', n2::w2' => + if Neq_bool n1 n2 then Nweq_bool w1' w2' else false + | nil, _ => Nw_is0 w2 + | _, nil => Nw_is0 w1 + end. + +Section NWORDMORPHISM. + 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 (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext5. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext5. exact (Ropp_ext Reqe). 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. + + Fixpoint gen_phiNword (w : Nword) : R := + match w with + | nil => 0 + | n :: nil => gen_phiN rO rI radd rmul n + | N0 :: w' => - gen_phiNword w' + | n::w' => gen_phiN rO rI radd rmul n - gen_phiNword w' + end. + + Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0. +Proof. +induction w; simpl in |- *; intros; auto. + reflexivity. + + destruct a. + destruct w. + reflexivity. + + rewrite IHw in |- *; trivial. + apply (ARopp_zero Rsth Reqe ARth). + + discriminate. +Qed. + + Lemma gen_phiNword_cons : forall w n, + gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w. +induction w. + destruct n; simpl in |- *; norm. + + intros. + destruct n; norm. +Qed. + + Lemma gen_phiNword_Nwcons : forall w n, + gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w. +destruct w; intros. + destruct n; norm. + + unfold Nwcons in |- *. + rewrite gen_phiNword_cons in |- *. + reflexivity. +Qed. + + Lemma gen_phiNword_ok : forall w1 w2, + Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2. +induction w1; intros. + simpl in |- *. + rewrite (gen_phiNword0_ok _ H) in |- *. + reflexivity. + + rewrite gen_phiNword_cons in |- *. + destruct w2. + simpl in H. + destruct a; try discriminate. + rewrite (gen_phiNword0_ok _ H) in |- *. + norm. + + simpl in H. + rewrite gen_phiNword_cons in |- *. + case_eq (Neq_bool a n); intros. + rewrite H0 in H. + rewrite <- (Neq_bool_ok _ _ H0) in |- *. + rewrite (IHw1 _ H) in |- *. + reflexivity. + + rewrite H0 in H; discriminate H. +Qed. + + +Lemma Nwadd_ok : forall x y, + gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y. +induction x; intros. + simpl in |- *. + norm. + + destruct y. + simpl Nwadd; norm. + + simpl Nwadd in |- *. + repeat rewrite gen_phiNword_cons in |- *. + rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- *. + destruct Reqe; constructor; trivial. + + rewrite IHx in |- *. + norm. + add_push (- gen_phiNword x); reflexivity. +Qed. + +Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x. +simpl in |- *. +unfold Nwopp in |- *; simpl in |- *. +intros. +rewrite gen_phiNword_Nwcons in |- *; norm. +Qed. + +Lemma Nwscal_ok : forall n x, + gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x. +induction x; intros. + norm. + + simpl Nwscal in |- *. + repeat rewrite gen_phiNword_cons in |- *. + rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *. + destruct Reqe; constructor; trivial. + + rewrite IHx in |- *. + norm. +Qed. + +Lemma Nwmul_ok : forall x y, + gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y. +induction x; intros. + norm. + + destruct a. + simpl Nwmul in |- *. + rewrite Nwopp_ok in |- *. + rewrite IHx in |- *. + rewrite gen_phiNword_cons in |- *. + norm. + + simpl Nwmul in |- *. + unfold Nwsub in |- *. + rewrite Nwadd_ok in |- *. + rewrite Nwscal_ok in |- *. + rewrite Nwopp_ok in |- *. + rewrite IHx in |- *. + rewrite gen_phiNword_cons in |- *. + norm. +Qed. + +(* Proof that [.] satisfies morphism specifications *) + Lemma gen_phiNword_morph : + ring_morph 0 1 radd rmul rsub ropp req + NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword. +constructor. + reflexivity. + + reflexivity. + + exact Nwadd_ok. + + intros. + unfold Nwsub in |- *. + rewrite Nwadd_ok in |- *. + rewrite Nwopp_ok in |- *. + norm. + + exact Nwmul_ok. + + exact Nwopp_ok. + + exact gen_phiNword_ok. +Qed. + +End NWORDMORPHISM. + + + (* syntaxification of constants in an abstract ring: - the inverse of gen_phiPOS - Why we do not reconnize only rI ?????? *) + the inverse of gen_phiPOS *) Ltac inv_gen_phi_pos rI add mul t := let rec inv_cst t := match t with @@ -390,6 +618,18 @@ End NMORPHISM. end in inv_cst t. +(* The (partial) inverse of gen_phiNword *) + Ltac inv_gen_phiNword rO rI add mul opp t := + match t with + rO => constr:NwO + | _ => + match inv_gen_phi_pos rI add mul t with + NotConstant => NotConstant + | ?p => constr:(Npos p::nil) + end + end. + + (* The inverse of gen_phiN *) Ltac inv_gen_phiN rO rI add mul t := match t with @@ -417,9 +657,18 @@ End NMORPHISM. end end. -(* A simpl tactic reconninzing nothing *) - Ltac inv_morph_nothing t := constr:(NotConstant). +(* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above + are only optimisations that directly returns the reifid constant + instead of resorting to the constant propagation of the simplification + algorithm. *) +Ltac inv_gen_phi rO rI cO cI t := + match t with + | rO => cO + | rI => cI + end. +(* A simple tactic recognizing no constant *) + Ltac inv_morph_nothing t := constr:(NotConstant). Ltac coerce_to_almost_ring set ext rspec := match type of rspec with @@ -441,7 +690,7 @@ Ltac abstract_ring_morphism set ext rspec := | 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" + constr:(gen_phiNword_morph set ext rspec) | _ => fail 1 "bad ring structure" end. @@ -502,7 +751,7 @@ Ltac ring_elements set ext rspec pspec sspec rk := | ring_morph _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => m | @semi_morph _ _ _ _ _ _ _ _ _ _ _ _ _ => constr:(SRmorph_Rmorph set m) - | _ => fail 2 " ici" + | _ => fail 2 "ring anomaly" end | _ => fail 1 "ill-formed ring kind" end in diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index 7419f184..b55c5443 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -108,31 +108,37 @@ Ltac FV Cst CstPow add mul sub opp pow t fv := (* syntaxification of ring expressions *) Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := let rec mkP t := + let f := match Cst t with | InitialRing.NotConstant => match t with | (radd ?t1 ?t2) => + fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(PEadd e1 e2) | (rmul ?t1 ?t2) => + fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(PEmul e1 e2) | (rsub ?t1 ?t2) => + fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(PEsub e1 e2) | (ropp ?t1) => + fun _ => let e1 := mkP t1 in constr:(PEopp e1) | (rpow ?t1 ?n) => match CstPow n with | InitialRing.NotConstant => - let p := Find_at t fv in constr:(PEX C p) - | ?c => let e1 := mkP t1 in constr:(PEpow e1 c) + fun _ => let p := Find_at t fv in constr:(PEX C p) + | ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c) end | _ => - let p := Find_at t fv in constr:(PEX C p) + fun _ => let p := Find_at t fv in constr:(PEX C p) end - | ?c => constr:(PEc c) - end + | ?c => fun _ => constr:(@PEc C c) + end in + f () in mkP t. Ltac ParseRingComponents lemma := diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 8b2ce26b..f963fc9c 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 9603 2007-02-07 00:41:16Z barras $ i*) +(*i $Id: newring.ml4 9968 2007-07-11 15:49:07Z barras $ i*) open Pp open Util @@ -166,8 +166,10 @@ let decl_constant na c = const_entry_boxed = true}, IsProof Lemma)) -let ltac_call tac args = +let ltac_call tac (args:glob_tactic_arg list) = TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) +let ltac_acall tac (args:glob_tactic_arg list) = + 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)) @@ -276,12 +278,18 @@ let coq_mk_reqe = my_constant "mk_reqe" let coq_semi_ring_theory = my_constant "semi_ring_theory" let coq_mk_seqe = my_constant "mk_seqe" +let ltac_inv_morph_gen = zltac"inv_gen_phi" let ltac_inv_morphZ = zltac"inv_gen_phiZ" let ltac_inv_morphN = zltac"inv_gen_phiN" +let ltac_inv_morphNword = zltac"inv_gen_phiNword" let coq_abstract = my_constant"Abstract" let coq_comp = my_constant"Computational" let coq_morph = my_constant"Morphism" +(* morphism *) +let coq_ring_morph = my_constant "ring_morph" +let coq_semi_morph = my_constant "semi_morph" + (* power function *) let ltac_inv_morph_nothing = zltac"inv_morph_nothing" let coq_pow_N_pow_N = my_constant "pow_N_pow_N" @@ -527,6 +535,18 @@ let dest_ring env sigma th_spec = | _ -> error "bad ring structure" +let dest_morph env sigma m_spec = + let m_typ = Retyping.get_type_of env sigma m_spec in + match kind_of_term m_typ with + App(f,[|r;zero;one;add;mul;sub;opp;req; + c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) + when f = Lazy.force coq_ring_morph -> + (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi) + | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) + when f = Lazy.force coq_semi_morph -> + (c,czero,cone,cadd,cmul,None,None,ceqb,phi) + | _ -> error "bad morphism structure" + type coeff_spec = Computational of constr (* equality test *) @@ -545,22 +565,34 @@ type cst_tac_spec = CstTac of raw_tactic_expr | Closed of reference list -let interp_cst_tac kind (zero,one,add,mul,opp) cst_tac = +let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = match cst_tac with Some (CstTac t) -> Tacinterp.glob_tactic t | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc) | None -> - (match opp, kind with - None, _ -> + (match rk, opp, kind with + Abstract, None, _ -> let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) - | Some opp, Some _ -> + | Abstract, Some opp, Some _ -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) - | _ -> error"a tactic must be specified for an almost_ring") + | Abstract, Some opp, None -> + let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in + TacArg + (TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) + | Computational _,_,_ -> + let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in + TacArg + (TacCall(dummy_loc,t,List.map carg [zero;one;zero;one])) + | Morphism mth,_,_ -> + let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in + let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in + TacArg + (TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone]))) let make_hyp env c = - let t = (Typeops.typing env c).uj_type in + let t = Retyping.get_type_of env Evd.empty c in lapp coq_mkhypo [|t;c|] let make_hyp_list env lH = @@ -608,7 +640,8 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign = 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 cst_tac = + interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = match pre with Some t -> Tacinterp.glob_tactic t @@ -980,7 +1013,8 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign = let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in - let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in + let cst_tac = + interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = match pre with Some t -> Tacinterp.glob_tactic t |