X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Ftactics%2Fring.ml;fp=components%2Ftactics%2Fring.ml;h=7695a4ff0c82d885b66c9a76f1a3478cd915823b;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/tactics/ring.ml b/components/tactics/ring.ml new file mode 100644 index 000000000..7695a4ff0 --- /dev/null +++ b/components/tactics/ring.ml @@ -0,0 +1,594 @@ +(* 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/. + *) + +(* $Id$ *) + +open CicReduction +open PrimitiveTactics +open ProofEngineTypes +open UriManager + +(** DEBUGGING *) + + (** perform debugging output? *) +let debug = false +let debug_print = fun _ -> () + + (** debugging print *) +let warn s = debug_print (lazy ("RING WARNING: " ^ (Lazy.force s))) + +(** CIC URIS *) + +(** + Note: For constructors URIs aren't really URIs but rather triples of + the form (uri, typeno, consno). This discrepancy is to preserver an + uniformity of invocation of "mkXXX" functions. +*) + +let equality_is_a_congruence_A = + uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var" +let equality_is_a_congruence_x = + uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var" +let equality_is_a_congruence_y = + uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var" + +let apolynomial_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind" +let apvar_uri = (apolynomial_uri, 0, 1) +let ap0_uri = (apolynomial_uri, 0, 2) +let ap1_uri = (apolynomial_uri, 0, 3) +let applus_uri = (apolynomial_uri, 0, 4) +let apmult_uri = (apolynomial_uri, 0, 5) +let apopp_uri = (apolynomial_uri, 0, 6) + +let quote_varmap_A_uri = uri_of_string "cic:/Coq/ring/Quote/variables_map/A.var" +let varmap_uri = uri_of_string "cic:/Coq/ring/Quote/varmap.ind" +let empty_vm_uri = (varmap_uri, 0, 1) +let node_vm_uri = (varmap_uri, 0, 2) +let varmap_find_uri = uri_of_string "cic:/Coq/ring/Quote/varmap_find.con" +let index_uri = uri_of_string "cic:/Coq/ring/Quote/index.ind" +let left_idx_uri = (index_uri, 0, 1) +let right_idx_uri = (index_uri, 0, 2) +let end_idx_uri = (index_uri, 0, 3) + +let abstract_rings_A_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/A.var" +let abstract_rings_Aplus_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aplus.var" +let abstract_rings_Amult_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Amult.var" +let abstract_rings_Aone_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aone.var" +let abstract_rings_Azero_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Azero.var" +let abstract_rings_Aopp_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aopp.var" +let abstract_rings_Aeq_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aeq.var" +let abstract_rings_vm_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/vm.var" +let abstract_rings_T_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/T.var" +let interp_ap_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/interp_ap.con" +let interp_sacs_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/interp_sacs.con" +let apolynomial_normalize_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con" +let apolynomial_normalize_ok_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con" + +(** CIC PREDICATES *) + + (** + check whether a term is a constant or not, if argument "uri" is given and is + not "None" also check if the constant correspond to the given one or not + *) +let cic_is_const ?(uri: uri option = None) term = + match uri with + | None -> + (match term with + | Cic.Const _ -> true + | _ -> false) + | Some realuri -> + (match term with + | Cic.Const (u, _) when (eq u realuri) -> true + | _ -> false) + +(** PROOF AND GOAL ACCESSORS *) + + (** + @param proof a proof + @return the uri of a given proof + *) +let uri_of_proof ~proof:(uri, _, _, _, _, _) = uri + + (** + @param status current proof engine status + @raise Failure if proof is None + @return current goal's metasenv + *) +let metasenv_of_status ((_,m,_,_,_, _), _) = m + + (** + @param status a proof engine status + @raise Failure when proof or goal are None + @return context corresponding to current goal + *) +let context_of_status status = + let (proof, goal) = status in + let metasenv = metasenv_of_status status in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + context + +(** CIC TERM CONSTRUCTORS *) + + (** + Create a Cic term consisting of a constant + @param uri URI of the constant + @proof current proof + @exp_named_subst explicit named substitution + *) +let mkConst ~uri ~exp_named_subst = + Cic.Const (uri, exp_named_subst) + + (** + Create a Cic term consisting of a constructor + @param uri triple where uri is the uri of an inductive + type, typeno is the type number in a mutind structure (0 based), consno is + the constructor number (1 based) + @exp_named_subst explicit named substitution + *) +let mkCtor ~uri:(uri, typeno, consno) ~exp_named_subst = + Cic.MutConstruct (uri, typeno, consno, exp_named_subst) + + (** + Create a Cic term consisting of a type member of a mutual induction + @param uri pair where uri is the uri of a mutual inductive + type and typeno is the type number (0 based) in the mutual induction + @exp_named_subst explicit named substitution + *) +let mkMutInd ~uri:(uri, typeno) ~exp_named_subst = + Cic.MutInd (uri, typeno, exp_named_subst) + +(** EXCEPTIONS *) + + (** + raised when the current goal is not ringable; a goal is ringable when is an + equality on reals (@see r_uri) + *) +exception GoalUnringable + +(** RING's FUNCTIONS LIBRARY *) + + (** + Check whether the ring tactic can be applied on a given term (i.e. that is + an equality on reals) + @param term to be tested + @return true if the term is ringable, false otherwise + *) +let ringable = + let is_equality = function + | Cic.MutInd (uri, 0, []) when (eq uri HelmLibraryObjects.Logic.eq_URI) -> true + | _ -> false + in + let is_real = function + | Cic.Const (uri, _) when (eq uri HelmLibraryObjects.Reals.r_URI) -> true + | _ -> false + in + function + | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) -> + warn (lazy "Goal Ringable!"); + true + | _ -> + warn (lazy "Goal Not Ringable :-(("); + false + + (** + split an equality goal of the form "t1 = t2" in its two subterms t1 and t2 + after checking that the goal is ringable + @param goal the current goal + @return a pair (t1,t2) that are two sides of the equality goal + @raise GoalUnringable if the goal isn't ringable + *) +let split_eq = function + | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term -> + warn (lazy ("" ^ (CicPp.ppterm t1) ^ "")); + warn (lazy ("" ^ (CicPp.ppterm t2) ^ "")); + (t1, t2) + | _ -> raise GoalUnringable + + (** + @param i an integer index representing a 1 based number of node in a binary + search tree counted in a fbs manner (i.e.: 1 is the root, 2 is the left + child of the root (if any), 3 is the right child of the root (if any), 4 is + the left child of the left child of the root (if any), ....) + @param proof the current proof + @return an index representing the same node in a varmap (@see varmap_uri), + the returned index is as defined in index (@see index_uri) + *) +let path_of_int n = + let rec digits_of_int n = + if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1)) + in + List.fold_right + (fun digit path -> + Cic.Appl [ + mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) []; + path]) + (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *) + (mkCtor end_idx_uri []) + + (** + Build a variable map (@see varmap_uri) from a variables array. + A variable map is almost a binary tree so this function receiving a var list + like [v;w;x;y;z] will build a varmap of shape: v + / \ + w x + / \ + y z + @param vars variables array + @return a cic term representing the variable map containing vars variables + *) +let btree_of_array ~vars = + let r = HelmLibraryObjects.Reals.r in + let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in + let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in + let size = Array.length vars in + let halfsize = size lsr 1 in + let rec aux n = (* build the btree starting from position n *) + (* + n is the position in the vars array _1_based_ in order to access + left and right child using (n*2, n*2+1) trick + *) + if n > size then + empty_vm_r + else if n > halfsize then (* no more children *) + Cic.Appl [node_vm_r; vars.(n-1); empty_vm_r; empty_vm_r] + else (* still children *) + Cic.Appl [node_vm_r; vars.(n-1); aux (n*2); aux (n*2+1)] + in + aux 1 + + (** + abstraction function: + concrete polynoms -----> (abstract polynoms, varmap) + @param terms list of conrete polynoms + @return a pair where aterms is a list of abstract polynoms + and varmap is the variable map needed to interpret them + *) +let abstract_poly ~terms = + let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *) + let varlist = ref [] in (* vars list in reverse order *) + let counter = ref 1 in (* index of next new variable *) + let rec aux = function (* TODO not tail recursive *) + (* "bop" -> binary operator | "uop" -> unary operator *) + | Cic.Appl (bop::t1::t2::[]) + when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.rplus_URI) bop) -> (* +. *) + Cic.Appl [mkCtor applus_uri []; aux t1; aux t2] + | Cic.Appl (bop::t1::t2::[]) + when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.rmult_URI) bop) -> (* *. *) + Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2] + | Cic.Appl (uop::t::[]) + when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.ropp_URI) uop) -> (* ~-. *) + Cic.Appl [mkCtor apopp_uri []; aux t] + | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r0_URI) t) -> (* 0. *) + mkCtor ap0_uri [] + | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r1_URI) t) -> (* 1. *) + mkCtor ap1_uri [] + | t -> (* variable *) + try + Hashtbl.find varhash t (* use an old var *) + with Not_found -> begin (* create a new var *) + let newvar = + Cic.Appl [mkCtor apvar_uri []; path_of_int !counter] + in + incr counter; + varlist := t :: !varlist; + Hashtbl.add varhash t newvar; + newvar + end + in + let aterms = List.map aux terms in (* abstract vars *) + let varmap = (* build varmap *) + btree_of_array ~vars:(Array.of_list (List.rev !varlist)) + in + (aterms, varmap) + + (** + given a list of abstract terms (i.e. apolynomials) build the ring "segments" + that is triples like (t', t'', t''') where + t' = interp_ap(varmap, at) + t'' = interp_sacs(varmap, (apolynomial_normalize at)) + t''' = apolynomial_normalize_ok(varmap, at) + at is the abstract term built from t, t is a single member of aterms + *) +let build_segments ~terms = + let theory_args_subst varmap = + [abstract_rings_A_uri, HelmLibraryObjects.Reals.r ; + abstract_rings_Aplus_uri, HelmLibraryObjects.Reals.rplus ; + abstract_rings_Amult_uri, HelmLibraryObjects.Reals.rmult ; + abstract_rings_Aone_uri, HelmLibraryObjects.Reals.r1 ; + abstract_rings_Azero_uri, HelmLibraryObjects.Reals.r0 ; + abstract_rings_Aopp_uri, HelmLibraryObjects.Reals.ropp ; + abstract_rings_vm_uri, varmap] in + let theory_args_subst' eq varmap t = + [abstract_rings_A_uri, HelmLibraryObjects.Reals.r ; + abstract_rings_Aplus_uri, HelmLibraryObjects.Reals.rplus ; + abstract_rings_Amult_uri, HelmLibraryObjects.Reals.rmult ; + abstract_rings_Aone_uri, HelmLibraryObjects.Reals.r1 ; + abstract_rings_Azero_uri, HelmLibraryObjects.Reals.r0 ; + abstract_rings_Aopp_uri, HelmLibraryObjects.Reals.ropp ; + abstract_rings_Aeq_uri, eq ; + abstract_rings_vm_uri, varmap ; + abstract_rings_T_uri, t] in + let interp_ap varmap = + mkConst interp_ap_uri (theory_args_subst varmap) in + let interp_sacs varmap = + mkConst interp_sacs_uri (theory_args_subst varmap) in + let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in + let apolynomial_normalize_ok eq varmap t = + mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in + let lxy_false = (** Cic funcion "fun (x,y):R -> false" *) + Cic.Lambda (Cic.Anonymous, HelmLibraryObjects.Reals.r, + Cic.Lambda (Cic.Anonymous, HelmLibraryObjects.Reals.r, HelmLibraryObjects.Datatypes.falseb)) + in + let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *) + List.map (* build ring segments *) + (fun t -> + Cic.Appl [interp_ap varmap ; t], + Cic.Appl ( + [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]), + Cic.Appl [apolynomial_normalize_ok lxy_false varmap HelmLibraryObjects.Reals.rtheory ; t] + ) aterms + + +let status_of_single_goal_tactic_result = + function + proof,[goal] -> proof,goal + | _ -> + raise (Fail (lazy "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")) + +(* Galla: spostata in variousTactics.ml + (** + auxiliary tactic "elim_type" + @param status current proof engine status + @param term term to cut + *) +let elim_type_tac ~term status = + warn (lazy "in Ring.elim_type_tac"); + Tacticals.thens ~start:(cut_tac ~term) + ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] status +*) + + (** + auxiliary tactic, use elim_type and try to close 2nd subgoal using proof + @param status current proof engine status + @param term term to cut + @param proof term used to prove second subgoal generated by elim_type + *) +(* FG: METTERE I NOMI ANCHE QUI? *) +let elim_type2_tac ~term ~proof = + let elim_type2_tac ~term ~proof status = + let module E = EliminationTactics in + warn (lazy "in Ring.elim_type2"); + ProofEngineTypes.apply_tactic + (Tacticals.thens ~start:(E.elim_type_tac term) + ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status + in + ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof) + +(* Galla: spostata in variousTactics.ml + (** + Reflexivity tactic, try to solve current goal using "refl_eqT" + Warning: this isn't equale to the coq's Reflexivity because this one tries + only refl_eqT, coq's one also try "refl_equal" + @param status current proof engine status + *) +let reflexivity_tac (proof, goal) = + warn (lazy "in Ring.reflexivity_tac"); + let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in + try + apply_tac (proof, goal) ~term:refl_eqt + with (Fail _) as e -> + let e_str = Printexc.to_string e in + raise (Fail ("Reflexivity failed with exception: " ^ e_str)) +*) + + (** lift an 8-uple of debrujins indexes of n *) +let lift ~n (a,b,c,d,e,f,g,h) = + match (List.map (CicSubstitution.lift n) [a;b;c;d;e;f;g;h]) with + | [a;b;c;d;e;f;g;h] -> (a,b,c,d,e,f,g,h) + | _ -> assert false + + (** + remove hypothesis from a given status starting from the last one + @param count number of hypotheses to remove + @param status current proof engine status + *) +let purge_hyps_tac ~count = + let purge_hyps_tac ~count status = + let module S = ProofEngineStructuralRules in + let (proof, goal) = status in + let rec aux n context status = + assert(n>=0); + match (n, context) with + | (0, _) -> status + | (n, hd::tl) -> + let name_of_hyp = + match hd with + None + | Some (Cic.Anonymous,_) -> assert false + | Some (Cic.Name name,_) -> name + in + aux (n-1) tl + (status_of_single_goal_tactic_result + (ProofEngineTypes.apply_tactic (S.clear ~hyps:[name_of_hyp]) status)) + | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left" + in + let (_, metasenv, _subst, _, _, _) = proof in + let (_, context, _) = CicUtil.lookup_meta goal metasenv in + let proof',goal' = aux count context status in + assert (goal = goal') ; + proof',[goal'] + in + ProofEngineTypes.mk_tactic (purge_hyps_tac ~count) + +(** THE TACTIC! *) + + (** + Ring tactic, does associative and commutative rewritings in Reals ring + @param status current proof engine status + *) + +let ring_tac status = + let (proof, goal) = status in + warn (lazy "in Ring tactic"); + let eqt = mkMutInd (HelmLibraryObjects.Logic.eq_URI, 0) [] in + let r = HelmLibraryObjects.Reals.r in + let metasenv = metasenv_of_status status in + let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in + let (t1, t2) = split_eq ty in (* goal like t1 = t2 *) + match (build_segments ~terms:[t1; t2]) with + | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin + if debug then + List.iter (* debugging, feel free to remove *) + (fun (descr, term) -> + warn (lazy (descr ^ " " ^ (CicPp.ppterm term)))) + (List.combine + ["t1"; "t1'"; "t1''"; "t1'_eq_t1''"; + "t2"; "t2'"; "t2''"; "t2'_eq_t2''"] + [t1; t1'; t1''; t1'_eq_t1''; + t2; t2'; t2''; t2'_eq_t2'']); + try + let new_hyps = ref 0 in (* number of new hypotheses created *) + ProofEngineTypes.apply_tactic + (Tacticals.first + ~tactics:[ + EqualityTactics.reflexivity_tac ; + exact_tac ~term:t1'_eq_t1'' ; + exact_tac ~term:t2'_eq_t2'' ; + exact_tac + ~term:( + Cic.Appl + [mkConst HelmLibraryObjects.Logic.sym_eq_URI + [equality_is_a_congruence_A, HelmLibraryObjects.Reals.r; + equality_is_a_congruence_x, t1'' ; + equality_is_a_congruence_y, t1 + ] ; + t1'_eq_t1'' + ]) ; + ProofEngineTypes.mk_tactic (fun status -> + let status' = (* status after 1st elim_type use *) + let context = context_of_status status in + let b,_ = (*TASSI : FIXME*) + are_convertible context t1'' t1 CicUniv.empty_ugraph in + if not b then begin + warn (lazy "t1'' and t1 are NOT CONVERTIBLE"); + let newstatus = + ProofEngineTypes.apply_tactic + (elim_type2_tac (* 1st elim_type use *) + ~proof:t1'_eq_t1'' + ~term:(Cic.Appl [eqt; r; t1''; t1])) + status + in + incr new_hyps; (* elim_type add an hyp *) + match newstatus with + (proof,[goal]) -> proof,goal + | _ -> assert false + end else begin + warn (lazy "t1'' and t1 are CONVERTIBLE"); + status + end + in + let (t1,t1',t1'',t1'_eq_t1'',t2,t2',t2'',t2'_eq_t2'') = + lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'') + in + let status'' = + ProofEngineTypes.apply_tactic + (Tacticals.first (* try to solve 1st subgoal *) + ~tactics:[ + exact_tac ~term:t2'_eq_t2''; + exact_tac + ~term:( + Cic.Appl + [mkConst HelmLibraryObjects.Logic.sym_eq_URI + [equality_is_a_congruence_A, HelmLibraryObjects.Reals.r; + equality_is_a_congruence_x, t2'' ; + equality_is_a_congruence_y, t2 + ] ; + t2'_eq_t2'' + ]) ; + ProofEngineTypes.mk_tactic (fun status -> + let status' = + let context = context_of_status status in + let b,_ = (* TASSI:FIXME *) + are_convertible context t2'' t2 CicUniv.empty_ugraph + in + if not b then begin + warn (lazy "t2'' and t2 are NOT CONVERTIBLE"); + let newstatus = + ProofEngineTypes.apply_tactic + (elim_type2_tac (* 2nd elim_type use *) + ~proof:t2'_eq_t2'' + ~term:(Cic.Appl [eqt; r; t2''; t2])) + status + in + incr new_hyps; (* elim_type add an hyp *) + match newstatus with + (proof,[goal]) -> proof,goal + | _ -> assert false + end else begin + warn (lazy "t2'' and t2 are CONVERTIBLE"); + status + end + in + try (* try to solve main goal *) + warn (lazy "trying reflexivity ...."); + ProofEngineTypes.apply_tactic + EqualityTactics.reflexivity_tac status' + with (Fail _) -> (* leave conclusion to the user *) + warn (lazy "reflexivity failed, solution's left as an ex :-)"); + ProofEngineTypes.apply_tactic + (purge_hyps_tac ~count:!new_hyps) status')]) + status' + in + status'')]) + status + with (Fail s) -> + raise (Fail (lazy ("Ring failure: " ^ Lazy.force s))) + end + | _ -> (* impossible: we are applying ring exacty to 2 terms *) + assert false + + (* wrap ring_tac catching GoalUnringable and raising Fail *) + +let ring_tac status = + try + ring_tac status + with GoalUnringable -> + raise (Fail (lazy "goal unringable")) + +let ring_tac = ProofEngineTypes.mk_tactic ring_tac +