From: marangon Date: Fri, 10 Mar 2006 12:59:53 +0000 (+0000) Subject: Added inversion principle creation for inductive predicates. X-Git-Tag: 0.4.95@7852~1610 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6f0fca547fdd3f4b57cee75d360262dc910f8854;p=helm.git Added inversion principle creation for inductive predicates. --- diff --git a/components/library/.depend b/components/library/.depend index 416a3ce3e..94e20194f 100644 --- a/components/library/.depend +++ b/components/library/.depend @@ -14,10 +14,10 @@ cicCoercion.cmo: refinementTool.cmo coercDb.cmi cicCoercion.cmi cicCoercion.cmx: refinementTool.cmx coercDb.cmx cicCoercion.cmi coercGraph.cmo: coercDb.cmi coercGraph.cmi coercGraph.cmx: coercDb.cmx coercGraph.cmi -librarySync.cmo: libraryDb.cmi coercGraph.cmi coercDb.cmi cicRecord.cmi \ - cicElim.cmi cicCoercion.cmi librarySync.cmi -librarySync.cmx: libraryDb.cmx coercGraph.cmx coercDb.cmx cicRecord.cmx \ - cicElim.cmx cicCoercion.cmx librarySync.cmi +librarySync.cmo: refinementTool.cmo libraryDb.cmi coercGraph.cmi coercDb.cmi \ + cicRecord.cmi cicElim.cmi cicCoercion.cmi librarySync.cmi +librarySync.cmx: refinementTool.cmx libraryDb.cmx coercGraph.cmx coercDb.cmx \ + cicRecord.cmx cicElim.cmx cicCoercion.cmx librarySync.cmi libraryNoDb.cmo: libraryNoDb.cmi libraryNoDb.cmx: libraryNoDb.cmi libraryClean.cmo: librarySync.cmi libraryNoDb.cmi libraryMisc.cmi \ diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 7209af691..91a838ddf 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -309,6 +309,16 @@ let generate_projections ~basedir refinement_toolkit uri fields = raise exn +let build_inversion_principle = ref (fun a b -> assert false);; + +let generate_inversion refinement_toolkit ~basedir uri obj = + match !build_inversion_principle uri obj with + None -> [] + | Some (ind_uri,ind_obj) -> + add_single_obj ind_uri ind_obj refinement_toolkit ~basedir; + [ind_uri] + + let add_obj refinement_toolkit uri obj ~basedir = add_single_obj uri obj refinement_toolkit ~basedir; let uris = ref [] in @@ -319,6 +329,7 @@ let add_obj refinement_toolkit uri obj ~basedir = | Cic.InductiveDefinition (_,_,_,attrs) -> uris := !uris @ generate_elimination_principles ~basedir uri refinement_toolkit; + uris := !uris @ generate_inversion refinement_toolkit ~basedir uri obj; let rec get_record_attrs = function | [] -> None diff --git a/components/library/librarySync.mli b/components/library/librarySync.mli index 812685c53..e9f2bd036 100644 --- a/components/library/librarySync.mli +++ b/components/library/librarySync.mli @@ -25,6 +25,9 @@ exception AlreadyDefined of UriManager.uri +(* this is a pointer to the function which builds the inversion principle *) +val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) option) ref + (* adds an object to the library together with all auxiliary lemmas on it *) (* (e.g. elimination principles, projections, etc.) *) (* it returns the list of the uris of the auxiliary lemmas generated *) diff --git a/components/tactics/inversion_principle.ml b/components/tactics/inversion_principle.ml new file mode 100644 index 000000000..2138893d3 --- /dev/null +++ b/components/tactics/inversion_principle.ml @@ -0,0 +1,203 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. +* + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let debug = false;; +let debug_print = + fun msg -> if debug then prerr_endline (Lazy.force msg) else () + +(* cuts away the last element of a list 'l' *) +let rec cut_last l = + match l with + | hd::tl when tl != [] -> hd:: (cut_last tl) + | _ -> [] +;; + +(* cuts away the first 'n' elements of a list 'l' *) +let rec cut_first n l = + if n>0 then + match l with + | hd::tl -> cut_first (n-1) tl + | [] -> [] + else l +;; + +(* returns the first 'n' elements of a list 'l' *) +let rec takefirst n l = + if n > 0 then + match l with + hd::tl when n > 0 -> hd:: takefirst (n-1) tl + | _ -> assert false + else [] +;; + +(* from a complex Cic.Prod term, returns the list of its components *) +let rec list_of_prod term = + match term with + | Cic.Prod (_,src,tgt) -> src::(list_of_prod tgt) + | _ -> [term] +;; + +let rec build_metas sort cons_list created_vars right_created_vars prop + uri typeno = + match cons_list with + | hd::tl -> + Cic.Prod( + Cic.Anonymous, + Cic.Implicit None, + build_metas sort tl + (List.map (CicSubstitution.lift 1) created_vars) + (List.map (CicSubstitution.lift 1) right_created_vars) + (List.map (CicSubstitution.lift 1) prop) uri typeno) + | [] -> + Cic.Prod( + Cic.Name("H"), (*new name?*) + Cic.Appl([Cic.MutInd(uri, typeno, [])] @ created_vars), + Cic.Appl (( (List.map (CicSubstitution.lift 1) prop) @ + (List.map (CicSubstitution.lift 1 ) right_created_vars) @ + (if Inversion.isSetType sort then [Cic.Rel 1] else [])(*H*)) + )) +;; + +(* computes the type of the abstract P *) +let rec get_prop_arity sort rightparam_tys(*only to name m's*) created_vars_ty + local_rvars left_created_vars nleft uri typeno = + match (created_vars_ty) with + hd::tl when (nleft > 0) -> + get_prop_arity sort rightparam_tys tl local_rvars left_created_vars + (nleft-1) uri typeno + | hd::tl -> + Cic.Prod( + Cic.Name("m" ^ string_of_int(List.length rightparam_tys) ), + hd, + get_prop_arity sort (List.tl rightparam_tys) + (List.map (CicSubstitution.lift 1) tl) + (List.map (CicSubstitution.lift 1) (local_rvars @ [Cic.Rel 1])) + (List.map (CicSubstitution.lift 1) left_created_vars) nleft uri typeno + ) + | [] -> + if Inversion.isSetType sort then + Cic.Prod(Cic.Anonymous, + Cic.Appl([Cic.MutInd(uri, typeno, [])] + @ (List.map (CicSubstitution.lift (-1)) left_created_vars) + @ (List.map (CicSubstitution.lift(-1)) local_rvars) ), + Cic.Sort(Cic.Prop)) + else + Cic.Sort Cic.Prop + | _ -> assert false +;; + +(* created vars is empty at the beginning *) +let rec build_theorem rightparam_tys arity_l (*arity_l only to name p's*) + arity cons_list created_vars created_vars_ty nleft + uri typeno = + match (arity) with + Cic.Prod(_,src,tgt) -> + Cic.Prod( + Cic.Name("p" ^ string_of_int(List.length arity_l)), + src, + build_theorem rightparam_tys + (List.tl arity_l) tgt cons_list + (List.map (CicSubstitution.lift 1) (created_vars @ [Cic.Rel 1])) + (List.map (CicSubstitution.lift 1) (created_vars_ty @ [src])) + nleft uri typeno) + | sort -> + Cic.Prod(Cic.Name("P"), + get_prop_arity sort rightparam_tys created_vars_ty [](*local vars*) + (takefirst nleft created_vars) (*left_created_vars*) nleft uri typeno, + build_metas sort cons_list created_vars (cut_first nleft created_vars) + [(Cic.Rel 1)] uri typeno ) +;; + +let build_inversion uri obj = + (*uri e obj of InductiveDefinition *) + let module PET = ProofEngineTypes in + let typeno = 0 in + let name,nleft,arity,cons_list = + match obj with + Cic.InductiveDefinition (tys,_,nleft,_) -> + let (name,_,arity,cons_list) = List.nth tys typeno in + (*we suppose there is only one inductiveType, so typeno=0 identically *) + (name,nleft,arity,cons_list) + |_ -> assert false + in + (*check if there are right parameters, else return void*) + if List.length (list_of_prod arity) = (nleft + 1) then + None + else + begin + let arity_l = cut_last (list_of_prod arity) in + let rightparam_tys = cut_first nleft arity_l in + let theorem = build_theorem rightparam_tys arity_l arity cons_list + [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in + (*DEBUG*) debug_print (lazy ("theorem prima di refine: " ^ (CicPp.ppterm + theorem))); + let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem + CicUniv.empty_ugraph in + (*DEBUG*) debug_print (lazy ("theorem dopo refine: " ^ (CicPp.ppterm + ref_theorem))); + let buri = UriManager.buri_of_uri uri in + let inversor_uri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in + let goal = CicMkImplicit.new_meta metasenv [] in + let metasenv' = (goal,[],ref_theorem)::metasenv in + let proof= (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem) in + let _,applies = + List.fold_right + (fun _ (i,applies) -> + i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies) + cons_list (2,[]) + in + let proof1,gl1 = + PET.apply_tactic + (Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ()) + (*if the number of applies is 1, we cannot use thens, but then_*) + ~continuation: + (match (List.length applies) with + 0 -> (Inversion.private_inversion_tac (Cic.Rel 1)) + | 1 -> (Tacticals.then_ + ~start:(Inversion.private_inversion_tac (Cic.Rel 1)) + ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2)) + ) + | _ -> (Tacticals.thens + ~start:(Inversion.private_inversion_tac (Cic.Rel 1)) + ~continuations:applies + ) + )) + (proof,goal) + in + let metasenv,bo,ty = + match proof1 with (_,metasenv,bo,ty) -> metasenv,bo,ty + in + assert (metasenv = []); + Some + (inversor_uri, + Cic.Constant (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[])) + end +;; + +let init () = ();; + +LibrarySync.build_inversion_principle := build_inversion;; diff --git a/components/tactics/inversion_principle.mli b/components/tactics/inversion_principle.mli new file mode 100644 index 000000000..7cdf29c24 --- /dev/null +++ b/components/tactics/inversion_principle.mli @@ -0,0 +1 @@ +val init: unit -> unit