diff -urN coq-8.0pl4/config/Makefile.template coq-8.0pl4.papuq/config/Makefile.template --- coq-8.0pl4/config/Makefile.template 2006-01-10 18:06:23.000000000 +0100 +++ coq-8.0pl4.papuq/config/Makefile.template 2007-04-01 15:45:01.000000000 +0200 @@ -96,7 +96,7 @@ # Unix systems and profiling: true # Unix systems and no profiling: strip # Win32 systems: true (actually strip is bogus) -STRIP=STRIPCOMMAND +STRIP=true # Options for reals (all/basic) REALS=REALSOPT diff -urN coq-8.0pl4/.depend coq-8.0pl4.papuq/.depend --- coq-8.0pl4/.depend 2006-02-25 00:39:55.000000000 +0100 +++ coq-8.0pl4.papuq/.depend 2007-04-01 15:45:01.000000000 +0200 @@ -496,14 +496,26 @@ ide/coq.cmi ide/coq_tactics.cmo: ide/coq_tactics.cmi ide/coq_tactics.cmx: ide/coq_tactics.cmi +ide/localization.cmo: ide/localization.cmi +ide/localization.cmx: ide/localization.cmi +ide/teachcfg.cmo: ide/teachcfg.cmi +ide/teachcfg.cmx: ide/teachcfg.cmi +ide/teachdebug.cmo: ide/teachdebug.cmi +ide/teachdebug.cmx: ide/teachdebug.cmi +ide/teachutils.cmo: ide/teachcfg.cmo ide/teachcfg.cmi ide/teachdebug.cmi ide/teachutils.cmi +ide/teachutils.cmx: ide/teachcfg.cmo ide/teachcfg.cmi ide/teachdebug.cmi ide/teachutils.cmi +ide/teachhint.cmo: ide/teachhint.cmi ide/localization.cmo ide/teachcfg.cmo ide/teachutils.cmo +ide/teachhint.cmx: ide/teachhint.cmi ide/localization.cmx ide/teachcfg.cmx ide/teachutils.cmx +ide/teaching.cmo: ide/coq.cmo ide/teachhint.cmo ide/teaching.cmi +ide/teaching.cmx: ide/coq.cmx ide/teachhint.cmx ide/teaching.cmi ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \ lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \ ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \ - ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi + ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi ide/teaching.cmo ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \ lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \ ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \ - ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi + ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi ide/teaching.cmx ide/find_phrase.cmo: ide/ideutils.cmi ide/find_phrase.cmx: ide/ideutils.cmx ide/highlight.cmo: ide/ideutils.cmi diff -urN coq-8.0pl4/ide/coqide.ml coq-8.0pl4.papuq/ide/coqide.ml --- coq-8.0pl4/ide/coqide.ml 2006-11-08 19:41:04.000000000 +0100 +++ coq-8.0pl4.papuq/ide/coqide.ml 2007-04-01 15:45:01.000000000 +0200 @@ -16,6 +16,11 @@ let out_some s = match s with | None -> failwith "Internal error in out_some" | Some f -> f +let invoke_if_any function_ref () = + match !function_ref with + | None -> () + | Some f -> f ();; + let cb_ = ref None let cb () = ((out_some !cb_):GData.clipboard) let last_cb_content = ref "" @@ -252,7 +257,7 @@ if Mutex.try_lock coq_computing then begin - prerr_endline ("Launching thread " ^ text); + (* prerr_endline ("Launching thread " ^ text); *) let w = Blaster_window.blaster_window () in if not (Mutex.try_lock w#lock) then begin break (); @@ -267,11 +272,11 @@ Glib.Timeout.add ~ms:300 ~callback:(fun () -> async !pulse ();true) in begin - prerr_endline "Getting lock"; + (* prerr_endline "Getting lock"; *) try f x; Glib.Timeout.remove idle; - prerr_endline "Releasing lock"; + (* prerr_endline "Releasing lock"; *) Mutex.unlock coq_computing; with e -> Glib.Timeout.remove idle; @@ -569,6 +574,11 @@ msg +let external_goal_handler : (unit -> unit) option ref = ref None;; +let external_wizard_start : (unit -> unit) option ref = ref None;; +let external_undo_handler : (unit -> unit) option ref = ref None;; +let external_redo_handler : (unit -> unit) option ref = ref None;; + class analyzed_view index = let {view = input_view_} as current_all_ = get_input_view index in let proof_view_ = out_some !proof_view in @@ -785,11 +795,12 @@ ~iter:current_line_start (String.make previous_line_spaces ' ') end - - + method private as_analyzed_view = (self :> analyzed_view) method show_goals = try proof_view#buffer#set_text ""; + (* invoke additional function if defined *) + invoke_if_any external_goal_handler (); let s = Coq.get_current_goals () in match s with | [] -> proof_buffer#insert (Coq.print_no_goal ()) @@ -865,7 +876,8 @@ (factory#add_item cp ~callback: (fun () -> ignore - (self#insert_this_phrase_on_success + (invoke_if_any external_redo_handler (); + self#insert_this_phrase_on_success true true false @@ -884,18 +896,18 @@ ~start:proof_buffer#start_iter ~stop:proof_buffer#end_iter last_shown_area; - prerr_endline "Before find_tag_limits"; + (* prerr_endline "Before find_tag_limits"; *) let s,e = find_tag_limits tag (new GText.iter it) in - prerr_endline "After find_tag_limits"; + (* prerr_endline "After find_tag_limits"; *) proof_buffer#apply_tag ~start:s ~stop:e last_shown_area; - prerr_endline "Applied tag"; + (* prerr_endline "Applied tag"; *) () | _ -> () end;false @@ -940,6 +952,16 @@ with e -> prerr_endline (Printexc.to_string e) end + (** + Makes coq process given 'phrase'. + @param verbosely - decides if show whole proof on EndProof + @param replace - unfolds executed command (adds "info " and + shows whole output) + @param phrase - coq command to execute + @param show_output - decides if show coq's output on success + @param show_error - decides if show coq's output on error + @param localize - translates error messages + *) method send_to_coq verbosely replace phrase show_output show_error localize = let display_output msg = self#insert_message (if show_output then msg else "") in @@ -1058,6 +1080,7 @@ method process_next_phrase verbosely display_goals do_highlight = + let _ = invoke_if_any external_redo_handler () in let get_next_phrase () = self#clear_message; prerr_endline "process_next_phrase starting now"; @@ -1110,7 +1133,13 @@ | Some ast -> sync (mark_processed loc) ast; true | None -> sync remove_tag loc; false) end - + + (** + Tries executing 'coqphrase'. On success 'inputphrase' + is inserted in currently edited script. Parameters + 'show_output', 'show_msg', 'localize' are the same as + for method send_to_coq + *) method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase = let mark_processed ast = @@ -1127,30 +1156,9 @@ let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in push_phrase start_of_phrase_mark end_of_phrase_mark ast; self#show_goals; - (*Auto insert save on success... - try (match Coq.get_current_goals () with - | [] -> - (match self#send_to_coq "Save.\n" true true true with - | Some ast -> - begin - let stop = self#get_start_of_input in - if stop#starts_line then - input_buffer#insert ~iter:stop "Save.\n" - else input_buffer#insert ~iter:stop "\nSave.\n"; - let start = self#get_start_of_input in - input_buffer#move_mark ~where:stop (`NAME "start_of_input"); - input_buffer#apply_tag_by_name "processed" ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - input_buffer#place_cursor stop; - let start_of_phrase_mark = - `MARK (input_buffer#create_mark start) in - let end_of_phrase_mark = - `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast - end - | None -> ()) - | _ -> ()) - with _ -> ()*) in + (* removed unnecessary code *) + in + flush stdout; match self#send_to_coq false false coqphrase show_output show_msg localize with | Some ast -> sync mark_processed ast; true | None -> @@ -1187,6 +1195,7 @@ self#process_until_iter_or_error input_buffer#end_iter method reset_initial = + invoke_if_any external_undo_handler (); sync (fun _ -> Stack.iter (function inf -> @@ -1277,12 +1286,14 @@ else prerr_endline "backtrack_to : discarded (lock is busy)" method go_to_insert = + invoke_if_any external_undo_handler (); let point = self#get_insert in if point#compare self#get_start_of_input>=0 then self#process_until_iter_or_error point else self#backtrack_to point method undo_last_step = + invoke_if_any external_undo_handler (); if Mutex.try_lock coq_may_stop then (!push_info "Undoing last step..."; (try @@ -2860,7 +2871,14 @@ ~key:GdkKeysyms._F12 *) ~callback:(Command_windows.command_window ())#window#present - in + in + (* begin JSA *) + let wizard_show_m = + configuration_factory#add_item + "Show _Wizard Window" + ~callback:(invoke_if_any external_wizard_start) + in + (* end JSA *) let toolbar_show_m = configuration_factory#add_item "Show/Hide _Toolbar" @@ -3331,7 +3349,10 @@ ;; -let start () = + +let ext_thread : Thread.t option ref = ref None;; + +let old_prepare () = let files = Coq.init () in ignore_break (); GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc"); @@ -3348,7 +3369,11 @@ (fun ~level msg -> failwith ("Coqide internal error: " ^ msg))); Command_windows.main (); Blaster_window.main 9; - main files; + main files;; + +let old_start () = + Thread.delay 2.0; (* wait 4 sec, stub for debug version *) + old_prepare (); while true do try GtkThread.main () @@ -3358,5 +3383,14 @@ Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e)); flush stderr; crash_save 127 - done + done;; +let ext_start_thread () = + ext_thread := Some (Thread.create old_start ());; + +let ext_stop_thread () = + Thread.kill (out_some !ext_thread);; + +let start () = + ext_start_thread (); (* start Coqide in separate thread *) + Coqtop.start();; (* and Coqtop in main *) diff -urN coq-8.0pl4/ide/coqide.mli coq-8.0pl4.papuq/ide/coqide.mli --- coq-8.0pl4/ide/coqide.mli 2005-01-21 18:21:33.000000000 +0100 +++ coq-8.0pl4.papuq/ide/coqide.mli 2007-04-01 15:45:02.000000000 +0200 @@ -12,5 +12,288 @@ command line, initialize the load path, load the input state, load the files given on the command line, load the ressource file, produce the output state if any, and finally will launch the interface. *) - val start : unit -> unit + +(* + * Return contents of option. + * + * Throws if empty. + *) +val out_some : 'a option -> 'a + +(* + * Tabs (aka pages) handling functions + *) +val decompose_tab : 'a Gobject.obj -> GPack.box * GMisc.image * GMisc.label +val set_tab_label : int -> string -> unit +val set_tab_image : icon:GtkStock.id -> int -> unit +val set_current_tab_image : icon:GtkStock.id -> unit +val set_current_tab_label : string -> unit +val get_tab_label : int -> string +val get_full_tab_label : int -> GMisc.label +val get_current_tab_label : unit -> string +val get_current_page : unit -> GObj.widget +val reset_tab_label : int -> unit + +(* + * Handler invoked on each page change + *) +val to_do_on_page_switch : (int->unit) list ref +type 'a viewable_script = { + view : Undo.undoable_view; + mutable analyzed_view : 'a option; + } +class type analyzed_views = + object ('a) + (* activates window - make it response to events*) + method activate : unit -> unit + (* detach window from events *) + method deactivate : unit -> unit + + (* handlers for active/unactive window *) + method active_keypress_handler : GdkEvent.Key.t -> bool + method disconnected_keypress_handler : GdkEvent.Key.t -> bool + + + (* save script *) + method auto_save : unit + + (* undoing script progress *) + method backtrack_to : GText.iter -> unit + method backtrack_to_no_lock : GText.iter -> unit + + (* activates blaster - CoqIDE automatic solver *) + method blaster : unit -> unit + + (* clear contents of message window *) + method clear_message : unit + + + (* name of last save, None means unnamed yet *) + method filename : string option + (* setter *) + method set_filename : string option -> unit + + (* true if scripting is active *) + method is_active : bool + + (* TEXT MANIPULATION METHODS *) + (* interphace for find *) + method find_phrase_starting_at : + GText.iter -> (GText.iter * GText.iter) option + (* returns iterator at current cursor position *) + method get_insert : GText.iter + (* returns beginning of script *) + method get_start_of_input : GText.iter + (* makes an indentation *) + method indent_current_line : unit + + (* message window with help *) + method help_for_keyword : unit -> unit + + (* adds given message to message window *) + method insert_message : string -> unit + method insert_this_phrase_on_success : + bool -> bool -> bool -> string -> string -> bool + (* shortcut for insert_this_phrase_on_success *) + method insert_command : string -> string -> unit + + (* true if buffer is read only *) + method read_only : bool + (* changes read only flag *) + method set_read_only : bool -> unit + + (* undo whole scripting *) + method reset_initial : unit + (* undo whole scripting, revert file contents from last save *) + method revert : unit + (* file save methods *) + method save : string -> bool + method save_as : string -> bool + + (* process one step *) + method process_next_phrase : bool -> bool -> bool -> bool + (* process whole buffer *) + method process_until_end_or_error : unit + (* process to given iter *) + method process_until_iter_or_error : GText.iter -> unit + (* process until current cursor *) + method go_to_insert : unit + (* + * Makes coq process given 'phrase'. + * verbosely - decides if show whole proof on EndProof + * replace - unfolds executed command (adds "info " and + * shows whole output) + * phrase - coq command to execute + * show_output - decides if show coq's output on success + * show_error - decides if show coq's output on error + * localize - translates error messages + *) + method send_to_coq : + bool -> + bool -> + string -> + bool -> bool -> bool -> (Util.loc * Vernacexpr.vernac_expr) option + + (* put message into message bar *) + method set_message : string -> unit + (* called to redisplay goals generated by Coq *) + method show_goals : unit + (* file stats to check modification time *) + method stats : Unix.stats option + (* obtains stats from file *) + method update_stats : unit + (* simple try tactic wizard + * tries each given tactic (progress) + * it is inserted on success + *) + method tactic_wizard : string list -> unit + (* back one script step *) + method undo_last_step : unit + + (* wrapper - disables 'auto_complete?' for invoked function *) + method without_auto_complete : ('b -> 'c) -> 'b -> 'c + + (* UNKNOWN METHODS *) + + method set_auto_complete : bool -> unit + method complete_at_offset : int -> bool + method add_detached_view : GWindow.window -> unit + method kill_detached_views : unit -> unit + method remove_detached_view : GWindow.window -> unit + method recenter_insert : unit + method show_goals_full : unit + method view : Undo.undoable_view + + (* unused??? *) + method electric_handler : GtkSignal.id + + end + +(* + * Defines signal which will be handled + * by crash_save + *) +val signals_to_crash : int list + +(* + * Saves copies of all scripts, then crash. + *) +val crash_save : int -> unit + +(* + * Disables CTRL-C signal + *) +val ignore_break : unit -> unit + +(* + * Stops current Coq computations. Thread safe. + *) +val break : unit -> unit + +(* + * Note for following lines: + * each script can be active or not + * at most one script can be active + * exaclty one script is being displayed (active or not) + *) + +(* + * Adds new page. + * + * Return: + * its number + *) +val add_input_view : analyzed_views viewable_script -> int + +(* + * Returns given page + * + * Parameters: + * int - number of page + *) +val get_input_view : int -> analyzed_views viewable_script + +(* + * Return object representing current active + * CoqIDE's page (the one with active script). + * + *) +val get_active_view : unit -> analyzed_views viewable_script + +(* + * Switch active script view. + *) +val set_active_view : int -> unit + +(* + * Switch view page. + *) +val set_current_view : int -> unit + +(* + * Removes view from pages. + *) +val kill_input_view : int -> unit + +(* + * Return number of displayed view + *) +val get_current_view_page : unit -> int + +(* + * Return currently displayed view + *) +val get_current_view : unit -> analyzed_views viewable_script + +(* + * Removes current view from pages. + * Same as kill_input_view (get_current_view_page ()) + *) +val remove_current_view_page : unit -> unit + +(* + * Activates nth tab as input + *) +val activate_input : int -> unit +(* + * Shows warning MessageBox + *) +val warning : string -> unit + +(* + * Regexp for picking errors from Coq's error messages + *) +val search_compile_error_regexp : Str.regexp +(* + * Errors iterator (for Coq's output) + *) +val search_next_error : unit -> string * int * int * int * string + +(* + * Original prepare and start functions. Now called from separate thread. + *) +val old_prepare : unit -> unit +val old_start : unit -> unit + +(* + * Starts new CoqIDE thread. + *) +val ext_start_thread : unit -> unit + +(* + * Stops running thread + *) +val ext_stop_thread : unit -> unit + +(* + * Allows to set handlers for CoqIDE events such as: + * - getting new goal + * - clicking Menu->Window->ShowWizard + * - undoing script moves + * - redoing script moves + *) +val external_goal_handler : (unit -> unit) option ref +val external_wizard_start : (unit -> unit) option ref +val external_undo_handler : (unit -> unit) option ref +val external_redo_handler : (unit -> unit) option ref diff -urN coq-8.0pl4/ide/coq.ml coq-8.0pl4.papuq/ide/coq.ml --- coq-8.0pl4/ide/coq.ml 2006-11-08 19:41:04.000000000 +0100 +++ coq-8.0pl4.papuq/ide/coq.ml 2007-04-01 15:45:01.000000000 +0200 @@ -173,6 +173,18 @@ | Success of int (* nb of goals after *) | Failed +(* + * Try to execute given tactic. Errors are processed + * silently, they are just printed on stderr. + * Test method - does not change current state. + * + * Parameters: + * s : string - tactic to execute + * + * Return: tried_tactic + * Interrupted/Failed on errors + * Success of numberGoals:int on success + *) let try_interptac s = try prerr_endline ("Starting try_interptac: "^s); @@ -207,6 +219,7 @@ | DuringCommandInterp (_,e) -> is_pervasive_exn e | _ -> false + let print_toplevel_error exc = let (dloc,exc) = match exc with @@ -354,10 +367,43 @@ prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); Vernacentries.abort_refine Lib.reset_mod (Util.dummy_loc,id) - +(* + * Reference to external menu generator, can be used to extend user menu + * it is invoked each time CoqIDE generates context menu for each hypothesis + * Function parameters: + * _1 : string - identifier of hypothesis + * _2 : string - content of hypothesis + * Return: + * list of pairs (description:string, coqCommandToExecute:string) + *) +let external_hyp_menu_handler : + (string -> string -> ( (string * string) list)) option ref + = ref None;; + +(* + * Hypothesis menu. Invoked to generate context menu. + * + * Parameters (Coq.hyp) : + * env : Environ.env - current environment + * sigma : Evd.evar_map - mapping of free variables + * coqident : Names.identifier - identifier of hypothesis + * ident : string - string representation of identifier + * ast : Term.constr - hypothesis body + * pr_ast : string - string representation of hypothesis body + * s : string - representation of whole line "name : body" + * + * Return: + * list of pairs (description:string, coqCommandToExecute:string) + *) let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) = - [("clear "^ident),("clear "^ident^"."); - + let additional = + match !external_hyp_menu_handler with + | None -> [] + | Some f -> f ident pr_ast + in + additional @ + [ + ("clear "^ident),("clear "^ident^"."); ("apply "^ident), ("apply "^ident^"."); @@ -394,6 +440,15 @@ ("inversion clear "^ident), ("inversion_clear "^ident^".")] +(* + * Conclusion menu. Invoked to generate context menu. + * + * Parameters (Coq.concl): + * concl : Term.constr - conclusion to generate menu for + * + * Return: + * list of pairs (description:string, coqCommandToExecute:string) + *) let concl_menu (_,_,concl,_) = let is_eq = is_equation concl in ["intro", "intro."; diff -urN coq-8.0pl4/ide/coq.mli coq-8.0pl4.papuq/ide/coq.mli --- coq-8.0pl4/ide/coq.mli 2006-11-08 19:41:04.000000000 +0100 +++ coq-8.0pl4.papuq/ide/coq.mli 2007-04-01 15:45:01.000000000 +0200 @@ -65,3 +65,5 @@ (* Message to display in lower status bar. *) val current_status : unit -> string + +val external_hyp_menu_handler : (string -> string -> ( (string * string) list)) option ref diff -urN coq-8.0pl4/ide/ideutils.ml coq-8.0pl4.papuq/ide/ideutils.ml --- coq-8.0pl4/ide/ideutils.ml 2006-01-06 16:40:37.000000000 +0100 +++ coq-8.0pl4.papuq/ide/ideutils.ml 2007-04-01 15:45:02.000000000 +0200 @@ -28,9 +28,9 @@ let debug = Options.debug let prerr_endline s = - if !debug then (prerr_endline s;flush stderr) + prerr_endline s;flush stderr (* JSA *) let prerr_string s = - if !debug then (prerr_string s;flush stderr) + prerr_string s;flush stderr (* JSA *) let lib_ide_file f = let coqlib = @@ -157,11 +157,19 @@ Some (GMain.Timeout.add ~ms:2000 ~callback:(fun () -> f (); highlight_timer := None; true)) +let compose_formatters formatter1 formatter2 = + let (f1, f2) = Format.pp_get_formatter_output_functions formatter1 () in + let (g1, g2) = Format.pp_get_formatter_output_functions formatter2 () in + Format.make_formatter + (fun s n1 n2 -> f1 s n1 n2; g1 s n1 n2) + (fun _ -> f2 (); g2 ()) (* Get back the standard coq out channels *) let read_stdout,clear_stdout = let out_buff = Buffer.create 100 in - Pp_control.std_ft := Format.formatter_of_buffer out_buff; + let formatter = compose_formatters + Format.std_formatter (Format.formatter_of_buffer out_buff) in + Pp_control.std_ft := formatter; (fun () -> Format.pp_print_flush !Pp_control.std_ft (); let r = Buffer.contents out_buff in Buffer.clear out_buff; r), diff -urN coq-8.0pl4/ide/localization.ml coq-8.0pl4.papuq/ide/localization.ml --- coq-8.0pl4/ide/localization.ml 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/localization.ml 2007-04-02 15:15:35.000000000 +0200 @@ -0,0 +1,79 @@ +(* + * Localization for Papug. + * + * Author: Jakub Sakowicz + * + *) + +class resource = + object(self) + method btn_apply = "Apply" + method btn_next = "Next" + method btn_unfold = "Unfold" + method lbl_apply def = "Apply " ^ def + method lbl_unfold def = "Unfold " ^ def + method prev_apply def = "Theorem " ^ def ^ " has been applied" + method prev_unfold def = "Definition " ^ def ^ " has been unfolded" + method lbl_impl = "Goal is an implication.\nAssume the premises" + method prev_impl def = "Assume " ^ def + method lbl_forall name type_name = + "Goal is an universally quantified statement.\nProve it for every " + ^ name ^ " in " ^ type_name + method prev_forall name type_name = + "Let " ^ name ^ " be an element of " ^ type_name + method lbl_conj = "Goal is a conjunction.\nBoth parts should be proved" + method prev_conj term = + "Let us prove the first conjunct of " ^ term ^ ".\nThe rest will be proved later" + method lbl_disj1 = "Goal is a disjunction.\nProve the right disjunct" + method prev_disj1 term = + "To show " ^ term ^ " we prove the right disjunct" + method lbl_disj2 = "Prove the left disjunct" + method prev_disj2 term = + "To show " ^ term ^ " we prove the left disjunct" + method lbl_disj3 = "Prove that negation of the left disjunct implies the right one" + method prev_disj3 term = + "We prove disjunction " ^ term ^ " using excluded middle" + method lbl_disj4 = "Prove that negation of the right disjunct implies the left one" + method prev_disj4 term = + "We prove disjunction " ^ term ^ " using excluded middle" + method lbl_eq_fun = + "Goal is an equality of functions.\nApply extensionality" + method prev_eq_fun = "To show equality of functions, we prove equality for all arguments" + method lbl_eq_pred = "Goal is an equality of predicates.\nApply extensionality" + method prev_eq_pred = "To show equality of predicates, we prove equivalence of their conditions" + method lbl_iff = "Goal is an equivalence.\nProve two implications" + method prev_iff = "Equivalence has been split into two implications.\nWe prove the first one." + method lbl_exists type_name term = "Goal is an existentially quantified statement.\nShow an element of type " ^ type_name ^ "\nsatisfying " ^ term + method prev_exists = "" + + method lbl_contr = "Prove by contradiction." + method prev_contr = "We prove by contradiction. Let us suppose that the conclusion does not hold" + + method lbl_trivial = "Obvious" + method prev_trivial = "Goal is obvious" + + method lbl_assumption = "Goal is an assumption" + method prev_assumption = "Goal is proved" + + method lbl_none = "None" + method lbl_no_proof = "No goals to prove" + method lbl_proof_finished = "Proved" + method lbl_end_proof = "End proof" + method btn_end = "End" + method lbl_show_proof = "Show proof" + method btn_show = "Show" + method lbl_title_prev = "Previous step" + method lbl_title_hint = "Hints" + method lbl_title_wizard = "Coq wizard" + method lbl_title_info = "Info" + + method ctxmenu_rewrite = "Rewrite" + method ctxmenu_rev_rewrite = "Rewrite backwards" + method ctxmenu_injection = "Equal constr." + method ctxmenu_discriminate = "Different constr." + method ctxmenu_destruct = "Use" + method ctxmenu_apply = "Apply" + method ctxmenu_induction ident = "Induction on " ^ ident + method ctxmenu_simpl = "Simplify" + end + diff -urN coq-8.0pl4/ide/localization.mli coq-8.0pl4.papuq/ide/localization.mli --- coq-8.0pl4/ide/localization.mli 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/localization.mli 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1,64 @@ +(* + * Localization interface for Papug. + * + * Author: Jakub Sakowicz + * + *) + +class resource : + object + method btn_apply : string + method btn_end : string + method btn_next : string + method btn_show : string + method btn_unfold : string + method ctxmenu_apply : string + method ctxmenu_destruct : string + method ctxmenu_discriminate : string + method ctxmenu_induction : string -> string + method ctxmenu_injection : string + method ctxmenu_rev_rewrite : string + method ctxmenu_rewrite : string + method ctxmenu_simpl : string + method lbl_apply : string -> string + method lbl_assumption : string + method lbl_conj : string + method lbl_contr : string + method lbl_disj1 : string + method lbl_disj2 : string + method lbl_disj3 : string + method lbl_disj4 : string + method lbl_end_proof : string + method lbl_eq_fun : string + method lbl_eq_pred : string + method lbl_exists : string -> string -> string + method lbl_forall : string -> string -> string + method lbl_iff : string + method lbl_impl : string + method lbl_no_proof : string + method lbl_none : string + method lbl_proof_finished : string + method lbl_show_proof : string + method lbl_title_hint : string + method lbl_title_info : string + method lbl_title_prev : string + method lbl_title_wizard : string + method lbl_trivial : string + method lbl_unfold : string -> string + method prev_apply : string -> string + method prev_assumption : string + method prev_conj : string -> string + method prev_contr : string + method prev_disj1 : string -> string + method prev_disj2 : string -> string + method prev_disj3 : string -> string + method prev_disj4 : string -> string + method prev_eq_fun : string + method prev_eq_pred : string + method prev_exists : string + method prev_forall : string -> string -> string + method prev_iff : string + method prev_impl : string -> string + method prev_trivial : string + method prev_unfold : string -> string + end diff -urN coq-8.0pl4/ide/localization-pl.ml coq-8.0pl4.papuq/ide/localization-pl.ml --- coq-8.0pl4/ide/localization-pl.ml 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/localization-pl.ml 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1,80 @@ +(* + * Localization for Papug. + * + * Author: Jakub Sakowicz + * + *) + +class resource = + object(self) + method btn_apply = "Uzyj" + method btn_next = "Dalej" + method btn_unfold = "Rozwin" + method lbl_apply def = "Uzyj " ^ def + method lbl_unfold def = "Rozwin " ^ def + method prev_apply def = "Uzyto twierdzenia " ^ def + method prev_unfold def = "Rozwinieto definicje " ^ def + method lbl_impl = "Teza jest implikacja. Nalezy zalozyc przeslanki" + method prev_impl def = "Zalozmy, ze " ^ def + method lbl_forall name type_name = + "Teza jest kwantyfikowana uniwersalnie. Nalezy ja dowiesc\ndla kazdego " + ^ name ^ " nalezacego do " ^ type_name + method prev_forall name type_name = + "Niech " ^ name ^ " bedzie dowolnym elementem " ^ type_name + method lbl_conj = "Teza jest koniunkcja. Nalezy dowiesc obie czesci" + method prev_conj term = + "Dowodzimy lewa strone " ^ term ^ ". Prawa zostanie udowodniona pozniej" + method lbl_disj1 = "Teza jest alternatywa. Mozna dowiesc prawa strone" + method prev_disj1 term = + "Aby dowiesc " ^ term ^ " dowodzimy prawej strony" + method lbl_disj2 = "Mozna dowiesc lewa strone" + method prev_disj2 term = + "Aby dowiesc " ^ term ^ " dowodzimy lewej strony" + method lbl_disj3 = "Mozna dowiesc, ze jesli nie zachodzi\n lewa strona to zachodzi prawa" + method prev_disj3 term = + "Dowodzimy alternatywy " ^ term ^ " korzystajac z prawa wylaczonego srodka" + method lbl_disj4 = "Mozna dowiesc, ze jesli nie zachodzi\n prawa strona to zachodzi lewa" + method prev_disj4 term = + "Dowodzimy alternatywy " ^ term ^ " korzystajac z prawa wylaczonego srodka" + method lbl_eq_fun = "Teza jest rownoscia funkcji.\n Mozna zastosowac ekstensjonalnosc" + method prev_eq_fun = "Aby dowiesc rownosc funkcji, dowodzimy ich rownosc dla wszystkich argumentow" + method lbl_eq_pred = "Teza jest rownoscia predykatow.\n Mozna zastosowac ekstensjonalnosc" + method prev_eq_pred = "Aby dowiesc rownosc predykatow, dowodzimy rownowaznosc ich warunkow" + + method lbl_iff = "Teza jest rownowaznoscia.\n Nalezy dowiesc implikacji w obie strony" + method prev_iff = "Uzyto reguly dla rownowaznosci. Powstaly dwie implikacje do dowiedzenia.\n Dowodzimy pierwszej z nich" + + method lbl_exists type_name term = "Teza jest kwantyfikowana egzystencjalnie.\nNalezy wskazac element typu " ^ type_name ^ "\nspelniajacy " ^ term + method prev_exists = "" + + method lbl_contr = "Rozpocznij dowod przez sprzecznosc." + method prev_contr = "Dowodzimy przez sprzecznosc. Zalozmy ze teza nie zachodzi." + + method lbl_trivial = "Teza jest oczywista" + method prev_trivial = "Teza udowodniona" + + method lbl_assumption = "Teza jest jednym z zalozen" + method prev_assumption = "Teza udowodniona" + + method lbl_none = "brak" + method lbl_no_proof = "Brak rzeczy do dowiedzenia" + method lbl_proof_finished = "Dowod zakonczony" + method lbl_end_proof = "Zakoncz skrypt" + method btn_end = "Zakoncz" + method lbl_show_proof = "Pokaz dowod" + method btn_show = "Pokaz" + method lbl_title_prev = "Poprzedni krok" + method lbl_title_hint = "Sugestie" + method lbl_title_wizard = "Coq wizard" + method lbl_title_info = "Info" + + method ctxmenu_rewrite = "Przepisz" + method ctxmenu_rev_rewrite = "Przepisz wspak" + method ctxmenu_injection = "Rownosc konstr." + method ctxmenu_discriminate = "Sprzecznosc konstr." + method ctxmenu_destruct = "Wykorzystaj" + method ctxmenu_apply = "Uzyj" + method ctxmenu_induction ident = "Indukcja po " ^ ident + method ctxmenu_simpl = "Uprosc" + end + diff -urN coq-8.0pl4/ide/teachcfg.ml coq-8.0pl4.papuq/ide/teachcfg.ml --- coq-8.0pl4/ide/teachcfg.ml 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/teachcfg.ml 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1,15 @@ +(* + * Papug config variables + * + * Author: Jakub Sakowicz + * + *) + +let only_applicable_hints = true;; + +let wizard_width = 500;; + +let wizard_label_width = 400;; + +let wizard_btn_width = 100;; + diff -urN coq-8.0pl4/ide/teachcfg.mli coq-8.0pl4.papuq/ide/teachcfg.mli --- coq-8.0pl4/ide/teachcfg.mli 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/teachcfg.mli 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1,27 @@ +(* + * Papug config variables + * + * Author: Jakub Sakowicz + * + *) + +(* + * Decides if to test application of hint + * to current goal. This slow down hint + * generation but ensures only applicable + * are displayed. + *) +val only_applicable_hints : bool + +(* + * Width of wizard window + *) +val wizard_width : int +(* + * Width of action label in wizard window + *) +val wizard_label_width : int +(* + * Width of standard button in wizard window + *) +val wizard_btn_width : int diff -urN coq-8.0pl4/ide/teachdebug.ml coq-8.0pl4.papuq/ide/teachdebug.ml --- coq-8.0pl4/ide/teachdebug.ml 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/teachdebug.ml 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1,24 @@ +(* + * Utilities for debugging Papug + * + * Author: Jakub Sakowicz + * + *) + +let old_formatter : Format.formatter option ref = ref None;; +let switch_output () = + match !old_formatter with + | None -> + old_formatter := Some !Pp_control.std_ft; + Pp_control.std_ft := Format.std_formatter + | Some formatter -> + Pp_control.std_ft := formatter; + old_formatter := None;; + +let debug_str str = + Printf.printf "%i\n" (String.length str); + let a = ref [] in + String.iter (fun c -> a := c::!a); + List.iter (fun c -> Printf.printf "%i " (int_of_char c)) (List.rev !a); + Printf.printf "\n";; + \ No newline at end of file diff -urN coq-8.0pl4/ide/teachdebug.mli coq-8.0pl4.papuq/ide/teachdebug.mli --- coq-8.0pl4/ide/teachdebug.mli 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/teachdebug.mli 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1,19 @@ +(* + * Utilities for debugging Papug + * + * Author: Jakub Sakowicz + * + *) + +(* + * Standard formatter is needed for pritty printing. However it + * causes empty coqide-output. This switches formatters. Used two + * times reverts changes. + * For debugging only. + *) +val switch_output : unit -> unit + +(* + * Prints debug information + *) +val debug_str : string -> unit diff -urN coq-8.0pl4/ide/teachhint.ml coq-8.0pl4.papuq/ide/teachhint.ml --- coq-8.0pl4/ide/teachhint.ml 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/teachhint.ml 2007-04-11 17:47:51.000000000 +0200 @@ -0,0 +1,219 @@ +(* + * Hint engine for Papug + * + * Author: Jakub Sakowicz + * + *) + +type hint_element = string * string * string * string option + +(* message resource, used to obtain all strings *) +let msg = new Localization.resource;; + +(* 1. HINTS *) + +(* + * Makes complex hint applicable, ie. converts + * apply f_equal (A:=nat) to + * apply (f_equal (A:=nat)) which is correct + *) +let improve_hint str = + let (kind, hint) = Teachutils.kind_of_hint str in + if (Str.string_match (Str.regexp "^.* (.+).*") hint 0) then + match kind with + | Teachutils.Apply -> "apply (" ^ hint ^ ")" + | Teachutils.Unfold -> "unfold (" ^ hint ^ ")" + | Teachutils.Eapply -> "eapply (" ^ hint ^ ")" + else str;; + +(* + * List of ignored hints (due to availability in some + * other way -- first order hints + *) +let ommit_list = [ "apply conj"; "apply or_introl"; "apply or_intror" ];; + +let get_hints () = + let command = "Print Hint." + in + try + ignore (Coq.interp false command); + let output = Ideutils.read_stdout () (* hints output from Coq *) + in + let tmp = + Teachutils.unique + (* 8th - remove duplicates *) + ( List.map + (* 7th - make some hints correct *) + improve_hint + ( List.filter + (* 6th - again filter empty *) + (fun s -> not (List.exists (fun el -> el = s) ommit_list + or String.length s = 0)) + ( List.map + (* 5th - trim unused spaces *) + Teachutils.trim_spaces + ( List.filter + ( fun s -> + (* 4th - remove empty lines *) + not (Str.string_match (Str.regexp "\\(^\\w*$\\)|\\(^$\\)") s 0)) + ( List.fold_right + (* 3rd - merge splitted lists *) + ( fun l -> fun res -> l@res ) + ( List.map + (* 2nd - split hints *) + ( fun s -> + Str.split (Str.regexp "([0-9]+)") s) + ( List.filter + (* 1st - filter titles etc. *) + (fun s -> not (Str.string_match (Str.regexp + "\\(^$\\)\\|\\(^In the database.*:\\)\\|\\(^Applicable Hints.*\\)") s 0)) + (Str.split (Str.regexp "\n") output))) + []))))) + in if Teachcfg.only_applicable_hints then + List.filter + (* 9th - test if applicable (optional) *) + (fun s -> Teachutils.test_app_tactic (s ^ ".")) tmp + else tmp + + with e -> + let (s,loc) = Coq.process_exn e in + assert (Glib.Utf8.validate s); + Printf.printf "%s\n" s; + [];; + + + +let get_commands_for_hint command = + List.map + (fun hint -> match Teachutils.kind_of_hint hint with + | (Teachutils.Apply, def) -> (msg#lbl_apply def), hint ^ ".", (msg#prev_apply def), + Some (Teachutils.get_theorem_def def) + | (Teachutils.Eapply, def) -> (msg#lbl_apply def), hint ^ ".", (msg#prev_apply def), + Some (Teachutils.get_theorem_def def) + | (Teachutils.Unfold, def) -> (msg#lbl_unfold def), hint ^ " in *.", (msg#prev_unfold def), None) + (get_hints ());; + +(* 2. FIRSTORDER AND NTT *) + +(* + * Firstorder kindmatcher. Tests goal and matches + * with firstorder conjunctives. Supported: + * quantifiers: existiential, universal + * disjunction, conjunction, implication + * predicate and functional equations + *) +let kind_matcher term = + match Term.kind_of_term term with + | Term.Prod(Names.Anonymous, a, b) -> (* implication *) + [ (msg#lbl_impl, "intro.\n", msg#prev_impl (Teachutils.string_of_type a), None ) ] + + | Term.Prod(a,b,c) -> (* universal quantifier *) + + let name = (Teachutils.string_of_name a) + and type_name = (Teachutils.string_of_type b) + in + [ ( msg#lbl_forall name type_name, "intro.\n", msg#prev_forall name type_name, None) ] + + | Term.App(opp, args) -> + if (Hipattern.is_disjunction term) then (* disjunction *) + [ (msg#lbl_disj1, "right.\n", msg#prev_disj1 (Teachutils.string_of_type term), None ); + (msg#lbl_disj2, "left.\n", msg#prev_disj2 (Teachutils.string_of_type term), None ); + (msg#lbl_disj3, "apply lem_classic_disj_1.\n", msg#prev_disj3 (Teachutils.string_of_type term), None); + (msg#lbl_disj4, "apply lem_classic_disj_2.\n", msg#prev_disj4 (Teachutils.string_of_type term), None) ] + + else if (Hipattern.is_equation term) then (* equation *) + let ttype = Array.get args 0 in + if Teachutils.is_predicate ttype then (* predicate equation *) + [ (msg#lbl_eq_pred, "apply ax_pred_ext.\n", msg#prev_eq_pred, None) ] + else (* functional equation *) + [ (msg#lbl_eq_fun, "apply ax_fun_ext.\n", msg#prev_eq_fun, None) ] + + else + (let name = Teachutils.string_of_constr opp in + match name with + + | "iff" -> (* if and only if *) + [ (msg#lbl_iff, "split.\n", msg#prev_iff, None) ] + + | "ex" -> (* existential quantifier *) + let ttype = Array.get args 0 + and tbody = Array.get args 1 in + let dec_body = match Term.kind_of_term tbody with + | Term.Lambda (n,t,lambda_body) -> + Teachutils.string_of_constr_env (Teachutils.ext_env n t) lambda_body + | _ -> Teachutils.string_of_constr tbody in + [ (msg#lbl_exists (Teachutils.string_of_type ttype) dec_body, + "eapply ex_intro.\n", msg#prev_exists, None) ] + + | _ -> + if (Hipattern.is_conjunction term) then + [ (msg#lbl_conj, "split.\n", msg#prev_conj (Teachutils.string_of_type term), None) ] + else raise Teachutils.Unmatched + ) + + | _ -> + raise Teachutils.Unmatched;; + +(* 3. NTT UNFOLDS *) + +(* + * Operations to check against unfold. Should be extended + * if next one are added. + *) +let operations_to_unfold = + [ "Sum"; "Minus"; "Intersection"; "FamilySum"; "PowerSet"; "Comp";"Whole";"Image" ];; + +(* + * Generate menu for unfold definition + * string - prefix for each unfold, allows to add some specific action + * string - definition name to unfold + *) +let unfold_menu_with pre op = + (msg#lbl_unfold op, pre ^ "unfold " ^ op ^ ".\n", msg#prev_unfold op, None);; + + +let get_unfolds gt = + if Teachutils.test_app_tactic "progress unfold In." then + List.map + (unfold_menu_with "unfold In; ") + (List.filter + (fun op -> Teachutils.test_app_tactic ("progress unfold " ^ op ^ ".") ) + operations_to_unfold) + else + List.map + (unfold_menu_with "") + (List.filter + (fun op -> Teachutils.test_app_tactic ("progress unfold " ^ op ^ ".") ) + operations_to_unfold);; + +(* 4. TRIVIALS *) + +let try_trivial_tactics gt = + if Teachutils.test_tactic "assumption." then + [ (msg#lbl_assumption, "info assumption.\n", msg#prev_assumption, None) ] + else + if Teachutils.test_tactic "trivial." then + [ (msg#lbl_trivial, "info trivial.\n", msg#prev_trivial, None) ] + else raise Teachutils.Unmatched;; + +(* 5. HYP MENU *) +let get_hyp_menu ident body = + (List.filter + (fun p -> Teachutils.test_app_tactic (snd p)) + [ + (msg#ctxmenu_rewrite, "rewrite " ^ ident ^ "."); + (msg#ctxmenu_rev_rewrite, "rewrite " ^ ident ^ "."); + (msg#ctxmenu_injection, "injection " ^ ident ^ "."); + (msg#ctxmenu_discriminate, "discriminate " ^ ident ^ "."); + (msg#ctxmenu_destruct, "destruct " ^ ident ^ "."); + (msg#ctxmenu_apply, "apply " ^ ident ^ "."); + (msg#ctxmenu_induction ident, "induction " ^ ident ^ ".") + ]) + @ + (List.filter + (fun p -> Teachutils.test_app_tactic ("progress " ^ (snd p))) + [ + (msg#ctxmenu_simpl, "simpl in " ^ ident ^ ".") + ]) + @ + [ ("--------", "") ];; diff -urN coq-8.0pl4/ide/teachhint.mli coq-8.0pl4.papuq/ide/teachhint.mli --- coq-8.0pl4/ide/teachhint.mli 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/teachhint.mli 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1,83 @@ +(* + * Interface of hint engine for Papug + * + * Author: Jakub Sakowicz + *) + +(* + * Type representing single Papug's hint. + * string - hint description + * string - previous step description after hint is executed + * string - tactic to invoke and insert to script + * string option - optional string for complex hint description + *) +type hint_element = + string * string * string * string option + +(* + * Generates hint from Coq's hint database. + * If Teachcfg.only_applicable_hints is set hints + * are checked before return. + * + * Parameters: + * goal term + * + * Return: + * list of hints + *) +val get_commands_for_hint : Term.types -> hint_element list + +(* + * Generates hints for first order conjunctives + * and NTT equality. + * + * Parameters: + * goal term + * + * Supported: + * quantifiers: existiential, universal + * disjunction, conjunction, implication + * predicate and functional equations + * + * Return: + * list of hints + *) +val kind_matcher : Term.types -> hint_element list + +(* + * Generates hints for unfolding NTT definitions such as + * Sum, Minus, Intersection etc. Only aplicable unfolds + * are generated. + * + * Parameters: + * goal_term + * + * Return: + * list of hints + *) +val get_unfolds : Term.types -> hint_element list + +(* + * Generates hints for trivial tactics (if one of + * hipothesis is equal to goal or if goal is solved + * using trivial) + * + * Parameters: + * goal_term + * + * Return: + * list of hints (info assumption or info trivial) + *) +val try_trivial_tactics : Term.types -> hint_element list + +(* + * Generates hints for context menu of given hypothesis + * + * Parameters: + * string : hypothesis name + * string : hypothesis body + * + * Return: + * pair (description, tactic ) + *) +val get_hyp_menu : string -> string -> (string * string) list \ No newline at end of file diff -urN coq-8.0pl4/ide/teaching.ml coq-8.0pl4.papuq/ide/teaching.ml --- coq-8.0pl4/ide/teaching.ml 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/teaching.ml 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1,226 @@ +(* + * Main body of Papug + * + * Author: Jakub Sakowicz + *) + +open GtkThread;; + +let msg = new Localization.resource;; + +let get_current_av () = + Coqide.out_some (Coqide.get_current_view ()).Coqide.analyzed_view;; + +let try_insert_on_current_av wizard command prev_step_desc = + let av = get_current_av () + in fun () -> + wizard#set_prev_step_desc prev_step_desc; + av#insert_command command command;; + +type state = Unknown | Edit | InProof;; + +class wizard () = + let window = GWindow.window ~title:msg#lbl_title_wizard ~screen:(Gdk.Screen.default ()) () in + + let _ = window#connect#destroy (fun () -> + Coqide.external_goal_handler := None; + Coqide.external_undo_handler := None; + Coqide.external_redo_handler := None) + in + let _ = window#resize ~width:Teachcfg.wizard_width ~height:100 in + let main_container = GPack.vbox ~packing:window#add () in + let frame_last = GBin.frame ~label:msg#lbl_title_prev ~packing:main_container#add () in + let label = GMisc.label ~text:"" ~packing:frame_last#add () in + let frame_hint = GBin.frame ~label:msg#lbl_title_hint ~packing:main_container#add () in + let line_container = GPack.vbox ~homogeneous:true ~packing:frame_hint#add () + in + object(self) + + val window = window + val prev_label = label + val line_container = line_container + val wizard_state = ref Unknown + val items : GObj.widget Teachutils.std_list = new Teachutils.std_list + val prev_step_desc = ref (msg#lbl_none) + + (* set last step description *) + method set_prev_step_desc desc = prev_step_desc := desc + + method private get_prev_step_desc = prev_step_desc + + method private window = window + + (* clear all showed items *) + method clear () = + items#iter (line_container#remove); + items#clear; + self#window#resize ~width:Teachcfg.wizard_width ~height:100 + + (* activate window *) + method activate () = + self#window#show () + + (* add item to list of showed in wizard *) + method add_item item = + items#push_back item + + (* + * Add item corresponding to single hint line + * + * Parameters: + * string - text description of hint + * string - first button label + * unit->unit - action for first button + * string option - optional second button label + * unit->unit option - optional second button action + * + * See Teachhint.hint_element_list + *) + method add_action_line label_text button_text button_action opt_button_text opt_button_action = + match opt_button_text with + | None -> assert (opt_button_action = None); + self#add_item (Teachutils.create_label_with_button line_container label_text button_text button_action) + | Some btn_text -> ( + match opt_button_action with + | None -> assert false + | Some btn_action -> + self#add_item (Teachutils.create_label_with_two_buttons + line_container label_text button_text button_action btn_text btn_action)) + + method private set_hint_text text = + let hbox = GPack.hbox ~packing:line_container#add () in + let _ = GMisc.label ~text:text ~width:Teachcfg.wizard_label_width ~packing:hbox#pack () in + self#add_item hbox#coerce + + (** + Generic scheme for adding action buttons. Function gets term and + returns list of triples (label, command to invoke, comment on step) + *) + method add_actions_generated_by get_fun goal_term = + try + List.iter + (fun (label, command, prev, opt_body) -> + match opt_body with + | None -> self#add_action_line + (label ^ " ") + msg#btn_next + (try_insert_on_current_av self command prev) + None + None + | Some body -> self#add_action_line + (label ^ " ") + (msg#btn_next) + (try_insert_on_current_av self command prev) + (Some (msg#btn_show)) + (Some (fun () -> Teachutils.show_info self#window msg#lbl_title_info body)) + ) + (get_fun goal_term) + with Teachutils.Unmatched -> (); + + (** + Adds proof by contradiction action. + *) + method add_contr_action_for_current_goal gt = + let add () = + self#add_action_line (msg#lbl_contr ^ " ") + msg#btn_next (try_insert_on_current_av self "info classic_contr.\n" msg#prev_contr) None None in + match Term.kind_of_term gt with + | Term.Ind(name, level) -> + if Teachutils.pp_string (Printer.pr_inductive Environ.empty_env (name,level)) = "False" + then () else add () + | _ -> add () + + (** + Adds actions for first order conjunctives. + *) + method add_main_action_for_current_goal gt = + self#add_actions_generated_by Teachhint.kind_matcher gt + + (** + Adds actions for predicates operations (Sum, Minus, etc..) + *) + method add_unfold_actions_for_current_goal gt = + self#add_actions_generated_by Teachhint.get_unfolds gt + + (** + Adds actions found in hint database + *) + method add_hint_actions_for_current_goal gt = + self#add_actions_generated_by Teachhint.get_commands_for_hint gt + + (** + Adds methods such as 'trivial' if applicable. + *) + method add_auto_actions_for_current_goal gt = + self#add_actions_generated_by Teachhint.try_trivial_tactics gt + + method private update_prev_step_desc = + prev_label#set_text !(self#get_prev_step_desc) + + (* goal change listener for CoqIDE, creates and shows hints *) + method regenerate_actions = + self#update_prev_step_desc; + match Teachutils.num_remaining_goals () with + | -1 -> (* no proof *) + if !wizard_state != Edit then + begin + wizard_state := Edit; + self#clear (); + self#set_hint_text msg#lbl_no_proof + end + else () + | 0 -> (* proved *) + wizard_state := InProof; + self#clear (); + self#set_hint_text msg#lbl_proof_finished ; + self#add_action_line msg#lbl_end_proof msg#btn_end + (try_insert_on_current_av self "Save.\n" "") None None; + self#add_action_line msg#lbl_show_proof msg#btn_show + (try_insert_on_current_av self "Show Proof.\n" "") None None + | _ -> let gt = Teachutils.goal_term () in (* standard *) + wizard_state := InProof; + self#clear (); + self#add_auto_actions_for_current_goal gt; + self#add_main_action_for_current_goal gt; + self#add_unfold_actions_for_current_goal gt; + self#add_hint_actions_for_current_goal gt; + self#add_contr_action_for_current_goal gt + + (* undo listener for CoqIDE *) + method undo_pressed () = + self#set_prev_step_desc ""; + self#update_prev_step_desc + + (* close wizard window *) + method close () = + Coqide.external_goal_handler := None; + Coqide.external_undo_handler := None; + Coqide.external_redo_handler := None; + window#destroy () + end + + +(* wizard singleton *) +let wizard_instance : wizard option ref = ref None;; + + +let internal_start () = + let w = new wizard () in + Coqide.external_goal_handler := Some (fun _ -> w#regenerate_actions); + Coqide.external_undo_handler := Some (w#undo_pressed); + Coqide.external_redo_handler := Some (w#undo_pressed); + w#activate (); + w;; + + +let start_wizard () = + match !wizard_instance with + | None -> wizard_instance := Some (internal_start ()) + | Some w -> w#close (); wizard_instance := Some (internal_start ());; + + +Coq.external_hyp_menu_handler := Some + (fun ident -> fun body -> Teachhint.get_hyp_menu ident body);; + + +Coqide.external_wizard_start := Some (fun () -> ignore (start_wizard ()));; diff -urN coq-8.0pl4/ide/teaching.mli coq-8.0pl4.papuq/ide/teaching.mli --- coq-8.0pl4/ide/teaching.mli 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/teaching.mli 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1,59 @@ +(* + * Interface of main body for Papug modification. + * It is teaching extension for CoqIDE. + * + * Author: Jakub Sakowicz + *) + +type state = Unknown | Edit | InProof +class wizard : + unit -> + object + (* activate window *) + method activate : unit -> unit + + (* set last step description *) + method set_prev_step_desc : string -> unit + + (* + * Add item corresponding to single hint line + * + * Parameters: + * string - text description of hint + * string - first button label + * unit->unit - action for first button + * string option - optional second button label + * unit->unit option - optional second button action + * + * See Teachhint.hint_element_list + *) + method add_action_line : + string -> + string -> + (unit -> unit) -> string option -> (unit -> unit) option -> unit + + (* action generators *) + method add_actions_generated_by : + (Term.types -> Teachhint.hint_element list) -> Term.types -> unit + method add_auto_actions_for_current_goal : Term.types -> unit + method add_contr_action_for_current_goal : Term.constr -> unit + method add_hint_actions_for_current_goal : Term.types -> unit + method add_main_action_for_current_goal : Term.types -> unit + method add_unfold_actions_for_current_goal : Term.types -> unit + + (* add item to list of showed in wizard *) + method add_item : GObj.widget -> unit + (* clear all showed items *) + method clear : unit -> unit + (* close wizard window *) + method close : unit -> unit + (* goal change listener for CoqIDE, creates and shows hints *) + method regenerate_actions : unit + (* undo listener for CoqIDE *) + method undo_pressed : unit -> unit + end + +(* + * Start new wizard instance. Window is created and displayed. + *) +val start_wizard : unit -> unit diff -urN coq-8.0pl4/ide/teachutils.ml coq-8.0pl4.papuq/ide/teachutils.ml --- coq-8.0pl4/ide/teachutils.ml 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/teachutils.ml 2007-04-01 19:34:54.000000000 +0200 @@ -0,0 +1,164 @@ +(* + * Common library for Papug + * + * Author: Jakub Sakowicz + * + *) + +open Teachdebug;; + +exception Unmatched;; + +(* utils *) + +let head l = match l with h::t -> h | _ -> raise Unmatched;; + +let unique l = + List.fold_right + (fun elt -> fun ak -> + if not (List.exists (fun e -> e = elt) ak) then + elt :: ak + else + ak) l [];; + +(* string utilities *) + +let trim_spaces str = + try + ignore (Str.search_forward (Str.regexp "\\( +\\)") str 0); + Str.string_after str (Str.match_end ()) + with _ -> str;; + + +(* printers *) + +let pp_string cmds = + Pp.msg_with Format.str_formatter cmds; + Format.flush_str_formatter();; + +let string_of_type typeterm = + pp_string (Printer.prtype typeterm);; + +let string_of_constr constrterm = + pp_string (Printer.prterm constrterm);; + +let ext_env name typeterm = + Termops.push_rel_assum (name, typeterm) (Global.env());; + +let string_of_constr_env env typeterm = + pp_string (Printer.prterm_env env typeterm);; + +let string_of_name name = + match name with + | Names.Name id -> Names.string_of_id id + | _ -> raise Unmatched;; + +(* goal utilities *) + +let refined_goal () = + let state = Pfedit.get_pftreestate () in + Refiner.frontier (Tacmach.proof_of_pftreestate state);; + +let num_remaining_goals () = + try + let goals = fst (refined_goal ()) in + List.length goals + with Util.UserError _ -> -1;; + +let goal_term () = + let goal = head (fst (refined_goal ())) in + goal.Evd.evar_concl;; + +(* parsing utilities *) + +type hint_kind = Apply | Unfold | Eapply;; + +let kind_of_hint hint = + Printf.printf "Kind of hint: %s\n" hint; + if (Str.string_match (Str.regexp "^apply.*") hint 0) then Apply, Str.string_after hint 5 + else if (Str.string_match (Str.regexp "^unfold.*") hint 0) then Unfold, Str.string_after hint 6 + else if (Str.string_match (Str.regexp "^eapply.*") hint 0) then Eapply, Str.string_after hint 6 + else ( debug_str hint; assert(false) );; + +(* tests if tactic solves current goal *) +let test_tactic string = + match Coq.try_interptac string with + | Coq.Success (-1) -> true + | _ -> false;; + + +(* tests if tactic is applicable *) +let test_app_tactic string = + (* Printf.printf "Testing applicable %s\n" string; *) + match Coq.try_interptac string with + | Coq.Success (_) -> true + | _ -> false;; + +(* tests if product is Predicate of some type T *) +let is_predicate prodterm = + match Term.kind_of_term prodterm with + | Term.Prod(_,_,c) -> + ( match Term.kind_of_term c with + | Term.Sort(Term.Prop(_)) -> true + | _ -> false + ) + | Term.App(cname, _) -> + ( let name = string_of_constr cname in + match name with + | "Predicate" -> true + | _ -> raise Unmatched + ) + | _ -> raise Unmatched;; + +(* returns theorem definition *) +let get_theorem_def theorem = + let theorem = head (Str.split (Str.regexp ";") theorem) in + let command = "Check " ^ theorem ^ "." in + try + ignore (Coq.interp false command); + let output = Ideutils.read_stdout () + in output + with e -> + let (s,loc) = Coq.process_exn e + in assert (Glib.Utf8.validate s); + Printf.printf "%s\n" s; + "";; + + +(* GUI utilities *) + +let create_label_with_button parent label_text button_text button_action = + let hbox = GPack.hbox ~packing:parent#add () in + let _ = GMisc.label ~text:label_text ~width:Teachcfg.wizard_label_width ~packing:hbox#pack () in + let hbox2 = GPack.hbox ~packing:hbox#pack ~width:Teachcfg.wizard_btn_width () in + let button = GButton.button ~label:button_text ~packing:hbox2#add () in + let _ = button#connect#clicked ~callback:button_action in + hbox#coerce;; + +let create_label_with_two_buttons parent label_text button_text button_action + opt_button_text opt_button_action = + let hbox = GPack.hbox ~packing:parent#add () in + let _ = GMisc.label ~text:label_text ~width:Teachcfg.wizard_label_width ~packing:hbox#pack () in + let hbox2 = GPack.hbox ~packing:hbox#pack ~width:(Teachcfg.wizard_btn_width/2) () in + let hbox3 = GPack.hbox ~packing:hbox#pack ~width:(Teachcfg.wizard_btn_width/2) () in + let button1 = GButton.button ~label:button_text ~packing:hbox2#add () in + let _ = button1#connect#clicked ~callback:button_action in + let button2 = GButton.button ~label:opt_button_text ~packing:hbox3#add () in + let _ = button2#connect#clicked ~callback:opt_button_action in + hbox#coerce;; + +let show_info parent title info_text = + let w = GWindow.dialog ~no_separator:true ~parent:parent + ~title:title ~modal:true ~resizable:true + () in + let _ = GMisc.label ~text:info_text ~packing:w#vbox#add () in + w#show ();; + +class ['a] std_list = + object(self) + val mutable impl : 'a list ref = ref [] + method clear = impl := [] + method push_back el = impl := el::!impl + method iter f = List.iter f !impl + end + diff -urN coq-8.0pl4/ide/teachutils.mli coq-8.0pl4.papuq/ide/teachutils.mli --- coq-8.0pl4/ide/teachutils.mli 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/ide/teachutils.mli 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1,180 @@ +(* + * Interface of common library for Papug + * + * Author: Jakub Sakowicz + * + *) + +(* + * Throws when invalid (non matching) kind of term/list/object + * is given. + *) +exception Unmatched + +(* GENERAL HELPERS *) + +(* + * Mutable list. Similar to STL. + * + *) +class ['a] std_list : + object + val mutable impl : 'a list ref + (* remove all objects *) + method clear : unit + (* iterates over self *) + method iter : ('a -> unit) -> unit + (* adds object to the end of list *) + method push_back : 'a -> unit + end + + +(* + * Return head of list. + * + * Throw: Unmatched if list is empty. + *) +val head : 'a list -> 'a + +(* + * Eliminate duplicates from list. + *) +val unique : 'a list -> 'a list + +(* + * Eliminate begining and following spaces + * from string, occurences of two or more spaces + * are reduced to one. + *) +val trim_spaces : string -> string + +(* PRINT AND PARSE HELPERS *) + +(* + * Converts ppcmds to string (print to string method) + *) +val pp_string : Pp.std_ppcmds -> string + +(* + * String description of type + *) +val string_of_type : Term.types -> string + +(* + * String description of term + *) +val string_of_constr : Term.constr -> string + +(* + * String description of term in given environment + *) +val string_of_constr_env : Environ.env -> Term.constr -> string + +(* + * String description of name + *) +val string_of_name : Names.name -> string + +(* MISC *) + +(* + * Exdends empty environment with bind (name:type) + *) +val ext_env : Names.name -> Term.types -> Environ.env + +(* GOAL TERMS UTILITIES *) + +(* + * Return number of goals remaining to prove + *) +val num_remaining_goals : unit -> int + +(* + * Return current goal term + *) +val goal_term : unit -> Term.constr + +(* HINTS *) + +(* + * Enumerator representing kind of hint from database + *) +type hint_kind = Apply | Unfold | Eapply + +(* + * Return pair (kind of hint, its body) + * + * Throw: Unmatched if string does not represent hint + *) +val kind_of_hint : string -> hint_kind * string + +(* + * Return true if tactic solves current goal + *) +val test_tactic : string -> bool + +(* + * Return true if tactic is applicable to current goal + *) +val test_app_tactic : string -> bool + +(* + * Returns true if term represents predicate. + * + * Throw: Unmatched if term is not a product type + *) +val is_predicate : Term.constr -> bool + +(* + * Return theorem definition, empty string + * if not found. + *) +val get_theorem_def : string -> string + +(* GUI *) + +(* + * Add widget containing text label and button. + * + * Parameters: + * GWindow.window_skel - parent of new widget + * string - label text + * string - button text + * unit->unit - callback function + * + * Return: + * new widget + *) +val create_label_with_button : + < add : GObj.widget -> unit; .. > -> + string -> string -> (unit -> unit) -> GObj.widget + +(* + * Add widget containing text label and two buttons + * + * Parameters: + * GWindow.window_skel - parent of new widget + * string - label text + * string - first button text + * unit->unit - first callback function + * string - second button text + * unit->unit - second callback function + * + * Return: + * new widget + *) +val create_label_with_two_buttons : + < add : GObj.widget -> unit; .. > -> + string -> + string -> (unit -> unit) -> string -> (unit -> unit) -> GObj.widget + +(* + * Shows modal window with some information + * + * Parameters: + * GWindow.window_skel - parent window + * string - title + * string - label + * + *) +val show_info : #GWindow.window_skel -> string -> string -> unit diff -urN coq-8.0pl4/Makefile coq-8.0pl4.papuq/Makefile --- coq-8.0pl4/Makefile 2006-02-24 15:55:22.000000000 +0100 +++ coq-8.0pl4.papuq/Makefile 2007-04-01 15:45:02.000000000 +0200 @@ -517,7 +517,9 @@ ide/ideutils.cmo ide/blaster_window.cmo ide/undo.cmo \ ide/find_phrase.cmo \ ide/highlight.cmo ide/coq.cmo ide/coq_commands.cmo \ - ide/coq_tactics.cmo ide/command_windows.cmo ide/coqide.cmo + ide/coq_tactics.cmo ide/command_windows.cmo ide/coqide.cmo \ + ide/localization.cmo ide/teachcfg.cmo ide/teachdebug.cmo \ + ide/teachutils.cmo ide/teachhint.cmo ide/teaching.cmo COQIDECMX=$(COQIDECMO:.cmo=.cmx) COQIDEFLAGS=-thread -I +lablgtk2 @@ -820,7 +822,9 @@ theories/Relations/Relation_Definitions.vo \ theories/Relations/Relation_Operators.vo \ theories/Relations/Relations.vo \ - theories/Relations/Rstar.vo + theories/Relations/Rstar.vo \ + theories/Logic/CoqTypesTheory.vo + WELLFOUNDEDVO=\ theories/Wellfounded/Disjoint_Union.vo \ diff -urN coq-8.0pl4/theories/Logic/CoqTypesTheory.v coq-8.0pl4.papuq/theories/Logic/CoqTypesTheory.v --- coq-8.0pl4/theories/Logic/CoqTypesTheory.v 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/theories/Logic/CoqTypesTheory.v 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1,315 @@ +Require Import Coq.Logic.Classical. +Require Import Relations_1_facts. + +(* + * podstawy teorii NTT + * oraz notacja dla IN + *) +Section Basic. + +(* po zakonczeniu sekcji wszystkie jej pojecia + beda parametryzowane typem U *) +Variable U : Type. + +Definition In (A : U -> Prop) (x : U) := + A x. +End Basic. + +Implicit Arguments In [ U ]. +Notation "x 'IN' A" := (In A x) (at level 10). +Hint Unfold In. + + +(* + * ogolne pojecia teorii + *) +Section Generic. + +(* po zakonczeniu sekcji wszystkie jej pojecia + beda parametryzowane typem U *) +Variable U : Type. + +(* predykat - wyraza istote "podzbioru typu" *) +Definition Predicate := U -> Prop. + + +(* istnieje typ pusty *) +Lemma lem_empty_type : exists Empty : Type, ~ exists x : Empty, True. +exists False. +unfold not. +intro. +elim H. auto. +Save. + + +(* caly zbior jako predykat *) +Definition Whole : Predicate := fun _ : U => True. + +(* pusty podzbior jako predykat *) +Definition EmptyPred : Predicate := fun _ : U => False. + +(* suma dwoch predykatow *) +Definition Sum (A B : Predicate) : Predicate := fun x => x IN A \/ x IN B. + +(* roznica dwoch predykatow *) +Definition Minus (A B : Predicate) : Predicate := fun x => x IN A /\ ~ x IN B. + +(* przeciecie dwoch predykatow *) +Definition Intersection (A B : Predicate) : Predicate := + fun x => x IN A /\ x IN B. + +(* typ potegowy *) +Definition PowerSetType : Type := U -> Prop. + +(* podtyp *) +(* Inductive SubType (P : Predicate) : Type := + ST_exist : forall x : U, x IN P -> SubType P. + *) + +(* rodzina zbiorow *) +Definition FamilyType := (U -> Prop) -> Prop. + +Definition FamilySum (R : FamilyType) : Predicate := + fun x : U => exists A : Predicate, A IN R /\ x IN A. + +Definition FamilyIntersection (R : FamilyType) : Predicate := + fun x : U => forall A, A IN R -> x IN A. + +(* pojecia rodziny, sumy, operacji na funkcjach itp., + beda parametryzowane dwoma typami + po opuszczeniu sekcji *) +Variable V : Type. +(* indeksowana rodzina zbiorow *) +Definition IndexedPredicate := V -> Predicate. + +Definition IndexedSum (R : IndexedPredicate) : Predicate := + fun x => exists v : V, R v x. + +Definition IndexedIntersection (R : IndexedPredicate) : Predicate := + fun x => forall v : V, R v x. + +Definition BinaryRelation := U -> V -> Prop. + +Variable f : U -> V. +Definition FunctionAsRelation : BinaryRelation := + fun x : U => fun y : V => f x = y. + +Definition Monomorphism : Prop := + forall x y : U, f x = f y -> x = y. + +Definition Epimorphism : Prop := + forall y : V, exists x : U, f x = y. + +Definition Comp (U V W : Type) (f : U -> V) (g : W -> U) : W -> V := + fun x : W => f (g x). + + +(* istotny aksjomat - ekstensjonalnosc funkcji w NTT *) +Axiom ax_fun_ext : + forall f g : U -> V, + (forall x : U, f x = g x) -> f = g. +Lemma lem_fun_ext_rev : + forall f g : U -> V, + f = g -> (forall x : U, f x = g x). +Proof. +intros. +rewrite H. trivial. +Save. + +End Generic. + + +(* definicje argumentow domyslnych + - wnioskowanych na podstawie typow pozostalych *) +Implicit Arguments Monomorphism [ U V ]. + +Implicit Arguments Comp [ U V W ]. + +Implicit Arguments Sum [ U ]. + +Implicit Arguments Minus [ U ]. + +Implicit Arguments Intersection [ U ]. + +Implicit Arguments FamilySum [ U ]. + +Implicit Arguments FamilyIntersection [ U ]. + +Implicit Arguments IndexedIntersection [ U V ]. + +Implicit Arguments Monomorphism [ U V]. + +Implicit Arguments Epimorphism [ U V ]. + + + +(* notacje teoriomnogosciowe *) +Notation "A 'u' B" := ( Sum A B ) (at level 11). +Hint Unfold Sum. +Notation "A '\' B" := ( Minus A B ) (at level 11). +Hint Unfold Minus. +Notation "A 'n' B" := ( Intersection A B ) (at level 11). +Hint Unfold Intersection. +Notation "f 'o' g" := ( Comp f g ) (at level 11). +Hint Unfold Comp. + +Hint Unfold Monomorphism. +Hint Unfold Epimorphism. + + +(* ponizsza sekcja zawiera operacje specyficzne dla funkcji *) +Section Functions. + +Definition Image (U V : Type) (f : U -> V) (A : Predicate U) : Predicate V := + fun y : V => exists x, x IN A /\ y = f x. + +Definition Preimage (U V : Type) (f : U -> V) (B : Predicate V) : Predicate U := + fun x : U => (f x) IN B. + +End Functions. + +Implicit Arguments Image [ U V ]. +Implicit Arguments Preimage [ U V ]. + + + +Definition PredIndSum (U V : Type) (P : Predicate U) + (I : IndexedPredicate V U) : Predicate V := + fun v => exists x:U, x IN P /\ I x v. +Implicit Arguments PredIndSum [ U V ]. + +(* definicja "podpredykatu" *) +Definition Subset (U : Type) (PA : Predicate U) (PB : Predicate U) : Prop := + forall x : U, x IN PA -> x IN PB. +Implicit Arguments Subset [ U ]. +Notation "A 'c' B" := (Subset A B) (at level 100). +Hint Unfold Subset. + +Definition NotEmpty (U : Type) (PA : Predicate U) : Prop := + exists x, x IN PA. +Implicit Arguments NotEmpty [ U ]. +Hint Unfold NotEmpty. + +(* sekcja zawierajaca ekstensjonalnosc dla predykatow + i lematy z niej plynace *) +Section PredExt. +Variable U : Type. + +(* kolejny istotny aksjomat - ekstensjonalnosc dla predykatow *) +Axiom ax_pred_ext : + forall p1 p2 : Predicate U, + (forall x : U, x IN p1 <-> x IN p2) -> p1 = p2. + +(* wlasnosci bycia podpredykatem *) +Lemma SubseteqsImplEq : + forall p1 p2 : Predicate U, + (p1 c p2) -> (p2 c p1) -> p1 = p2. +intros. +apply ax_pred_ext. +intros. +unfold iff. split. +apply H. +apply H0. +Save. + +Lemma SubsetTransitivity : + forall p1 p2 p3 : Predicate U, + (p1 c p2) -> (p2 c p3) -> (p1 c p3). +auto. +Save. + +Lemma lem_pred_ext_rev : + forall A B : Predicate U, + A = B -> (forall x : U, x IN A <-> x IN B). +Proof. +intros. +rewrite H. +split; trivial. +Save. + + +End PredExt. +Implicit Arguments ax_pred_ext [ U ]. +Implicit Arguments lem_pred_ext_rev [ U A B]. +Implicit Arguments SubseteqsImplEq [ U ]. + +Inductive Empty : Type := . + +Definition IsEmpty (U : Type) (P : Predicate U) : Prop := + ~ exists x : U, x IN P. +Implicit Arguments IsEmpty [ U ]. + +(* podstawowe lematy o typach *) +Lemma lem_empty_is_empty : forall P : Predicate Empty, IsEmpty P. +intros. +unfold IsEmpty. +unfold not. +intros. +destruct H. +destruct x. +Save. + +Inductive Unit : Type := + singleton : Unit. + +Lemma lem_unit_is_single : forall x y : Unit, x = y. +intros. +destruct x. +destruct y. +tauto. +Save. + +Inductive Bool : Type := + b_true : Bool +| b_false : Bool. + +Section PowerSet. +Variable U : Type. +Definition PowerSet (A : Predicate U) : Predicate (PowerSetType U) + := fun pu => pu c A. +End PowerSet. +Implicit Arguments PowerSet [ U ]. + +Section SumType. +Inductive SumType (U V : Type) : Type := + in_left (_ : U) +| in_right (_ : V). +End SumType. + +(* produkt - dla typow *) +Section ProductType. +Inductive ProductType (U V : Type) : Type := + prod_t : U -> V -> ProductType U V. +End ProductType. + +(* lematy ulatwiajace korzystanie z prawa + wylaczonego srodka *) +Lemma lem_classic_disj_1 : + forall A B : Prop, (~ A -> B) -> A \/ B. +intro A. intro B. +apply NNPP. +tauto. +Save. + +Lemma lem_classic_disj_2 : + forall A B : Prop, (~ B -> A) -> A \/ B. +intro A. intro B. +apply NNPP. +tauto. +Save. + + +(* aksjomat tworzenia funkcji z relacji, + postulowany w NTT *) +Axiom ax_fun_from_rel : + forall U V : Type, forall R : BinaryRelation U V, + (forall x : U , exists y : V, R x y /\ + forall x : U , forall y z : V, R x y /\ R x z -> y = z) -> + exists f : U -> V, forall x : U, forall y : V , f x = y <-> R x y. + +(* taktyka dla dowodow przez sprzecznosc w narzedziu Papug *) +Ltac classic_contr := + match goal with + | |- ?A => apply NNPP; unfold not at 1; intro + end. + diff -urN coq-8.0pl4/theories7/Logic/CoqTypesTheory.v coq-8.0pl4.papuq/theories7/Logic/CoqTypesTheory.v --- coq-8.0pl4/theories7/Logic/CoqTypesTheory.v 1970-01-01 01:00:00.000000000 +0100 +++ coq-8.0pl4.papuq/theories7/Logic/CoqTypesTheory.v 2007-04-01 15:45:02.000000000 +0200 @@ -0,0 +1 @@ +