1 (* ======================================================================================== *)
2 (* Proof-objects for HOL-light, exportation to Coq *)
4 (* Steven Obua, TU Mnchen, December 2004 *)
5 (* Chantal Keller, Laboratoire d'Informatique de Polytechnique (France), January 2010 *)
7 (* based on Sebastian Skalberg's HOL4 proof-objects *)
8 (* ======================================================================================== *)
11 #load "depgraph.cma";;
14 module type Proofobject_primitives =
19 val proof_REFL : term -> proof
20 val proof_TRANS : proof * proof -> proof
21 val proof_MK_COMB : proof * proof -> proof
22 val proof_ASSUME : term -> proof
23 val proof_EQ_MP : proof -> proof -> proof
24 val proof_IMPAS : proof -> proof -> proof
25 val proof_DISCH : proof -> term -> proof
26 val proof_DEDUCT_ANTISYM_RULE : proof * term -> proof * term -> proof
27 val proof_BETA : term -> proof
28 val proof_ABS : term -> proof -> proof
29 val proof_INST_TYPE : (hol_type * hol_type) list -> proof -> proof
30 val proof_INST : (term * term) list -> proof -> proof
31 val proof_new_definition : string -> hol_type -> term -> proof
32 val proof_CONJ : proof -> proof -> proof
33 val proof_CONJUNCT1 : proof -> proof
34 val proof_CONJUNCT2 : proof -> proof
35 val proof_new_basic_type_definition :
36 string -> string * string -> term * term -> proof -> proof
37 val proof_SPEC : term -> proof -> proof
38 val proof_SYM : proof -> proof
39 val proof_GEN : proof -> term -> proof
40 val proof_DISJ1 : proof -> term -> proof
41 val proof_DISJ2 : proof -> term -> proof
42 val proof_NOTI : proof -> proof
43 val proof_NOTE : proof -> proof
44 val proof_CONTR : proof -> term -> proof
45 val proof_DISJCASES : proof -> proof -> proof -> proof
46 val proof_CHOOSE : term -> proof -> proof -> proof
47 val proof_EXISTS : term -> term -> proof -> proof
49 val new_axiom_name : string -> string
50 val proof_new_axiom : string -> term -> proof
52 val save_proof : string -> proof -> (term option) -> unit
53 val proof_database : unit -> ((string * proof * (term option)) list)
55 val export_saved_proofs : unit -> unit
56 val export_one_proof : string -> unit
57 val export_list : string list -> unit
61 module Proofobjects : Proofobject_primitives = struct
64 let THEORY_NAME = "hollight";;
68 (****** Utilities ******)
70 (* this is a little bit dangerous, because the function is not injective,
71 but I guess one can live with that *)
74 | "\\" -> "_backslash_"
76 | ">" -> "_greaterthan_"
78 | "?" -> "_questionmark_"
79 | "!" -> "_exclamationmark_"
94 let mfc s = implode (map modify (explode s));;
96 let ensure_export_directory thyname =
97 let dir = Sys.getenv "HOLPROOFEXPORTDIR" in
98 let dirsub = Filename.concat dir "hollight" in
99 let dirsubsub = Filename.concat dirsub thyname in
100 let mk d = if Sys.file_exists d then () else Unix.mkdir d 509
101 in mk dir; mk dirsub; mk dirsubsub; dirsubsub;;
104 (****** Proofs ******)
106 type proof_info_rec =
107 {disk_info: (string * string) option ref;
112 type proof_info = Info of proof_info_rec;;
115 | Proof of (proof_info * proof_content * (unit -> unit))
118 | Pbeta of string * hol_type * term
119 | Pinstt of proof * (string * hol_type) list
120 | Pabs of proof * string * hol_type
121 | Pdisch of proof * term
123 | Pspec of proof * term
124 | Pinst of proof * (string * hol_type * term) list
125 | Pgen of proof * string * hol_type
127 | Ptrans of proof * proof
128 | Pcomb of proof * proof
129 | Peqmp of proof * proof
130 | Pexists of proof * term * term
131 | Pchoose of string * hol_type * proof * proof
132 | Pconj of proof * proof
133 | Pconjunct1 of proof
134 | Pconjunct2 of proof
135 | Pdisj1 of proof * term
136 | Pdisj2 of proof * term
137 | Pdisjcases of proof * proof * proof
140 | Pcontr of proof * term
141 | Pimpas of proof * proof
142 | Paxm of string * term
143 | Pdef of string * hol_type * term
144 | Ptyintro of hol_type * string * hol_type list * string * string * term;;
146 let content_of (Proof (_,p,_)) = p;;
148 let inc_references (Proof(Info{references=r},_,_) as p) = incr r; p;;
150 let mk_proof p = Proof(Info {disk_info = ref None; status = ref 0; references = ref 0; queued = ref false}, p, fun () -> ());;
152 let global_ax_counter = let counter = ref 1 in let f = fun () -> (incr counter; !counter - 1) in f;;
154 let new_axiom_name n = "ax_"^n^"_"^(string_of_int (global_ax_counter () ));;
157 (* corresponds to REFL *)
159 let proof_REFL t = mk_proof (Prefl t);;
162 (* corresponds to TRANS, with a simple improvment *)
164 let proof_TRANS (p,q) =
165 match (content_of p, content_of q) with
168 | _ -> mk_proof (Ptrans (inc_references p, inc_references q));;
171 (* corresponds to MK_COMB -> Pcomb *)
173 let proof_MK_COMB (p1,p2) =
174 match (content_of p1, content_of p2) with
175 | (Prefl tm1, Prefl tm2) -> mk_proof (Prefl (mk_comb (tm1, tm2)))
176 | _ -> mk_proof (Pcomb (inc_references p1, inc_references p2));;
179 (* corresponds to ASSUME -> Phyp *)
181 let proof_ASSUME t = mk_proof (Phyp t);;
184 (* corresponds to EQ_MP, with a simple improvment *)
186 let proof_EQ_MP p q =
187 match content_of p with
189 | _ -> mk_proof (Peqmp(inc_references p, inc_references q));;
192 (* corresponds to IMP_ANTISYM_RULE th1 th2
194 used only in the extended mode *)
196 (* A1 |- t1 ==> t2 A2 |- t2 ==> t1 *)
197 (* ------------------------------------- IMP_ANTISYM_RULE *)
198 (* A1 u A2 |- t1 <=> t2 *)
200 let proof_IMPAS p1 p2 = mk_proof (Pimpas (inc_references p1, inc_references p2));;
203 (* corresponds to DISCH
205 used only in the extended mode *)
208 (* -------------------- DISCH `u` *)
209 (* A - {u} |- u ==> t *)
211 let proof_DISCH p t = mk_proof (Pdisch(inc_references p, t));;
214 (* corresponds to DEDUCT_ANTISYM_RULE *)
215 (* made with IMPAS and DISCH (whereas in HOL-Light IMPAS is made with DAR and UNDISCH...) *)
218 (* ---------------------------------- *)
219 (* (A - {q}) u (B - {p}) |- p <=> q *)
221 let proof_DEDUCT_ANTISYM_RULE (p1,t1) (p2,t2) =
222 proof_IMPAS (proof_DISCH p1 t2) (proof_DISCH p2 t1);;
225 (* BETA is a base rule *)
229 let f,_ = dest_comb tm in
230 let v,bod = dest_abs f in
231 let (x, ty) = dest_var v in
232 mk_proof (Pbeta (x, ty, bod))
234 | _ -> failwith "proof_BETA"
237 (* corresponds to ABS, with a simple improvment *)
242 mk_proof (Pabs(inc_references p, s, ty))
243 | _ -> failwith "proof_ABS: not a variable";;
246 (* corresponds to INST_TYPE -> Pinstt *)
248 let proof_INST_TYPE s p =
249 mk_proof (Pinstt(inc_references p, List.map (
250 fun (ty1, ty2) -> match ty2 with
251 | Tyvar s -> (s, ty1)
252 | _ -> failwith "proof_INST_TYPE: some redex is not a type variable"
256 (* corresponds to INST *)
259 mk_proof (Pinst(inc_references p, List.map (
260 fun (t1, t2) -> match t2 with
263 | _ -> failwith "proof_INST: some redex is not a term variable"
267 (* proof_new_definition is called in Thm.new_basic_definition. This
268 latter helps to define basic concepts such as T, AND... (almost
269 everything in Bool)... and to define derived rules!! -> Pdef *)
271 let proof_new_definition cname ty t =
272 mk_proof (Pdef (cname, ty, t));;
275 (* proof_new_axiom is called in Thm.new_axiom. This latter transforms
276 a term of type bool into a theorem. The main three axioms are
277 ETA_AX, SELECT_AX and INFINITY_AX. The other axiom is ax (in
280 let proof_new_axiom axname t = mk_proof (Paxm (axname, t));;
283 (* corresponds to CONJ
285 used only in the extended mode *)
287 let proof_CONJ p1 p2 = mk_proof (Pconj (inc_references p1, inc_references p2));;
290 (* corresponds to CONJUNCT1
292 used only in the extended mode
293 also used in Thm.new_basic_definition *)
295 let proof_CONJUNCT1 p = mk_proof (Pconjunct1 (inc_references p));;
298 (* corresponds to CONJUNCT2
300 used only in the extended mode
301 also used in Thm.new_basic_definition *)
303 let proof_CONJUNCT2 p = mk_proof (Pconjunct2 (inc_references p));;
306 (* used only in Thm.new_basic_definition for the same purpose as for
307 CONJUNCTi -> Ptyintro *)
309 let proof_new_basic_type_definition tyname (absname, repname) (pt,tt) _ =
310 let rty = type_of tt in
311 let tyvars = sort (<=) (type_vars_in_term pt) in
313 mk_proof(Ptyintro(rty, tyname, tyvars, absname, repname, pt));;
316 (* ---- used only in substitute_proof calls ---- *)
318 (* corresponds to Bool.SPEC, the !-elimination rule *)
320 let proof_SPEC s p = mk_proof (Pspec(inc_references p, s));;
323 (* corresponds to Equal.SYM, the symmetry rule *)
325 let proof_SYM p = mk_proof (Psym(inc_references p));;
328 (* corresponds to Bool.GEN, the !-introduction rule *)
333 mk_proof (Pgen(inc_references p, s, ty))
334 | _ -> failwith "proof_GEN: not a term variable";;
337 (* corresponds to Bool.DISJ1, the \/-left introduction rule *)
339 let proof_DISJ1 p a = mk_proof (Pdisj1 (inc_references p, a));;
342 (* corresponds to Bool.DISJ2, the \/-right introduction rule *)
344 let proof_DISJ2 p a = mk_proof (Pdisj2 (inc_references p, a));;
347 (* corresponds to Bool.NOT_INTRO, the following rule: *)
349 (* -------------- NOT_INTRO *)
352 let proof_NOTI p = mk_proof (Pnoti (inc_references p));;
355 (* corresponds to Bool.NOT_ELIM, the following rule: *)
357 (* -------------- NOT_ELIM *)
360 let proof_NOTE p = mk_proof (Pnote (inc_references p));;
363 (* corresponds to Bool.CONTR, the intuitionistic F-elimination rule: *)
365 (* -------- CONTR `t` *)
368 let proof_CONTR p a = mk_proof (Pcontr (inc_references p, a));;
371 (* corresponds to Bool.DISJ_CASES, the \/-elimination rule: *)
372 (* A |- t1 \/ t2 A1 u {t1} |- t A2 u {t2} |- t *)
373 (* ------------------------------------------------------ DISJ_CASES *)
374 (* A u A1 u A2 |- t *)
376 let proof_DISJCASES p q r =
377 mk_proof (Pdisjcases (inc_references p, inc_references q, inc_references r));;
380 (* corresponds to Bool.CHOOSE, the ?-elimination rule: *)
381 (* A1 |- ?x. s[x] A2 |- t *)
382 (* ------------------------------- CHOOSE (`v`,(A1 |- ?x. s)) *)
383 (* A1 u (A2 - {s[v/x]}) |- t *)
384 (* Where v is not free in A2 - {s[v/x]} or t. *)
386 let proof_CHOOSE a p q =
387 let (x,ty) = dest_var a in
388 mk_proof (Pchoose (x, ty, inc_references p, inc_references q));;
391 (* corresponds to Bool.EXISTS, the ?-introduction rule: *)
393 (* ------------- EXISTS (`?x. p`,`u`) *)
397 let proof_EXISTS etm y p =
398 let _,x = dest_comb etm in
399 mk_proof (Pexists (inc_references p, x, y));;
402 (****** Utilities for exportation ******)
404 let content_of (Proof (_,x,_)) = x;;
407 let disk_info_of (Proof(Info {disk_info=di},_,_)) = !di;;
410 let set_disk_info_of (Proof(Info {disk_info=di},_,_)) thyname thmname =
411 di := Some (thyname,thmname);;
413 let reset_disk_info_of1 ((Proof(Info {disk_info=di}, _, _)) as p) =
415 let reset_disk_info_of2 (Proof(Info {disk_info=di}, _, _)) =
419 let references (Proof (Info info,_,_)) = !(info.references);;
422 let glob_counter = ref 0;;
425 let get_counter () = incr glob_counter; !glob_counter;;
428 let get_iname = string_of_int o get_counter;;
431 let next_counter () = !glob_counter;;
435 match (content_of p) with
443 let do_share p = references p > 1 & not (trivial p);;
446 (****** Types and terms modification ******)
448 let idT = Hashtbl.create 17;;
449 let defT = Hashtbl.create 17;;
451 let idT_ref = ref 1;;
452 let defT_ref = ref 1;;
455 try Hashtbl.find idT x with | Not_found -> let n = !idT_ref in incr idT_ref; Hashtbl.add idT x n; n;;
458 try Hashtbl.find defT x with | Not_found -> let n = !defT_ref in incr defT_ref; Hashtbl.add defT x n; n;;
465 | Narrow of ntype * ntype
466 | Ntdef of int * ntype list;;
469 let rec hol_type2ntype = function
470 | Tyvar x -> Ntvar (make_idT x)
471 | Tyapp (s, _) when s = "bool" -> Nbool
472 (* | Tyapp (s, _) when s = "ind" -> Nnum *)
473 | Tyapp (s, l) when s = "fun" ->
475 | [a;b] -> Narrow (hol_type2ntype a, hol_type2ntype b)
476 | _ -> failwith "hol_type2ntype: wrong number of arguments for fun")
477 | Tyapp (s, l) -> Ntdef (make_defT s, List.map hol_type2ntype l);;
480 let idV = Hashtbl.create 17;;
481 let defV = Hashtbl.create 17;;
483 let idV_ref = ref 1;;
484 let defV_ref = ref 1;;
488 fst (Hashtbl.find idV x)
490 let n = !idV_ref in incr idV_ref; Hashtbl.add idV x (n,X); n;;
492 let make_defV x X f =
493 try let (a,_,_) = (Hashtbl.find defV x) in a with | Not_found -> let n = !defV_ref in incr defV_ref; Hashtbl.add defV x (n,X,f); n;;
511 | Nvar of int * ntype
513 | Ndef of int * ntype
514 | Napp of nterm * nterm
515 | Nabs of ntype * nterm;;
518 let rec ext_var x (ty: ntype) i = function
519 | [] -> Nvar (make_idV x ty, ty)
520 | (y,typ)::l -> if ((x = y) && (ty = typ)) then Ndbr i else ext_var x ty (i+1) l;;
523 let rec term2nterm l = function
524 | Var (x, ty) -> ext_var x (hol_type2ntype ty) 0 l
525 | Comb (t1, t2) -> Napp (term2nterm l t1, term2nterm l t2)
529 let typ = hol_type2ntype ty in
530 Nabs (typ, term2nterm ((x,typ)::l) t2)
531 | _ -> failwith "term2nterm: first argument of an abstraction is not a variable")
532 | Const (s, ty) when s = "=" ->
533 (match hol_type2ntype ty with
534 | Narrow(a, _) -> Ncst (Heq a)
535 | _ -> failwith "term2nterm: constant = must have arrow type")
536 | Const (s, ty) when s = "@" ->
537 (match hol_type2ntype ty with
538 | Narrow(_, a) -> Ncst (Heps a)
539 | _ -> failwith "term2nterm: constant @ must have arrow type")
540 | Const (s, ty) when s = "/\\" -> Ncst Hand
541 | Const (s, ty) when s = "\\/" -> Ncst Hor
542 | Const (s, ty) when s = "~" -> Ncst Hnot
543 | Const (s, ty) when s = "==>" -> Ncst Himp
544 | Const (s, ty) when s = "T" -> Ncst Htrue
545 | Const (s, ty) when s = "F" -> Ncst Hfalse
546 | Const (s, ty) when s = "_FALSITY_" -> Ncst Hfalse
547 | Const (s, ty) when s = "!" ->
548 (match hol_type2ntype ty with
549 | Narrow(Narrow (a, _), _) -> Ncst (Hforall a)
550 | _ -> failwith "term2nterm: constant ! must have arrow type")
551 | Const (s, ty) when s = "?" ->
552 (match hol_type2ntype ty with
553 | Narrow(Narrow (a, _), _) -> Ncst (Hexists a)
554 | _ -> failwith "term2nterm: constant ? must have arrow type")
556 let typ = hol_type2ntype ty in
557 Ndef(make_defV s typ true, typ);;
559 let term2nterm t = term2nterm [] t;;
562 (****** Proof exportation ******)
564 let rec print_list out str snil scons = function
566 | t::q -> out "("; out scons; out " "; str t; out " "; print_list out str snil scons q; out ")";;
569 let print_names out x = out (string_of_int x); out "%positive";;
572 let print_type (out: string -> unit) ty =
574 let rec print_ntype = function
575 | Ntvar x -> out "(TVar "; print_names out x; out ")"
576 | Nbool -> out "Bool"
578 | Narrow(a, b) -> out "("; print_ntype a; out " --> "; print_ntype b; out ")"
579 | Ntdef(s, l) -> out "(TDef "; print_names out s; out " "; print_list out print_ntype "Tnil" "Tcons" l; out ")" in
584 let print_cst out = function
585 | Heq ty -> out "(Heq "; print_type out ty; out ")"
586 | Heps ty -> out "(Heps "; print_type out ty; out ")"
591 | Htrue -> out "Htrue"
592 | Hfalse -> out "Hfalse"
593 | Hforall ty -> out "(Hforall "; print_type out ty; out ")"
594 | Hexists ty -> out "(Hexists "; print_type out ty; out ")";;
597 let print_term out t =
599 let rec print_nterm = function
600 | Ndbr n -> out "(Dbr "; out (string_of_int n); out ")"
601 | Nvar(x, ty) -> out "(Var "; print_names out x; out " "; print_type out ty; out ")"
602 | Ncst c -> out "(Cst "; print_cst out c; out ")"
603 | Ndef(a, ty) -> out "(Def "; print_names out a; out " "; print_type out ty; out ")"
604 | Napp(t1, t2) -> out "(App "; print_nterm t1; out " "; print_nterm t2; out ")"
605 | Nabs(ty, t) -> out "(Abs "; print_type out ty; out " "; print_nterm t; out ")" in
614 type nproof_content =
616 | Npbeta of int * ntype * nterm
617 | Npinstt of nproof_content * (int * ntype) list
618 | Npabs of nproof_content * int * ntype
619 | Npdisch of nproof_content * nterm
621 | Npspec of nproof_content * nterm
622 | Npinst of nproof_content * (int * ntype * nterm) list
623 | Npgen of nproof_content * int * ntype
624 | Npsym of nproof_content
625 | Nptrans of nproof_content * nproof_content
626 | Npcomb of nproof_content * nproof_content
627 | Npeqmp of nproof_content * nproof_content
628 | Npexists of nproof_content * nterm * nterm
629 | Npchoose of int * ntype * nproof_content * nproof_content
630 | Npconj of nproof_content * nproof_content
631 | Npconjunct1 of nproof_content
632 | Npconjunct2 of nproof_content
633 | Npdisj1 of nproof_content * nterm
634 | Npdisj2 of nproof_content * nterm
635 | Npdisjcases of nproof_content * nproof_content * nproof_content
636 | Npnoti of nproof_content
637 | Npnote of nproof_content
638 | Npcontr of nproof_content * nterm
639 | Npimpas of nproof_content * nproof_content
640 | Npaxm of string * nterm
641 | Npdef of int * ntype * nterm
642 | Nptyintro of ntype * ntype * int * int * nterm
646 let the_types = Hashtbl.create 17;;
647 let count_types = ref (-1);;
649 let share_types out ty =
651 let rec share_types ty =
652 try Hashtbl.find the_types ty with
655 let name = THEORY_NAME^"_type_"^(string_of_int !count_types) in
658 let n1 = share_types a in
659 let n2 = share_types b in
660 out "\nDefinition "; out name; out " := "; out n1; out " --> "; out n2; out "."
662 let names = List.map share_types l in
663 out "\nDefinition "; out name; out " := TDef "; print_names out i; out " "; print_list out out "Tnil" "Tcons" names; out "."
664 | t -> out "\nDefinition "; out name; out " := "; print_type out t; out ".");
665 Hashtbl.add the_types ty name;
671 let the_terms = Hashtbl.create 17;;
672 let count_terms = ref (-1);;
674 let share_csts out out_types name = function
676 let n = share_types out_types a in
677 out "\nDefinition "; out name; out " := Cst (Heq "; out n; out ")."
679 let n = share_types out_types a in
680 out "\nDefinition "; out name; out " := Cst (Heps "; out n; out ")."
681 | Hand -> out "\nDefinition "; out name; out " := Cst Hand."
682 | Hor -> out "\nDefinition "; out name; out " := Cst Hor."
683 | Hnot -> out "\nDefinition "; out name; out " := Cst Hnot."
684 | Himp -> out "\nDefinition "; out name; out " := Cst Himp."
685 | Htrue -> out "\nDefinition "; out name; out " := Cst Htrue."
686 | Hfalse -> out "\nDefinition "; out name; out " := Cst Hfalse."
688 let n = share_types out_types a in
689 out "\nDefinition "; out name; out " := Cst (Hforall "; out n; out ")."
691 let n = share_types out_types a in
692 out "\nDefinition "; out name; out " := Cst (Hexists "; out n; out ")."
694 let share_terms out out_types tm =
696 let rec share_terms tm =
697 try Hashtbl.find the_terms tm with
700 let name = THEORY_NAME^"_term_"^(string_of_int !count_terms) in
703 let n1 = share_terms t1 in
704 let n2 = share_terms t2 in
705 out "\nDefinition "; out name; out " := App "; out n1; out " "; out n2; out "."
707 let n = share_terms t in
708 let ny = share_types out_types ty in
709 out "\nDefinition "; out name; out " := Abs "; out ny; out " "; out n; out "."
711 let ny = share_types out_types ty in
712 out "\nDefinition "; out name; out " := Var "; print_names out i; out " "; out ny; out "."
714 let ny = share_types out_types ty in
715 out "\nDefinition "; out name; out " := Def "; print_names out i; out " "; out ny; out "."
716 | Ncst c -> share_csts out out_types name c
717 | t -> out "\nDefinition "; out name; out " := "; print_term out t; out ".");
718 Hashtbl.add the_terms tm name;
724 let export_proof out share_type share_term p =
726 let rec wp = function
728 let tm2 = share_term tm in
729 out "(Prefl "; out tm2; out ")"
730 | Npbeta (n, ty, tm) ->
731 let tm2 = share_term tm in
732 let ty2 = share_type ty in
733 out "(Pbeta "; print_names out n; out " "; out ty2; out " "; out tm2; out ")"
734 | Npinstt(p,lambda) ->
737 out " "; print_list out (fun (s, ty) ->
738 let ty2 = share_type ty in
739 out "("; print_names out s; out ", "; out ty2; out ")") "nil" "cons" lambda; out ")"
741 let ty2 = share_type ty in
744 out " "; print_names out x;
745 out " "; out ty2; out ")"
747 let tm2 = share_term tm in
750 out " "; out tm2; out ")"
752 let tm2 = share_term tm in
753 out "(Phyp "; out tm2; out ")"
755 | Npdef(_, _, _) -> ()
756 | Nptyintro(_, _, _, _, _) -> ()
758 let t2 = share_term t in
761 out " "; out t2; out ")"
765 out " "; print_list out (fun (s, ty, t) ->
766 let t2 = share_term t in
767 let ty2 = share_type ty in
768 out "("; print_names out s; out ", "; out ty2; out ", "; out t2; out ")") "nil" "cons" theta; out ")"
770 let ty2 = share_type ty in
773 out " "; print_names out x; out " "; out ty2; out ")"
796 | Npexists(p,ex,w) ->
797 let ex2 = share_term ex in
798 let w2 = share_term w in
801 out " "; out ex2; out " "; out w2; out ")"
802 | Npchoose(x,ty,p1,p2) ->
803 let ty2 = share_type ty in
804 out "(Pchoose "; print_names out x; out " "; out ty2; out " ";
830 let tm2 = share_term tm in
833 out " "; out tm2; out ")"
835 let tm2 = share_term tm in
838 out " "; out tm2; out ")"
839 | Npdisjcases(p1,p2,p3) ->
856 let tm2 = share_term tm in
859 out " "; out tm2; out ")"
860 | Nfact(thm) -> out "(Poracle "; out thm; out "_def)" in
865 let export_ht out share_term h t thmname =
866 out "\n\n\nDefinition "; out thmname; out "_h := ";
868 | [] -> out "hyp_empty"
869 | _ -> print_list out (fun tm ->
870 let tm2 = share_term tm in
871 out tm2) "nil" "cons" h);
872 out ".\n\nDefinition "; out thmname; out "_t := ";
873 let t2 = share_term t in
877 let export_lemma out share_type share_term p thmname =
878 out "\n\nLemma "; out thmname; out "_lemma : deriv "; out thmname; out "_h "; out thmname;
879 out "_t.\nProof.\n vm_cast_no_check (proof2deriv_correct "; export_proof out share_type share_term p; out ").\nQed.";;
882 let export_lemma_def out tree thmname =
883 out "\n\nLemma "; out thmname; out "_lemma : deriv "; out thmname; out "_h "; out thmname;
884 out "_t.\nProof.\n vm_cast_no_check (proof2deriv_correct "; out tree; out ").\nQed.";;
887 let export_sig out thmname =
888 out "\n\nDefinition "; out thmname; out "_def := my_exist "; out thmname; out "_lemma.";;
891 let export_def out thmname =
892 out "\n\nParameter "; out thmname; out "_lemma : deriv "; out thmname; out "_h "; out thmname; out "_t.";;
895 let export_tdef out thmname =
896 out "\n\nParameter "; out thmname; out "_lemma : deriv "; out thmname; out "_h "; out thmname; out "_t.";;
899 let export_axiom out thmname =
900 out "\n\nAxiom "; out thmname; out "_lemma : deriv "; out thmname; out "_h "; out thmname; out "_t.";;
903 (* Transforming a proof into a derivation *)
905 let rec opt_nth n l =
907 | 0, (x::_) -> Some x
909 | p, (_::l) -> opt_nth (p-1) l
913 let type_cst = function
914 | Heq a -> Narrow(a, Narrow(a, Nbool))
915 | Heps a -> Narrow(Narrow(a, Nbool), a)
916 | Hand -> Narrow(Nbool, Narrow(Nbool, Nbool))
917 | Hor -> Narrow(Nbool, Narrow(Nbool, Nbool))
918 | Hnot -> Narrow(Nbool, Nbool)
919 | Himp -> Narrow(Nbool, Narrow(Nbool, Nbool))
922 | Hforall a -> Narrow(Narrow(a, Nbool), Nbool)
923 | Hexists a -> Narrow(Narrow(a, Nbool), Nbool);;
926 let rec infer g = function
927 | Ndbr n -> opt_nth n g
928 | Nvar (_, a) -> Some a
929 | Ncst c -> Some (type_cst c)
930 | Ndef (_, a) -> Some a
932 (match infer g t1, infer g t2 with
933 | Some (Narrow (u1, u2)), Some v -> if u1 = v then Some u2 else None
936 (match infer (a::g) u with
937 | Some b -> Some (Narrow (a, b))
941 let rec close_aux t x a i =
943 | Ndbr n -> Ndbr (if n < i then n else n+1)
944 | Nvar (y, b) -> if ((x = y) && (a = b)) then Ndbr i else Nvar (y, b)
945 | Napp (t1, t2) -> Napp (close_aux t1 x a i, close_aux t2 x a i)
946 | Nabs (b, u) -> Nabs(b, close_aux u x a (i+1))
949 let close t x a = close_aux t x a 0;;
952 let rec subst_idt_type_aux x = function
954 | (y,a)::q -> if x = y then a else subst_idt_type_aux x q;;
956 let rec subst_idt_type t s =
958 | Ntvar x -> subst_idt_type_aux x s
959 | Ntdef (a, l) -> Ntdef (a, subst_idt_list_type l s)
960 | Narrow (a, b) -> Narrow (subst_idt_type a s, subst_idt_type b s)
963 and subst_idt_list_type l s = List.map (fun t -> subst_idt_type t s) l;;
965 let rec subst_idt t s =
967 | Nvar (x, y) -> Nvar (x, subst_idt_type y s)
968 | Ncst (Heq a) -> Ncst (Heq (subst_idt_type a s))
969 | Ncst (Heps a) -> Ncst (Heps (subst_idt_type a s))
970 | Ncst (Hforall a) -> Ncst (Hforall (subst_idt_type a s))
971 | Ncst (Hexists a) -> Ncst (Hexists(subst_idt_type a s))
972 | Ndef (c, d) -> Ndef (c, subst_idt_type d s)
973 | Napp (t1, t2) -> Napp (subst_idt t1 s, subst_idt t2 s)
974 | Nabs (a, t) -> Nabs (subst_idt_type a s, subst_idt t s)
977 let subst_idt_context g s = List.map (fun a -> subst_idt_type a s) g;;
979 let rec subst_idv_aux x y s =
982 | (z, t, u)::q -> if ((x = z) && (y = t)) then u else subst_idv_aux x y q;;
984 let rec subst_idv t s =
986 | Nvar (x, y) -> subst_idv_aux x y s
987 | Napp (t1, t2) -> Napp (subst_idv t1 s, subst_idv t2 s)
988 | Nabs (a, t) -> Nabs (a, subst_idv t s)
991 let rec wf_substitution_idv = function
994 match infer [] t with
995 | Some z -> if (y = z) then wf_substitution_idv q else false
999 let rec is_not_free x y = function
1000 | Nvar (z, t) -> (x != z) or (not (y = t))
1001 | Napp (t1, t2) -> (is_not_free x y t1) && (is_not_free x y t2)
1002 | Nabs (_, u) -> is_not_free x y u
1006 let rec lift_term u i j =
1008 | Ndbr n -> if n >= i then Ndbr (j + n) else Ndbr n
1009 | Napp (u1, u2) -> Napp (lift_term u1 i j, lift_term u2 i j)
1010 | Nabs (a, t) -> Nabs (a, lift_term t (i+1) j)
1013 let rec subst_db t n u =
1015 | Ndbr i -> if i < n then Ndbr i else if i = n then u else Ndbr (i-1)
1016 | Napp (t1, t2) -> Napp (subst_db t1 n u, subst_db t2 n u)
1017 | Nabs (a, t) -> Nabs (a, subst_db t (n+1) (lift_term u 0 1))
1020 let nopen t u = subst_db t 0 u;;
1023 let heq a t u = Napp (Napp (Ncst (Heq a), t), u);;
1024 let hequiv t u = Napp (Napp (Ncst (Heq Nbool), t), u);;
1025 let himp t u = Napp (Napp (Ncst Himp, t), u);;
1026 let hand t u = Napp (Napp (Ncst Hand, t), u);;
1027 let hor t u = Napp (Napp (Ncst Hor, t), u);;
1028 let hnot t = Napp (Ncst Hnot, t);;
1029 let htrue = Ncst Htrue;;
1030 let hfalse = Ncst Hfalse;;
1031 let hforall a p = Napp (Ncst (Hforall a), Nabs (a, p));;
1032 let hexists a p = Napp (Ncst (Hexists a), Nabs (a, p));;
1035 let hyp_empty = [];;
1037 let rec hyp_remove e = function
1039 | t::q -> if (e = t) then q else t::(hyp_remove e q);;
1041 let rec hyp_add e = function
1043 | t::q -> if (e = t) then t::q else t::(hyp_add e q);;
1045 let hyp_union l m = List.fold_left (fun n e -> hyp_add e n) m l;;
1047 let hyp_map f l = List.fold_left (fun m e -> hyp_add (f e) m) [] l;;
1049 let hyp_singl e = [e];;
1051 let rec hyp_is_not_free x y = function
1053 | t::q -> (is_not_free x y t) && (hyp_is_not_free x y q);;
1055 let hyp_subst_idt h s = hyp_map (fun t -> subst_idt t s) h;;
1057 let hyp_subst_idv h s = hyp_map (fun t -> subst_idv t s) h;;
1060 let rec eq_type a b = match (a,b) with
1061 | Ntvar i, Ntvar j -> i = j
1062 | Nbool, Nbool -> true
1063 | Nnum, Nnum -> true
1064 | Narrow(a1, b1), Narrow(a2, b2) -> (eq_type a1 a2) && (eq_type b1 b2)
1065 | Ntdef(i,l), Ntdef(j,m) -> (i = j) && (eq_list_type l m)
1068 and eq_list_type l m = match (l,m) with
1070 | t1::q1, t2::q2 -> (eq_type t1 t2) && (eq_list_type q1 q2)
1074 let eq_cst a b = match (a,b) with
1075 | Heq a, Heq b -> eq_type a b
1076 | Heps a, Heps b -> eq_type a b
1077 | Hand, Hand -> true
1079 | Hnot, Hnot -> true
1080 | Himp, Himp -> true
1081 | Htrue, Htrue -> true
1082 | Hfalse, Hfalse -> true
1083 | Hforall a, Hforall b -> eq_type a b
1084 | Hexists a, Hexists b -> eq_type a b
1088 let rec eq_term a b = match (a,b) with
1089 | Ndbr i, Ndbr j -> i = j
1090 | Nvar(i,a), Nvar(j,b) -> (i = j) && (eq_type a b)
1091 | Ncst c, Ncst d -> eq_cst c d
1092 | Ndef(i,a), Ndef(j,b) -> (i = j) && (eq_type a b)
1093 | Napp(a1,b1), Napp(a2,b2) -> (eq_term a1 a2) && (eq_term b1 b2)
1094 | Nabs(t1,a1), Nabs(t2,a2) -> (eq_type t1 t2) && (eq_term a1 a2)
1098 let derivs = Hashtbl.create 17;;
1101 let rec proof2deriv = function
1104 (match infer [] t with
1105 | Some a -> Some (hyp_empty, heq a t t)
1106 | None -> (print_string "Nprefl\n"); None)
1108 | Npbeta (x, y, t) ->
1109 (match infer [] t with
1110 | Some a -> Some (hyp_empty,
1111 heq a (Napp (Nabs (y, close t x y), Nvar (x, y))) t)
1112 | None -> (print_string "Npbeta\n"); None)
1115 (match proof2deriv q with
1116 | Some (h,v) -> Some (hyp_subst_idt h l, subst_idt v l)
1117 | None -> (print_string "Npinstt\n"); None)
1119 | Npabs (q, x, y) ->
1120 (match proof2deriv q with
1123 | Napp (Napp (Ncst (Heq a), t1), t2) ->
1124 if hyp_is_not_free x y h then
1125 Some (h, heq (Narrow (y, a)) (Nabs (y, close t1 x y)) (Nabs (y, close t2 x y)))
1126 else ((print_string "Npabs\n"); None)
1127 | _ -> (print_string "Npabs\n"); None)
1128 | None -> (print_string "Npabs\n"); None)
1131 (match proof2deriv q, infer [] t with
1132 | Some (h, u), Some Nbool -> Some (hyp_remove t h, himp t u)
1133 | _, _ -> (print_string "Npdisch\n"); None)
1136 (match infer [] t with
1137 | Some Nbool -> Some (hyp_singl t, t)
1138 | _ -> (print_string "Nphyp\n"); None)
1141 (match proof2deriv q, infer [] t with
1142 | Some (h, u), Some a ->
1144 | Napp (Ncst (Hforall b), Nabs (c, v)) ->
1145 if ((eq_type a b) && (eq_type b c)) then
1147 else ((print_string "Npspec\n"); None)
1148 | _ -> (print_string "Npspec\n"); None)
1149 | _, _ -> (print_string "Npspec\n"); None)
1152 (match proof2deriv q, wf_substitution_idv l with
1153 | Some (h, v), true -> Some (hyp_subst_idv h l, subst_idv v l)
1154 | _, _ -> (print_string "Npinst\n"); None)
1156 | Npgen (q, x, y) ->
1157 (match proof2deriv q with
1159 if hyp_is_not_free x y h then
1160 Some (h, hforall y (close t x y))
1161 else ((print_string "Npgen\n"); None)
1162 | None -> (print_string "Npgen\n"); None)
1165 (match proof2deriv q with
1168 | Napp (Napp (Ncst (Heq a), u), v) -> Some (h, heq a v u)
1169 | _ -> (print_string "Npsym\n"); None)
1170 | None -> (print_string "Npsym\n"); None)
1172 | Nptrans (q1, q2) ->
1173 (match proof2deriv q1, proof2deriv q2 with
1174 | Some (h1, t1), Some (h2, t2) ->
1176 | Napp (Napp (Ncst (Heq a), u1), u2),
1177 Napp (Napp (Ncst (Heq b), v2), v3) ->
1178 if ((eq_type a b) && (eq_term u2 v2)) then
1179 Some (hyp_union h1 h2, heq a u1 v3)
1180 else ((print_string "Nptrans\n"); None)
1181 | _, _ -> (print_string "Nptrans\n"); None)
1182 | _, _ -> (print_string "Nptrans\n"); None)
1184 | Npcomb (q1, q2) ->
1185 (match proof2deriv q1, proof2deriv q2 with
1186 | Some (h1, t1), Some (h2, t2) ->
1188 | Napp (Napp (Ncst (Heq (Narrow (a, b))), f), g),
1189 Napp (Napp (Ncst (Heq c), u), v) ->
1190 if (eq_type a c) then
1191 Some (hyp_union h1 h2, heq b (Napp (f, u)) (Napp (g, v)))
1192 else ((print_string "Npcomb\n"); None)
1193 | _, _ -> (print_string "Npcomb\n"); None)
1194 | _, _ -> (print_string "Npcomb\n"); None)
1196 | Npeqmp (q1, q2) ->
1197 (match proof2deriv q1, proof2deriv q2 with
1198 | Some (h1, t1), Some (h2, t2) ->
1200 | Napp (Napp (Ncst (Heq Nbool), a), b) ->
1201 if (eq_term a t2) then
1202 Some (hyp_union h1 h2, b)
1203 else ((print_string "Npeqmp\n"); None)
1204 | _ -> (print_string "Npeqmp\n"); None)
1205 | _, _ -> (print_string "Npeqmp\n"); None)
1207 | Npexists (q, b, t) ->
1208 (match proof2deriv q, b, infer [] t with
1209 | Some (h, u), Nabs (bb, a), Some aa ->
1210 if ((eq_type aa bb) && (eq_term (nopen a t) u)) then
1211 Some (h, hexists aa a)
1212 else ((print_string "Npexists\n"); None)
1213 | _, _, _ -> (print_string "Npexists\n"); None)
1215 | Npchoose (v, aa, q1, q2) ->
1216 (match proof2deriv q1, proof2deriv q2 with
1217 | Some (h1, t), Some (h2, c) ->
1219 | Napp (Ncst (Hexists bb), Nabs (cc, a)) ->
1220 let s = hyp_remove (nopen a (Nvar (v, aa))) h2 in
1221 if ((eq_type aa bb) && (eq_type bb cc) && (hyp_is_not_free v aa s) && (is_not_free v aa c)
1222 && (is_not_free v aa a)) then
1223 Some (hyp_union h1 s, c)
1224 else ((print_string "Npchoose\n"); None)
1225 | _ -> (print_string "Npchoose\n"); None)
1226 | _, _ -> (print_string "Npchoose\n"); None)
1228 | Npconj (q1, q2) ->
1229 (match proof2deriv q1, proof2deriv q2 with
1230 | Some (h1, a), Some (h2, b) ->
1231 Some (hyp_union h1 h2, hand a b)
1232 | _, _ -> (print_string "Npconj\n"); None)
1235 (match proof2deriv q with
1238 | Napp (Napp (Ncst Hand, t), u) ->
1240 | _ -> (print_string "Npconjunct1\n"); None)
1241 | _ -> (print_string "Npconjunct1\n"); None)
1244 (match proof2deriv q with
1247 | Napp (Napp (Ncst Hand, t), u) ->
1249 | _ -> (print_string "Npconjunct2\n"); None)
1250 | _ -> (print_string "Npconjunct2\n"); None)
1253 (match proof2deriv q, infer [] b with
1254 | Some (h, a), Some Nbool -> Some (h, hor a b)
1255 | _, _ -> (print_string "Npdisj1\n"); None)
1258 (match proof2deriv q, infer [] a with
1259 | Some (h, b), Some Nbool -> Some (h, hor a b)
1260 | _, _ -> (print_string "Npdisj1\n"); None)
1262 | Npdisjcases (q1, q2, q3) ->
1263 (match proof2deriv q1, proof2deriv q2, proof2deriv q3 with
1264 | Some (h1, t), Some (h2, c1), Some (h3, c2) ->
1266 | Napp (Napp (Ncst Hor, a), b) ->
1267 if (eq_term c1 c2) then
1268 Some (hyp_union h1 (hyp_union (hyp_remove a h2) (hyp_remove b h3)), c1)
1269 else ((print_string "Npdisjcases\n"); None)
1270 | _ -> (print_string "Npdisjcases\n"); None)
1271 | _, _, _ -> (print_string "Npisjcases\n"); None)
1274 (match proof2deriv q with
1277 | Napp (Napp (Ncst Himp, a), Ncst Hfalse) -> Some (h, hnot a)
1278 | _ -> (print_string "Npnoti\n"); None)
1279 | _ -> (print_string "Npnoti\n"); None)
1282 (match proof2deriv q with
1285 | Napp (Ncst Hnot, a) -> Some (h, himp a hfalse)
1286 | _ -> (print_string "Npnote\n"); None)
1287 | _ -> (print_string "Npnote\n"); None)
1290 (match proof2deriv q, infer [] a with
1291 | Some (h, t), Some Nbool ->
1293 | Ncst Hfalse -> Some (hyp_remove (hnot a) h, a)
1294 | _ -> (print_string "Npcontr\n"); None)
1295 | _, _ -> (print_string "Npcontr\n"); None)
1297 | Npimpas (q1, q2) ->
1298 (match proof2deriv q1, proof2deriv q2 with
1299 | Some (h1, t), Some (h2, u) ->
1301 | Napp (Napp (Ncst Himp, a1), b1),
1302 Napp (Napp (Ncst Himp, b2), a2) ->
1303 if ((eq_term a1 a2) && (eq_term b1 b2)) then
1304 Some (hyp_union h1 h2, hequiv b1 a1)
1305 else ((print_string ("Npimpas1; 1: "^(string_of_bool (eq_term a1 a2))^"; 2: "^(string_of_bool (eq_term b1 b2))^"\n"));
1306 let out = print_string in
1307 print_term out a1; out "\n"; print_term out a2; out "\n"; print_term out b1; out "\n"; print_term out b2; out "\n"; None)
1308 | _, _ -> (print_string "Npimpas2\n"); None)
1309 | _, _ -> (print_string "Npimpas3\n"); None)
1312 (try Some (Hashtbl.find derivs thm) with
1313 | Not_found -> (print_string ("Nfact "^thm^"\n")); None)
1315 | Npdef (i, a, t) -> Some (hyp_empty, heq a (Ndef (i, a)) t)
1317 | Npaxm (_, t) -> Some (hyp_empty, t)
1319 | Nptyintro (rty, aty, mk_name, dest_name, p) ->
1321 let mk_type = Narrow(rty, aty) in
1322 let dest_type = Narrow(aty, rty) in
1324 let a_name = make_idV "a" aty in
1325 let a = Nvar(a_name, aty) in
1326 let r_name = make_idV "r" rty in
1327 let r = Nvar(r_name, rty) in
1329 Some (hyp_empty, hand (heq aty (Napp (Ndef (mk_name, mk_type), Napp (Ndef (dest_name, dest_type), a))) a)
1330 (hequiv (Napp (p, r)) (heq rty (Napp (Ndef (dest_name, dest_type), Napp (Ndef (mk_name, mk_type), r))) r)));;
1333 (* Dealing with dependencies *)
1335 let rec make_dependencies_aux dep_graph proof_of_thm = function
1337 | (thmname, p, c_opt)::il ->
1342 Depgraph.Dep.add_dep dep_graph thm thmname;
1345 let write_proof p il =
1347 let rec share_info_of p il =
1348 match (disk_info_of p) with
1349 | Some (thyname,thmname) -> Some(thyname,thmname,il)
1352 let name = THEORY_NAME^"_"^(get_iname ()) in
1353 set_disk_info_of p THEORY_NAME name;
1354 Depgraph.Dep.add_thm dep_graph name;
1355 Some(THEORY_NAME,name,(name,p,None)::il)
1359 and wp' il = function
1360 | Prefl tm -> Nprefl (term2nterm tm), il
1361 | Pbeta(x, ty, tm) ->
1362 let typ = hol_type2ntype ty in
1363 Npbeta(make_idV x typ , typ, term2nterm tm), il
1364 | Pinstt(p,lambda) ->
1365 let p', res = wp il p in
1366 Npinstt(p', List.map (
1367 fun (s,ty) -> (make_idT s, hol_type2ntype ty)
1370 let p', res = wp il p in
1371 let typ = hol_type2ntype ty in
1372 Npabs(p',make_idV x typ,typ), res
1374 let p', res = wp il p in
1375 Npdisch(p', term2nterm tm), res
1376 | Phyp tm -> Nphyp (term2nterm tm), il
1377 | Paxm(th,tm) -> Npaxm(th, term2nterm tm), il
1378 | Pdef(name,ty,tm) ->
1379 let typ = hol_type2ntype ty in
1380 Npdef(make_defV name typ true, typ, term2nterm tm), il
1381 | Ptyintro(rty2, tyname, tyvars, absname, repname, pt) ->
1382 let rty = hol_type2ntype rty2 in
1383 let new_name = make_defT tyname in
1385 let ntyvars = List.map hol_type2ntype tyvars in
1386 let aty = Ntdef(new_name, ntyvars) in
1388 let mk_name = make_defV absname (Narrow(rty, aty)) false in
1389 let dest_name = make_defV repname (Narrow(aty, rty)) false in
1391 Nptyintro(rty, aty, mk_name, dest_name, term2nterm pt), il
1393 let p', res = wp il p in
1394 Npspec(p', term2nterm t), res
1396 let p', res = wp il p in
1397 Npinst(p', List.map (
1399 let typ = hol_type2ntype ty in
1400 (make_idV s typ, typ, term2nterm te)
1403 let p', res = wp il p in
1404 let typ = hol_type2ntype ty in
1405 Npgen(p', make_idV x typ, typ), res
1407 let p', res = wp il p in
1410 let p1', il' = wp il p1 in
1411 let p2', res = wp il' p2 in
1412 Nptrans(p1', p2'), res
1414 let p1', il' = wp il p1 in
1415 let p2', res = wp il' p2 in
1416 Npcomb(p1', p2'), res
1418 let p1', il' = wp il p1 in
1419 let p2', res = wp il' p2 in
1420 Npeqmp(p1', p2'), res
1421 | Pexists(p,ex,w) ->
1422 let p', res = wp il p in
1423 Npexists(p', term2nterm ex, term2nterm w), res
1424 | Pchoose(x,ty,p1,p2) ->
1425 let p1', il' = wp il p1 in
1426 let p2', res = wp il' p2 in
1427 let typ = hol_type2ntype ty in
1428 Npchoose(make_idV x typ, typ, p1', p2'), res
1430 let p1', il' = wp il p1 in
1431 let p2', res = wp il' p2 in
1432 Npconj(p1', p2'), res
1434 let p1', il' = wp il p1 in
1435 let p2', res = wp il' p2 in
1436 Npimpas(p1', p2'), res
1438 let p', res = wp il p in
1441 let p', res = wp il p in
1444 let p', res = wp il p in
1445 Npdisj1(p', term2nterm tm), res
1447 let p', res = wp il p in
1448 Npdisj2(p', term2nterm tm), res
1449 | Pdisjcases(p1,p2,p3) ->
1450 let p1', il' = wp il p1 in
1451 let p2', il'' = wp il' p2 in
1452 let p3', res = wp il'' p3 in
1453 Npdisjcases(p1', p2', p3'), res
1455 let p', res = wp il p in
1458 let p', res = wp il p in
1461 let p', res = wp il p in
1462 Npcontr(p', term2nterm tm), res
1465 match share_info_of p il with
1466 | Some(_, thmname, il') -> wdi thmname, il'
1467 | None -> wp' il (content_of p) in
1469 match disk_info_of p with
1470 | Some(_, thmname') -> if thmname' = thmname then wp' il (content_of p) else (wdi thmname', il)
1471 | None -> wp' il (content_of p) in
1473 let p', il = write_proof p il in
1474 set_disk_info_of p THEORY_NAME thmname;
1475 Hashtbl.add proof_of_thm thmname p';
1476 make_dependencies_aux dep_graph proof_of_thm il;;
1479 let make_dependencies out out_share out_sharet new_file count_thms path ((thmname, pr, _) as p) =
1481 let dep_graph = Depgraph.Dep.create () in
1482 let proof_of_thm = Hashtbl.create (references pr) in
1483 Depgraph.Dep.add_thm dep_graph thmname;
1485 make_dependencies_aux dep_graph proof_of_thm [p];
1487 let share_type ty = share_types out_sharet ty in
1488 let share_term ty = share_terms out_share out_sharet ty in
1491 if thmname = (THEORY_NAME^"_DEF_T") then (
1492 match content_of pr with
1494 let tm = hequiv htrue (term2nterm t) in
1495 Hashtbl.add derivs thmname (hyp_empty, tm);
1496 export_ht out share_term hyp_empty tm thmname;
1497 export_lemma_def out "DEF_T" thmname;
1498 export_sig out thmname
1500 ) else if thmname = (THEORY_NAME^"_DEF__slash__backslash_") then (
1501 match content_of pr with
1503 let tm = heq (Narrow (Nbool, Narrow (Nbool, Nbool))) (Ncst Hand) (term2nterm t) in
1504 Hashtbl.add derivs thmname (hyp_empty, tm);
1505 export_ht out share_term hyp_empty tm thmname;
1506 export_lemma_def out "DEF_AND" thmname;
1507 export_sig out thmname
1509 ) else if thmname = (THEORY_NAME^"_DEF__equal__equal__greaterthan_") then (
1510 match content_of pr with
1512 let tm = heq (Narrow (Nbool, Narrow (Nbool, Nbool))) (Ncst Himp) (term2nterm t) in
1513 Hashtbl.add derivs thmname (hyp_empty, tm);
1514 export_ht out share_term hyp_empty tm thmname;
1515 export_lemma_def out "DEF_IMP" thmname;
1516 export_sig out thmname
1518 ) else if thmname = (THEORY_NAME^"_DEF__exclamationmark_") then (
1519 match content_of pr with
1521 let a2 = hol_type2ntype a in
1523 | Narrow (Narrow (b, _), _) ->
1524 let tm = heq a2 (Ncst (Hforall b)) (term2nterm t) in
1525 Hashtbl.add derivs thmname (hyp_empty, tm);
1526 export_ht out share_term hyp_empty tm thmname;
1527 export_lemma_def out "DEF_FORALL" thmname;
1528 export_sig out thmname
1531 ) else if thmname = (THEORY_NAME^"_DEF__questionmark_") then (
1532 match content_of pr with
1534 let a2 = hol_type2ntype a in
1536 | Narrow (Narrow (b, _), _) ->
1537 let tm = heq a2 (Ncst (Hexists b)) (term2nterm t) in
1538 Hashtbl.add derivs thmname (hyp_empty, tm);
1539 export_ht out share_term hyp_empty tm thmname;
1540 export_lemma_def out "DEF_EXISTS" thmname;
1541 export_sig out thmname
1544 ) else if thmname = (THEORY_NAME^"_DEF__backslash__slash_") then (
1545 match content_of pr with
1547 let tm = heq (Narrow (Nbool, Narrow (Nbool, Nbool))) (Ncst Hor) (term2nterm t) in
1548 Hashtbl.add derivs thmname (hyp_empty, tm);
1549 export_ht out share_term hyp_empty tm thmname;
1550 export_lemma_def out "DEF_OR" thmname;
1551 export_sig out thmname
1553 ) else if thmname = (THEORY_NAME^"_DEF_F") then (
1554 match content_of pr with
1556 let tm = hequiv (Ncst Hfalse) (term2nterm t) in
1557 Hashtbl.add derivs thmname (hyp_empty, tm);
1558 export_ht out share_term hyp_empty tm thmname;
1559 export_lemma_def out "DEF_F" thmname;
1560 export_sig out thmname
1562 ) else if thmname = (THEORY_NAME^"_DEF__tilde_") then (
1563 match content_of pr with
1565 let tm = heq (Narrow (Nbool, Nbool)) (Ncst Hnot) (term2nterm t) in
1566 Hashtbl.add derivs thmname (hyp_empty, tm);
1567 export_ht out share_term hyp_empty tm thmname;
1568 export_lemma_def out "DEF_NOT" thmname;
1569 export_sig out thmname
1571 ) else if thmname = (THEORY_NAME^"_DEF__FALSITY_") then (
1572 let tm = heq Nbool (Ncst Hfalse) (Ncst Hfalse) in
1573 Hashtbl.add derivs thmname (hyp_empty, tm);
1574 export_ht out share_term hyp_empty tm thmname;
1575 export_lemma_def out "(Prefl (Cst Hfalse))" thmname;
1576 export_sig out thmname
1577 ) else if thmname = (THEORY_NAME^"_ax__1") then (
1578 match content_of pr with
1580 let tm2 = term2nterm tm in
1581 Hashtbl.add derivs thmname (hyp_empty, tm2);
1582 export_ht out share_term hyp_empty tm2 thmname;
1583 export_lemma_def out "ETA_AX" thmname;
1584 export_sig out thmname
1586 ) else if thmname = (THEORY_NAME^"_ax__2") then (
1587 match content_of pr with
1589 let tm2 = term2nterm tm in
1590 Hashtbl.add derivs thmname (hyp_empty, tm2);
1591 export_ht out share_term hyp_empty tm2 thmname;
1592 export_lemma_def out "SELECT_AX" thmname;
1593 export_sig out thmname
1598 Depgraph.Dep_top.iter_top (
1601 if !count_thms = 1000 then (count_thms := 0; new_file ());
1603 let p = Hashtbl.find proof_of_thm thm in
1604 (match proof2deriv p with
1606 Hashtbl.add derivs thm (h, t);
1607 export_ht out share_term h t thm;
1609 | Npdef _ -> export_def out thm
1610 | Nptyintro _ -> export_tdef out thm
1611 | Npaxm _ -> export_axiom out thm
1612 | _ -> export_lemma out share_type share_term p thm);
1614 | None -> failwith ("Erreur make_dependencies "^thm^" de "^thmname^": no derivation associated to the proof\n"))
1615 with | Not_found -> failwith ("Erreur make_dependencies "^thm^": proof_of_thm not found\n"));
1621 let the_proof_database = ref ([]:(string*proof*(term option)) list);;
1625 let rec search_proof_name n db =
1626 match db with [] -> n | ((m, _, _)::db') -> if n=m then n^"_"^(string_of_int (Random.int 1073741823)) else search_proof_name n db'
1628 let save_proof name p c_opt =
1629 let name' = search_proof_name name (!the_proof_database) in
1630 the_proof_database := (name', p, c_opt)::(!the_proof_database);;
1632 let proof_database () = !the_proof_database;;
1635 (* Utilities to define Coq interpretation functions *)
1637 let ut = Hashtbl.create 17;;
1641 let filein = Pervasives.open_in "interpretation.txt" in
1647 let s1 = input_line filein in
1649 let s2 = input_line filein in
1650 Hashtbl.add ut s1 s2
1653 | End_of_file -> close_in filein
1654 | _ -> failwith ("Error line "^(string_of_int !line)^".")
1655 ) with | Sys_error _ -> ()
1658 let tc_regexp = Str.regexp "\?[0-9]*";;
1660 let make_tc_parameter out x n =
1661 if Str.string_match tc_regexp x 0 then (
1662 let i = Str.match_end () in
1663 if i <> String.length x then (
1664 out "\nParameter "; out THEORY_NAME; out "_idT_"; out (mfc x); out " : Type.\nParameter "; out THEORY_NAME; out "_idT_inhab_"; out (mfc x);
1665 out " : "; out THEORY_NAME; out "_idT_"; out (mfc x); out "."
1668 out "\nParameter "; out THEORY_NAME; out "_idT_"; out (mfc x); out " : Type.\nParameter "; out THEORY_NAME; out "_idT_inhab_"; out (mfc x);
1669 out " : "; out THEORY_NAME; out "_idT_"; out (mfc x); out "."
1672 let make_tc_list out x n =
1673 if Str.string_match tc_regexp x 0 then (
1674 let i = Str.match_end () in
1675 if i <> String.length x then (
1676 out "\n("; out (string_of_int n); out ", mkTT "; out THEORY_NAME; out "_idT_inhab_"; out (mfc x); out ")::"
1679 out "\n("; out (string_of_int n); out ", mkTT "; out THEORY_NAME; out "_idT_inhab_"; out (mfc x); out ")::"
1683 let defT_ut = Hashtbl.create 17;;
1685 let make_tdt_parameter out x _ =
1687 let y = Hashtbl.find ut x in
1688 Hashtbl.add defT_ut x y
1689 ) with | Not_found -> (
1690 out "\nParameter "; out THEORY_NAME; out "_defT_"; out (mfc x); out " : Type.";
1691 out "\nParameter "; out THEORY_NAME; out "_defT_inhab_"; out (mfc x); out " : "; out THEORY_NAME; out "_defT_"; out (mfc x); out ".\n";
1692 Hashtbl.add defT_ut x ("fun _ => mkTT "^THEORY_NAME^"_defT_inhab_"^(mfc x))
1695 let make_tdt_list out x n =
1697 let s = Hashtbl.find defT_ut x in
1698 out "\n("; out (string_of_int n); out ", "; out s; out ")::";
1699 ) with | Not_found -> (
1700 out "\n("; out (string_of_int n); out ", fun _ => mkTT tt)::"
1704 let se_regexp = Str.regexp "_[0-9]*";;
1706 let make_se_parameter out x (_,ty) =
1707 if Str.string_match se_regexp x 0 then (
1708 let i = Str.match_end () in
1709 if i <> String.length x then (
1710 out "\nParameter "; out THEORY_NAME; out "_idV_"; out (mfc x); out " : tr_type tc tdt "; print_type out ty; out "."
1713 out "\nParameter "; out THEORY_NAME; out "_idV_"; out (mfc x); out " : tr_type tc tdt "; print_type out ty; out "."
1716 let make_se_list out x (n,ty) =
1717 if Str.string_match se_regexp x 0 then (
1718 let i = Str.match_end () in
1719 if i <> String.length x then (
1720 out "\n("; print_names out n; out ", existT (fun (t: type) => tr_type tc tdt t) "; print_type out ty; out " "; out THEORY_NAME; out "_idV_"; out (mfc x); out ")::"
1723 out "\n("; print_names out n; out ", existT (fun (t: type) => tr_type tc tdt t) "; print_type out ty; out " "; out THEORY_NAME; out "_idV_"; out (mfc x); out ")::"
1727 let defV_ut = Hashtbl.create 17;;
1729 let make_sdt_parameter out x (_,ty,_) =
1730 if ((x <> "T") && (x <> "/\\") && (x <> "==>") && (x <> "!") && (x <> "?") && (x <> "\\/") && (x <> "F") && (x <> "~") && (x <> "_FALSITY_")) then (
1732 let y = Hashtbl.find ut x in
1733 Hashtbl.add defV_ut x y
1734 ) with | Not_found -> (
1735 out "\nParameter "; out THEORY_NAME; out "_defV_"; out (mfc x); out " : tr_type tc tdt "; print_type out ty; out "."
1739 let make_sdt_list out x (n,ty,_) =
1741 let s = Hashtbl.find defV_ut x in
1742 out "\n("; print_names out n; out ", existT (fun (t: type) => tr_type tc tdt t) "; print_type out ty; out " ("; out s; out "))::"
1743 ) with | Not_found -> (
1744 if ((x <> "T") && (x <> "/\\") && (x <> "==>") && (x <> "!") && (x <> "?") && (x <> "\\/") && (x <> "F") && (x <> "~") && (x <> "_FALSITY_")) then (
1745 out "\n("; print_names out n; out ", existT (fun (t: type) => tr_type tc tdt t) "; print_type out ty; out " "; out THEORY_NAME; out "_defV_"; out (mfc x); out ")::"
1750 (* Main function: list of proofs exportation *)
1752 let export_list thmname_list =
1756 let path = ensure_export_directory THEORY_NAME in
1759 let rec proof_of_thm acc acc2 = function
1762 if List.mem s thmname_list then
1763 proof_of_thm ((THEORY_NAME^"_"^(mfc s), reset_disk_info_of1 p, c)::acc) (acc2+1) q
1764 else match content_of p with
1765 | Paxm _ | Pdef _ | Ptyintro _ -> proof_of_thm ((THEORY_NAME^"_"^(mfc s), reset_disk_info_of1 p, c)::acc) (acc2+1) q
1766 | _ -> proof_of_thm acc acc2 q in
1768 let l, total_thms = proof_of_thm [] 0 (proof_database ()) in
1771 let count_thms = ref 0 in
1772 let count_files = ref 1 in
1776 let file = ref (open_out (Filename.concat path (THEORY_NAME^"_1.v"))) in
1777 let count_file = ref 0 in
1778 let out s = (output_string !file s; incr count_file; if !count_file = 1000 then (count_file := 0; flush !file)) in
1779 out "(*** This file has been automatically generated from HOL-Light source files. ***)\n\nRequire Export List NArith.\nRequire Export hol deriv proof.\n\n";
1781 (* Temporary file *)
1783 let (file_temp_name, file_temp_aux) = Filename.open_temp_file (THEORY_NAME^"_") ".v" in
1784 let file_temp = ref file_temp_aux in
1785 let count_file_temp = ref 0 in
1786 let out_temp s = (output_string !file_temp s; incr count_file_temp; if !count_file_temp = 1000 then (count_file_temp := 0; flush !file_temp)) in
1791 close_out !file_temp
1792 with | Sys_error s -> raise (Sys_error ("move_temp1: "^s)));
1795 let buf = Pervasives.open_in file_temp_name in
1799 let l = input_line buf in
1802 with | End_of_file -> close_in buf)
1803 with | Sys_error s -> raise (Sys_error ("move_temp3: "^s))) in
1811 file_temp := open_out file_temp_name;
1815 file := open_out (Filename.concat path (THEORY_NAME^"_"^(string_of_int !count_files)^".v"));
1816 out "(*** This file has been automatically generated from HOL-Light source files. ***)\n\nRequire Export "; out THEORY_NAME; out "_"; out (string_of_int (!count_files-1)); out ".\n\n" in
1819 (* Coq files generation *)
1821 let date1 = Unix.time () in
1822 List.iter (make_dependencies out_temp out out new_file count_thms path) l;
1823 let date2 = Unix.time () in
1826 move_temp (); close_out !file;
1831 let make = open_out (Filename.concat path "Makefile") in
1832 let out = output_string make in
1833 out "# This file has been automatically generated from HOL-Light source files.\n\nCOQ=ssrcoq\nFLAGS=-dont-load-proofs -dump-glob /dev/null -compile\n\nSRC=";
1834 for i = 1 to !count_files do
1835 out " "; out THEORY_NAME; out "_"; out (string_of_int i); out ".v";
1837 out "\nOBJ=$(SRC:.v=.vo)\nGLOB=$(SRC:.v=.glob)\n\n\nall: $(OBJ)\n\n\n%.vo: %.v\n\t$(COQ) $(FLAGS) $(^:.v=)\n\n\nclean:\n\trm -f $(OBJ) $(GLOB) *~";
1841 (* Interpretation *)
1843 let interp = open_out (Filename.concat path "interpretation.v") in
1844 let out = output_string interp in
1845 out "(*** This file has been automatically generated from HOL-Light source files. ***)\n\nRequire Import ssreflect eqtype ssrnat ssrbool.\nRequire Import List NArith ZArith.ZOdiv_def.\nRequire Import hol cast typing translation axioms.\n\nOpen Local Scope positive_scope.\n\n";
1850 Hashtbl.iter (make_tc_parameter out) idT;
1851 out "\n\nDefinition tc_list :=";
1852 Hashtbl.iter (make_tc_list out) idT;
1853 out "\nnil.\n\nDefinition tc := list_tc2tc tc_list.\n\n";
1856 Hashtbl.iter (make_tdt_parameter out) defT;
1857 out "\n\nDefinition tdt_list : list_tdt :=";
1858 Hashtbl.iter (make_tdt_list out) defT;
1859 out "\nnil.\n\nDefinition tdt := list_tdt2tdt tdt_list.\n\n";
1862 Hashtbl.iter (make_se_parameter out) idV;
1863 out "\n\nDefinition se_list :=";
1864 Hashtbl.iter (make_se_list out) idV;
1865 out "\nnil.\n\nDefinition se := list_se2se se_list.\n\n";
1868 Hashtbl.iter (make_sdt_parameter out) defV;
1869 out "\n\nDefinition sdt_list :=";
1870 Hashtbl.iter (make_sdt_list out) defV;
1871 out "\nnil.\n\nDefinition sdt := list_sdt2sdt sdt_list.";
1876 print_string "Generated "; print_int !total; print_string " facts for "; print_int total_thms; print_string " theorems.\n";
1877 print_string "Exportation duration: "; print_float (date2 -. date1); print_string "s.\n"
1881 (* Main function: all proofs exportation *)
1883 let export_saved_proofs () = export_list (List.map (fun (s,_,_) -> s) (proof_database ()));;
1886 (* Main function: one proof exportation *)
1888 let export_one_proof name = export_list [name];;
1894 include Proofobjects;;