open ProofEngineTypes
open UriManager
-open HelmLibraryObjects
-
(** DEBUGGING *)
(** perform debugging output? *)
*)
let ringable =
let is_equality = function
- | Cic.MutInd (uri, 0, []) when (eq uri Logic.eq_URI) -> true
+ | Cic.MutInd (uri, 0, []) when (eq uri HelmLibraryObjects.Logic.eq_URI) -> true
| _ -> false
in
let is_real = function
- | Cic.Const (uri, _) when (eq uri Reals.r_URI) -> true
+ | Cic.Const (uri, _) when (eq uri HelmLibraryObjects.Reals.r_URI) -> true
| _ -> false
in
function
@return a cic term representing the variable map containing vars variables
*)
let btree_of_array ~vars =
- let r = Reals.r in
+ 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 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) -> (* +. *)
+ 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 Reals.rmult_URI) bop) -> (* *. *)
+ 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 Reals.ropp_URI) uop) -> (* ~-. *)
+ 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 Reals.r0_URI) t) -> (* 0. *)
+ | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r0_URI) t) -> (* 0. *)
mkCtor ap0_uri []
- | t when (cic_is_const ~uri:(Some Reals.r1_URI) t) -> (* 1. *)
+ | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r1_URI) t) -> (* 1. *)
mkCtor ap1_uri []
| t -> (* variable *)
try
*)
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_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, 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_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 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))
+ 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 *)
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]
+ Cic.Appl [apolynomial_normalize_ok lxy_false varmap HelmLibraryObjects.Reals.rtheory ; t]
) aterms
@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 "in Ring.elim_type2";
ProofEngineTypes.apply_tactic
- (Tacticals.thens ~start:(E.elim_type_tac ~term)
+ (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)
match (n, context) with
| (0, _) -> status
| (n, hd::tl) ->
- aux (n-1) tl
- (status_of_single_goal_tactic_result
- (ProofEngineTypes.apply_tactic (S.clear ~hyp:hd) status))
+ 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 ~hyp:name_of_hyp) status))
| (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
let (_, metasenv, _, _) = proof in
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 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 *)
try
let new_hyps = ref 0 in (* number of new hypotheses created *)
ProofEngineTypes.apply_tactic
- (Tacticals.try_tactics
+ (Tacticals.first
~tactics:[
"reflexivity", EqualityTactics.reflexivity_tac ;
"exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
"exact sym_eqt su t1 ...", exact_tac
~term:(
Cic.Appl
- [mkConst Logic.sym_eq_URI
- [equality_is_a_congruence_A, Reals.r;
+ [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
] ;
in
let status'' =
ProofEngineTypes.apply_tactic
- (Tacticals.try_tactics (* try to solve 1st subgoal *)
+ (Tacticals.first (* try to solve 1st subgoal *)
~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;
+ [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
] ;
projects / helm.git / blobdiff