diff options
28 files changed, 925 insertions, 335 deletions
diff --git a/Makefile.common b/Makefile.common index 73c76e5a4..d4dc8256f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -743,7 +743,7 @@ INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) $(INTEGE NUMBERSVO:= $(NUMBERSCOMMONVO) $(NATURALVO) $(INTEGERVO) $(NATINTVO) -SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theories/Setoids/Setoid.vo +SETOIDSVO:= theories/Setoids/Setoid.vo # theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo UNICODEVO:= theories/Unicode/Utf8.vo 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") diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 86a1081ec..c27e6b05d 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -32,6 +32,10 @@ open Rawterm open Hiddentac open Typeclasses open Typeclasses_errors +open Classes +open Topconstr +open Pfedit +open Command open Evd @@ -69,9 +73,9 @@ let rec e_trivial_fail_db db_list local_db goal = and e_my_find_search db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in let hintl = - if occur_existential concl then + if occur_existential concl then list_map_append (Hint_db.map_all hdc) (local_db::db_list) - else + else list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list) in let tac_of_hint = @@ -101,9 +105,9 @@ and e_trivial_resolve db_list local_db gl = with Bound | Not_found -> [] let e_possible_resolve db_list local_db gl = - try List.map snd - (e_my_find_search db_list local_db - (List.hd (head_constr_bound gl [])) gl) + try + List.map snd (e_my_find_search db_list local_db + (List.hd (head_constr_bound gl [])) gl) with Bound | Not_found -> [] let find_first_goal gls = @@ -121,6 +125,8 @@ module SearchProblem = struct type state = search_state + let debug = ref false + let success s = (sig_it (fst s.tacres)) = [] let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) @@ -139,19 +145,29 @@ module SearchProblem = struct try let (lgls,ptl) = apply_tac_list tac glls in let v' p = v (ptl p) in -(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) -(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) +(* if !debug then *) +(* begin *) +(* let evars = Evarutil.nf_evars (Refiner.project glls) in *) +(* msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *) +(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) *) +(* end; *) ((lgls,v'),pptac) :: aux tacl with e when Logic.catchable_exception e -> aux tacl in aux l + let nb_empty_evars s = + Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0 + (* Ordering of states is lexicographic on depth (greatest first) then number of remaining goals. *) let compare s s' = let d = s'.depth - s.depth in - let nbgoals s = List.length (sig_it (fst s.tacres)) in - if d <> 0 then d else nbgoals s - nbgoals s' + let nbgoals s = + List.length (sig_it (fst s.tacres)) + + nb_empty_evars (sig_sig (fst s.tacres)) + in + if d <> 0 then d else nbgoals s - nbgoals s' let branching s = if s.depth = 0 then @@ -223,7 +239,8 @@ let make_initial_state n gls dblist localdbs = let e_depth_search debug p db_list local_dbs gls = try - let tac = if debug then Search.debug_depth_first else Search.depth_first in + let tac = if debug then + (SearchProblem.debug := true; Search.debug_depth_first) else Search.depth_first in let s = tac (make_initial_state p gls db_list local_dbs) in s.tacres with Not_found -> error "EAuto: depth first search failed" @@ -350,6 +367,8 @@ let inverse = lazy (gen_constant ["Classes"; "Relations"] "inverse") let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep") let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") +let equivalence = lazy (gen_constant ["Classes"; "Relations"] "Equivalence") + let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence") let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence") @@ -378,7 +397,7 @@ let arrow_morphism a b = let setoid_refl pars x = applistc (Lazy.force setoid_refl_proj) (pars @ [x]) -let morphism_class = lazy (Lazy.force morphism_class, Lazy.force respect_proj) +let morphism_class_proj = lazy (Lazy.force morphism_class, Lazy.force respect_proj) exception Found of (constr * constr * (types * types) list * constr * constr array * (constr * (constr * constr * constr * constr)) option array) @@ -390,16 +409,17 @@ let split_head = function hd :: tl -> hd, tl | [] -> assert(false) -let build_signature isevars env m cstrs finalcstr = +let build_signature isevars env m (cstrs : 'a option list) (f : 'a -> constr) = let new_evar isevars env t = Evarutil.e_new_evar isevars env (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t in let mk_relty ty obj = - let relty = coq_relation ty in - match obj with - | None -> new_evar isevars env relty - | Some (p, (a, r, oldt, newt)) -> r + match obj with + | None -> + let relty = coq_relation ty in + new_evar isevars env relty + | Some x -> f x in let rec aux t l = let t = Reductionops.whd_betadelta env (Evd.evars_of !isevars) t in @@ -409,36 +429,41 @@ let build_signature isevars env m cstrs finalcstr = let relty = mk_relty ty obj in let arg' = mkApp (Lazy.force respectful, [| ty ; relty ; b ; arg |]) in arg', (ty, relty) :: evars - | _, _ -> + | _, [finalcstr] -> (match finalcstr with None -> let rel = mk_relty t None in rel, [t, rel] | Some (t, rel) -> rel, [t, rel]) + | _, _ -> assert false in aux m cstrs -let reflexivity_proof env evars carrier relation x = +let reflexivity_proof_evar env evars carrier relation x = let goal = mkApp (Lazy.force reflexive_type, [| carrier ; relation |]) in let inst = Evarutil.e_new_evar evars env goal in (* try resolve_one_typeclass env goal *) - mkApp (Lazy.force reflexive_proof, [| carrier ; relation ; inst ; x |]) + mkApp (Lazy.force reflexive_proof, [| carrier ; relation ; inst ; x |]) (* with Not_found -> *) (* let meta = Evarutil.new_meta() in *) (* mkCast (mkMeta meta, DEFAULTcast, mkApp (relation, [| x; x |])) *) -let symmetric_proof env carrier relation = +let find_class_proof proof_type proof_method env carrier relation = let goal = - mkApp (Lazy.force symmetric_type, [| carrier ; relation |]) + mkApp (Lazy.force proof_type, [| carrier ; relation |]) in try let inst = resolve_one_typeclass env goal in - mkApp (Lazy.force symmetric_proof, [| carrier ; relation ; inst |]) + mkApp (Lazy.force proof_method, [| carrier ; relation ; inst |]) with e when Logic.catchable_exception e -> raise Not_found +let reflexive_proof env = find_class_proof reflexive_type reflexive_proof env +let symmetric_proof env = find_class_proof symmetric_type symmetric_proof env +let transitive_proof env = find_class_proof transitive_type transitive_proof env + let resolve_morphism env sigma oldt m args args' cstr evars = - let (morphism_cl, morphism_proj) = Lazy.force morphism_class in + let (morphism_cl, morphism_proj) = Lazy.force morphism_class_proj in let morph_instance, proj, sigargs, m', args, args' = (* if is_equiv env sigma m then *) (* let params, rest = array_chop 3 args in *) @@ -462,7 +487,8 @@ let resolve_morphism env sigma oldt m args args' cstr evars = let morphargs', morphobjs' = array_chop first args' in let appm = mkApp(m, morphargs) in let appmtype = Typing.type_of env sigma appm in - let signature, sigargs = build_signature evars env appmtype (Array.to_list morphobjs') cstr in + let cstrs = List.map (function None -> None | Some (_, (a, r, _, _)) -> Some (a, r)) (Array.to_list morphobjs') in + let signature, sigargs = build_signature evars env appmtype (cstrs @ [cstr]) (fun (a, r) -> r) in let cl_args = [| appmtype ; signature ; appm |] in let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in let morph = Evarutil.e_new_evar evars env app in @@ -478,7 +504,7 @@ let resolve_morphism env sigma oldt m args args' cstr evars = let (carrier, relation), sigargs = split_head sigargs in match y with None -> - let refl_proof = reflexivity_proof env evars carrier relation x in + let refl_proof = reflexivity_proof_evar env evars carrier relation x in [ refl_proof ; x ; x ] @ acc, sigargs, x :: typeargs' | Some (p, (_, _, _, t')) -> [ p ; t'; x ] @ acc, sigargs, t' :: typeargs') @@ -490,93 +516,135 @@ let resolve_morphism env sigma oldt m args args' cstr evars = [ a, r ] -> (proof, (a, r, oldt, newt)) | _ -> assert(false) -let build_new gl env sigma occs origt newt hyp hypinfo concl cstr evars = +let rewrite_unif_flags = { + Unification.modulo_conv_on_closed_terms = false; + Unification.use_metas_eagerly = true; + Unification.modulo_conv = false +} + +let rewrite2_unif_flags = { + Unification.modulo_conv_on_closed_terms = true; + Unification.use_metas_eagerly = true; + Unification.modulo_conv = false + } + +(* let unification_rewrite c1 c2 cl but gl = *) +(* let (env',c1) = *) +(* try *) +(* (\* ~flags:(false,true) to allow to mark occurences that must not be *) +(* rewritten simply by replacing them with let-defined definitions *) +(* in the context *\) *) +(* w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) (c1,but) cl.evd *) +(* with *) +(* Pretype_errors.PretypeError _ -> *) +(* (\* ~flags:(true,true) to make Ring work (since it really *) +(* exploits conversion) *\) *) +(* w_unify_to_subterm ~flags:rewrite2_unif_flags *) +(* (pf_env gl) (c1,but) cl.evd *) +(* in *) +(* let cl' = {cl with evd = env' } in *) +(* let c2 = Clenv.clenv_nf_meta cl' c2 in *) +(* check_evar_map_of_evars_defs env' ; *) +(* env',Clenv.clenv_value cl', c1, c2 *) + +let allowK = true + +let unify_eqn gl (cl, rel, l2r, c1, c2) t = + try + let env' = + try clenv_unify allowK ~flags:rewrite_unif_flags + CONV (if l2r then c1 else c2) t cl + with Pretype_errors.PretypeError _ -> (* For Ring essentially *) + clenv_unify allowK ~flags:rewrite2_unif_flags + CONV (if l2r then c1 else c2) t cl + in + let c1 = Clenv.clenv_nf_meta env' c1 + and c2 = Clenv.clenv_nf_meta env' c2 + and typ = Clenv.clenv_type env' in + let (rel, args) = destApp typ in + let relargs, args = array_chop (Array.length args - 2) args in + let rel = mkApp (rel, relargs) in + let car = pf_type_of gl c1 in + let prf = Clenv.clenv_value env' in + let res = + if l2r then (prf, (car, rel, c1, c2)) + else + try (mkApp (symmetric_proof (pf_env gl) car rel, [| c1 ; c2 ; prf |]), (car, rel, c2, c1)) + with Not_found -> + (prf, (car, mkApp (Lazy.force inverse, [| car ; rel |]), c2, c1)) + in Some (env', res) + with _ -> None + +let build_new gl env sigma occs hypinfo concl cstr evars = let is_occ occ = occs = [] || List.mem occ occs in let rec aux t occ cstr = - match kind_of_term t with - | _ when eq_constr t origt -> - if is_occ occ then + match unify_eqn gl hypinfo t with + | Some (env', (prf, hypinfo as x)) -> + if is_occ occ then ( + evars := Evd.evar_merge !evars (Evd.evars_of (Evd.undefined_evars env'.evd)); match cstr with - None -> Some (hyp, hypinfo), succ occ + None -> Some x, succ occ | Some _ -> let (car, r, orig, dest) = hypinfo in let res = try Some (resolve_morphism env sigma t (mkLambda (Name (id_of_string "x"), car, mkRel 1)) - (* (mkApp (Lazy.force coq_id, [| car |])) *) - [| origt |] [| Some (hyp, hypinfo) |] cstr evars) + (* (Termops.refresh_universes (mkApp (Lazy.force coq_id, [| car |]))) *) + [| orig |] [| Some x |] cstr evars) with Not_found -> None - in res, succ occ + in res, succ occ) else None, succ occ - - | App (m, args) -> - let args', occ = - Array.fold_left - (fun (acc, occ) arg -> let res, occ = aux arg occ None in (res :: acc, occ)) - ([], occ) args - in - let res = - if List.for_all (fun x -> x = None) args' then None - else - let args' = Array.of_list (List.rev args') in - (try Some (resolve_morphism env sigma t m args args' cstr evars) - with Not_found -> None) - in res, occ - - | Prod (_, x, b) -> - let x', occ = aux x occ None in - let b', occ = aux b occ None in - let res = - if x' = None && b' = None then None - else - (try Some (resolve_morphism env sigma t - (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |] - cstr evars) - with Not_found -> None) - in res, occ - - | _ -> None, occ + | None -> + match kind_of_term t with + | App (m, args) -> + let args', occ = + Array.fold_left + (fun (acc, occ) arg -> let res, occ = aux arg occ None in (res :: acc, occ)) + ([], occ) args + in + let res = + if List.for_all (fun x -> x = None) args' then None + else + let args' = Array.of_list (List.rev args') in + (try Some (resolve_morphism env sigma t m args args' cstr evars) + with Not_found -> None) + in res, occ + + | Prod (_, x, b) -> + let x', occ = aux x occ None in + let b', occ = aux b occ None in + let res = + if x' = None && b' = None then None + else + (try Some (resolve_morphism env sigma t + (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |] + cstr evars) + with Not_found -> None) + in res, occ + + | _ -> None, occ in aux concl 1 cstr - -let decompose_setoid_eqhyp gl env sigma c left2right t = - let (c, (car, rel, x, y) as res) = - match kind_of_term t with - (* | App (equiv, [| a; r; s; x; y |]) -> *) - (* if dir then (c, (a, r, s, x, y)) *) - (* else (c, (a, r, s, y, x)) *) - | App (r, args) when Array.length args >= 2 -> - let relargs, args = array_chop (Array.length args - 2) args in - let rel = mkApp (r, relargs) in - let typ = pf_type_of gl rel in - (if isArity typ then - let (ctx, ar) = destArity typ in - (match ctx with - [ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy -> - (c, (sx, rel, args.(0), args.(1))) - | _ -> error "Only binary relations are supported") - else error "Not a relation") - | _ -> error "Not a relation" - in - if left2right then res - else - try (mkApp (symmetric_proof env car rel, [| x ; y ; c |]), (car, rel, y, x)) - with Not_found -> - (c, (car, mkApp (Lazy.force inverse, [| car ; rel |]), y, x)) + +(* Adapted from setoid_replace. *) + +let decompose_setoid_eqhyp gl c left2right = + let ctype = pf_type_of gl c in + let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in + let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in + let rec split_last_two = function + | [c1;c2] -> [],(c1, c2) + | x::y::z -> + let l,res = split_last_two (y::z) in x::l, res + | _ -> error "The term provided is not an applied relation" in + let others, (c1,c2) = split_last_two args in + eqclause, mkApp (equiv, Array.of_list others), left2right, c1, c2 let resolve_all_typeclasses env evd = resolve_all_evars false (true, 15) env (fun ev evi -> Typeclasses.class_of_constr evi.Evd.evar_concl <> None) evd -(* let _ = *) -(* Typeclasses.solve_instanciation_problem := *) -(* (fun env evd ev evi -> resolve_all_typeclasses env evd, true) *) - -let cl_rewrite_clause c left2right occs clause gl = - let env = pf_env gl in - let sigma = project gl in - let hyp = pf_type_of gl c in - let hypt, (typ, rel, origt, newt as hypinfo) = decompose_setoid_eqhyp gl env sigma c left2right hyp in +let cl_rewrite_clause_aux hypinfo occs clause gl = let concl, is_hyp = match clause with Some ((_, id), _) -> pf_get_hyp_typ gl id, Some id @@ -588,23 +656,48 @@ let cl_rewrite_clause c left2right occs clause gl = | Some _ -> (mkProp, Lazy.force impl) in let evars = ref (Evd.create_evar_defs Evd.empty) in - let eq, _ = build_new gl env sigma occs origt newt hypt hypinfo concl (Some cstr) evars in + let env = pf_env gl in + let sigma = project gl in + let eq, _ = build_new gl env sigma occs hypinfo concl (Some cstr) evars in match eq with Some (p, (_, _, oldt, newt)) -> - evars := Typeclasses.resolve_typeclasses env (Evd.evars_of !evars) !evars; - evars := Evarutil.nf_evar_defs !evars; - let p = Evarutil.nf_isevar !evars p in - let newt = Evarutil.nf_isevar !evars newt in - let undef = Evd.undefined_evars !evars in - tclTHEN (Refiner.tclEVARS (Evd.evars_of undef)) - (match is_hyp with - | Some id -> Tactics.apply_in true id [p,NoBindings] - | None -> - let meta = Evarutil.new_meta() in - let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in - refine term) gl - | None -> tclIDTAC gl + (try + evars := Typeclasses.resolve_typeclasses env (Evd.evars_of !evars) !evars; + let p = Evarutil.nf_isevar !evars p in + let newt = Evarutil.nf_isevar !evars newt in + let undef = Evd.undefined_evars !evars in + let unfoldrefs = List.map (fun s -> [], EvalConstRef s) [destConst (Lazy.force impl)] in + let rewtac, cleantac = + match is_hyp with + | Some id -> +(* let meta = Evarutil.new_meta() in *) +(* let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in *) +(* tclTHEN *) +(* (tclEVARS (evars_of clenv.evd)) *) + cut_replacing id newt (fun x -> + refine (mkApp (p, [| mkVar id |]))), + unfold_in_hyp unfoldrefs (([], id), Tacexpr.InHyp) + | None -> + let meta = Evarutil.new_meta() in + let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in + refine term, Tactics.unfold_in_concl unfoldrefs + in + let evartac = + let evd = Evd.evars_of undef in + if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd) + else tclIDTAC + in tclTHENLIST [evartac; rewtac; cleantac] gl + with UserError (env, e) -> + tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints") gl) + | None -> + let (_, _, l2r, x, y) = hypinfo in + raise (Pretype_errors.PretypeError (pf_env gl, Pretype_errors.NoOccurrenceFound (if l2r then x else y))) + (* tclFAIL 1 (str"setoid rewrite failed") gl *) +let cl_rewrite_clause c left2right occs clause gl = + let hypinfo = decompose_setoid_eqhyp gl c left2right in + cl_rewrite_clause_aux hypinfo occs clause gl + open Genarg open Extraargs @@ -616,6 +709,7 @@ TACTIC EXTEND class_rewrite | [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o [] None ] END + let clsubstitute o c = let is_tac id = match kind_of_term c with Var id' when id' = id -> true | _ -> false in Tacticals.onAllClauses @@ -680,7 +774,7 @@ END let _ = Typeclasses.solve_instanciations_problem := resolve_argument_typeclasses false (true, 15) - + TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" debug(d) search_mode(s) depth(depth) ] -> [ fun gl -> let env = pf_env gl in @@ -697,21 +791,439 @@ END let _ = Classes.refine_ref := Refine.refine -open Pretype_errors +(* Compatibility with old Setoids *) + +TACTIC EXTEND setoid_rewrite + [ "setoid_rewrite" orient(o) constr(c) ] + -> [ cl_rewrite_clause c o [] None ] + | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) ] -> + [ cl_rewrite_clause c o [] (Some (([],id), []))] + | [ "setoid_rewrite" orient(o) constr(c) "at" occurences(occ) ] -> + [ cl_rewrite_clause c o occ None] + | [ "setoid_rewrite" orient(o) constr(c) "at" occurences(occ) "in" hyp(id)] -> + [ cl_rewrite_clause c o occ (Some (([],id), []))] + | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurences(occ)] -> + [ cl_rewrite_clause c o occ (Some (([],id), []))] +END + +(* let solve_obligation lemma = *) +(* tclTHEN (Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None))) *) +(* (eapply_with_bindings (Constrintern.interp_constr Evd.empty (Global.env()) lemma, NoBindings)) *) + +let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l) + +let declare_instance a aeq n s = ((dummy_loc,Name n),Explicit, + CApp (dummy_loc, (None, mkIdentC (id_of_string s)), + [(a,None);(aeq,None)])) + +let anew_instance instance fields = new_instance [] instance fields None (fun _ -> ()) + +let require_library dirpath = + let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in + Library.require_library [qualid] (Some false) + +let init_setoid () = + require_library "Coq.Setoids.Setoid" + +let declare_instance_refl a aeq n lemma = + let instance = declare_instance a aeq (add_suffix n "_refl") "Reflexive" + in anew_instance instance + [((dummy_loc,id_of_string "reflexive"),[],lemma)] + +let declare_instance_sym a aeq n lemma = + let instance = declare_instance a aeq (add_suffix n "_sym") "Symmetric" + in anew_instance instance + [((dummy_loc,id_of_string "symmetric"),[],lemma)] + +let declare_instance_trans a aeq n lemma = + let instance = declare_instance a aeq (add_suffix n "_trans") "Transitive" + in anew_instance instance + [((dummy_loc,id_of_string "transitive"),[],lemma)] + +let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None)) + +let declare_relation a aeq n refl symm trans = + init_setoid (); + match (refl,symm,trans) with + (None, None, None) -> + let instance = declare_instance a aeq n "Equivalence" + in ignore( + Flags.make_silent true; + anew_instance instance + [((dummy_loc,id_of_string "equiv_refl"), [], CHole(dummy_loc,Some GoalEvar)); + ((dummy_loc,id_of_string "equiv_sym"), [], CHole(dummy_loc,Some GoalEvar)); + ((dummy_loc,id_of_string "equiv_trans"),[], CHole(dummy_loc,Some GoalEvar))]); + solve_nth 1 constr_tac; solve_nth 2 constr_tac; solve_nth 3 constr_tac; + Flags.make_silent false; msg (Printer.pr_open_subgoals ()) + | (Some lemma1, None, None) -> + ignore (declare_instance_refl a aeq n lemma1) + | (None, Some lemma2, None) -> + ignore (declare_instance_sym a aeq n lemma2) + | (None, None, Some lemma3) -> + ignore (declare_instance_trans a aeq n lemma3) + | (Some lemma1, Some lemma2, None) -> + ignore (declare_instance_refl a aeq n lemma1); + ignore (declare_instance_sym a aeq n lemma2) + | (Some lemma1, None, Some lemma3) -> + let lemma_refl = declare_instance_refl a aeq n lemma1 in + let lemma_trans = declare_instance_trans a aeq n lemma3 in + let instance = declare_instance a aeq n "PreOrder" + in ignore( + anew_instance instance + [((dummy_loc,id_of_string "preorder_refl"), [], mkIdentC lemma_refl); + ((dummy_loc,id_of_string "preorder_trans"),[], mkIdentC lemma_trans)]) + | (None, Some lemma2, Some lemma3) -> + let lemma_sym = declare_instance_sym a aeq n lemma2 in + let lemma_trans = declare_instance_trans a aeq n lemma3 in + let instance = declare_instance a aeq n "PER" + in ignore( + anew_instance instance + [((dummy_loc,id_of_string "per_sym"), [], mkIdentC lemma_sym); + ((dummy_loc,id_of_string "per_trans"),[], mkIdentC lemma_trans)]) + | (Some lemma1, Some lemma2, Some lemma3) -> + let lemma_refl = declare_instance_refl a aeq n lemma1 in + let lemma_sym = declare_instance_sym a aeq n lemma2 in + let lemma_trans = declare_instance_trans a aeq n lemma3 in + let instance = declare_instance a aeq n "Equivalence" + in ignore( + anew_instance instance + [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl); + ((dummy_loc,id_of_string "equiv_sym"), [], mkIdentC lemma_sym); + ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)]) + +VERNAC COMMAND EXTEND AddRelation + [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> + [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ] + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "as" ident(n) ] -> + [ declare_relation a aeq n (Some lemma1) None None ] + | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> + [ declare_relation a aeq n None None None ] +END + +VERNAC COMMAND EXTEND AddRelation2 + [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + "as" ident(n) ] -> + [ declare_relation a aeq n None (Some lemma2) None ] + | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + [ declare_relation a aeq n None (Some lemma2) (Some lemma3) ] +END + +VERNAC COMMAND EXTEND AddRelation3 + [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + [ declare_relation a aeq n (Some lemma1) None (Some lemma3) ] + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) + "as" ident(n) ] -> + [ declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] + | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + "as" ident(n) ] -> + [ declare_relation a aeq n None None (Some lemma3) ] +END + +let mk_qualid s = + Libnames.Qualid (dummy_loc, Libnames.qualid_of_string s) -let typeclass_error e = - match e with - | UnsolvableImplicit (evi, (InternalHole | ImplicitArg _)) -> - (match class_of_constr evi.evar_concl with - Some c -> true - | None -> false) - | _ -> false +let cHole = CHole (dummy_loc, None) + +open Entries +open Libnames + +let respect_projection r ty = + let ctx, inst = Sign.decompose_prod_assum ty in + let mor, args = destApp inst in + let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in + let app = mkApp (mkConst (Lazy.force respect_proj), + Array.append args [| instarg |]) in + it_mkLambda_or_LetIn app ctx + +let declare_projection n instance_id r = + let ty = Global.type_of_global r in + let c = constr_of_global r in + let term = respect_projection c ty in + let typ = Typing.type_of (Global.env ()) Evd.empty term in + let typ = + let n = + let rec aux t = + match kind_of_term t with + App (f, [| a ; rel; a'; rel' |]) when eq_constr f (Lazy.force respectful) -> + succ (aux rel') + | _ -> 0 + in + let init = + match kind_of_term typ with + App (f, args) when eq_constr f (Lazy.force respectful) -> + mkApp (f, fst (array_chop (Array.length args - 2) args)) + | _ -> typ + in aux init + in + let ctx,ccl = Reductionops.decomp_n_prod (Global.env()) Evd.empty (3 * n) typ + in it_mkProd_or_LetIn ccl ctx + in + let cst = + { const_entry_body = term; + const_entry_type = Some typ; + const_entry_opaque = false; + const_entry_boxed = false } + in + ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) + +(* try *) +(* Command.declare_definition n (Decl_kinds.Local, false, Decl_kinds.Definition) [] None *) +(* (CAppExpl (dummy_loc, *) +(* (None, mk_qualid "Coq.Classes.Morphisms.respect"), *) +(* [ cHole; cHole; cHole; mkIdentC instance_id ])) *) +(* None (fun _ _ -> ()) *) +(* with _ -> () *) + +let build_morphism_signature m = + let env = Global.env () in + let m = Constrintern.interp_constr Evd.empty env m in + let t = Typing.type_of env Evd.empty m in + let isevars = ref (Evd.create_evar_defs Evd.empty) in + let cstrs = + let rec aux t = + match kind_of_term t with + | Prod (na, a, b) -> + None :: aux b + | _ -> [None] + in aux t + in + let sig_, evars = build_signature isevars env t cstrs snd in + let _ = List.iter + (fun (ty, relty) -> + let equiv = mkApp (Lazy.force equivalence, [| ty; relty |]) in + ignore(Evarutil.e_new_evar isevars env equiv)) + evars + in + let morph = + mkApp (mkInd (Lazy.force morphism_class).cl_impl, [| t; sig_; m |]) + in +(* let morphev = Evarutil.e_new_evar isevars env morph in *) + let evd = resolve_all_evars_once false (true, 15) env + (fun x evi -> class_of_constr evi.Evd.evar_concl <> None) !isevars in + Evarutil.nf_isevar evd morph + +let default_morphism sign m = + let env = Global.env () in + let isevars = ref (Evd.create_evar_defs Evd.empty) in + let t = Typing.type_of env Evd.empty m in + let sign, evars = + build_signature isevars env t sign (fun (ty, rel) -> rel) + in + let morph = + mkApp (mkInd (Lazy.force morphism_class).cl_impl, [| t; sign; m |]) + in + let mor = resolve_one_typeclass env morph in + mor, respect_projection mor morph + +let unfold_respectful = lazy (Tactics.unfold_in_concl [[], EvalConstRef (destConst (Lazy.force respectful))]) + +let ($) g f = fun x -> g (f x) + +VERNAC COMMAND EXTEND AddSetoid1 + [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + [ init_setoid (); + let lemma_refl = declare_instance_refl a aeq n (mkappc "Seq_refl" [a;aeq;t]) in + let lemma_sym = declare_instance_sym a aeq n (mkappc "Seq_sym" [a;aeq;t]) in + let lemma_trans = declare_instance_trans a aeq n (mkappc "Seq_trans" [a;aeq;t]) in + let instance = declare_instance a aeq n "Equivalence" + in ignore( + anew_instance instance + [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl); + ((dummy_loc,id_of_string "equiv_sym"), [], mkIdentC lemma_sym); + ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])] + | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> + [ init_setoid (); + let instance_id = add_suffix n "_Morphism" in + let instance = build_morphism_signature m in + if Lib.is_modtype () then + let cst = Declare.declare_internal_constant instance_id + (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) + in + add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst }; + declare_projection n instance_id (ConstRef cst) + else + let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in + Flags.silently + (fun () -> + Command.start_proof instance_id kind instance + (fun _ -> function + Libnames.ConstRef cst -> + add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst }; + declare_projection n instance_id (ConstRef cst) + | _ -> assert false); + Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) (); + Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () ] + + | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> + [ init_setoid (); + let instance_id = add_suffix n "_Morphism" in + let instance = + ((dummy_loc,Name instance_id), Implicit, + CApp (dummy_loc, (None, mkRefC + (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism"))), + [(s,None);(m,None)])) + in + if Lib.is_modtype () then (context ~hook:(fun r -> declare_projection n instance_id r) [ instance ]) + else ( + Flags.silently + (fun () -> + ignore(new_instance [] instance [] None (fun cst -> declare_projection n instance_id (ConstRef cst))); + Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) (); + Flags.if_verbose (msg $ Printer.pr_open_subgoals) ()) + ] +END + +(** Bind to "rewrite" too *) + +(** Taken from original setoid_replace, to emulate the old rewrite semantics where + lemmas are first instantiated once and then rewrite proceeds. *) + +let unification_rewrite l2r c1 c2 cl but gl = + let (env',c') = + try + (* ~flags:(false,true) to allow to mark occurences that must not be + rewritten simply by replacing them with let-defined definitions + in the context *) + Unification.w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) ((if l2r then c1 else c2),but) cl.evd + with + Pretype_errors.PretypeError _ -> + (* ~flags:(true,true) to make Ring work (since it really + exploits conversion) *) + Unification.w_unify_to_subterm ~flags:rewrite2_unif_flags + (pf_env gl) ((if l2r then c1 else c2),but) cl.evd + in + let cl' = {cl with evd = env' } in + let c1 = Clenv.clenv_nf_meta cl' c1 + and c2 = Clenv.clenv_nf_meta cl' c2 in + cl', Clenv.clenv_value cl', l2r, c1, c2 + +let get_hyp gl c clause l2r = + match kind_of_term (pf_type_of gl c) with + Prod _ -> + let cl, rel, _, c1, c2 = decompose_setoid_eqhyp gl c l2r in + let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in + unification_rewrite l2r c1 c2 cl but gl + | _ -> decompose_setoid_eqhyp gl c l2r -let class_apply c = - try Tactics.apply_with_ebindings c - with PretypeError (env, e) when typeclass_error e -> - tclFAIL 1 (str"typeclass resolution failed") +let general_s_rewrite l2r c ~new_goals gl = + let hypinfo = get_hyp gl c None l2r in + cl_rewrite_clause_aux hypinfo [] None gl -TACTIC EXTEND class_apply -| [ "class_apply" constr_with_bindings(t) ] -> [ class_apply t ] +let general_s_rewrite_in id l2r c ~new_goals gl = + let hypinfo = get_hyp gl c (Some id) l2r in + cl_rewrite_clause_aux hypinfo [] (Some (([],id), [])) gl + +let general_s_rewrite_clause = function + | None -> general_s_rewrite + | Some id -> general_s_rewrite_in id + +let _ = Equality.register_general_setoid_rewrite_clause general_s_rewrite_clause + +(* [setoid_]{reflexivity,symmetry,transitivity} tactics *) + +let relation_of_constr c = + match kind_of_term c with + | App (f, args) when Array.length args >= 2 -> + let relargs, args = array_chop (Array.length args - 2) args in + mkApp (f, relargs), args + | _ -> error "Not an applied relation" + +let setoid_reflexivity gl = + let env = pf_env gl in + let rel, args = relation_of_constr (pf_concl gl) in + try + apply (reflexive_proof env (pf_type_of gl args.(0)) rel) gl + with Not_found -> + tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared reflexive relation") + gl + +let setoid_symmetry gl = + let env = pf_env gl in + let rel, args = relation_of_constr (pf_concl gl) in + try + apply (symmetric_proof env (pf_type_of gl args.(0)) rel) gl + with Not_found -> + tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared symmetric relation") + gl + +let setoid_transitivity c gl = + let env = pf_env gl in + let rel, args = relation_of_constr (pf_concl gl) in + try + apply_with_bindings + ((transitive_proof env (pf_type_of gl args.(0)) rel), + Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ]) gl + with Not_found -> + tclFAIL 0 + (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared transitive relation") gl + +let setoid_symmetry_in id gl = + let ctype = pf_type_of gl (mkVar id) in + let binders,concl = Sign.decompose_prod_assum ctype in + let (equiv, args) = decompose_app concl in + let rec split_last_two = function + | [c1;c2] -> [],(c1, c2) + | x::y::z -> let l,res = split_last_two (y::z) in x::l, res + | _ -> error "The term provided is not an equivalence" + in + let others,(c1,c2) = split_last_two args in + let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in + let new_hyp' = mkApp (he, [| c2 ; c1 |]) in + let new_hyp = it_mkProd_or_LetIn new_hyp' binders in + tclTHENS (cut new_hyp) + [ intro_replacing id; + tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ] ] + gl + +let _ = Tactics.register_setoid_reflexivity setoid_reflexivity +let _ = Tactics.register_setoid_symmetry setoid_symmetry +let _ = Tactics.register_setoid_symmetry_in setoid_symmetry_in +let _ = Tactics.register_setoid_transitivity setoid_transitivity + +TACTIC EXTEND setoid_symmetry + [ "setoid_symmetry" ] -> [ setoid_symmetry ] + | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] +END + +TACTIC EXTEND setoid_reflexivity + [ "setoid_reflexivity" ] -> [ setoid_reflexivity ] +END + +TACTIC EXTEND setoid_transitivity + [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] END + +(* open Pretype_errors *) + +(* let typeclass_error e = *) +(* match e with *) +(* | UnsolvableImplicit (evi, (InternalHole | ImplicitArg _)) -> *) +(* (match class_of_constr evi.evar_concl with *) +(* Some c -> true *) +(* | None -> false) *) +(* | _ -> false *) + +(* let class_apply c = *) +(* try Tactics.apply_with_ebindings c *) +(* with PretypeError (env, e) when typeclass_error e -> *) +(* tclFAIL 1 (str"typeclass resolution failed") *) + +(* TACTIC EXTEND class_apply *) +(* | [ "class_apply" constr_with_bindings(t) ] -> [ class_apply t ] *) +(* END *) + +(* let default_morphism ?(filter=fun _ -> true) m = *) +(* match List.filter filter (morphism_table_find m) with *) +(* [] -> raise Not_found *) +(* | m1::ml -> *) +(* if ml <> [] then *) +(* Flags.if_warn msg_warning *) +(* (strbrk "There are several morphisms associated to \"" ++ *) +(* pr_lconstr m ++ strbrk "\". Morphism " ++ prmorphism m m1 ++ *) +(* strbrk " is randomly chosen."); *) +(* relation_morphism_of_constr_morphism m1 *) + diff --git a/tactics/equality.ml b/tactics/equality.ml index b6c3acfac..93b555b34 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -51,10 +51,6 @@ open Indrec -- Eduardo (19/8/97) *) -let general_s_rewrite_clause = function - | None -> general_s_rewrite - | Some id -> general_s_rewrite_in id - (* Ad hoc asymmetric general_elim_clause *) let general_elim_clause with_evars cls c elim = match cls with | None -> @@ -81,6 +77,13 @@ let elimination_sort_of_clause = function else back to the old approach *) +let general_s_rewrite_clause = function + | None -> general_s_rewrite + | Some id -> general_s_rewrite_in id + +let general_setoid_rewrite_clause = ref general_s_rewrite_clause +let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause + let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl = let ctype = pf_apply get_type_of gl c in (* A delta-reduction would be here too strong, since it would @@ -88,7 +91,7 @@ let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl = let t = snd (decompose_prod (whd_betaiotazeta ctype)) in let head = if isApp t then fst (destApp t) else t in if relation_table_mem head && l = NoBindings then - general_s_rewrite_clause cls lft2rgt c [] gl + !general_setoid_rewrite_clause cls lft2rgt c [] gl else (* Original code. In particular, [splay_prod] performs delta-reduction. *) let env = pf_env gl in @@ -97,7 +100,7 @@ let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl = match match_with_equation t with | None -> if l = NoBindings - then general_s_rewrite_clause cls lft2rgt c [] gl + then !general_setoid_rewrite_clause cls lft2rgt c [] gl else error "The term provided does not end with an equation" | Some (hdcncl,_) -> let hdcncls = string_of_inductive hdcncl in @@ -109,7 +112,13 @@ let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl = with Not_found -> error ("Cannot find rewrite principle "^rwr_thm) in - general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl + try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl + with e -> + let eq = build_coq_eq () in + if not (eq_constr eq head) then + try !general_setoid_rewrite_clause cls lft2rgt c [] gl + with _ -> raise e + else raise e let general_rewrite_ebindings = general_rewrite_ebindings_clause None diff --git a/tactics/equality.mli b/tactics/equality.mli index 475304fb6..846487f96 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -41,6 +41,10 @@ val rewriteRL : constr -> tactic (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *) +val register_general_setoid_rewrite_clause : + (identifier option -> + bool -> constr -> new_goals:constr list -> tactic) -> unit + val general_rewrite_bindings_in : bool -> identifier -> constr with_bindings -> evars_flag -> tactic val general_rewrite_in : diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 0fff16cf9..dd0fecc82 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -150,82 +150,82 @@ let refine_tac = h_refine open Setoid_replace -TACTIC EXTEND setoid_replace - [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] -> - [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] -> - [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> - [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> - [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] -> - [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] -> - [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> - [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> - [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] -END - -TACTIC EXTEND setoid_rewrite - [ "setoid_rewrite" orient(b) constr(c) ] - -> [ general_s_rewrite b c ~new_goals:[] ] - | [ "setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ] - -> [ general_s_rewrite b c ~new_goals:l ] - | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] -> - [ general_s_rewrite_in h b c ~new_goals:[] ] - | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] -> - [ general_s_rewrite_in h b c ~new_goals:l ] -END - -VERNAC COMMAND EXTEND AddSetoid1 - [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid n a aeq t ] -| [ "Add" "Morphism" constr(m) ":" ident(n) ] -> - [ new_named_morphism n m None ] -| [ "Add" "Morphism" constr(m) "with" "signature" morphism_signature(s) "as" ident(n) ] -> - [ new_named_morphism n m (Some s)] -END - -VERNAC COMMAND EXTEND AddRelation1 - [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> - [ add_relation n a aeq (Some t) (Some t') None ] -| [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "as" ident(n) ] -> - [ add_relation n a aeq (Some t) None None ] -| [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> - [ add_relation n a aeq None None None ] -END - -VERNAC COMMAND EXTEND AddRelation2 - [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> - [ add_relation n a aeq None (Some t') None ] -| [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> - [ add_relation n a aeq None (Some t') (Some t'') ] -END - -VERNAC COMMAND EXTEND AddRelation3 - [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "transitivity" "proved" "by" constr(t') "as" ident(n) ] -> - [ add_relation n a aeq (Some t) None (Some t') ] -| [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> - [ add_relation n a aeq (Some t) (Some t') (Some t'') ] -| [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(t) "as" ident(n) ] -> - [ add_relation n a aeq None None (Some t) ] -END - -TACTIC EXTEND setoid_symmetry - [ "setoid_symmetry" ] -> [ setoid_symmetry ] - | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] -END - -TACTIC EXTEND setoid_reflexivity - [ "setoid_reflexivity" ] -> [ setoid_reflexivity ] -END - -TACTIC EXTEND setoid_transitivity - [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] -END +(* TACTIC EXTEND setoid_replace *) +(* [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] -> *) +(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] -> *) +(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *) +(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *) +(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] -> *) +(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] -> *) +(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *) +(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *) +(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] *) +(* END *) + +(* TACTIC EXTEND setoid_rewrite *) +(* [ "setoid_rewrite" orient(b) constr(c) ] *) +(* -> [ general_s_rewrite b c ~new_goals:[] ] *) +(* | [ "setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ] *) +(* -> [ general_s_rewrite b c ~new_goals:l ] *) +(* | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] -> *) +(* [ general_s_rewrite_in h b c ~new_goals:[] ] *) +(* | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] -> *) +(* [ general_s_rewrite_in h b c ~new_goals:l ] *) +(* END *) + +(* VERNAC COMMAND EXTEND AddSetoid1 *) +(* [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> *) +(* [ add_setoid n a aeq t ] *) +(* | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> *) +(* [ new_named_morphism n m None ] *) +(* | [ "Add" "Morphism" constr(m) "with" "signature" morphism_signature(s) "as" ident(n) ] -> *) +(* [ new_named_morphism n m (Some s)] *) +(* END *) + +(* VERNAC COMMAND EXTEND AddRelation1 *) +(* [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *) +(* [ add_relation n a aeq (Some t) (Some t') None ] *) +(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "as" ident(n) ] -> *) +(* [ add_relation n a aeq (Some t) None None ] *) +(* | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> *) +(* [ add_relation n a aeq None None None ] *) +(* END *) + +(* VERNAC COMMAND EXTEND AddRelation2 *) +(* [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *) +(* [ add_relation n a aeq None (Some t') None ] *) +(* | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> *) +(* [ add_relation n a aeq None (Some t') (Some t'') ] *) +(* END *) + +(* VERNAC COMMAND EXTEND AddRelation3 *) +(* [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "transitivity" "proved" "by" constr(t') "as" ident(n) ] -> *) +(* [ add_relation n a aeq (Some t) None (Some t') ] *) +(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> *) +(* [ add_relation n a aeq (Some t) (Some t') (Some t'') ] *) +(* | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(t) "as" ident(n) ] -> *) +(* [ add_relation n a aeq None None (Some t) ] *) +(* END *) + +(* TACTIC EXTEND setoid_symmetry *) +(* [ "setoid_symmetry" ] -> [ setoid_symmetry ] *) +(* | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] *) +(* END *) + +(* TACTIC EXTEND setoid_reflexivity *) +(* [ "setoid_reflexivity" ] -> [ setoid_reflexivity ] *) +(* END *) + +(* TACTIC EXTEND setoid_transitivity *) +(* [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] *) +(* END *) (* Inversion lemmas (Leminv) *) diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 0214a940c..7e7b81ebf 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -2017,7 +2017,3 @@ let setoid_transitivity c gl = Optimize -> transitivity_red true c gl ;; -Tactics.register_setoid_reflexivity setoid_reflexivity;; -Tactics.register_setoid_symmetry setoid_symmetry;; -Tactics.register_setoid_symmetry_in setoid_symmetry_in;; -Tactics.register_setoid_transitivity setoid_transitivity;; diff --git a/test-suite/typeclasses/clrewrite.v b/test-suite/typeclasses/clrewrite.v index 5c56a0daf..2978fda26 100644 --- a/test-suite/typeclasses/clrewrite.v +++ b/test-suite/typeclasses/clrewrite.v @@ -108,4 +108,4 @@ Section Trans. apply H0. Qed. -End Trans.
\ No newline at end of file +End Trans. diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index bf2602180..da302ea9d 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -101,6 +101,31 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "using" "relation" constr(rel) "by" tactic(t) := setoidreplacein (rel x y) id ltac:t. + + +Ltac red_subst_eq_morphism concl := + match concl with + | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R' + | ?R ==> ?R' => red ; intros ; red_subst_eq_morphism R' + | _ => idtac + end. + +Ltac destruct_morphism := + match goal with + | [ |- @Morphism ?A ?R ?m ] => constructor + end. + +Ltac reverse_arrows x := + match x with + | @Logic.eq ?A ==> ?R' => revert_last ; reverse_arrows R' + | ?R ==> ?R' => do 3 revert_last ; reverse_arrows R' + | _ => idtac + end. + +Ltac add_morphism_tactic := (try destruct_morphism) ; + match goal with + | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y) + end. Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z. Proof with auto. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 87111b1a7..78962fd1b 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -660,48 +660,50 @@ Add Relation key E.eq transitivity proved by E.eq_trans as KeySetoid. -Add Relation t Equal - reflexivity proved by Equal_refl - symmetry proved by Equal_sym - transitivity proved by Equal_trans +Implicit Arguments Equal [[elt]]. + +Add Relation (t elt) Equal + reflexivity proved by (@Equal_refl elt) + symmetry proved by (@Equal_sym elt) + transitivity proved by (@Equal_trans elt) as EqualSetoid. -Add Morphism In with signature E.eq ==> Equal ==> iff as In_m. +Add Morphism (@In elt) with signature E.eq ==> Equal ==> iff as In_m. Proof. -unfold Equal; intros elt k k' Hk m m' Hm. +unfold Equal; intros k k' Hk m m' Hm. rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition. Qed. -Add Morphism MapsTo - with signature E.eq ==> @Logic.eq ==> Equal ==> iff as MapsTo_m. +Add Morphism (@MapsTo elt) + with signature E.eq ==> Logic.eq ==> Equal ==> iff as MapsTo_m. Proof. -unfold Equal; intros elt k k' Hk e m m' Hm. +unfold Equal; intros k k' Hk e m m' Hm. rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; intuition. Qed. -Add Morphism Empty with signature Equal ==> iff as Empty_m. +Add Morphism (@Empty elt) with signature Equal ==> iff as Empty_m. Proof. -unfold Empty; intros elt m m' Hm; intuition. +unfold Empty; intros m m' Hm; intuition. rewrite <-Hm in H0; eauto. rewrite Hm in H0; eauto. Qed. -Add Morphism is_empty with signature Equal ==> @Logic.eq as is_empty_m. +Add Morphism (@is_empty elt) with signature Equal ==> Logic.eq as is_empty_m. Proof. -intros elt m m' Hm. +intros m m' Hm. rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition. Qed. -Add Morphism mem with signature E.eq ==> Equal ==> @Logic.eq as mem_m. +Add Morphism (@mem elt) with signature E.eq ==> Equal ==> Logic.eq as mem_m. Proof. -intros elt k k' Hk m m' Hm. +intros k k' Hk m m' Hm. rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition. Qed. -Add Morphism find with signature E.eq ==> Equal ==> @Logic.eq as find_m. +Add Morphism (@find elt) with signature E.eq ==> Equal ==> Logic.eq as find_m. Proof. -intros elt k k' Hk m m' Hm. +intros k k' Hk m m' Hm. generalize (find_mapsto_iff m k)(find_mapsto_iff m' k') (not_find_in_iff m k)(not_find_in_iff m' k'); do 2 destruct find; auto; intros. @@ -710,27 +712,27 @@ rewrite <- H1, Hk, Hm, H2; auto. symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto. Qed. -Add Morphism add with signature - E.eq ==> @Logic.eq ==> Equal ==> Equal as add_m. +Add Morphism (@add elt) with signature + E.eq ==> Logic.eq ==> Equal ==> Equal as add_m. Proof. -intros elt k k' Hk e m m' Hm y. +intros k k' Hk e m m' Hm y. rewrite add_o, add_o; do 2 destruct eq_dec; auto. elim n; rewrite <-Hk; auto. elim n; rewrite Hk; auto. Qed. -Add Morphism remove with signature +Add Morphism (@remove elt) with signature E.eq ==> Equal ==> Equal as remove_m. Proof. -intros elt k k' Hk m m' Hm y. +intros k k' Hk m m' Hm y. rewrite remove_o, remove_o; do 2 destruct eq_dec; auto. elim n; rewrite <-Hk; auto. elim n; rewrite Hk; auto. Qed. -Add Morphism map with signature @Logic.eq ==> Equal ==> Equal as map_m. +Add Morphism (@map elt elt') with signature Logic.eq ==> Equal ==> Equal as map_m. Proof. -intros elt elt' f m m' Hm y. +intros f m m' Hm y. rewrite map_o, map_o, Hm; auto. Qed. @@ -1102,7 +1104,7 @@ Module WProperties (E:DecidableType)(M:WSfun E). End Elt. - Add Morphism cardinal with signature Equal ==> @Logic.eq as cardinal_m. + Add Morphism (@cardinal elt) with signature Equal ==> Logic.eq as cardinal_m. Proof. intros; apply Equal_cardinal; auto. Qed. End WProperties. diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 8ee74649e..b0c8ee008 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -339,7 +339,7 @@ exact (H1 (refl_equal true) _ Ha). Qed. Add Morphism Empty with signature Equal ==> iff as Empty_m. -Proof. +Proof. intros; do 2 rewrite is_empty_iff; rewrite H; intuition. Qed. @@ -429,13 +429,13 @@ Add Relation t Subset the two previous lemmas, in order to allow conversion of SubsetSetoid coming from separate Facts modules. See bug #1738. *) -Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m. +Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1. Proof. -unfold Subset, impl; intros; eauto with set. + do 2 red ; intros. unfold Subset, impl; intros; eauto with set. Qed. Add Morphism Empty with signature Subset --> impl as Empty_s_m. -Proof. +Proof. unfold Subset, Empty, impl; firstorder. Qed. diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index 866c3f620..c2bba9283 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -125,7 +125,7 @@ Module Raw (X: DecidableType). Lemma In_eq : forall (s : t) (x y : elt), X.eq x y -> In x s -> In y s. Proof. - intros s x y; do 2 setoid_rewrite InA_alt; firstorder eauto. + intros s x y; setoid_rewrite InA_alt; firstorder eauto. Qed. Hint Immediate In_eq. diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v index db09c2ec7..e885d25bc 100644 --- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v +++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v @@ -143,7 +143,7 @@ Hypothesis A0 : A 0. Hypothesis AS : forall n : NZ, A n <-> A (S n). (* Below, we use only -> direction *) Add Morphism A with signature NZeq ==> iff as A_morph. -Proof A_wd. +Proof. apply A_wd. Qed. Let B (n : Z) := A (Z_to_NZ n). diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 730d8a00f..084560de3 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -64,7 +64,7 @@ something like this. The same goes for "relation". *) Hypothesis A_wd : predicate_wd NZeq A. Add Morphism A with signature NZeq ==> iff as A_morph. -Proof A_wd. +Proof. apply A_wd. Qed. Theorem NZcentral_induction : forall z : NZ, A z -> diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 0708e060a..bc3600f9c 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -396,7 +396,7 @@ Variable A : NZ -> Prop. Hypothesis A_wd : predicate_wd NZeq A. Add Morphism A with signature NZeq ==> iff as A_morph. -Proof A_wd. +Proof. apply A_wd. Qed. Section Center. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 0a3d1a586..27d9c72bd 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *) Definition if_zero (A : Set) (a b : A) (n : N) : A := recursion a (fun _ _ => b) n. -Add Morphism if_zero with signature @eq ==> @eq ==> Neq ==> @eq as if_zero_wd. +Add Morphism (if_zero A) with signature (eq ==> eq ==> Neq ==> eq) as if_zero_wd. Proof. intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)). reflexivity. unfold fun2_eq; now intros. assumption. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 9ddaa9a2f..7b4645be3 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -407,7 +407,7 @@ Variable R : N -> N -> Prop. Hypothesis R_wd : relation_wd Neq Neq R. Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2. -Proof R_wd. +Proof. apply R_wd. Qed. Theorem le_ind_rel : (forall m : N, R 0 m) -> diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index e66bc8ebf..c063c7bc1 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -148,15 +148,15 @@ intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2. now symmetry. Qed. -Add Relation (fun A B : Type => A -> B -> Prop) relations_eq - reflexivity proved by (fun A B : Type => proj1 (relations_eq_equiv A B)) - symmetry proved by (fun A B : Type => proj2 (proj2 (relations_eq_equiv A B))) - transitivity proved by (fun A B : Type => proj1 (proj2 (relations_eq_equiv A B))) +Add Relation (A -> B -> Prop) (@relations_eq A B) + reflexivity proved by (proj1 (relations_eq_equiv A B)) + symmetry proved by (proj2 (proj2 (relations_eq_equiv A B))) + transitivity proved by (proj1 (proj2 (relations_eq_equiv A B))) as relations_eq_rel. -Add Morphism well_founded with signature relations_eq ==> iff as well_founded_wd. +Add Morphism (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd. Proof. -unfold relations_eq, well_founded; intros A R1 R2 H; +unfold relations_eq, well_founded; intros R1 R2 H; split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor; intros y H4; apply H3; [now apply <- H | now apply -> H]. Qed. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 5199333ed..cde670075 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -200,7 +200,7 @@ Proof. unfold Qeq, Qopp; simpl. Open Scope Z_scope. intros. - replace (- Qnum x1 * ' Qden x2) with (- (Qnum x1 * ' Qden x2)) by ring. + replace (- Qnum x * ' Qden y) with (- (Qnum x * ' Qden y)) by ring. rewrite H in |- *; ring. Close Scope Z_scope. Qed. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index 8d76b4f4e..61b70ba68 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -83,9 +83,9 @@ Variable leA : A -> A -> Prop. Variable leB : B -> B -> Prop. Inductive le_AsB : A + B -> A + B -> Prop := - | le_aa : forall x y:A, leA x y -> le_AsB (inl B x) (inl B y) - | le_ab : forall (x:A) (y:B), le_AsB (inl B x) (inr A y) - | le_bb : forall x y:B, leB x y -> le_AsB (inr A x) (inr A y). + | le_aa : forall x y:A, leA x y -> le_AsB (inl x) (inl y) + | le_ab : forall (x:A) (y:B), le_AsB (inl x) (inr y) + | le_bb : forall x y:B, leB x y -> le_AsB (inr x) (inr y). End Disjoint_Union. diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index f93a12955..34bff6354 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -10,8 +10,8 @@ Set Implicit Arguments. -Require Export Setoid_tac. -Require Export Setoid_Prop. +Require Export Coq.Classes.Equivalence. +Require Export Coq.Relations.Relation_Definitions. (** For backward compatibility *) diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 026a305b1..2f8ef8d11 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require Import Relations. +Require Import Coq.Relations.Relations. Require Import List. Require Import Multiset. Require Import Arith. diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index f6ce84f98..a86d19c09 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -21,7 +21,7 @@ Section Wf_Disjoint_Union. Notation Le_AsB := (le_AsB A B leA leB). - Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x). + Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl x). Proof. induction 1. apply Acc_intro; intros y H2. @@ -30,7 +30,7 @@ Section Wf_Disjoint_Union. Qed. Lemma acc_B_sum : - well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x). + well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr x). Proof. induction 2. apply Acc_intro; intros y H3. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index de3b76e95..ff8033eeb 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -931,7 +931,7 @@ Module EqualityModulo (M:SomeNumber). Add Morphism Zopp : Zopp_eqm. Proof. - intros; change (-x1 == -x2) with (0-x1 == 0-x2). + intros; change (-x == -y) with (0-x == 0-y). rewrite H; red; auto. Qed. |