+++ /dev/null
-(* 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/.
- *)
-
-open CicReduction
-open PrimitiveTactics
-open ProofEngineTypes
-open UriManager
-
-open HelmLibraryObjects
-
-(** DEBUGGING *)
-
- (** perform debugging output? *)
-let debug = false
-
- (** debugging print *)
-let warn s =
- if debug then
- prerr_endline ("RING WARNING: " ^ 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 <uri, typeno, consno> 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 <uri, typeno> 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 Logic.eq_URI) -> true
- | _ -> false
- in
- let is_real = function
- | Cic.Const (uri, _) when (eq uri Reals.r_URI) -> true
- | _ -> false
- in
- function
- | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) ->
- warn "Goal Ringable!";
- true
- | _ ->
- warn "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 ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>");
- warn ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>");
- (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 = 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 <aterms, varmap> 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 Reals.rplus_URI) bop) -> (* +. *)
- Cic.Appl [mkCtor applus_uri []; aux t1; aux t2]
- | Cic.Appl (bop::t1::t2::[])
- when (cic_is_const ~uri:(Some Reals.rmult_URI) bop) -> (* *. *)
- Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2]
- | Cic.Appl (uop::t::[])
- when (cic_is_const ~uri:(Some Reals.ropp_URI) uop) -> (* ~-. *)
- Cic.Appl [mkCtor apopp_uri []; aux t]
- | t when (cic_is_const ~uri:(Some Reals.r0_URI) t) -> (* 0. *)
- mkCtor ap0_uri []
- | t when (cic_is_const ~uri:(Some 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, Reals.r ;
- abstract_rings_Aplus_uri, Reals.rplus ;
- abstract_rings_Amult_uri, Reals.rmult ;
- abstract_rings_Aone_uri, Reals.r1 ;
- abstract_rings_Azero_uri, Reals.r0 ;
- abstract_rings_Aopp_uri, Reals.ropp ;
- abstract_rings_vm_uri, varmap] in
- let theory_args_subst' eq varmap t =
- [abstract_rings_A_uri, Reals.r ;
- abstract_rings_Aplus_uri, Reals.rplus ;
- abstract_rings_Amult_uri, Reals.rmult ;
- abstract_rings_Aone_uri, Reals.r1 ;
- abstract_rings_Azero_uri, Reals.r0 ;
- abstract_rings_Aopp_uri, 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, Reals.r,
- Cic.Lambda (Cic.Anonymous, Reals.r, 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 Reals.rtheory ; t]
- ) aterms
-
-
-let status_of_single_goal_tactic_result =
- function
- proof,[goal] -> proof,goal
- | _ ->
- raise (Fail "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 "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
- *)
-let elim_type2_tac ~term ~proof status =
- let module E = EliminationTactics in
- warn "in Ring.elim_type2";
- Tacticals.thens ~start:(E.elim_type_tac ~term)
- ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] status
-
-(* 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 "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 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) ->
- aux (n-1) tl
- (status_of_single_goal_tactic_result (S.clear ~hyp:hd status))
- | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
- in
- let (_, metasenv, _, _) = proof in
- let (_, context, _) = CicUtil.lookup_meta goal metasenv in
- let proof',goal' = aux count context status in
- assert (goal = goal') ;
- proof',[goal']
-
-(** 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 "in Ring tactic";
- let eqt = mkMutInd (Logic.eq_URI, 0) [] in
- let r = 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
- List.iter (* debugging, feel free to remove *)
- (fun (descr, term) ->
- warn (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 *)
- Tacticals.try_tactics
- status
- ~tactics:[
- "reflexivity", EqualityTactics.reflexivity_tac ;
- "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
- "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
- "exact sym_eqt su t1 ...", exact_tac
- ~term:(
- Cic.Appl
- [mkConst Logic.sym_eq_URI
- [equality_is_a_congruence_A, Reals.r;
- equality_is_a_congruence_x, t1'' ;
- equality_is_a_congruence_y, t1
- ] ;
- t1'_eq_t1''
- ]) ;
- "elim_type eqt su t1 ...", (fun status ->
- let status' = (* status after 1st elim_type use *)
- let context = context_of_status status in
- if not (are_convertible context t1'' t1) then begin
- warn "t1'' and t1 are NOT CONVERTIBLE";
- let newstatus =
- elim_type2_tac (* 1st elim_type use *)
- status ~proof:t1'_eq_t1''
- ~term:(Cic.Appl [eqt; r; t1''; t1])
- in
- incr new_hyps; (* elim_type add an hyp *)
- match newstatus with
- (proof,[goal]) -> proof,goal
- | _ -> assert false
- end else begin
- warn "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'' =
- Tacticals.try_tactics (* try to solve 1st subgoal *)
- status'
- ~tactics:[
- "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
- "exact sym_eqt su t2 ...",
- exact_tac
- ~term:(
- Cic.Appl
- [mkConst Logic.sym_eq_URI
- [equality_is_a_congruence_A, Reals.r;
- equality_is_a_congruence_x, t2'' ;
- equality_is_a_congruence_y, t2
- ] ;
- t2'_eq_t2''
- ]) ;
- "elim_type eqt su t2 ...", (fun status ->
- let status' =
- let context = context_of_status status in
- if not (are_convertible context t2'' t2) then begin
- warn "t2'' and t2 are NOT CONVERTIBLE";
- let newstatus =
- elim_type2_tac (* 2nd elim_type use *)
- status ~proof:t2'_eq_t2''
- ~term:(Cic.Appl [eqt; r; t2''; t2])
- in
- incr new_hyps; (* elim_type add an hyp *)
- match newstatus with
- (proof,[goal]) -> proof,goal
- | _ -> assert false
- end else begin
- warn "t2'' and t2 are CONVERTIBLE";
- status
- end
- in
- try (* try to solve main goal *)
- warn "trying reflexivity ....";
- EqualityTactics.reflexivity_tac status'
- with (Fail _) -> (* leave conclusion to the user *)
- warn "reflexivity failed, solution's left as an ex :-)";
- purge_hyps_tac ~count:!new_hyps status')]
- in
- status'')]
- with (Fail s) ->
- raise (Fail ("Ring failure: " ^ 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 "goal unringable")
-
projects / helm.git / blobdiff