diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/ring/Setoid_ring_theory.v | 2 | ||||
| -rw-r--r-- | contrib/rtauto/Bintree.v | 4 | ||||
| -rw-r--r-- | contrib/setoid_ring/InitialRing.v | 2 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 3 | ||||
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 173 |
5 files changed, 113 insertions, 71 deletions
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v index 4ec8433fe..f50a2f30a 100644 --- a/contrib/ring/Setoid_ring_theory.v +++ b/contrib/ring/Setoid_ring_theory.v @@ -245,7 +245,7 @@ Lemma Saux1 : forall a:A, a + a == a -> a == 0. intros. rewrite <- (plus_zero_left a). rewrite (plus_comm 0 a). -setoid_replace (a + 0) with (a + (a + - a)); auto. +setoid_replace (a + 0) with (a + (a + - a)) by auto. rewrite (plus_assoc a a (- a)). rewrite H. apply opp_def. diff --git a/contrib/rtauto/Bintree.v b/contrib/rtauto/Bintree.v index 67a952b73..d410606a7 100644 --- a/contrib/rtauto/Bintree.v +++ b/contrib/rtauto/Bintree.v @@ -107,7 +107,7 @@ intro ne;right;congruence. left;reflexivity. Defined. -Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (m<>m) (refl_equal m) . +Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (refl_equal m). fix 1;intros [mm|mm|]. simpl; rewrite pos_eq_dec_refl; reflexivity. simpl; rewrite pos_eq_dec_refl; reflexivity. @@ -116,7 +116,7 @@ Qed. Theorem pos_eq_dec_ex : forall m n, pos_eq m n =true -> exists h:m=n, - pos_eq_dec m n = left (m<>n) h. + pos_eq_dec m n = left h. fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence). simpl;intro e. elim (pos_eq_dec_ex _ _ e). diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index 6542d280c..56b08a8fa 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -243,7 +243,7 @@ Section ZMORPHISM. Zplus Zmult Zeq_bool gen_phiZ). apply mkRmorph;simpl;try rrefl. apply gen_phiZ_add. apply gen_phiZ_mul. apply gen_Zeqb_ok. - apply (Smorph_morph Rsth Reqe Rth Zsth Zth SRmorph gen_phiZ_ext). + apply (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext). Qed. End ZMORPHISM. diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index caa704595..cefdcf52b 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -59,8 +59,7 @@ Section Power. induction j;simpl. rewrite IHj. rewrite (mul_comm x (pow_pos x j *pow_pos x j)). - set (w:= x*pow_pos x j);unfold w at 2. - rewrite (mul_comm x (pow_pos x j));unfold w. + setoid_rewrite (mul_comm x (pow_pos x j)) at 2. repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). apply (Seq_refl _ _ Rsth). diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 6c3b6337a..bce41b9b5 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -201,7 +201,8 @@ let constr_of = function let stdlib_modules = [["Coq";"Setoids";"Setoid"]; ["Coq";"Lists";"List"]; - ["Coq";"Init";"Datatypes"] + ["Coq";"Init";"Datatypes"]; + ["Coq";"Init";"Logic"]; ] let coq_constant c = @@ -212,6 +213,7 @@ let coq_cons = coq_constant "cons" let coq_nil = coq_constant "nil" let coq_None = coq_constant "None" let coq_Some = coq_constant "Some" +let coq_eq = coq_constant "eq" let lapp f args = mkApp(Lazy.force f,args) @@ -448,10 +450,12 @@ let (theory_to_obj, obj_to_theory) = export_function = export_th } -let setoid_of_relation r = +let setoid_of_relation env a r = lapp coq_mk_Setoid - [|r.rel_a; r.rel_aeq; - Option.get r.rel_refl; Option.get r.rel_sym; Option.get r.rel_trans |] + [|a ; r ; + Class_tactics.reflexive_proof env a r ; + Class_tactics.symmetric_proof env a r ; + Class_tactics.transitive_proof env a r |] let op_morph r add mul opp req m1 m2 m3 = lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] @@ -459,63 +463,108 @@ let op_morph r add mul opp req m1 m2 m3 = let op_smorph r add mul req m1 m2 = lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |] -let default_ring_equality (r,add,mul,opp,req) = - let is_setoid = function - {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> - eq_constr req rel (* Qu: use conversion ? *) - | _ -> false in - match default_relation_for_carrier ~filter:is_setoid r with - Leibniz _ -> - let setoid = lapp coq_eq_setoid [|r|] in - let op_morph = - match opp with +(* let default_ring_equality (r,add,mul,opp,req) = *) +(* let is_setoid = function *) +(* {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *) +(* eq_constr req rel (\* Qu: use conversion ? *\) *) +(* | _ -> false in *) +(* match default_relation_for_carrier ~filter:is_setoid r with *) +(* Leibniz _ -> *) +(* let setoid = lapp coq_eq_setoid [|r|] in *) +(* let op_morph = *) +(* match opp with *) +(* Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *) +(* | None -> lapp coq_eq_smorph [|r;add;mul|] in *) +(* (setoid,op_morph) *) +(* | Relation rel -> *) +(* let setoid = setoid_of_relation rel in *) +(* let is_endomorphism = function *) +(* { args=args } -> List.for_all *) +(* (function (var,Relation rel) -> *) +(* var=None && eq_constr req rel *) +(* | _ -> false) args in *) +(* let add_m = *) +(* try default_morphism ~filter:is_endomorphism add *) +(* with Not_found -> *) +(* error "ring addition should be declared as a morphism" in *) +(* let mul_m = *) +(* try default_morphism ~filter:is_endomorphism mul *) +(* with Not_found -> *) +(* error "ring multiplication should be declared as a morphism" in *) +(* let op_morph = *) +(* 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 *) +(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ *) +(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) +(* str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *) +(* str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *) +(* str"\""); *) +(* op_morph) *) +(* | None -> *) +(* (msgnl *) +(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ *) +(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) +(* str"\""++spc()++str"and \""++ *) +(* pr_constr mul_m.morphism_theory++str"\""); *) +(* op_smorph r add mul req add_m.lem mul_m.lem) in *) +(* (setoid,op_morph) *) + +let ring_equality (r,add,mul,opp,req) = + match kind_of_term req with + | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) -> + let setoid = lapp coq_eq_setoid [|r|] in + 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 - let is_endomorphism = function - { args=args } -> List.for_all - (function (var,Relation rel) -> - var=None && eq_constr req rel - | _ -> false) args in - let add_m = - try default_morphism ~filter:is_endomorphism add + (setoid,op_morph) + | _ -> + let setoid = setoid_of_relation (Global.env ()) r req in + let signature = [Some (r,req);Some (r,req);Some(r,req)] in + let add_m, add_m_lem = + try Class_tactics.default_morphism signature add with Not_found -> error "ring addition should be declared as a morphism" in - let mul_m = - try default_morphism ~filter:is_endomorphism mul + let mul_m, mul_m_lem = + try Class_tactics.default_morphism signature mul with Not_found -> error "ring multiplication should be declared as a morphism" in let op_morph = 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 - (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ - str"and morphisms \""++pr_constr add_m.morphism_theory++ - str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ - str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ - str"\""); - op_morph) + (let opp_m,opp_m_lem = + try Class_tactics.default_morphism (List.tl signature) 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 + (str"Using setoid \""++pr_constr req++str"\""++spc()++ + str"and morphisms \""++pr_constr add_m ++ + str"\","++spc()++ str"\""++pr_constr mul_m++ + str"\""++spc()++str"and \""++pr_constr opp_m++ + str"\""); + op_morph) | None -> - (msgnl - (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ - str"and morphisms \""++pr_constr add_m.morphism_theory++ - str"\""++spc()++str"and \""++ - pr_constr mul_m.morphism_theory++str"\""); - op_smorph r add mul req add_m.lem mul_m.lem) in - (setoid,op_morph) - + (msgnl + (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ + str"and morphisms \""++pr_constr add_m ++ + str"\""++spc()++str"and \""++ + pr_constr mul_m++str"\""); + op_smorph r add mul req add_m_lem mul_m_lem) in + (setoid,op_morph) + let build_setoid_params r add mul opp req eqth = match eqth with Some th -> th - | None -> default_ring_equality (r,add,mul,opp,req) + | None -> ring_equality (r,add,mul,opp,req) let dest_ring env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in @@ -980,25 +1029,19 @@ let (ftheory_to_obj, obj_to_ftheory) = classify_function = (fun (_,x) -> Substitute x); export_function = export_th } -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 _ -> +let field_equality r inv req = + match kind_of_term req with + | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) -> mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) - | 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 + | _ -> + let _setoid = setoid_of_relation (Global.env ()) r req in + let signature = [Some (r,req);Some(r,req)] in + let inv_m, inv_m_lem = + try Class_tactics.default_morphism signature inv with Not_found -> error "field inverse should be declared as a morphism" in - inv_m.lem - + inv_m_lem + let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odiv = check_required_library (cdir@["Field_tac"]); let env = Global.env() in @@ -1011,7 +1054,7 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi let (pow_tac, pspec) = interp_power env power in let sspec = interp_sign env sign in let dspec = interp_div env odiv in - let inv_m = default_field_equality r inv req in + let inv_m = field_equality r inv req in let rk = reflect_coeff morphth in let params = exec_tactic env 9 (field_ltac"field_lemmas") |