diff options
| -rw-r--r-- | pretyping/typeclasses_errors.ml | 2 | ||||
| -rw-r--r-- | pretyping/typeclasses_errors.mli | 4 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 111 | ||||
| -rw-r--r-- | test-suite/success/dependentind.v | 4 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 95 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 66 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 4 |
8 files changed, 181 insertions, 107 deletions
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 4db826108..ae806cbf5 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -28,7 +28,7 @@ type typeclass_error = | NotAClass of constr | UnboundMethod of global_reference * identifier located (* Class name, method *) | NoInstance of identifier located * constr list - | UnsatisfiableConstraints of evar_map + | UnsatisfiableConstraints of evar_defs | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *) exception TypeClassError of env * typeclass_error diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index a697087d2..f97aed96a 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -28,7 +28,7 @@ type typeclass_error = | NotAClass of constr | UnboundMethod of global_reference * identifier located (* Class name, method *) | NoInstance of identifier located * constr list - | UnsatisfiableConstraints of evar_map + | UnsatisfiableConstraints of evar_defs | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *) exception TypeClassError of env * typeclass_error @@ -39,6 +39,6 @@ val unbound_method : env -> global_reference -> identifier located -> 'a val no_instance : env -> identifier located -> constr list -> 'a -val unsatisfiable_constraints : env -> evar_map -> 'a +val unsatisfiable_constraints : env -> evar_defs -> 'a val mismatched_ctx_inst : env -> contexts -> constr_expr list -> named_context -> 'a diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 8d9ee36e9..2061d00a5 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -130,7 +130,6 @@ type search_state = { tacres : goal list sigma * validation; pri : int; last_tactic : std_ppcmds; - custom_tactic : tactic; dblist : Auto.Hint_db.t list; localdb : Auto.Hint_db.t list } @@ -253,22 +252,19 @@ end module Search = Explore.Make(SearchProblem) -let make_initial_state n gls ~(tac:tactic) dblist localdbs = +let make_initial_state n gls dblist localdbs = { depth = n; tacres = gls; pri = 0; last_tactic = (mt ()); - custom_tactic = tac; dblist = dblist; localdb = localdbs } let e_depth_search debug s = - try - let tac = if debug then - (SearchProblem.debug := true; Search.debug_depth_first) else Search.depth_first in - let s = tac s in + let tac = if debug then + (SearchProblem.debug := true; Search.debug_depth_first) else Search.depth_first in + let s = tac s in s.tacres - with Not_found -> error "EAuto: depth first search failed" let e_breadth_search debug s = try @@ -277,27 +273,23 @@ let e_breadth_search debug s = in let s = tac s in s.tacres with Not_found -> error "EAuto: breadth first search failed" -let e_search_auto ~(tac:tactic) debug (in_depth,p) lems db_list gls = +let e_search_auto debug (in_depth,p) lems db_list gls = let sigma = Evd.sig_sig (fst gls) and gls' = Evd.sig_it (fst gls) in let local_dbs = List.map (fun gl -> make_local_hint_db lems ({it = gl; sigma = sigma})) gls' in - let state = make_initial_state p gls ~tac db_list local_dbs in + let state = make_initial_state p gls db_list local_dbs in if in_depth then e_depth_search debug state else e_breadth_search debug state -let full_eauto ~(tac:tactic) debug n lems gls = +let full_eauto debug n lems gls = let dbnames = current_db_names () in let dbnames = list_subtract dbnames ["v62"] in let db_list = List.map searchtable_map dbnames in - e_search_auto ~tac debug n lems db_list gls + e_search_auto debug n lems db_list gls exception Found of evar_map -let default_evars_tactic = - fun x -> raise (UserError ("default_evars_tactic", mt())) -(* tclFAIL 0 (Pp.mt ()) *) - let valid goals p res_sigma l = let evm = List.fold_left2 @@ -309,7 +301,7 @@ let valid goals p res_sigma l = !res_sigma goals l in raise (Found evm) -let resolve_all_evars_once ?(tac=default_evars_tactic) debug (mode, depth) env p evd = +let resolve_all_evars_once debug (mode, depth) env p evd = let evm = Evd.evars_of evd in let goals, evm' = Evd.fold @@ -323,7 +315,7 @@ let resolve_all_evars_once ?(tac=default_evars_tactic) debug (mode, depth) env p let goals = List.rev goals in let gls = { it = List.map snd goals; sigma = evm' } in let res_sigma = ref evm' in - let gls', valid' = full_eauto ~tac debug (mode, depth) [] (gls, valid goals p res_sigma) in + let gls', valid' = full_eauto debug (mode, depth) [] (gls, valid goals p res_sigma) in res_sigma := Evarutil.nf_evars (sig_sig gls'); try ignore(valid' []); assert(false) with Found evm' -> Evarutil.nf_evar_defs (Evd.evars_reset_evd evm' evd) @@ -333,7 +325,7 @@ exception FoundTerm of constr let resolve_one_typeclass env gl = let gls = { it = [ Evd.make_evar (Environ.named_context_val env) gl ] ; sigma = Evd.empty } in let valid x = raise (FoundTerm (fst (Refiner.extract_open_proof Evd.empty (List.hd x)))) in - let gls', valid' = full_eauto ~tac:tclIDTAC false (true, 15) [] (gls, valid) in + let gls', valid' = full_eauto false (true, 15) [] (gls, valid) in try ignore(valid' []); assert false with FoundTerm t -> let term = Evarutil.nf_evar (sig_sig gls') t in if occur_existential term then raise Not_found else term @@ -343,19 +335,21 @@ let has_undefined p evd = (evi.evar_body = Evar_empty && p ev evi)) (Evd.evars_of evd) false -let rec resolve_all_evars ~(tac:tactic) debug m env p oevd = +let resolve_all_evars debug m env p oevd = (* let evd = resolve_all_evars_once ~tac debug m env p evd in *) (* if has_undefined p evd then raise Not_found *) (* else evd *) - let rec aux n evd = - if has_undefined p evd then - if n > 0 then - let evd' = resolve_all_evars_once ~tac debug m env p evd in - aux (pred n) evd' - else raise Not_found - else evd - in aux 3 oevd - + try + let rec aux n evd = + if has_undefined p evd then + if n > 0 then + let evd' = resolve_all_evars_once debug m env p evd in + aux (pred n) evd' + else None + else Some evd + in aux 3 oevd + with Not_found -> None + (** Handling of the state of unfolded constants. *) open Libobject @@ -805,29 +799,15 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars = | _ -> None, occ in aux env concl 1 cstr -(* 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 resolve_argument_typeclasses ?(tac=tclIDTAC) d p env evd onlyargs all = +let resolve_typeclass_evars d p env evd onlyargs = let pred = if onlyargs then (fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) && class_of_constr evi.Evd.evar_concl <> None) else (fun ev evi -> class_of_constr evi.Evd.evar_concl <> None) - in - try - resolve_all_evars ~tac d p env pred evd - with - | Not_found -> - if all then - (* Unable to satisfy the constraints. *) - Typeclasses_errors.unsatisfiable_constraints env (Evd.evars_of evd) - else evd - | e -> - if all then raise e else evd - + in resolve_all_evars d p env pred evd + let cl_rewrite_tactic = lazy (Tacinterp.interp <:tactic<setoid_rewrite_tac>>) let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause gl = @@ -882,8 +862,11 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd) else tclIDTAC in tclTHENLIST [evartac; rewtac] gl - with UserError (s, pp) -> - tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints:" ++ fnl () ++ pp) gl) + with + | TypeClassError (_env, UnsatisfiableConstraints _evm) -> + tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints.") gl + | Not_found -> + tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints.") gl) | None -> let {l2r=l2r; c1=x; c2=y} = !hypinfo in raise (Pretype_errors.PretypeError (pf_env gl, Pretype_errors.NoOccurrenceFound (if l2r then x else y))) @@ -946,17 +929,27 @@ ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ] END -VERNAC COMMAND EXTEND Typeclasses_Settings -| [ "Typeclasses" "eauto" ":=" debug(d) search_mode(s) depth(depth) ] -> [ - let mode = match s with Some t -> t | None -> true in - let depth = match depth with Some i -> i | None -> 15 in - Typeclasses.solve_instanciations_problem := - resolve_argument_typeclasses d (mode, depth) ] -END +let solve_inst debug mode depth env evd onlyargs all = + match resolve_typeclass_evars debug (mode, depth) env evd onlyargs with + | None -> + if all then + (* Unable to satisfy the constraints. *) + Typeclasses_errors.unsatisfiable_constraints env evd + else (* Best effort: do nothing *) evd + | Some evd -> evd let _ = Typeclasses.solve_instanciations_problem := - resolve_argument_typeclasses false (true, 15) + solve_inst false true 15 + +VERNAC COMMAND EXTEND Typeclasses_Settings + | [ "Typeclasses" "eauto" ":=" debug(d) search_mode(s) depth(depth) ] -> [ + let mode = match s with Some t -> t | None -> true in + let depth = match depth with Some i -> i | None -> 15 in + Typeclasses.solve_instanciations_problem := + solve_inst d mode depth + ] +END TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" debug(d) search_mode(s) depth(depth) ] -> [ fun gl -> @@ -967,8 +960,10 @@ TACTIC EXTEND typeclasses_eauto let evd = Evd.create_evar_defs sigma in let mode = match s with Some t -> t | None -> true in let depth = match depth with Some i -> i | None -> 15 in - let evd' = resolve_argument_typeclasses d (mode, depth) env evd false false in - Refiner.tclEVARS (Evd.evars_of evd') gl ] + match resolve_typeclass_evars d (mode, depth) env evd false with + | Some evd' -> Refiner.tclEVARS (Evd.evars_of evd') gl + | None -> tclIDTAC gl + ] END let _ = diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 8b8ce0098..be7b77ef0 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -35,7 +35,7 @@ Inductive ctx : Type := | empty : ctx | snoc : ctx -> type -> ctx. -Notation " Γ , τ " := (snoc Γ τ) (at level 20, t at next level). +Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity). Fixpoint conc (Γ Δ : ctx) : ctx := match Δ with @@ -43,7 +43,7 @@ Fixpoint conc (Γ Δ : ctx) : ctx := | snoc Δ' x => snoc (conc Γ Δ') x end. -Notation " Γ ; Δ " := (conc Γ Δ) (at level 20). +Notation " Γ ; Δ " := (conc Γ Δ) (at level 25, left associativity). Inductive term : ctx -> type -> Type := | ax : forall Γ τ, term (Γ, τ) τ diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index b4b217e38..4765bf0ee 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -30,12 +30,20 @@ Unset Strict Implicit. (** Respectful morphisms. *) -Definition respectful_dep (A : Type) (R : relation A) - (B : A -> Type) (R' : forall x y, B x -> B y -> Prop) : relation (forall x : A, B x) := - fun f g => forall x y : A, R x y -> R' x y (f x) (g y). +(** The fully dependent version, not used yet. *) -Definition respectful A B (R : relation A) (R' : relation B) : relation (A -> B) := - fun f g => forall x y : A, R x y -> R' (f x) (g y). +Definition respectful_hetero + (A B : Type) + (C : A -> Type) (D : B -> Type) + (R : A -> B -> Prop) + (R' : forall (x : A) (y : B), C x -> D y -> Prop) : + (forall x : A, C x) -> (forall x : B, D x) -> Prop := + fun f g => forall x y, R x y -> R' x y (f x) (g y). + +(** The non-dependent version is an instance where we forget dependencies. *) + +Definition respectful (A B : Type) (R : relation A) (R' : relation B) : relation (A -> B) := + Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R'). (** Notations reminiscent of the old syntax for declaring morphisms. *) @@ -114,49 +122,32 @@ Implicit Arguments Morphism [A]. Typeclasses unfold relation. -(** Leibniz *) - -(* Instance 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. *) +(** Subrelations induce a morphism on the identity, not used for morphism search yet. *) -(** Any 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. *) +Lemma subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id. +Proof. firstorder. Qed. -Class SubRelation A (R S : relation A) : Prop := - subrelation :> Morphism (S ==> R) id. +(** The subrelation property goes through products as usual. *) -Instance iff_impl_subrelation : SubRelation Prop impl iff. -Proof. reduce. tauto. Qed. +Instance [ sub : subrelation A R₁ R₂ ] => + morphisms_subrelation : ! subrelation (B -> A) (R ==> R₁) (R ==> R₂). +Proof. firstorder. Qed. -Instance iff_inverse_impl_subrelation : SubRelation Prop (inverse impl) iff. -Proof. - reduce. tauto. -Qed. - -Instance [ sub : SubRelation A R₁ R₂ ] => - morphisms_subrelation : SubRelation (B -> A) (R ==> R₁) (R ==> R₂). -Proof. - reduce. apply* sub. apply H. assumption. -Qed. +Instance [ sub : subrelation A R₂ R₁ ] => + morphisms_subrelation_left : ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3. +Proof. firstorder. Qed. -Instance [ sub : SubRelation A R₂ R₁ ] => - morphisms_subrelation_left : SubRelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3. -Proof. - reduce. apply* H. apply* sub. assumption. -Qed. +(** [Morphism] is itself a covariant morphism for [subrelation]. *) -Lemma subrelation_morphism [ SubRelation A R₁ R₂, ! Morphism R₂ m ] : Morphism R₁ m. +Lemma subrelation_morphism [ subrelation A R₁ R₂, ! Morphism R₁ m ] : Morphism R₂ m. Proof. intros. apply* H. apply H0. Qed. +Instance morphism_subrelation_morphism : + Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A). +Proof. reduce. subst. firstorder. Qed. + Inductive done : nat -> Type := did : forall n : nat, done n. @@ -428,6 +419,10 @@ Instance (A : Type) [ Reflexive B R' ] => Reflexive (@Logic.eq A ==> R'). Proof. simpl_relation. Qed. +Instance [ Morphism (A -> B) (inverse R ==> R') m ] => + Morphism (R ==> inverse R') m | 10. +Proof. firstorder. Qed. + (** [respectful] is a morphism for relation equivalence. *) Instance respectful_morphism : @@ -450,7 +445,7 @@ Proof. Qed. Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B), - inverse (R ==> R') ==rel (inverse R ==> inverse R'). + inverse (R ==> R') <->rel (inverse R ==> inverse R'). Proof. intros. unfold flip, respectful. @@ -515,6 +510,26 @@ Ltac morphism_normalization := Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances. +(** Morphisms for relations *) + +Instance [ PartialOrder A eqA R ] => + partial_order_morphism : Morphism (eqA ==> eqA ==> iff) R. +Proof with auto. + intros. rewrite partial_order_equivalence. + simpl_relation. firstorder. + transitivity x... transitivity x0... + transitivity y... transitivity y0... +Qed. + +Instance Morphism (relation_equivalence (A:=A) ==> + relation_equivalence ==> relation_equivalence) relation_conjunction. + Proof. firstorder. Qed. + +Instance Morphism (relation_equivalence (A:=A) ==> + relation_equivalence ==> relation_equivalence) relation_disjunction. + Proof. firstorder. Qed. + + (** Morphisms for quantifiers *) Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A). @@ -576,5 +591,5 @@ Program Instance {A : Type} => all_inverse_impl_morphism : Qed. Lemma inverse_pointwise_relation A (R : relation A) : - pointwise_relation (inverse R) ==rel inverse (pointwise_relation (A:=A) R). + pointwise_relation (inverse R) <->rel inverse (pointwise_relation (A:=A) R). Proof. reflexivity. Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 009ee1e86..3d5c6a7ee 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -11,7 +11,7 @@ This is the basic theory needed to formalize morphisms and setoids. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Universitcopyright 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 $ *) @@ -212,10 +212,33 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid (fun f g => forall (x y : a), R x y -> R' (f x) (g y)). *) + +(** We define the various operations which define the algebra on relations. + They are essentially liftings of the logical operations. *) + Definition relation_equivalence {A : Type} : relation (relation A) := fun (R R' : relation A) => forall x y, R x y <-> R' x y. -Infix "==rel" := relation_equivalence (at level 70). +Infix "<->rel" := relation_equivalence (at level 70). + +Class subrelation {A:Type} (R R' : relation A) := + is_subrelation : forall x y, R x y -> R' x y. + +Implicit Arguments subrelation [[A]]. + +Infix "->rel" := subrelation (at level 70). + +Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := + fun x y => R x y /\ R' x y. + +Infix "//\\" := relation_conjunction (at level 55). + +Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := + fun x y => R x y \/ R' x y. + +Infix "\\//" := relation_disjunction (at level 55). + +(** Relation equivalence is an equivalence, and subrelation defines a partial order. *) Program Instance relation_equivalence_equivalence : Equivalence (relation A) relation_equivalence. @@ -225,3 +248,42 @@ Program Instance relation_equivalence_equivalence : unfold relation_equivalence in *. apply transitivity with (y x0 y0) ; [ apply H | apply H0 ]. Qed. + +Program Instance subrelation_preorder : + PreOrder (relation A) subrelation. + +(** *** Partial Order. + A partial order is a preorder which is additionally antisymmetric. + We give an equivalent definition, up-to an equivalence relation + on the carrier. *) + +Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder := + partial_order_equivalence : relation_equivalence eqA (R //\\ flip R). + + +(** The equivalence proof is sufficient for proving that [R] must be a morphism + for equivalence (see Morphisms). + It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) + +Instance [ PartialOrder A eqA R ] => partial_order_antisym : ! Antisymmetric A eqA R. +Proof with auto. + reduce_goal. pose partial_order_equivalence. red in r. + apply <- r. firstorder. +Qed. + +(** The partial order defined by subrelation and relation equivalence. *) + +Program Instance subrelation_partial_order : + ! PartialOrder (relation A) relation_equivalence subrelation. + + Next Obligation. + Proof. + unfold relation_equivalence in *. firstorder. + Qed. + +Instance iff_impl_subrelation : subrelation iff impl. +Proof. firstorder. Qed. + +Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). +Proof. firstorder. Qed. + diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index f31115d99..f2dcdd0e0 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -27,9 +27,11 @@ Ltac destruct_pairs := repeat (destruct_one_pair). Ltac destruct_one_ex := let tac H := let ph := fresh "H" in destruct H as [H ph] in + let tacT H := let ph := fresh "X" in destruct H as [H ph] in match goal with | [H : (ex _) |- _] => tac H | [H : (sig ?P) |- _ ] => tac H + | [H : (sigT ?P) |- _ ] => tacT H | [H : (ex2 _) |- _] => tac H end. diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 4adfaf6aa..b9f187784 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -488,9 +488,9 @@ let explain_no_instance env (_,id) l = str "applied to arguments" ++ spc () ++ prlist_with_sep pr_spc (pr_lconstr_env env) l -let explain_unsatisfiable_constraints env evm = +let explain_unsatisfiable_constraints env evd = str"Unable to satisfy the following typeclass constraints:" ++ fnl() ++ - Evd.pr_evar_map evm + Evd.pr_evar_map (Evd.evars_of (Evd.undefined_evars evd)) let explain_mismatched_contexts env c i j = str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ |