diff options
| -rw-r--r-- | Makefile.common | 4 | ||||
| -rw-r--r-- | contrib/subtac/g_subtac.ml4 | 2 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 11 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 1 | ||||
| -rw-r--r-- | tactics/class_setoid.ml4 | 138 | ||||
| -rw-r--r-- | theories/Classes/Init.v | 2 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 350 | ||||
| -rw-r--r-- | theories/Classes/Relations.v | 340 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 26 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 48 | ||||
| -rw-r--r-- | theories/Program/Basics.v | 2 | ||||
| -rw-r--r-- | toplevel/classes.ml | 57 | ||||
| -rw-r--r-- | toplevel/classes.mli | 2 |
13 files changed, 570 insertions, 413 deletions
diff --git a/Makefile.common b/Makefile.common index 3ba5fcede4..c0537f264e 100644 --- a/Makefile.common +++ b/Makefile.common @@ -704,8 +704,8 @@ SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theor UNICODEVO:= theories/Unicode/Utf8.vo -CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/SetoidClass.vo \ - theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo +CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/Morphisms.vo \ + theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo THEORIESVO:=\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 51e1a1709d..337cd16967 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -140,7 +140,7 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations VERNAC COMMAND EXTEND Subtac_Set_Solver | [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ - Subtac.require_library "Coq.Program.Tactics"; + Coqlib.check_required_library ["Coq";"Program";"Tactics"]; Tacinterp.add_tacdef false [((dummy_loc, id_of_string "obligations_tactic"), true, t)] ] END diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index febfb04947..f9ab283ada 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -216,6 +216,7 @@ let instances r = with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id) let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false) +let solve_instanciations_problem = ref (fun _ _ -> assert false) let resolve_typeclass env ev evi (evd, defined as acc) = try @@ -250,7 +251,7 @@ let resolve_one_typeclass_evd env evd types = let evm' = Evd.evars_of evd' in match Evd.evar_body (Evd.find evm' ev) with Evar_empty -> raise Not_found - | Evar_defined c -> c + | Evar_defined c -> Evarutil.nf_evar evm' c else raise Not_found with Exit -> raise Not_found @@ -278,6 +279,8 @@ let destClassApp c = | _ -> None let resolve_typeclasses ?(check=true) env sigma evd = +(* try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *) +(* with _ -> *) let evm = Evd.evars_of evd in let tc_evars = let f ev evi acc = @@ -296,14 +299,14 @@ let resolve_typeclasses ?(check=true) env sigma evd = (fun ev evi acc -> if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then resolve_typeclass env ev evi acc - else acc) + else acc) (Evd.evars_of evars) (evars, false) in if not progress then evars' else sat (Evarutil.nf_evar_defs evars') - in sat evd - + in sat (Evarutil.nf_evar_defs evd) + let class_of_constr c = let extract_ind c = match kind_of_term c with diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index ec3350a586..db408c8898 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -64,6 +64,7 @@ val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_def val resolve_typeclasses : ?check:bool -> env -> evar_map -> evar_defs -> evar_defs val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref +val solve_instanciations_problem : (env -> evar_defs -> evar_defs) ref type substitution = (identifier * constr) list diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4 index dcc3ffbd24..b0a6b36c6d 100644 --- a/tactics/class_setoid.ml4 +++ b/tactics/class_setoid.ml4 @@ -54,6 +54,7 @@ let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2") let iff = lazy (gen_constant ["Init"; "Logic"] "iff") let impl = lazy (gen_constant ["Program"; "Basics"] "impl") let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow") +let coq_id = lazy (gen_constant ["Program"; "Basics"] "id") let reflexive_type = lazy (gen_constant ["Classes"; "Relations"] "Reflexive") let reflexive_proof = lazy (gen_constant ["Classes"; "Relations"] "reflexive") @@ -66,8 +67,8 @@ let transitive_proof = lazy (gen_constant ["Classes"; "Relations"] "transitive") let inverse = lazy (gen_constant ["Classes"; "Relations"] "inverse") -let respectful_dep = lazy (gen_constant ["Classes"; "Relations"] "respectful_dep") -let respectful = lazy (gen_constant ["Classes"; "Relations"] "respectful") +let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep") +let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence") let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence") @@ -100,7 +101,7 @@ exception Found of (constr * constr * (types * types) list * constr * constr arr let resolve_morphism_evd env evd app = let ev = Evarutil.e_new_evar evd env app in - let evd' = resolve_typeclasses ~check:false env (Evd.evars_of !evd) !evd in + let evd' = resolve_typeclasses ~check:true env (Evd.evars_of !evd) !evd in let evm' = Evd.evars_of evd' in match Evd.evar_body (Evd.find evm' (fst (destEvar ev))) with Evd.Evar_empty -> raise Not_found @@ -141,17 +142,18 @@ let build_signature isevars env m cstrs finalcstr = | _, _ -> assert false in aux m cstrs -let reflexivity_proof env carrier relation x = - let goal = +let reflexivity_proof env evars carrier relation x = + let goal = mkApp (Lazy.force reflexive_type, [| carrier ; relation |]) in - try let inst = resolve_one_typeclass env goal in - 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 inst = Evarutil.e_new_evar evars env goal in + (* try resolve_one_typeclass env goal *) + 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 resolve_morphism env sigma direction oldt m args args' cstr = +let resolve_morphism env sigma oldt m args args' cstr evars = let (morphism_cl, morphism_proj) = Lazy.force morphism_class in let morph_instance, proj, sigargs, m', args, args' = (* if is_equiv env sigma m then *) @@ -165,45 +167,38 @@ let resolve_morphism env sigma direction oldt m args args' cstr = (* let m' = mkApp (m, [| a; r; s |]) in *) (* inst, proj, ctxargs, m', rest, rest' *) (* else *) - let evars = ref (Evd.create_evar_defs Evd.empty) in - let pars = - match Array.length args with - 1 -> [1] - | 2 -> [2;1] - | 3 -> [3;2;1] - | _ -> [4;3;2;1] - in - try - List.iter (fun n -> - evars := Evd.create_evar_defs Evd.empty; - let morphargs, morphobjs = array_chop (Array.length args - n) args in - let morphargs', morphobjs' = array_chop (Array.length args - n) 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 cl_args = [| appmtype ; signature ; appm |] in - let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in - try - let morph = resolve_morphism_evd env evars app in - let evm = Evd.evars_of !evars in - let sigargs = List.map - (fun x, y -> Reductionops.nf_evar evm x, Reductionops.nf_evar evm y) - sigargs - in - let appm = Reductionops.nf_evar evm appm in - let cl_args = Array.map (Reductionops.nf_evar evm) cl_args in - let proj = - mkApp (mkConst morphism_proj, - Array.append cl_args [|morph|]) - in - raise (Found (morph, proj, sigargs, appm, morphobjs, morphobjs')) - with Not_found -> () - | Reduction.NotConvertible -> () - | Stdpp.Exc_located (_, Pretype_errors.PretypeError _) - | Pretype_errors.PretypeError _ -> ()) - pars; - raise Not_found - with Found x -> x + let first = + let first = ref (-1) in + for i = 0 to Array.length args' - 1 do + if !first = -1 && args'.(i) <> None then first := i + done; + !first + in +(* try *) + let morphargs, morphobjs = array_chop first args in + 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 cl_args = [| appmtype ; signature ; appm |] in + let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in +(* let morph = resolve_morphism_evd env evars app in *) + let morph = Evarutil.e_new_evar evars env app in +(* let evm = Evd.evars_of !evars in *) +(* let sigargs = List.map *) +(* (fun x, y -> Reductionops.nf_evar evm x, Reductionops.nf_evar evm y) *) +(* sigargs *) +(* in *) +(* let appm = Reductionops.nf_evar evm appm in *) +(* let cl_args = Array.map (Reductionops.nf_evar evm) cl_args in *) + let proj = + mkApp (mkConst morphism_proj, + Array.append cl_args [|morph|]) + in + morph, proj, sigargs, appm, morphobjs, morphobjs' +(* with Reduction.NotConvertible *) +(* | Stdpp.Exc_located (_, Pretype_errors.PretypeError _) *) +(* | Pretype_errors.PretypeError _ -> raise Not_found *) in let projargs, respars, typeargs = array_fold_left2 @@ -211,7 +206,7 @@ let resolve_morphism env sigma direction oldt m args args' cstr = let (carrier, relation), sigargs = split_head sigargs in match y with None -> - let refl_proof = reflexivity_proof env carrier relation x in + let refl_proof = reflexivity_proof env evars carrier relation x in [ refl_proof ; x ; x ] @ acc, sigargs, x :: typeargs' | Some (p, (_, _, _, t')) -> [ p ; t'; x ] @ acc, sigargs, t' :: typeargs') @@ -223,13 +218,24 @@ let resolve_morphism env sigma direction oldt m args args' cstr = [ a, r ] -> (proof, (a, r, oldt, newt)) | _ -> assert(false) -let build_new gl env sigma direction occs origt newt hyp hypinfo concl cstr = +let build_new gl env sigma occs origt newt hyp 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 - Some (hyp, hypinfo), succ occ + match cstr with + None -> Some (hyp, hypinfo), 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) + with Not_found -> None + in res, succ occ else None, succ occ | App (m, args) -> @@ -242,7 +248,7 @@ let build_new gl env sigma direction occs origt newt hyp hypinfo concl cstr = 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 direction t m args args' cstr) + (try Some (resolve_morphism env sigma t m args args' cstr evars) with Not_found -> None) in res, occ @@ -252,9 +258,9 @@ let build_new gl env sigma direction occs origt newt hyp hypinfo concl cstr = let res = if x' = None && b' = None then None else - (try Some (resolve_morphism env sigma direction t + (try Some (resolve_morphism env sigma t (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |] - cstr) + cstr evars) with Not_found -> None) in res, occ @@ -287,6 +293,13 @@ let decompose_setoid_eqhyp gl env sigma c left2right t = if left2right then res else (c, (car, mkApp (Lazy.force inverse, [| car ; rel |]), y, x)) +let resolve_all_typeclasses env evd = + Eauto.resolve_all_evars env (fun x -> Typeclasses.class_of_constr x <> 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 @@ -302,10 +315,19 @@ let cl_rewrite_clause c left2right occs clause gl = None -> (mkProp, mkApp (Lazy.force inverse, [| mkProp; Lazy.force impl |])) | Some _ -> (mkProp, Lazy.force impl) in - let eq, _ = build_new gl env sigma left2right occs origt newt hypt hypinfo concl (Some cstr) 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 match eq with Some (p, (_, _, oldt, newt)) -> - (match is_hyp with +(* evars := Typeclasses.resolve_typeclasses ~check:false env (Evd.evars_of !evars) !evars; *) + evars := Classes.resolve_all_typeclasses env !evars; +(* evars := resolve_all_typeclasses env !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 diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index b5352e720a..aec2608735 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -1 +1 @@ -Ltac typeclass_instantiation := eauto 50 with typeclass_instances || eauto. +Ltac typeclass_instantiation := eauto with typeclass_instances || eauto. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v new file mode 100644 index 0000000000..09a58fa019 --- /dev/null +++ b/theories/Classes/Morphisms.v @@ -0,0 +1,350 @@ +(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Typeclass-based morphisms with standard instances for equivalence relations. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud + 91405 Orsay, France *) + +(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) + +Require Import Coq.Program.Program. +Require Import Coq.Classes.Init. +Require Export Coq.Classes.Relations. + +Set Implicit Arguments. +Unset Strict Implicit. + +(** * Morphisms. + + We now turn to the definition of [Morphism] and declare standard instances. + These will be used by the [clrewrite] tactic later. *) + +(** Respectful morphisms. *) + +Definition respectful_depT (A : Type) (R : relationT A) + (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) := + fun f g => forall x y : A, R x y -> R' x y (f x) (g y). + +Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) := + Eval compute in (respectful_depT eqa (fun _ _ => eqb)). + +Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) := + fun f g => forall x y : A, R x y -> R' (f x) (g y). + +(** Notations reminiscent of the old syntax for declaring morphisms. + We use three + or - for type morphisms, and two for [Prop] ones. + *) + +Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20). +Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20). + +Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20). +Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20). + +(** A morphism on a relation [R] is an object respecting the relation (in its kernel). + The relation [R] will be instantiated by [respectful] and [A] by an arrow type + for usual morphisms. *) + +Class Morphism A (R : relationT A) (m : A) := + respect : R m m. + +(** Here we build an equivalence instance for functions which relates respectful ones only. *) + +Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := + { morph : A -> B | respectful R R' morph morph }. + +Ltac obligations_tactic ::= program_simpl. + +Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] => + respecting_equiv : Equivalence respecting + (fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)). + + Next Obligation. + Proof. + constructor ; intros. + destruct x ; simpl. + apply r ; auto. + Qed. + + Next Obligation. + Proof. + constructor ; intros. + sym ; apply H. + sym ; auto. + Qed. + + Next Obligation. + Proof. + constructor ; intros. + trans ((`y) y0). + apply H ; auto. + apply H0. refl. + Qed. + +(** Can't use the definition [notT] as it gives a universe inconsistency. *) + +Ltac obligations_tactic ::= program_simpl ; simpl_relation. + +Program Instance notT_arrow_morphism : + Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False). + +Program Instance not_iso_morphism : + Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False). + +Program Instance not_impl_morphism : + Morphism (Prop -> Prop) (impl --> impl) not. + +Program Instance not_iff_morphism : + Morphism (Prop -> Prop) (iff ++> iff) not. + +(** We make the type implicit, it can be infered from the relations. *) + +Implicit Arguments Morphism [A]. + +(** Leibniz *) + +Program Definition eq_morphism A : Morphism (eq ++> eq ++> iff) (eq (A:=A)). +Proof. intros ; constructor ; intros. + obligations_tactic. + subst. + intuition. +Qed. + +(* Program Definition arrow_morphism `A B` (m : A -> B) : Morphism (eq ++> eq) m. *) + +(** Any binary morphism respecting some relations up to [iff] respects + them up to [impl] in each way. Very important instances as we need [impl] + morphisms at the top level when we rewrite. *) + +Program Instance `A` (R : relation A) `B` (R' : relation B) + [ ? Morphism (R ++> R' ++> iff) m ] => + + iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m. + + Next Obligation. + Proof. + destruct respect with x y x0 y0 ; auto. + Qed. + +Program Instance `A` (R : relation A) `B` (R' : relation B) + [ ? Morphism (R ++> R' ++> iff) m ] => + iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m. + + Next Obligation. + Proof. + destruct respect with x y x0 y0 ; auto. + Qed. + +(** The complement of a relation conserves its morphisms. *) + +Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => + complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R). + + Next Obligation. + Proof. + unfold complement ; intros. + pose (respect). + pose (r x y H). + pose (r0 x0 y0 H0). + intuition. + Qed. + +(** The inverse too. *) + +Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => + inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R). + + Next Obligation. + Proof. + unfold inverse ; unfold flip. + apply respect ; auto. + Qed. + +(* Definition respectful' A (R : relation A) B (R' : relation B) (f : A -> B) : relation A := *) +(* fun x y => R x y -> R' (f x) (f y). *) + +(* Definition morphism_respectful' A (R : relation A) B (R' : relation B) (f : A -> B) *) +(* [ ? Morphism (R ++> R') f ] (x y : A) : respectful' R R' f x y. *) +(* intros. *) +(* destruct H. *) +(* red in respect0. *) +(* red. *) +(* apply respect0. *) +(* Qed. *) + +(* Existing Instance morphism_respectful'. *) + +(* Goal forall A [ Equivalence A (eqA : relation A) ] (R : relation A) [ ? Morphism (eqA ++> iff) m ] (x y : A) *) +(* [ ? Morphism (eqA ++> eqA) m' ] (m' : A -> A), eqA x y -> True. *) +(* intros. *) +(* cut (relation A) ; intros R'. *) +(* cut ((eqA ++> R') m' m') ; intros. *) +(* assert({ R' : relation A & Reflexive R' }). *) +(* econstructor. *) +(* typeclass_instantiation. *) + + +(* assert (exists R' : relation A, Morphism ((fun x y => eqA x y -> R' (m' x) (m' y)) ++> iff) m). *) +(* eapply ex_intro. *) +(* unfold respectful. *) +(* typeclass_instantiation. *) + + +(* assert (exists R', Morphism (R' ++> iff) m /\ Morphism (eqA ++> R') m'). *) +(* typeclass_instantiation. *) +(* Set Printing All. *) +(* Show Proof. *) + + +(* apply respect. *) + +(** Partial applications are ok when a proof of refl is available. *) + +(** A proof of [R x x] is available. *) + +(* Program Instance (A : Type) (R : relation A) B (R' : relation B) *) +(* [ ? Morphism (R ++> R') m ] [ ? Morphism R x ] => *) +(* morphism_partial_app_morphism : ? Morphism R' (m x). *) + +(* Next Obligation. *) +(* Proof with auto. *) +(* apply (respect (m:=m))... *) +(* apply respect. *) +(* Qed. *) + + +(** Morpshism declarations for partial applications. *) + +Program Instance [ Transitive A (R : relation A) ] (x : A) => + trans_contra_inv_impl_morphism : ? Morphism (R --> inverse impl) (R x). + + Next Obligation. + Proof with auto. + trans y... + Qed. + +Program Instance [ Transitive A (R : relation A) ] (x : A) => + trans_co_impl_morphism : ? Morphism (R ++> impl) (R x). + + Next Obligation. + Proof with auto. + trans x0... + Qed. + +Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) => + trans_sym_co_inv_impl_morphism : ? Morphism (R ++> inverse impl) (R x). + + Next Obligation. + Proof with auto. + trans y... + sym... + Qed. + +Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) => + trans_sym_contra_impl_morphism : ? Morphism (R --> impl) (R x). + + Next Obligation. + Proof with auto. + trans x0... + sym... + Qed. + +Program Instance [ Equivalence A (R : relation A) ] (x : A) => + equivalence_partial_app_morphism : ? Morphism (R ++> iff) (R x). + + Next Obligation. + Proof with auto. + split. intros ; trans x0... + intros. + trans y... + sym... + Qed. + +(** With symmetric relations, variance is no issue ! *) + +Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B) + [ Morphism _ (R ++> R') m ] => + sym_contra_morphism : ? Morphism (R --> R') m. + + Next Obligation. + Proof with auto. + repeat (red ; intros). apply respect. + sym... + Qed. + +(** [R] is reflexive, hence we can build the needed proof. *) + +Program Instance [ Reflexive A (R : relation A) ] B (R' : relation B) + [ ? Morphism (R ++> R') m ] (x : A) => + reflexive_partial_app_morphism : ? Morphism R' (m x). + + Next Obligation. + Proof with auto. + intros. + apply (respect (m:=m))... + refl. + Qed. + +(** Every symmetric and transitive relation gives rise to an equivariant morphism. *) + +Program Instance [ Transitive A (R : relation A), Symmetric A R ] => + trans_sym_morphism : ? Morphism (R ++> R ++> iff) R. + + Next Obligation. + Proof with auto. + split ; intros. + trans x0... trans x... sym... + + trans y... trans y0... sym... + Qed. + +Program Instance [ Equivalence A (R : relation A) ] => + equiv_morphism : ? Morphism (R ++> R ++> iff) R. + + Next Obligation. + Proof with auto. + split ; intros. + trans x0... trans x... sym... + + trans y... trans y0... sym... + Qed. + +(** In case the rewrite happens at top level. *) + +Program Instance iff_inverse_impl_id : + ? Morphism (iff ++> inverse impl) id. + +Program Instance inverse_iff_inverse_impl_id : + ? Morphism (iff --> inverse impl) id. + +Program Instance iff_impl_id : + ? Morphism (iff ++> impl) id. + +Program Instance inverse_iff_impl_id : + ? Morphism (iff --> impl) id. + +(** Standard instances for [iff] and [impl]. *) + +(** Logical conjunction. *) + +(* Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and. *) + +(* Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and. *) + +Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and. + +(** Logical disjunction. *) + +(* Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or. *) + +(* Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or. *) + +Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or. diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v index 6ecd4ac3c7..694cab59bc 100644 --- a/theories/Classes/Relations.v +++ b/theories/Classes/Relations.v @@ -7,11 +7,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based setoids, tactics and standard instances. - TODO: explain clrewrite, clsubstitute and so on. +(* Typeclass-based relations, tactics and standard instances. + This is the basic theory needed to formalize morphisms and setoids. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud + Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) @@ -25,14 +25,14 @@ Unset Strict Implicit. Definition relationT A := A -> A -> Type. Definition relation A := A -> A -> Prop. -Definition inverse A (R : relation A) : relation A := flip R. +Definition inverse A (R : relation A) : relation A := fun x y => R y x. Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R. Proof. intros ; unfold inverse. apply (flip_flip R). Qed. -Definition complementT A (R : relationT A) := fun x y => ! R x y. +Definition complementT A (R : relationT A) := fun x y => notT (R x y). -Definition complement A (R : relation A) := fun x y => ~ R x y. +Definition complement A (R : relation A) := fun x y => R x y -> False. (** These are convertible. *) @@ -112,7 +112,6 @@ Program Instance [ Reflexive A (R : relation A) ] => Next Obligation. Proof. - unfold complement in * ; intros. apply H. apply reflexive. Qed. @@ -122,7 +121,6 @@ Program Instance [ Irreflexive A (R : relation A) ] => Next Obligation. Proof. - unfold complement in * ; intros. red ; intros. apply (irreflexive H). Qed. @@ -131,12 +129,54 @@ Program Instance [ Symmetric A (R : relation A) ] => complement_symmetric : Symm Next Obligation. Proof. - unfold complement in *. red ; intros H'. apply (H (symmetric H')). Qed. -(** Tactics to solve goals. Each tactic comes in two flavors: +(** * Standard instances. *) + +Ltac simpl_relation := + try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; + repeat (red ; intros) ; try ( solve [ intuition ]). + +Ltac obligations_tactic ::= simpl_relation. + +(** The arrow is a reflexive and transitive relation on types. *) + +Program Instance arrow_refl : ? Reflexive arrow := + reflexive X := id. + +Program Instance arrow_trans : ? Transitive arrow := + transitive X Y Z f g := g o f. + +(** Isomorphism. *) + +Definition iso (A B : Type) := + A -> B * B -> A. + +Program Instance iso_refl : ? Reflexive iso. +Program Instance iso_sym : ? Symmetric iso. +Program Instance iso_trans : ? Transitive iso. + +(** Logical implication. *) + +Program Instance impl_refl : ? Reflexive impl. +Program Instance impl_trans : ? Transitive impl. + +(** Logical equivalence. *) + +Program Instance iff_refl : ? Reflexive iff. +Program Instance iff_sym : ? Symmetric iff. +Program Instance iff_trans : ? Transitive iff. + +(** Leibniz equality. *) + +Program Instance eq_refl : ? Reflexive (@eq A). +Program Instance eq_sym : ? Symmetric (@eq A). +Program Instance eq_trans : ? Transitive (@eq A). + +(** ** General tactics to solve goals on relations. + Each tactic comes in two flavors: - a tactic to immediately solve a goal without user intervention - a tactic taking input from the user to make progress on a goal *) @@ -216,6 +256,9 @@ Ltac relation_trans := | [ H : ?R ?A ?B ?C ?D ?X ?Y, H' : ?R ?A ?B ?C ?D ?Y ?Z |- ?R ?A ?B ?C ?D ?X ?Z ] => apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z) H H') + + | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => + apply (transitive (R:=R A B C D E) (x:=X) (y:=Y) (z:=Z) H H') end. Ltac relation_transitive Y := @@ -242,254 +285,13 @@ Ltac trans Y := relation_transitive Y. Ltac relation_tac := relation_refl || relation_sym || relation_trans. -(** * Morphisms. - - We now turn to the definition of [Morphism] and declare standard instances. - These will be used by the [clrewrite] tactic later. *) - -(** Respectful morphisms. *) - -Definition respectful_depT (A : Type) (R : relationT A) - (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) := - fun f g => forall x y : A, R x y -> R' x y (f x) (g y). - -Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) := - Eval compute in (respectful_depT eqa (fun _ _ => eqb)). - -Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) := - fun f g => forall x y : A, R x y -> R' (f x) (g y). - -(** Notations reminiscent of the old syntax for declaring morphisms. - We use three + or - for type morphisms, and two for [Prop] ones. - *) - -Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20). -Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20). - -Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20). -Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20). - -(** A morphism on a relation [R] is an object respecting the relation (in its kernel). - The relation [R] will be instantiated by [respectful] and [A] by an arrow type - for usual morphisms. *) - -Class Morphism A (R : relationT A) (m : A) := - respect : R m m. - -Ltac simpl_morphism := - try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; - try (red ; intros) ; try ( solve [ intuition ]). - -Ltac obligations_tactic ::= simpl_morphism. - -(** The arrow is a reflexive and transitive relation on types. *) - -Program Instance arrow_refl : ? Reflexive arrow := - reflexive X := id. - -Program Instance arrow_trans : ? Transitive arrow := - transitive X Y Z f g := g o f. - -(** Can't use the definition [notT] as it gives a to universe inconsistency. *) - -Program Instance notT_arrow_morphism : - Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False). - -(** Isomorphism. *) - -Definition iso (A B : Type) := - A -> B * B -> A. - -Program Instance iso_refl : ? Reflexive iso. -Program Instance iso_sym : ? Symmetric iso. -Program Instance iso_trans : ? Transitive iso. - -Program Instance not_iso_morphism : - Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False). - -(** Logical implication. *) - -Program Instance impl_refl : ? Reflexive impl. -Program Instance impl_trans : ? Transitive impl. - -Program Instance not_impl_morphism : - Morphism (Prop -> Prop) (impl --> impl) not. - -(** Logical equivalence. *) - -Program Instance iff_refl : ? Reflexive iff. -Program Instance iff_sym : ? Symmetric iff. -Program Instance iff_trans : ? Transitive iff. - -Program Instance not_iff_morphism : - Morphism (Prop -> Prop) (iff ++> iff) not. - -(** We make the type implicit, it can be infered from the relations. *) - -Implicit Arguments Morphism [A]. - -(** If you have a morphism from [RA] to [RB] you have a contravariant morphism - from [RA] to [inverse RB]. *) - -Program Instance `A` (RA : relation A) `B` (RB : relation B) [ ? Morphism (RA ++> RB) m ] => - morph_impl_co_contra_inverse : - ? Morphism (RA --> inverse RB) m. - - Next Obligation. - Proof. - apply respect. - apply H. - Qed. - -(** Every transitive relation gives rise to a binary morphism on [impl], - contravariant in the first argument, covariant in the second. *) - -Program Instance [ Transitive A (R : relation A) ] => - trans_contra_co_morphism : ? Morphism (R --> R ++> impl) R. - - Next Obligation. - Proof with auto. - trans x... - trans x0... - Qed. - -(** Dually... *) - -Program Instance [ Transitive A (R : relation A) ] => - trans_co_contra_inv_impl_morphism : ? Morphism (R ++> R --> inverse impl) R. - - Obligations Tactic := idtac. - - Next Obligation. - Proof with auto. - intros. - destruct (trans_contra_co_morphism (R:=inverse R)). - revert respect0. - unfold respectful, inverse, flip in * ; intros. - apply respect0 ; auto. - Qed. - -Obligations Tactic := simpl_morphism. - -(** With symmetric relations, variance is no issue ! *) - -Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B) - [ Morphism _ (R ++> R') m ] => - sym_contra_morphism : ? Morphism (R --> R') m. - - Next Obligation. - Proof with auto. - apply respect. - sym... - Qed. - -(** Every symmetric and transitive relation gives rise to an equivariant morphism. *) - -Program Instance [ Transitive A (R : relation A), Symmetric A R ] => - trans_sym_morphism : ? Morphism (R ++> R ++> iff) R. - - Next Obligation. - Proof with auto. - split ; intros. - trans x0... trans x... sym... - - trans y... trans y0... sym... - Qed. - -(** The complement of a relation conserves its morphisms. *) - -Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => - complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R). - - Next Obligation. - Proof. - red ; unfold complement ; intros. - pose (respect). - pose (r x y H). - pose (r0 x0 y0 H0). - intuition. - Qed. - -(** The inverse too. *) - -Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => - inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R). - - Next Obligation. - Proof. - unfold inverse ; unfold flip. - apply respect ; auto. - Qed. - -Program Instance [ Transitive A (R : relation A), Symmetric A R ] => - trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R. - - Next Obligation. - Proof with auto. - trans y... - sym... - trans y0... - sym... - Qed. - -(** Any binary morphism respecting some relations up to [iff] respects - them up to [impl] in each way. Very important instances as we need [impl] - morphisms at the top level when we rewrite. *) - -Program Instance `A` (R : relation A) `B` (R' : relation B) - [ ? Morphism (R ++> R' ++> iff) m ] => - iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m. - - Next Obligation. - Proof. - destruct respect with x y x0 y0 ; auto. - Qed. - -Program Instance `A` (R : relation A) `B` (R' : relation B) - [ ? Morphism (R ++> R' ++> iff) m ] => - iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m. - - Next Obligation. - Proof. - destruct respect with x y x0 y0 ; auto. - Qed. - -(** Standard instances for [iff] and [impl]. *) - -(** Logical conjunction. *) - -Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and. - -Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and. - -Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and. - -(** Logical disjunction. *) - -Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or. - -Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or. - -Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or. - -(** Leibniz equality. *) - -Program Instance eq_refl : ? Reflexive (@eq A). -Program Instance eq_sym : ? Symmetric (@eq A). -Program Instance eq_trans : ? Transitive (@eq A). - -Program Definition eq_morphism A : Morphism (eq ++> eq ++> iff) (eq (A:=A)) := - trans_sym_morphism. - -Program Instance `A B` (m : A -> B) => arrow_morphism : ? Morphism (eq ++> eq) m. - (** The [PER] typeclass. *) Class PER (carrier : Type) (pequiv : relationT carrier) := per_sym :> Symmetric pequiv ; per_trans :> Transitive pequiv. -(** We can build a PER on the coq function space if we have PERs on the domain and +(** We can build a PER on the Coq function space if we have PERs on the domain and codomain. *) Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => @@ -520,38 +322,10 @@ Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] => Solve Obligations using unfold flip ; program_simpl ; eapply antisymmetric ; eauto. -(** Here we build an equivalence instance for functions which relates respectful ones only. *) - -Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := - { morph : A -> B | respectful R R' morph morph }. - -Ltac obligations_tactic ::= program_simpl. - -Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] => - respecting_equiv : Equivalence respecting - (fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)). +Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq (R : relation A) ] => + inverse_antisymmetric : ? Antisymmetric eq (inverse R). - Next Obligation. - Proof. - constructor ; intros. - destruct x ; simpl. - apply r ; auto. - Qed. - - Next Obligation. - Proof. - constructor ; intros. - sym ; apply H. - sym ; auto. - Qed. - - Next Obligation. - Proof. - constructor ; intros. - trans ((`y) y0). - apply H ; auto. - apply H0. refl. - Qed. + Solve Obligations using unfold inverse, flip ; program_simpl ; eapply antisymmetric ; eauto. (** Leibinz equality [eq] is an equivalence relation. *) diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 78e53aa012..5e18ef2aff 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -23,6 +23,7 @@ Set Implicit Arguments. Unset Strict Implicit. Require Export Coq.Classes.Relations. +Require Export Coq.Classes.Morphisms. (** A setoid wraps an equivalence. *) @@ -30,6 +31,10 @@ Class Setoid A := equiv : relation A ; setoid_equiv :> Equivalence A equiv. +Program Instance [ eqa : Equivalence A (eqA : relation A) ] => + equivalence_setoid : Setoid A := + equiv := eqA ; setoid_equiv := eqa. + (** Shortcuts to make proof search easier. *) Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv. @@ -43,8 +48,8 @@ Proof. eauto with typeclass_instances. Qed. (** Standard setoids. *) -Program Instance eq_setoid : Setoid A := - equiv := eq ; setoid_equiv := eq_equivalence. +(* Program Instance eq_setoid : Setoid A := *) +(* equiv := eq ; setoid_equiv := eq_equivalence. *) Program Instance iff_setoid : Setoid Prop := equiv := iff ; setoid_equiv := iff_equivalence. @@ -56,14 +61,7 @@ Program Instance iff_setoid : Setoid Prop := Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope. -Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope. - -Lemma nequiv_sym : forall [ s : Setoid A ] (x y : A), x =/= y -> y =/= x. -Proof with auto. - intros ; red ; intros. - apply H. - sym... -Qed. +Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : type_scope. (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *) @@ -82,15 +80,15 @@ Ltac clsubst_nofail := Tactic Notation "clsubst" "*" := clsubst_nofail. -Lemma nequiv_equiv : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z. -Proof. - intros; intro. +Lemma nequiv_equiv_trans : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z. +Proof with auto. + intros; intro. assert(z == y) by relation_sym. assert(x == y) by relation_trans. contradiction. Qed. -Lemma equiv_nequiv : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z. +Lemma equiv_nequiv_trans : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z. Proof. intros; intro. assert(y == x) by relation_sym. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 39809865cd..fb7f8827bf 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -39,51 +39,3 @@ Ltac setoideq_ext := [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y) end. -Ltac setoid_tactic := - match goal with - | [ H : ?eq ?x ?y |- ?eq ?y ?x ] => sym ; apply H - | [ |- ?eq ?x ?x ] => refl - | [ H : ?eq ?x ?y, H' : ?eq ?y ?z |- ?eq' ?x ?z ] => trans y ; [ apply H | apply H' ] - | [ H : ?eq ?x ?y, H' : ?eq ?z ?y |- ?eq' ?x ?z ] => trans y ; [ apply H | sym ; apply H' ] - | [ H : ?eq ?y ?x, H' : ?eq ?z ?y |- ?eq' ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ] - | [ H : ?eq ?y ?x, H' : ?eq ?y ?z |- ?eq' ?x ?z ] => trans y ; [ sym ; apply H | apply H' ] - - | [ H : ?eq ?x ?y |- @equiv _ _ _ ?y ?x ] => sym ; apply H - | [ |- @equiv _ _ _ ?x ?x ] => refl - | [ H : ?eq ?x ?y, H' : ?eq ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | apply H' ] - | [ H : ?eq ?x ?y, H' : ?eq ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | sym ; apply H' ] - | [ H : ?eq ?y ?x, H' : ?eq ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ] - | [ H : ?eq ?y ?x, H' : ?eq ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | apply H' ] - - | [ H : @equiv ?A ?R ?s ?x ?y |- @equiv _ _ _ ?y ?x ] => sym ; apply H - | [ |- @equiv _ _ _ ?x ?x ] => refl - | [ H : @equiv ?A ?R ?s ?x ?y, H' : @equiv ?A ?R ?s ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | apply H' ] - | [ H : @equiv ?A ?R ?s ?x ?y, H' : @equiv ?A ?R ?s ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | sym ; apply H' ] - | [ H : @equiv ?A ?R ?s ?y ?x, H' : @equiv ?A ?R ?s ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ] - | [ H : @equiv ?A ?R ?s ?y ?x, H' : @equiv ?A ?R ?s ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | apply H' ] - - | [ H : not (@equiv ?A ?R ?s ?X ?X) |- _ ] => elim H ; refl - | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : @equiv ?A ?R ?s ?Y ?X |- _ ] => elim H ; sym ; apply H - | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : ?R ?Y ?X |- _ ] => elim H ; sym ; apply H - | [ H : not (@equiv ?A ?R ?s ?X ?Y) |- False ] => elim H ; clear H ; setoid_tactic - end. -(** Need to fix fresh to not fail if some arguments are not identifiers. *) -(* Ltac setoid_sat ::= *) -(* match goal with *) -(* | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add_hypothesis name (equiv_sym H) *) -(* | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *) -(* | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add_hypothesis name (equiv_trans H H') *) -(* | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *) -(* | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *) -(* end. *) - -Ltac setoid_sat := - match goal with - | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_sym H) - | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H) - | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_trans H H') - | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H') - | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H') - end. -Ltac setoid_saturate := repeat setoid_sat. - diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index e5bc98dee3..014ff3a016 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -139,5 +139,3 @@ Tactic Notation "exist" constr(x) := exists x. Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y. Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w. - -Notation " ! A " := (notT A) (at level 200, A at level 100) : type_scope. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index d84fb3e561..92a5dfc8b7 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -492,3 +492,60 @@ let _ = (fun env evd ev evi -> Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *) solve_by_tac env evd ev evi (Lazy.force tactic)) + +let prod = lazy (Coqlib.build_prod ()) + +let build_conjunction evm = + List.fold_left + (fun (acc, evs) (ev, evi) -> + if class_of_constr evi.evar_concl <> None then + mkApp ((Lazy.force prod).Coqlib.typ, [|evi.evar_concl; acc |]), evs + else acc, Evd.add evs ev evi) + (Coqlib.build_coq_True (), Evd.empty) evm + +let destruct_conjunction evm_list evm evm' term = + let _, evm = + List.fold_right + (fun (ev, evi) (term, evs) -> + if class_of_constr evi.evar_concl <> None then + match kind_of_term term with + | App (x, [| _ ; _ ; proof ; term |]) -> + let evs' = Evd.define evs ev proof in + (term, evs') + | _ -> assert(false) + else + match (Evd.find evm' ev).evar_body with + Evar_empty -> raise Not_found + | Evar_defined c -> + let evs' = Evd.define evs ev c in + (term, evs')) + evm_list (term, evm) + in evm + +(* let solve_by_tac env evd evar evi t = *) +(* let goal = {it = evi; sigma = (Evd.evars_of evd) } in *) +(* let (res, valid) = t goal in *) +(* if res.it = [] then *) +(* let prooftree = valid [] in *) +(* let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *) +(* if obls = [] then *) +(* let evd' = evars_reset_evd res.sigma evd in *) +(* let evd' = evar_define evar proofterm evd' in *) +(* evd', true *) +(* else evd, false *) +(* else evd, false *) + +let resolve_all_typeclasses env evd = + let evm = Evd.evars_of evd in + let evm_list = Evd.to_list evm in + let goal, typesevm = build_conjunction evm_list in + let evars = ref (Evd.create_evar_defs typesevm) in + let term = resolve_one_typeclass_evd env evars goal in + let evm' = destruct_conjunction evm_list evm (Evd.evars_of !evars) term in + Evd.create_evar_defs evm' + +let _ = + Typeclasses.solve_instanciations_problem := + (fun env evd -> + Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *) + resolve_all_typeclasses env evd) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 93fc1b552c..cfe881cb31 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -69,3 +69,5 @@ val push_named_context : named_context -> env -> env val name_typeclass_binders : Idset.t -> Topconstr.local_binder list -> Topconstr.local_binder list * Idset.t + +val resolve_all_typeclasses : env -> evar_defs -> evar_defs |