let premise_prefix = "prem:";;
let lemma_prefix = "lemma:";;
+let hide_coercions = ref true;;
+
(* e se mettessi la conversione di BY nell'apply_context ? *)
(* sarebbe carino avere l'invariante che la proof2pres
generasse sempre prove con contesto vuoto *)
generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
else raise Not_a_proof
| C.AAppl (id,li) ->
- (try rewrite
+ (try coercion
+ seed li ~ids_to_inner_types ~ids_to_inner_sorts
+ with NotApplicable ->
+ try rewrite
seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
try inductive
seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
+ with NotApplicable ->
+ try transitivity
+ seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
let subproofs, args =
build_subproofs_and_args
}
| _ -> raise NotApplicable
+and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
+ match li with
+ | ((Cic.AConst _) as he)::tl
+ | ((Cic.AMutInd _) as he)::tl
+ | ((Cic.AMutConstruct _) as he)::tl when
+ CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
+ !hide_coercions ->
+ let rec last =
+ function
+ [] -> assert false
+ | [t] -> t
+ | _::tl -> last tl
+ in
+ acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+ | _ -> raise NotApplicable
+
and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
let module C2A = Cic2acic in
}
else raise NotApplicable
| _ -> raise NotApplicable
+
+and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
+ let module C2A = Cic2acic in
+ let module K = Content in
+ let module C = Cic in
+ match li with
+ | C.AConst (sid,uri,exp_named_subst)::args
+ when LibraryObjects.is_trans_eq_URI uri ->
+ let exp_args = List.map snd exp_named_subst in
+ let t1,t2,t3,p1,p2 =
+ match exp_args@args with
+ | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
+ | _ -> raise NotApplicable
+ in
+ { K.proof_name = name;
+ K.proof_id = gen_id proof_prefix seed;
+ K.proof_context = [];
+ K.proof_apply_context = [];
+ K.proof_conclude =
+ { K.conclude_id = gen_id conclude_prefix seed;
+ K.conclude_aref = id;
+ K.conclude_method = "Eq_chain";
+ K.conclude_args =
+ K.Term t1::
+ (transitivity_aux
+ seed ~ids_to_inner_types ~ids_to_inner_sorts p1)@
+ [K.Term t2]@
+ (transitivity_aux
+ seed ~ids_to_inner_types ~ids_to_inner_sorts p2)@
+ [K.Term t3];
+ K.conclude_conclusion =
+ try Some
+ (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+ with Not_found -> None
+ }
+ }
+ | _ -> raise NotApplicable
+
+and transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts t =
+ let module C2A = Cic2acic in
+ let module K = Content in
+ let module C = Cic in
+ match t with
+ | C.AAppl (_,C.AConst (sid,uri,exp_named_subst)::args)
+ when LibraryObjects.is_trans_eq_URI uri ->
+ let exp_args = List.map snd exp_named_subst in
+ let t1,t2,t3,p1,p2 =
+ match exp_args@args with
+ | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
+ | _ -> raise NotApplicable
+ in
+ (transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p1)
+ @[K.Term t2]
+ @(transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p2)
+ | _ -> [K.ArgProof
+ (acic2content seed ~ids_to_inner_sorts ~ids_to_inner_types t)]
+
;;
+
let map_conjectures
seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
=