]> matita.cs.unibo.it Git - helm.git/commitdiff
Added inversion principle creation for inductive predicates.
authormarangon <??>
Fri, 10 Mar 2006 12:59:53 +0000 (12:59 +0000)
committermarangon <??>
Fri, 10 Mar 2006 12:59:53 +0000 (12:59 +0000)
components/library/.depend
components/library/librarySync.ml
components/library/librarySync.mli
components/tactics/inversion_principle.ml [new file with mode: 0644]
components/tactics/inversion_principle.mli [new file with mode: 0644]

index 416a3ce3e7998e25266429969fb22bd79b3d3cd9..94e20194f2a035686df30969f07d5230198e5b50 100644 (file)
@@ -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 \
index 7209af691af65009968952cb187ec537fddc5e22..91a838ddf5e9f5a588f369342bb6b07f0387b334 100644 (file)
@@ -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
index 812685c5361816b701eb3fabae9b816ab3453eee..e9f2bd0369ee45b9df98a984985f64184f1a4291 100644 (file)
@@ -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 (file)
index 0000000..2138893
--- /dev/null
@@ -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 (file)
index 0000000..7cdf29c
--- /dev/null
@@ -0,0 +1 @@
+val init: unit -> unit