diff options
| -rw-r--r-- | doc/refman/Classes.tex | 264 | ||||
| -rw-r--r-- | tactics/auto.ml | 69 | ||||
| -rw-r--r-- | tactics/auto.mli | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 67 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 16 |
5 files changed, 376 insertions, 42 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 3a90a59f1..e3ecbb804 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -2,6 +2,7 @@ \def\eol{\setlength\parskip{0pt}\par} \def\indent#1{\noindent\kern#1} \def\cst#1{\textsf{#1}} +\def\tele#1{\overrightarrow{#1}} \achapter{\protect{Type Classes}} \aauthor{Matthieu Sozeau} @@ -12,12 +13,12 @@ \end{flushleft} This chapter presents a quick reference of the commands related to type -classes. It is not meant as an introduction to type classes altough it -may become one in the future. For an actual introduction, there is a +classes. For an actual introduction to type classes, there is a description of the system \cite{sozeau08} and the literature on type classes in \Haskell which also applies. \asection{Class and Instance declarations} +\label{ClassesInstances} The syntax for class and instance declarations is a mix between the record syntax of \Coq~and the type classes syntax of \Haskell: @@ -32,7 +33,7 @@ record syntax of \Coq~and the type classes syntax of \Haskell: \eol\indent{3.00em}$\cst{f}_m : \phi_m$. \medskip} { - + \medskip \kw{Instance} \classid{Id} $t_1 \cdots t_n$ := \eol\indent{3.00em}$\cst{f}_1 := b_1$ ; @@ -45,6 +46,263 @@ record syntax of \Coq~and the type classes syntax of \Haskell: Reset Initial. \end{coq_eval} +The $\tele{\alpha_i : \tau_i}$ variables are called the \emph{parameters} +of the class and the $\tele{f_k : \phi_k}$ are called the +\emph{methods}. Each class definition gives rise to a corresponding +record declaration and each instance is a regular definition whose type +is an instantiation of the record type. + +We'll use the following example class in the rest of the chapter: + +\begin{coq_example*} +Class Eq (A : Type) := + eq : A -> A -> bool ; + eq_leibniz : forall x y, eq x y = true -> x = y. +\end{coq_example*} + +This class implements a boolean equality test which is compatible with +leibniz equality on some type. An example implementation is: + +\begin{coq_example*} +Instance Eq unit := + eq x y := true ; + eq_leibniz x y H := + match x, y return x = y with tt, tt => refl_equal tt end. +\end{coq_example*} + +If one does not give all the members in the \texttt{Instance} +declaration, Coq enters the proof-mode and the user is asked to build +inhabitants of the remaining fields, e.g.: + +\begin{coq_example*} +Instance eq_bool : Eq bool := + eq x y := if x then y else negb y. +\end{coq_example*} + +\begin{coq_example} + Proof. intros x y H. + destruct x ; destruct y ; try discriminate ; reflexivity. + Defined. +\end{coq_example} + +One has to take care that the transparency of every field is determined +by the transparency of the \texttt{Instance} proof. One can use +alternatively the \texttt{Program} \texttt{Instance} \comindex{Program Instance} variant which has +richer facilities for dealing with obligations. + +\asection{Binding classes} + +Once a type class is declared, one can use it in class binders: +\begin{coq_example} + Definition neq {A : Type} [ Eq A ] (x y : A) := negb (eq x y). +\end{coq_example} + +When one calls a class method, a constraint is generated that is +satisfied only in contexts where the appropriate instances can be +found. In the example above, a constraint \texttt{Eq A} is generated and +satisfied by \texttt{[ Eq A ]}. In case no satisfying constraint can be +found, an error is raised: + +\begin{coq_example} + Definition neq' (A : Type) (x y : A) := negb (eq x y). +\end{coq_example} + +The algorithm used to solve constraints is a variant of the eauto tactic +that does proof search with a set of lemmas (the instances). It will use +local hypotheses as well as declared lemmas in the +\texttt{typeclass\_instances} database. Hence the example can also be +written: + +\begin{coq_example} + Definition neq' (A : Type) (eqa : Eq A) (x y : A) := negb (eq x y). +\end{coq_example} + +However, the bracketed binders should be used instead as they have +particular support for type classes: +\begin{itemize} +\item They automatically set the maximally implicit status for type + class arguments, making derived functions as easy to use as class + methods. In the example above, \texttt{A} and \texttt{eqa} should be + set maximally implicit. +\item They support implicit quantification on class arguments and + partialy applied type classes \S \ref{classes:implicitquant} +\item They support implicit quantification on superclasses (see section + \S \ref{classes:superclasses} +\end{itemize} + +\subsection{Implicit quantification} + +Implicit quantification is an automatic elaboration of a statement with +free variables into a closed statement where these variables are +quantified explicitely. Implicit generalization is done only inside +bracketed binders. + +Following the previous example, one can write: +\begin{coq_example} + Definition neq_impl [ eqa : Eq A ] (x y : A) := negb (eq x y). +\end{coq_example} + +Here \texttt{A} is implicitely generalized, and the resulting function +is equivalent to the one above. One must be careful that \emph{all} the +free variables are generalized, which may result in confusing errors in +case of typos. + +\asection{Parameterized Instances} + +One can declare parameterized instances as in \Haskell simply by giving +the constraints as a binding context before the instance, e.g.: + +\begin{coq_example*} +Instance [ eqa : Eq A, eqb : Eq B ] => prod_eq : Eq (A * B) := + eq x y := match x, y with + | (la, ra), (lb, rb) => andb (eq la lb) (eq ra rb) + end. +\end{coq_example*} +\begin{coq_eval} +Admitted. +\end{coq_eval} + +These instances are used just as well as lemmas in the instances hint database. + +\asection{Building hierarchies} + +\subsection{Superclasses} +One can also parameterize classes by other classes, generating a +hierarchy of classes and superclasses. In the same way, we give the +superclasses as a binding context: + +\begin{coq_example} +Class [ eqa : Eq A ] => Ord := + le : A -> A -> bool. +\end{coq_example} + +This declaration means that any instance of the \texttt{Ord} class must +have an instance of \texttt{Eq}. The parameters of the subclass contains +at least all the parameters of its superclasses in their order of +appearance (here \texttt{A} is the only one). + +Internally, \texttt{Ord} will become a record type with two parameters: +a type \texttt{A} and an object of type \texttt{Eq A}. However, one can +still use it as if it had a single parameter inside class binders: the +generalization of superclasses will be done automatically. +\begin{coq_example} +Definition le_eq [ Ord A ] (x y : A) := + andb (le x y) (le y x). +\end{coq_example} + +In some cases, to be able to specify sharing of structures, one may want to give +explicitely the superclasses. It is is possible to do it directly in regular +binders, and using the \texttt{!} modifier in class binders. For +example: + +\begin{coq_example*} +Definition lt [ eqa : Eq A, ! Ord eqA ] (x y : A) := + andb (le x y) (neq x y). +\end{coq_example*} + +The \texttt{!} modifier switches the way a binder is parsed back to the +regular interpretation of Coq. In particular, it uses the implicit +arguments mechanism if available, as shown in the example. + +\subsection{Substructures} + +Substructures are components of a class which are instances of a class +themselves. They often arise when using classes for logical properties, +e.g.: + +\begin{coq_eval} +Require Import Relations. +\end{coq_eval} +\begin{coq_example*} +Class Reflexive (A : Type) (R : relation A) := + reflexivity : forall x, R x x. +Class Transitive (A : Type) (R : relation A) := + transitivity : forall x y z, R x y -> R y z -> R x z. +\end{coq_example*} + +This declares singleton classes for reflexive and transitive relations. +These may be used as part of other classes: + +\begin{coq_example*} +Class PreOrder (A : Type) (R : relation A) := + PreOrder_Reflexive :> Reflexive A R ; + PreOrder_Transitive :> Transitive A R. +\end{coq_example*} + +The syntax \texttt{:>} indicates that each \texttt{PreOrder} can be seen +as a \texttt{Reflexive} relation. So each time a reflexive relation is +needed, a preorder can be used instead. This is very similar to the +coercion mechanism of \texttt{Structure} declarations. +The implementation simply declares the projection as an instance. + +One can also declare existing objects or structure +projections using the \texttt{Existing Instance} command to achieve the +same effect. + +\section{Summary of the commands +\label{TypeClassCommands}} + +\subsection{\tt Class {\ident} {\binder$_1$ \ldots \binder$_n$} + : \sort := field$_1$ ; \ldots ; field$_k$.} +\comindex{Class} +\label{Class} + +The \texttt{Class} command is used to declare a type class with +parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to +{\tt field$_k$}. A optional context of the form {\tt [ C$_1$, \ldots + C$_j$ ] =>} can be put before the name of the class to declare +superclasses. + +\subsection{\tt Instance {\ident} : {Class} {t$_1$ \ldots t$_n$} + := field$_1$ := b$_1$ ; \ldots ; field$_i$ := b$_i$} +\comindex{Instance} +\label{Instance} + +The \texttt{Instance} command is used to declare a type class instance +named {\ident} of the class \emph{Class} with parameters {t$_1$} to {t$_n$} and +fields {\tt b$_1$} to {\tt b$_i$}, where each field must be a declared +field of the class. Missing fields must be filled in interactive proof mode. + +A arbitrary context of the form {\tt \binder$_1$ \ldots \binder$_n$ =>} +can be put before the name of the instance to declare a parameterized instance. + +Besides the {\tt Class} and {\tt Instance} vernacular commands, there +are a few other commands related to type classes. + +\subsection{\tt Existing Instance {\ident}} +\comindex{Existing Instance} +\label{ExistingInstance} + +This commands adds an arbitrary constant whose type ends with an applied +type class to the instance database. It can be used for redeclaring +instances at the end of sections, or declaring structure projections as +instances. This is almost equivalent to {\tt Hint Resolve {\ident} : + typeclass\_instances}. + +\subsection{\tt Typeclasses unfold {\ident$_1$ \ldots \ident$_n$}} +\comindex{Typeclasses unfold} +\label{TypeclassesUnfold} + +This commands declares {\ident} as an unfoldable constant during type +class resolution. It is useful when some constants prevent some +unifications and make resolution fail. It happens in particular when constants are +used to abbreviate type, like {\tt relation A := A -> A -> Prop}. +This is equivalent to {\tt Hint Unfold {\ident} : typeclass\_instances}. + +\subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]} +\comindex{Typeclasses eauto} +\label{TypeclassesEauto} + +This commands allows to customize the type class resolution tactic, +based on a variant of eauto. The flags semantics are: +\begin{itemize} +\item {\tt debug} In debug mode, the trace of successfully applied + tactics is printed. +\item {\tt dfs, bfs} This sets the search strategy to depth-first search + (the default) or breadth-first search. +\item {\emph{depth}} This sets the depth of the search (the default is 100). +\end{itemize} + %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/tactics/auto.ml b/tactics/auto.ml index 816bd61ca..2c327b71b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -591,11 +591,17 @@ let auto_unif_flags = { (* Try unification with the precompiled clause, then use registered Apply *) +let unify_resolve_nodelta (c,clenv) gls = + let clenv' = connect_clenv gls clenv in + let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gls in + h_simplest_apply c gls + let unify_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false ~flags clenv' gls in h_apply true false (c,NoBindings) gls + (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) @@ -648,33 +654,54 @@ let rec trivial_fail_db mod_delta db_list local_db gl = (List.map tclCOMPLETE (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl -and my_find_search mod_delta db_list local_db hdc concl = - let flags = - if mod_delta then {auto_unif_flags with use_metas_eagerly = true} - else auto_unif_flags +and my_find_search_nodelta db_list local_db hdc concl = + let tacl = + if occur_existential concl then + list_map_append + (fun (st, db) -> (Hint_db.map_all hdc db)) + (local_db::db_list) + else + list_map_append (fun (_, db) -> + Hint_db.map_auto (hdc,concl) db) + (local_db::db_list) in + List.map + (fun {pri=b; pat=p; code=t} -> + (b, + match t with + | Res_pf (term,cl) -> unify_resolve_nodelta (term,cl) + | ERes_pf (_,c) -> (fun gl -> error "eres_pf") + | Give_exact c -> exact_check c + | Res_pf_THEN_trivial_fail (term,cl) -> + tclTHEN + (unify_resolve_nodelta (term,cl)) + (trivial_fail_db false db_list local_db) + | Unfold_nth c -> unfold_in_concl [[],c] + | Extern tacast -> + conclPattern concl (Option.get p) tacast)) + tacl + +and my_find_search mod_delta = + if mod_delta then my_find_search_delta + else my_find_search_nodelta + +and my_find_search_delta db_list local_db hdc concl = + let flags = {auto_unif_flags with use_metas_eagerly = true} in let tacl = if occur_existential concl then list_map_append (fun (st, db) -> - let st = - if mod_delta then - {flags with modulo_delta = st} - else flags - in + let st = {flags with modulo_delta = st} in List.map (fun x -> (st,x)) (Hint_db.map_all hdc db)) (local_db::db_list) else list_map_append (fun ((ids, csts as st), db) -> let st, l = - if not mod_delta then - flags, Hint_db.map_auto (hdc,concl) db - else - let l = - if (Idpred.is_empty ids && Cpred.is_empty csts) - then Hint_db.map_auto (hdc,concl) db - else Hint_db.map_all hdc db - in {flags with modulo_delta = st}, l + let l = + if (Idpred.is_empty ids && Cpred.is_empty csts) + then Hint_db.map_auto (hdc,concl) db + else Hint_db.map_all hdc db + in {flags with modulo_delta = st}, l in List.map (fun x -> (st,x)) l) (local_db::db_list) in @@ -682,18 +709,18 @@ and my_find_search mod_delta db_list local_db hdc concl = (fun (st, {pri=b; pat=p; code=t}) -> (b, match t with - | Res_pf (term,cl) -> unify_resolve st (term,cl) + | Res_pf (term,cl) -> unify_resolve st (term,cl) | ERes_pf (_,c) -> (fun gl -> error "eres_pf") | Give_exact c -> exact_check c | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_resolve st (term,cl)) - (trivial_fail_db mod_delta db_list local_db) + (trivial_fail_db true db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> conclPattern concl (Option.get p) tacast)) - tacl - + tacl + and trivial_resolve mod_delta db_list local_db cl = try let hdconstr = List.hd (head_constr_bound cl []) in diff --git a/tactics/auto.mli b/tactics/auto.mli index 7853235be..5b151162c 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -141,6 +141,8 @@ val default_search_depth : int ref val auto_unif_flags : Unification.unify_flags (* Try unification with the precompiled clause, then use registered Apply *) +val unify_resolve_nodelta : (constr * clausenv) -> tactic + val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic (* [ConclPattern concl pat tacast]: diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 3894dfd1f..e6172d3df 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -91,25 +91,72 @@ open Unification (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) (***************************************************************************) +(* no delta yet *) + let unify_e_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false ~flags clenv' gls in h_simplest_eapply c gls -let rec e_trivial_fail_db db_list local_db goal = +let unify_e_resolve_nodelta (c,clenv) gls = + let clenv' = connect_clenv gls clenv in + let _ = clenv_unique_resolver false clenv' gls in + h_simplest_eapply c gls + +let rec e_trivial_fail_db mod_delta db_list local_db goal = let tacl = registered_e_assumption :: (tclTHEN Tactics.intro (function g'-> let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in - (e_trivial_fail_db db_list + (e_trivial_fail_db mod_delta db_list (add_hint_list hintl local_db) g'))) :: - (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) + (List.map fst (e_trivial_resolve mod_delta db_list local_db (pf_concl goal)) ) in tclFIRST (List.map tclCOMPLETE tacl) goal -and e_my_find_search db_list local_db hdc concl = +and e_my_find_search mod_delta = + if mod_delta then e_my_find_search_delta + else e_my_find_search_nodelta + +and e_my_find_search_nodelta db_list local_db hdc concl = + let hdc = head_of_constr_reference hdc in + let hintl = + if occur_existential concl then + list_map_append (fun (st, db) -> Hint_db.map_all hdc db) (local_db::db_list) + else + list_map_append (fun (st, db) -> + Hint_db.map_auto (hdc,concl) db) (local_db::db_list) + in + let tac_of_hint = + fun {pri=b; pat = p; code=t} -> + (b, + let tac = + match t with + | Res_pf (term,cl) -> unify_resolve_nodelta (term,cl) + | ERes_pf (term,cl) -> unify_e_resolve_nodelta (term,cl) + | Give_exact (c) -> e_give_exact_constr c + | Res_pf_THEN_trivial_fail (term,cl) -> + tclTHEN (unify_e_resolve_nodelta (term,cl)) + (e_trivial_fail_db false db_list local_db) + | Unfold_nth c -> unfold_in_concl [[],c] + | Extern tacast -> conclPattern concl + (Option.get p) tacast + in + (tac,fmt_autotactic t)) + (*i + fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); + try tac gls + with e when Logic.catchable_exception(e) -> + (Format.print_string "Fail\n"; + Format.print_flush (); + raise e) + i*) + in + List.map tac_of_hint hintl + +and e_my_find_search_delta db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in let hintl = if occur_existential concl then @@ -131,7 +178,7 @@ and e_my_find_search db_list local_db hdc concl = | Give_exact (c) -> e_give_exact_constr c | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve st (term,cl)) - (e_trivial_fail_db db_list local_db) + (e_trivial_fail_db true db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> conclPattern concl (Option.get p) tacast @@ -148,16 +195,16 @@ and e_my_find_search db_list local_db hdc concl = in List.map tac_of_hint hintl -and e_trivial_resolve db_list local_db gl = +and e_trivial_resolve mod_delta db_list local_db gl = try Auto.priority - (e_my_find_search db_list local_db + (e_my_find_search mod_delta db_list local_db (List.hd (head_constr_bound gl [])) gl) with Bound | Not_found -> [] -let e_possible_resolve db_list local_db gl = +let e_possible_resolve mod_delta db_list local_db gl = try List.map snd - (e_my_find_search db_list local_db + (e_my_find_search mod_delta db_list local_db (List.hd (head_constr_bound gl [])) gl) with Bound | Not_found -> [] @@ -248,7 +295,7 @@ module SearchProblem = struct in let rec_tacs = let l = - filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) + filter_tactics s.tacres (e_possible_resolve false s.dblist (List.hd s.localdb) (pf_concl g)) in List.map (fun ((lgls,_) as res, pp) -> diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index a57914fdd..015eb7323 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -42,7 +42,7 @@ Class Reflexive A (R : relation A) := reflexivity : forall x, R x x. Class Irreflexive A (R : relation A) := - irreflexivity : forall x, R x x -> False. + irreflexivity :> Reflexive A (complement R). Class Symmetric A (R : relation A) := symmetry : forall x y, R x y -> R y x. @@ -86,15 +86,15 @@ Program Instance [ Transitive A R ] => flip_Transitive : Transitive (flip R). Program Instance [ Reflexive A (R : relation A) ] => Reflexive_complement_Irreflexive : Irreflexive (complement R). -Program Instance [ Irreflexive A (R : relation A) ] => - Irreflexive_complement_Reflexive : Reflexive (complement R). - Next Obligation. Proof. + unfold complement. red. intros H. - apply (irreflexivity H). + intros H' ; apply H'. + apply (reflexivity H). Qed. + Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R). Next Obligation. @@ -152,13 +152,13 @@ Program Instance eq_Transitive : Transitive (@eq A). (** A [PreOrder] is both Reflexive and Transitive. *) -Class PreOrder A (R : relation A) := +Class PreOrder A (R : relation A) : Prop := PreOrder_Reflexive :> Reflexive R ; PreOrder_Transitive :> Transitive R. (** A partial equivalence relation is Symmetric and Transitive. *) -Class PER (carrier : Type) (pequiv : relation carrier) := +Class PER (carrier : Type) (pequiv : relation carrier) : Prop := PER_Symmetric :> Symmetric pequiv ; PER_Transitive :> Transitive pequiv. @@ -178,7 +178,7 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => (** The [Equivalence] typeclass. *) -Class Equivalence (carrier : Type) (equiv : relation carrier) := +Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop := Equivalence_Reflexive :> Reflexive equiv ; Equivalence_Symmetric :> Symmetric equiv ; Equivalence_Transitive :> Transitive equiv. |