diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-29 12:30:25 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-29 12:30:25 +0000 |
commit | 73798a12d39b03e1823b93c1364a86d14e2eec0a (patch) | |
tree | 1095b79d71bdacfcf2acc311b9e4a3aa98f64d4c | |
parent | ea24960e35ee39f8ed719583886f7b56587a879c (diff) |
Fix eauto still using delta when it shouldn't (should make CoRN compile
in reasonable time), add (unfinished) documentation on type classes.
Put some classes into Prop explicitely as singleton inductive types are
no longer in Prop by default even if all the arguments are (is that
really what we want? roconnor says no).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10868 85f007b7-540e-0410-9357-904b9bb8a0f7
-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. |