From 9e5abfcf937cb4fa85387cbd2b6503c2bf21a32c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 27 Apr 2006 10:07:47 +0000 Subject: [PATCH] Equality chains. -This line, and those below, will be ignored-- M acic_content/acic2content.ml --- components/acic_content/acic2content.ml | 61 +++++++++++++++++++++++++ 1 file changed, 61 insertions(+) diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml index 57b8502bb..e72d466d5 100644 --- a/components/acic_content/acic2content.ml +++ b/components/acic_content/acic2content.ml @@ -505,6 +505,9 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = 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 @@ -843,8 +846,66 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = } 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) = -- 2.39.2