diff options
| author |  Erik Martin-Dorel <erik@martin-dorel.org> | 2018-08-22 23:29:35 +0200 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2018-08-22 23:29:35 +0200 |
| commit | 26b3bf9f070e9aee45c6e3d19bca475d4ae8ed37 (patch) | |
| tree | 64b5b138c91b75c464e66eecd5dc19542ad68276 | |
| parent | 3b9e1e4742a2dafce6ac2ef4bfa95d22e43c3c59 (diff) | |
| parent | 7ee9486a616b12ea99490b134c1417792ef78459 (diff) | |
Merge pull request #200 from craff/master
Update phox support
| -rw-r--r-- | generic/proof-site.el | 26 | ||||
| -rw-r--r-- | pg-init.el | 2 | ||||
| -rw-r--r-- | phox/.cvsignore | 13 | ||||
| -rw-r--r-- | phox/README | 18 | ||||
| -rw-r--r-- | phox/README.pbrpm | 26 | ||||
| -rw-r--r-- | phox/example.phx | 22 | ||||
| -rw-r--r-- | phox/phox-extraction.el | 178 | ||||
| -rw-r--r-- | phox/phox-font.el | 102 | ||||
| -rw-r--r-- | phox/phox-fun.el | 440 | ||||
| -rw-r--r-- | phox/phox-lang.el | 64 | ||||
| -rw-r--r-- | phox/phox-outline.el | 69 | ||||
| -rw-r--r-- | phox/phox-pbrpm.el | 318 | ||||
| -rw-r--r-- | phox/phox-sym-lock.el | 401 | ||||
| -rw-r--r-- | phox/phox-tags.el | 92 | ||||
| -rw-r--r-- | phox/phox.el | 366 | ||||
| -rw-r--r-- | phox/sqrt2.phx | 253 | ||||
| -rw-r--r-- | phox/square-root-2.phx | 368 |
17 files changed, 405 insertions, 2353 deletions
diff --git a/generic/proof-site.el b/generic/proof-site.el index c7d721cd..dccc32a9 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -14,7 +14,7 @@ ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;;; Commentary: -;; +;; ;; Loading stubs and configuration for site and choice of provers. ;; ;; NB: Normally users do not need to edit this file. Developers/installers @@ -32,12 +32,12 @@ ;;; Code: ;; Entries in proof-assistant-table-default are lists of the form -;; +;; ;; (SYMBOL NAME FILE-EXTENSION [AUTOMODE-REGEXP] [IGNORED-EXTENSIONS-LIST]) ;; ;; FILE-EXTENSION is without dot ".". AUTOMODE-REGEXP is put into ;; auto-mode-alist, if it is not present, a regexp will be made up from -;; FILE-EXTENSION. IGNORED-EXTENSIONS-LIST, if present, is appended to +;; FILE-EXTENSION. IGNORED-EXTENSIONS-LIST, if present, is appended to ;; completion-ignored-extensions. See proof-assistant-table for more info. ;; (defconst proof-assistant-table-default @@ -47,10 +47,10 @@ (isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (easycrypt "EasyCrypt" "ec" "\\.eca?\\'") + (phox "PhoX" "phx" nil (".phi" ".pho")) ;; Obscure instances or conflict with other Emacs modes. - ;; (phox "PhoX" "phx") ;; (lego "LEGO" "l") ;; (ccc "CASL Consistency Checker" "ccc") @@ -61,7 +61,7 @@ (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci") - + ;; Incomplete/obsolete: ;; (hol98 "HOL" "sml") @@ -303,21 +303,21 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'." (run-hooks 'proof-ready-for-assistant-hook)))))) -(defvar proof-general-configured-provers +(defvar proof-general-configured-provers (or (mapcar 'intern (split-string (or (getenv "PROOFGENERAL_ASSISTANTS") ""))) proof-assistants (mapcar (lambda (astnt) (car astnt)) proof-assistant-table)) "A list of the configured proof assistants. Set on startup to contents of environment variable PROOFGENERAL_ASSISTANTS, the lisp variable `proof-assistants', or the contents of `proof-assistant-table'.") - + ;; Add auto-loads and load-path elements to support the ;; proof assistants selected, and define stub major mode functions (let ((assistants proof-general-configured-provers)) (while assistants (let* ((assistant (car assistants)) ; compiler bogus warning here - (tableentry + (tableentry (or (assoc assistant proof-assistant-table) (error "Symbol %s is not in proof-assistant-table (in proof-site)" @@ -377,16 +377,16 @@ the lisp variable `proof-assistants', or the contents of `proof-assistant-table' ;; (defun proof-chose-prover (prompt) - (completing-read prompt - (mapcar 'symbol-name + (completing-read prompt + (mapcar 'symbol-name proof-general-configured-provers))) (defun proofgeneral (prover) "Start proof general for prover PROVER." (interactive (list (proof-chose-prover "Start Proof General for theorem prover: "))) - (proof-ready-for-assistant (intern prover) - (nth 1 (assoc (intern prover) + (proof-ready-for-assistant (intern prover) + (nth 1 (assoc (intern prover) proof-assistant-table-default))) (require (intern prover))) @@ -398,7 +398,7 @@ the lisp variable `proof-assistants', or the contents of `proof-assistant-table' prover "/example." (nth 2 (assoc (intern prover) proof-assistant-table-default))))) - + (provide 'proof-site) @@ -55,7 +55,7 @@ (eval-when-compile (let ((byte-compile-directories '("generic" "lib" - "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell"))) + "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox"))) (dolist (dir byte-compile-directories) (add-to-list 'load-path (expand-file-name dir pg-init--pg-root))))) diff --git a/phox/.cvsignore b/phox/.cvsignore deleted file mode 100644 index f0b14b7a..00000000 --- a/phox/.cvsignore +++ /dev/null @@ -1,13 +0,0 @@ -config -config.dos -*~ -#*# -*.o -*.a -*.cmo -*.cmi -*.cmx -*.pho -*.phi -*.pht -*.math.tex diff --git a/phox/README b/phox/README deleted file mode 100644 index 635360fb..00000000 --- a/phox/README +++ /dev/null @@ -1,18 +0,0 @@ -PhoX Proof General, for Phox. - -Written by Christophe Raffalli and others - -Status: supported -Maintainer: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> -PhoX version: 0.8 -PhoX homepage: http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html - -=========================================================================== - -This mode has support for script management with PhoX, and some -other features ported from PhoX's own Emacs mode. - - - -$Id$ - diff --git a/phox/README.pbrpm b/phox/README.pbrpm deleted file mode 100644 index c0c7bc1b..00000000 --- a/phox/README.pbrpm +++ /dev/null @@ -1,26 +0,0 @@ -**** -Projet PhoX : Proof By Rules Popup Menu (PBRPM) -***** - ------ -Fichiers concernés : - ProofGeneral/generic/pg-goals.el - ProofGeneral/generic/pg-pbrpm.el - ProofGeneral/phox/phox.el - ProofGeneral/phox/phox-pbrpm.el - - -- Dans pg-goals.el - -(l. 58-59) - inclusion de pg-pbrpm.el - déclaration du 'CTRL + Click Droit' associé à pg-pbrpm-button-action (dans pg-pbrpm.el) - -- Dans pg-pbrpm.el - - Fonctions indépendantes de PhoX implémentant le PBRPM. - -- Dans phox.el - -(l. 86) inclus phox-pbrpm.el -(l. 103-104) ajoute le menu de gestion du buffer de selections dans le menu de PhoX - -- Dans phox-pbrpm.el - - Fonctions spécifiques à PhoX.
\ No newline at end of file diff --git a/phox/example.phx b/phox/example.phx deleted file mode 100644 index 5dacbb20..00000000 --- a/phox/example.phx +++ /dev/null @@ -1,22 +0,0 @@ -(* - Example proof script for PhoX Proof General - - $Id$ -*) - -(* -goal /\n:N (ack n N1 >= N2). -intro 2. -elim H. -trivial. -elim -1 [case] H0. -trivial. -trivial. -save ack_lem7. -*) - -prop (* test *) (* just un test *) test /\X (X -> X). -print $0. -trivial. -save. - diff --git a/phox/phox-extraction.el b/phox/phox-extraction.el deleted file mode 100644 index 84937f36..00000000 --- a/phox/phox-extraction.el +++ /dev/null @@ -1,178 +0,0 @@ -;; $State$ $Date$ $Revision$ -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; program extraction. -;; -;; note : program extraction is still experimental This file is very -;; dependant of the actual state of program extraction in phox. -;;--------------------------------------------------------------------------;; - -(require 'cl) - -(eval-when-compile - (defvar phox-prog-name nil)) - -(declare-function proof-shell-invisible-command "proof-shell" (str)) - -;; configuration : - -(defvar phox-prog-orig "phox -pg" "original name of phox binary.") - -(defun phox-prog-flags-modify(option) -"ask for a string that are options to pass to phox binary" -(interactive "soption :") -; pas d'analyse de la réponse, -(let ((process)) - (if (and phox-prog-name - (progn (string-match " \\|$" phox-prog-name) - (setq process - (substring phox-prog-name 0 (match-beginning 0)) - ) - ) - (processp (get-process process)) - (eq (process-status process) 'run)) - (error "Error : exit phox process first !") - ) -(if (string-match "^ *$" option) - (progn - (message - "no option other than default ones will be passed to phox binary.") - (setq phox-prog-name phox-prog-orig)) - (progn - (message (format "option %s will be passed to phox binary." option )) - (setq phox-prog-name (concat phox-prog-orig " " option)) - ) - ) -) -) - - -(defun phox-prog-flags-extract() -"pass option -f to phox binary. A program can be extracted from -proof of theorem_name with : -compile theorem_name. -output." -(interactive) -(phox-prog-flags-modify "-f") -(message -"WARNING : program extraction is experimental and can disturb the prover !") -) - -(defun phox-prog-flags-erase() -"no option to phox binary." -(interactive) -(phox-prog-flags-modify "")) - -; encore une fonction qui devrait être redéfinie en cas d'autres -; options possibles que -f - -(defun phox-toggle-extraction() -"toggle between extraction mode and ordinary mode for phox process." -(interactive) -(cond ((string-equal phox-prog-name phox-prog-orig) ;; à améliorer (espaces) - (phox-prog-flags-extract)) - ((string-match "\-f$" phox-prog-name) (phox-prog-flags-erase)) - (t (error "option must be empty or -f, use phox-prog-flags-modify."))) -) - -;; commands - -; compilation -(defun phox-compile-theorem(name) - "Interactive function : -ask for the name of a theorem and send a compile command to PhoX for it." - (interactive "stheorem : ") - (proof-shell-invisible-command (concat "compile " name))) - -(defun phox-compile-theorem-on-cursor() -"Interactive function : -send a compile command to PhoX for the theorem which name is under the cursor." - (interactive) - (let (start end) - (save-excursion -; (modify-syntax-entry ?\. "w") - (forward-word 1) - (setq start (point)) - (forward-word -1) - (setq end (point))) - (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1))) - (phox-compile-theorem (buffer-substring start end)))) - -; extraction - -(defun phox-output () - -"Interactive function : -send output command to phox in order to obtain programs -extracted from proofs of all compiled theorems." - - -(interactive) -(proof-shell-invisible-command "output")) - -(defun phox-output-theorem (name) -"Interactive function : -ask for the name of a theorem and send an output command to PhoX for it -in order to obtain a programm extracted from the known proof of this theorem." - (interactive "stheorem : ") - (proof-shell-invisible-command (concat "output " name))) - -(defun phox-output-theorem-on-cursor() -"Interactive function : -send an output command to PhoX for the theorem which name is under the cursor -in order to obtain a programm extracted from the known proof of this theorem." - (interactive) - (let (start - end -; (syntax (char-to-string (char-syntax ?\.))) - ) - (save-excursion -; (modify-syntax-entry ?\. "w") ; à modifier globablement ? - (forward-word 1) - (setq start (point)) - (forward-word -1) - (setq end (point))) -; (modify-syntax-entry ?\. syntax) - (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1))) - (phox-output-theorem (buffer-substring start end)))) - -; Definitions of lambda-mu terms (tdef nom_de_term = terme.) and -; normalization (eval term.) have to be "visible" proof commands. - -;; menu - - (defvar phox-extraction-menu - '("Extraction" - ["Program extraction enabled" - phox-toggle-extraction - :style radio - :selected(string-match "\-f$" phox-prog-name) - ] - ["------------------------------" nil nil - ] - ["Compile theorem on cursor" phox-compile-theorem-on-cursor - :active(string-match "\-f$" phox-prog-name) - ] - ["Extraction for theorem on cursor" phox-output-theorem-on-cursor - :active(string-match "\-f$" phox-prog-name) - ] - ["Extraction for all compiled theorems" phox-output - :active(string-match "\-f$" phox-prog-name) - ] - ["------------------------------" nil nil - ] - ["Compile theorem : " phox-compile-theorem - :active(string-match "\-f$" phox-prog-name) - ] - ["Extraction for theorem : " phox-output-theorem - :active(string-match "\-f$" phox-prog-name) - ] - ) -"A list of menu items to deal with program extraction. -Warning, program extraction is still experimental -and can disturb the prover !" -) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(provide 'phox-extraction) diff --git a/phox/phox-font.el b/phox/phox-font.el deleted file mode 100644 index 3e86dd28..00000000 --- a/phox/phox-font.el +++ /dev/null @@ -1,102 +0,0 @@ -(defvar phox-sym-lock-enabled nil) ; da: for clean compile -(defvar phox-sym-lock-color nil) ; da: for clean compile -(defvar phox-sym-lock-keywords nil) ; da: for clean compile -(declare-function phox-sym-lock "phox-sym-lock") - -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; Font lock keywords -;;--------------------------------------------------------------------------;; - -(defconst phox-font-lock-keywords - (list -;commands - '("(\\*\\([^*]\\|\\*+[^*)]\\)*\\(\\*+)\\|\\**$\\)" - 0 'font-lock-comment-face t) - '("\"\\([^\\\"]\\|\\\\.\\)*\"" - 0 'font-lock-string-face t) - (cons (concat "\\([ \t]\\|^\\)\\(" - "Cst\\|" - "Data\\|" - "I\\(mport\\|nductive\\)\\|" - "Use\\|" - "Sort\\|" - "new_\\(intro\\|e\\(lim\\|quation\\)\\|rewrite\\)\\|" - "a\\(dd_path\\|uthor\\)\\|" - "c\\(l\\(aim\\|ose_def\\)\\|or\\(ollary\\)?\\)\\|" - "d\\(e\\(f\\(\\(_thlist\\|rec\\)\\)?\\|l\\(_proof\\)\\)\\|ocuments\\|epend\\)\\|" - "e\\(lim_after_intro\\|xport\\|del\\|show\\)\\|" - "f\\(act\\|lag\\)\\|" - "goal\\|" - "in\\(clude\\|stitute\\)\\|" - "lem\\(ma\\)?\\|" - "p\\(ath\\|r\\(int\\(_sort\\)?\\|iority\\|op\\(osition\\)?\\|ove_claim\\)\\)\\|" - "quit\\|" - "s\\(ave\\|earch\\)\\|" - "t\\(ex\\(_syntax\\)?\\|heo\\(rem\\)?\\|itle\\|ype\\)" - "\\)[ \t\n\r.]") - '(0 'font-lock-keyword-face t)) -;proof command - (cons (concat "\\([ \t]\\|^\\)\\(" - "a\\(bort\\|fter\\|nd\\|pply\\|ssume\\|xiom\\)\\|" - "by\\(_absurd\\)?\\|" - "constraints\\|" - "elim\\|" - "deduce\\|" - "evaluate\\(_hyp\\)?\\|" - "from\\|" - "goals\\|" - "in\\(tros?\\|stance\\)\\|" - "l\\(oc\\(al\\|k\\)\\|e\\(t\\|fts?\\)\\)\\|" - "next\\|" - "of\\|" - "prove\\|" - "r\\(e\\(write\\(_hyp\\)?\\|name\\)\\|mh\\)\\|" - "s\\(elect\\|how\\|lh\\)\\|" - "t\\(hen\\|rivial\\)\\|" - "u\\(se\\|n\\(do\\|fold\\(_hyp\\)?\\|lock\\)\\)\\|" - "with" - "\\)[ \t.]") - '(0 'font-lock-type-face t)))) -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; phox-sym-lock tables -;;--------------------------------------------------------------------------;; - -(if (featurep 'xemacs) (require 'phox-sym-lock)) - -;; to change this table, xfd -fn '-adobe-symbol-*--12-*' may be -;; used to determine the symbol character codes. -(defconst phox-sym-lock-keywords-table - '((">=" 0 1 179) - ("<=" 0 1 163) - ("!=" 0 1 185) - (":<" 0 1 206) - ("[^:]\\(:\\)[^:= \n\t\r]" 1 7 206) - ("\\\\/" 0 1 36) - ("/\\\\" 0 1 34) - ("\\<or\\>" 0 3 218) - ("\\<in\\>" 0 3 206) - ("\\<notin\\>" 0 4 207) - ("\\<inter\\>" 0 3 199) - ("\\<union\\>" 0 3 200) - ("\\<minus\\>" 0 3 45) - ("&" 0 1 217) - ("<->" 0 1 171) - ("=>" 0 1 222) - ("\\<subset\\>" 0 4 204) - ("->" 0 1 174) - ("~" 0 1 216) - ("\\\\" 0 1 108))) -; "If non nil: Overrides default Phox-Sym-Lock patterns for PhoX.") - -(defun phox-sym-lock-start () - (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled) - (progn - (setq phox-sym-lock-color - (face-foreground 'font-lock-function-name-face)) - (if (not phox-sym-lock-keywords) - (phox-sym-lock phox-sym-lock-keywords-table))))) - - -(provide 'phox-font) diff --git a/phox/phox-fun.el b/phox/phox-fun.el deleted file mode 100644 index 08f46c96..00000000 --- a/phox/phox-fun.el +++ /dev/null @@ -1,440 +0,0 @@ -;; $State$ $Date$ $Revision$ -;; syntax - -(require 'span) -(require 'proof-syntax) -(require 'proof-script) - -(eval-when-compile - (require 'proof-utils)) - -(defconst phox-forget-id-command "del %s.\n") -(defconst phox-forget-proof-command "del_proof %s.\n") -(defconst phox-forget-new-elim-command "edel elim %s.\n") -(defconst phox-forget-new-intro-command "edel intro %s.\n") -(defconst phox-forget-new-equation-command "edel equation %s.\n") -(defconst phox-forget-close-def-command "edel closed %s.\n") -; phox-comments-regexp : a sequence of comments and white spaces -(defconst phox-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*") -; phox-strict-comments-regexp : a not empty sequence of comments and white spaces -(defconst phox-strict-comments-regexp "\\([ \n\t\r]+\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*\\|\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)+\\)") -(defconst phox-ident-regexp "\\(\\([^() \n\t\r=\\[.]\\|\\(\\.[^() \n\t\r]\\)\\)+\\)") -(defconst phox-inductive-option "\\(\\[[^]]*]\\)?") -(defconst phox-spaces-regexp "[ \n\t\r]*") -(defconst phox-sy-definition-regexp (concat - "\\(Cst\\|\\(def\\(rec\\)?\\)\\)" - phox-comments-regexp - "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)")) -(defconst phox-sy-inductive-regexp (concat - "Inductive" - phox-comments-regexp - phox-inductive-option - phox-comments-regexp - "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)")) -(defconst phox-inductive-regexp (concat - "Inductive" - phox-comments-regexp - phox-inductive-option - phox-comments-regexp - phox-ident-regexp)) -(defconst phox-data-regexp (concat - "\\(Data\\|type\\)" - phox-comments-regexp - phox-inductive-option - phox-comments-regexp - phox-ident-regexp)) -(defconst phox-definition-regexp (concat - "\\(Cst\\|def\\(_thlist\\|rec\\)?\\|claim\\|Sort\\)" - phox-comments-regexp - phox-ident-regexp)) -(defconst phox-prove-claim-regexp (concat - "prove_claim" - phox-comments-regexp - phox-ident-regexp)) -(defconst phox-new-elim-regexp (concat - "new_elim\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - phox-ident-regexp)) -(defconst phox-new-intro-regexp (concat - "new_intro\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - phox-ident-regexp)) -(defconst phox-new-rewrite-regexp (concat - "new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - phox-ident-regexp)) -(defconst phox-new-equation-regexp (concat - "new_equation\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - phox-ident-regexp)) -(defconst phox-close-def-regexp (concat - "close_def" - phox-comments-regexp - "\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]")) - -(defun phox-init-syntax-table (&optional TABLE) - "Set appropriate values for syntax table in current buffer, -or for optional argument TABLE." -;; useful for using forward-word - (modify-syntax-entry ?_ "w" TABLE) - (modify-syntax-entry ?\. "w" TABLE) -;; Configure syntax table for block comments - (modify-syntax-entry ?\* ". 23" TABLE) - (modify-syntax-entry ?\( "()1" TABLE) - (modify-syntax-entry ?\) ")(4" TABLE) -;; à compléter éventuellement -) - - -;; completions : - -(defvar phox-top-keywords -'( -"goal" -"restart" -"quit" -"theorem" -"claim" -"cst" -"Cst" -"def" -"def_thlist" -"del" -"del_proof" -"Sort" -"close_def" -"edel" -"new_elim" -"new_intro" -"new_equation" -"new_rewrite" -"Data" -"type" -"Inductive" -"add_path" -"Import" -"include" -"Use" -"tex_syntax" -"depend" -"eshow" -"flag" -"path" -"print" -"print_sort" -"priority" -"prove_claim" -"search" -"compile" -"tdef" -"eval" -"output" -"compile" -"compute" -"Local" -) -"Names of phox top commands." -) - -(defvar phox-proof-keywords -'( -"axiom" -"elim" -"intro" -"intros" -"apply" -"by_absurd" -"from" -"left" -"lefts" -"prove" -"use" -"auto" -"trivial" -"rewrite" -"rewrite_hyp" -"unfold" -"unfold_hyp" -"constraints" -"instance" -"lock" -"unlock" -"goals" -"after" -"next" -"select" -"local" -"rename" -"rmh" -"slh" -"abort" -"save" -"undo" -"Try" -) -"Name of phox proof commands." -) - - - -(defun phox-find-and-forget (span) - (let (str ans tmp (lsp -1) name sname) ;; da: added name,sname. are tmp/lsp not used? - (while span - (setq str (span-property span 'cmd)) - - (cond - - ((eq (span-property span 'type) 'comment)) - - ((eq (span-property span 'type) 'proverproc)) - - ((eq (span-property span 'type) 'goalsave) - (if (proof-string-match phox-prove-claim-regexp str) - (setq ans (concat (format phox-forget-proof-command - (match-string 4 str)) ans)) - (setq ans (concat (format phox-forget-id-command - (span-property span 'name)) ans)))) - - ((proof-string-match phox-new-elim-regexp str) - (setq ans - (concat (format phox-forget-new-elim-command - (match-string 3 str)) ans))) - - ((proof-string-match phox-new-intro-regexp str) - (setq ans - (concat (format phox-forget-new-intro-command - (match-string 3 str)) ans))) - - ((proof-string-match phox-new-rewrite-regexp str) ; deprecated - (setq ans - (concat (format phox-forget-new-equation-command - (match-string 3 str)) ans))) - - ((proof-string-match phox-new-equation-regexp str) - (setq ans - (concat (format phox-forget-new-equation-command - (match-string 3 str)) ans))) - - ((proof-string-match phox-close-def-regexp str) - (setq ans - (concat (format phox-forget-close-def-command - (match-string 4 str)) ans))) - - ((proof-string-match phox-sy-definition-regexp str) - (setq ans - (concat (format phox-forget-id-command - (concat "$" (match-string 7 str))) ans))) - - ((proof-string-match phox-sy-inductive-regexp str) - (setq ans - (concat (format phox-forget-id-command - (concat "$" (match-string 10 str))) ans))) - - ((proof-string-match phox-inductive-regexp str) - (setq ans - (concat (format phox-forget-id-command - (match-string 8 str)) ans))) - - ((proof-string-match phox-data-regexp str) - (setq - name (match-string 8 str) - sname (concat (downcase (substring name 0 1)) - (substring name 1 nil)) - ans (concat (format phox-forget-id-command - sname) ans))) - - ((proof-string-match phox-definition-regexp str) - (setq ans (concat (format phox-forget-id-command - (match-string 6 str)) ans)))) - - (setq lsp (span-start span)) - (setq span (next-span span 'type))) - - (when ans (list ans)))) ; was (or ans proof-no-command) - -;; -;; Doing commands -;; - -(defalias 'phox-assert-next-command-interactive 'proof-assert-next-command-interactive) -;; da: might be able to achieve commented out effect with proof-electric-terminator-noterminator -;; "Process until the end of the next unprocessed command after point. -;; If inside a comment, just process until the start of the comment." -;; (interactive) -;; ; (if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n")) -;; (proof-with-script-buffer -;; (goto-char (proof-queue-or-locked-end)) -;; (proof-assert-next-command) -;; (proof-maybe-follow-locked-end))) - -;;--------------------------------------------------------------------------;; -;; Obtaining some informations on the system. -;; -;;--------------------------------------------------------------------------;; -;; All the commands in section "Obtaining some informations on the -;; system." (see cmd_top.tex) are associated to a -;; function, and appear in the submenu "State" [pr]. - -(defun phox-depend-theorem(theorem) - "Interactive function : -ask for a string and and send a depend command to PhoX for it. - -Gives the list of all axioms which have been used to prove the theorem." - -(interactive "stheorem: ") -(proof-shell-invisible-command (concat "depend " theorem))) - -(defun phox-eshow-extlist(extlist) - "Interactive function : -ask for a string and send an eshow command to PhoX for it. - -Shows the given extension-list. Possible extension lists are : equation -(the list of equations added to unification introduced by the new_equation -command), elim, intro, (the introduction and elimination rules -introduced by the new_elim and new_intro {-t} commands), closed -(closed definitions introduced by the close_def command) and tex -(introduced by the tex_syntax command)." - -(interactive "sextension list: ") -(proof-shell-invisible-command (concat "eshow " extlist))) - -(defun phox-flag-name(name) -"Interactive function : -ask for a string and send a flag command to PhoX for it. - - Print the value of an internal flag of the - system. The different flags are listed in the doc, see flag." - -(interactive "sname: ") -(proof-shell-invisible-command (concat "flag " name))) - - -(defun phox-path() -"Interactive function : - send a path command to PhoX. - - Prints the list of all paths. This path list is used to find - files when using the include command." - - -(interactive) -(proof-shell-invisible-command "path")) - -(defun phox-print-expression(expr) -"Interactive function : -ask for a string and send a print command to PhoX for it. - - In case argument expr - is a closed expression of the language in use, prints it and gives its - sort, gives an (occasionally) informative error message otherwise. In - case expr is a defined expression (constant, theorem ...) - gives the definition." - -(interactive "sexpr: ") -(proof-shell-invisible-command (concat "print " expr))) - -(defun phox-print-sort-expression(expr) -"Interactive function : -ask for a string and send a print_sort command to PhoX for it. - - Similar to print, but gives more information on sorts of bounded - variable in expressions." - -(interactive "sexpr: ") -(proof-shell-invisible-command (concat "print_sort " expr))) - - -(defun phox-priority-symbols-list(symblist) -"Interactive function : -ask for a string and send a priority command to PhoX for it. - - Print the priority of the given symbols. If no symbol are - given, print the priority of all infix and prefix symbols. -." - -(interactive "slist of symbols (possibly empty): ") -(proof-shell-invisible-command (concat "priority" symblist))) - - -(defun phox-search-string(string type) - "Interactive function: -ask for a string and possibly a type and send a search command to PhoX for it. - - Prints the list of all loaded symbols which have type and whose name - contains the string. If no type is given, it prints all symbols whose - name contains string." - -(interactive -"sstring : -stype (nothing for any type, 'a as type parameter) :") -(proof-shell-invisible-command (concat "search \"" string "\" " type))) - -;; The followings are proof commands (doc in cmd_proof.tex) : - -(defun phox-constraints() -"Interactive function : - send a constraints command to PhoX. - - Prints the constraints which should be fulfilled by unification variables, - only works in proofs." - - -(interactive) -(proof-shell-invisible-command "constraints")) - -(defun phox-goals() -"Interactive function : - send a goals command to PhoX. - - Prints the list of all remaining goals, only works in proofs." - - -(interactive) -(proof-shell-invisible-command "goals")) - -;; menu - -(defvar phox-state-menu - '("State" -["dependencies of a theorem" phox-depend-theorem t] -["show an extension list" phox-eshow-extlist t] -["value of a flag" phox-flag-name t] -["list of all paths" phox-path t] -["print expression" phox-print-expression t] -["print expression with sorts" phox-print-sort-expression t] -["priority of symbols (all if arg. empty)" phox-priority-symbols-list t] -["search for loaded symbols matching string" phox-search-string t] -["------------------" nil nil] -["constraints (proof command)" phox-constraints t] -["goals (proof command)" phox-goals t] -) -"Phox menu for informations on state of the system." -) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;;--------------------------------------------------------------------------;; -;; -;; Deleting symbols -;; -;;--------------------------------------------------------------------------;; -;; obsolète probablement, sinon à modifier pour en étendre la portée. - -(defun phox-delete-symbol(symbol) - "Interactive function : -ask for a symbol and send a delete command to PhoX for it." - (interactive "ssymbol : ") - (proof-shell-invisible-command (concat "del " symbol))) - -(defun phox-delete-symbol-on-cursor() -"Interactive function : -send a delete command to PhoX for the symbol whose name is under the cursor." - (interactive) - (let (start end) - (save-excursion - (forward-word -1) - (setq start (point)) - (forward-word 1) - (setq end (point))) - (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1))) - (phox-delete-symbol (buffer-substring start end)))) - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(provide 'phox-fun) diff --git a/phox/phox-lang.el b/phox/phox-lang.el deleted file mode 100644 index dc6ad9ed..00000000 --- a/phox/phox-lang.el +++ /dev/null @@ -1,64 +0,0 @@ -;; $State$ $Date$ $Revision$ -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; messages in various languages - -(provide 'phox-lang) -(require 'cl) ; for case - -(defvar phox-lang - (let* ((s (or (getenv "LC_ALL") - (getenv "LANG") - (getenv "LANGUAGE"))) - (loc (and s - (> (length s) 1) - (substring s 0 2)))) - (cond - ((or (string= loc "en") (string= loc "us")) 'en) - ((string= loc "fr") 'fr) - (t 'en)))) - -(defun phox-lang-absurd () - (case phox-lang - (en "By absurd") - (fr "Par l'absurde"))) - -(defun phox-lang-suppress (s) - (case phox-lang - (en (concat "Remove hypothesis " s " (if it became useless)")) - (fr (concat "Supprimer l'hypothèse " s " (si elle est devenue inutile)")))) - -(defun phox-lang-opendef () - (case phox-lang - (en "Expand the definition: ") - (fr "Ouvre la définition : "))) - -(defun phox-lang-instance (s) - (case phox-lang - (en (concat "Choose " s " = ")) - (fr (concat "Choisissons " s " = ")))) - -(defun phox-lang-open-instance (s) - (case phox-lang - (en (concat "Choose " s " = \\[ \\]")) - (fr (concat "Choisissons " s " = \\[ \\]")))) - -(defun phox-lang-lock (s) - (case phox-lang - (en (concat "Lock variable " s)) - (fr (concat "Vérouille la variable " s)))) - -(defun phox-lang-unlock (s) - (case phox-lang - (en (concat "Unlock variable " s)) - (fr (concat "Dévérouille la variable " s)))) - -(defun phox-lang-prove (s) - (case phox-lang - (en (concat "Let us prove \\[" s "\\]")) - (fr (concat "Prouvons \\[" s "\\]")))) - -(defun phox-lang-let (s) - (case phox-lang - (en (concat "Let \\[ \\] = \\[" s "\\]")) - (fr (concat "Définissons \\[ \\] = \\[" s "\\]")))) diff --git a/phox/phox-outline.el b/phox/phox-outline.el deleted file mode 100644 index 7ee2710f..00000000 --- a/phox/phox-outline.el +++ /dev/null @@ -1,69 +0,0 @@ -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; PARAMÉTRAGE du MODE outline -;;--------------------------------------------------------------------------;; - -(require 'outline) - -(declare-function phox-lang-absurd "nofile") -(declare-function phox-lang-suppress "nofile") -(declare-function phox-lang-instance "nofile") -(declare-function phox-lang-open-instance "nofile") -(declare-function phox-lang-opendef "nofile") -(declare-function phox-lang-unlock "nofile") -(declare-function phox-lang-lock "nofile") -(declare-function phox-lang-prove "nofile") -(declare-function phox-lang-let "nofile") - - -(defconst phox-outline-title-regexp "\\((\\*[ \t\n]*title =\\)") -(defconst phox-outline-section-regexp "\\((\\*\\*+\\)") -(defconst phox-outline-save-regexp "\\((\\*#\\)") -(defconst - phox-outline-theo-regexp - "\\((\\*lem\\)\\|\\((\\*prop\\)\\|\\((\\*fact\\)\\|\\((\\*theo\\)\\|\\((\\*def\\)\\|\\((\\*cst\\)") -(defconst - phox-outline-theo2-regexp - "\\(lem\\)\\|\\(prop\\)\\|\\(fact\\)\\|\\(theo\\)\\|\\(def\\)\\|\\(cst\\)\\|\\(claim\\)\\|\\(new_\\)") - -(defconst - phox-outline-regexp - (concat - phox-outline-title-regexp "\\|" - phox-outline-section-regexp "\\|" - phox-outline-save-regexp "\\|" - phox-outline-theo-regexp "\\|" - phox-outline-theo2-regexp)) - -(defconst phox-outline-heading-end-regexp "\\(\\*)[ \t]*\n\\)\\|\\(\\.[ \t]*\n\\)") - -;;(if phox-outline -;; (add-hook 'phox-mode-hook (lambda () (outline-minor-mode 1))) -;; ) - -(defun phox-outline-level() - "Find the level of current outline heading in some PhoX libraries." - (let ((retour 0)) - (save-excursion - (cond ((looking-at phox-outline-title-regexp) 1) - ((looking-at phox-outline-section-regexp) - (min 6 (- (match-end 0) (match-beginning 0)))) ; valeur maxi 6 - ((looking-at phox-outline-theo-regexp) 7) - ((looking-at (concat phox-outline-save-regexp "\\|" - phox-outline-theo2-regexp ) - ) 8) - ) - ))) - -(defun phox-setup-outline () - "Set up local variable for outline mode" - (make-local-variable 'outline-heading-end-regexp) - (setq outline-heading-end-regexp phox-outline-heading-end-regexp) - (make-local-variable 'outline-regexp) - (setq outline-regexp phox-outline-regexp) - (make-local-variable 'outline-level) - (setq outline-level 'phox-outline-level) - (outline-minor-mode 1) -) - -(provide 'phox-outline) diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el deleted file mode 100644 index 544fa1c4..00000000 --- a/phox/phox-pbrpm.el +++ /dev/null @@ -1,318 +0,0 @@ -;; $State$ $Date$ $Revision$ -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; the proof by rules popup menu part -;; -;; Note : program extraction is still experimental This file is very -;; dependant of the actual state of our developments -;;--------------------------------------------------------------------------;; - -(require 'pg-pbrpm) - -(declare-function phox-lang-absurd "nofile") -(declare-function phox-lang-suppress "nofile") -(declare-function phox-lang-instance "nofile") -(declare-function phox-lang-open-instance "nofile") -(declare-function phox-lang-opendef "nofile") -(declare-function phox-lang-unlock "nofile") -(declare-function phox-lang-lock "nofile") -(declare-function phox-lang-prove "nofile") -(declare-function phox-lang-let "nofile") -(declare-function int-char "nofile") -(declare-function char= "nofile") - -;;--------------------------------------------------------------------------;; -;; Syntactic functions -;;--------------------------------------------------------------------------;; -(setq - pg-pbrpm-start-goal-regexp "^goal \\([0-9]+\\)/[0-9]+\\( (new)\\)?$" - pg-pbrpm-start-goal-regexp-par-num 1 - pg-pbrpm-end-goal-regexp "^$" - pg-pbrpm-start-hyp-regexp "^\\([A-Za-z0-9_.']+\\) := " - pg-pbrpm-start-hyp-regexp-par-num 1 - pg-pbrpm-start-concl-regexp "^ *|- " - pg-pbrpm-auto-select-regexp "\\(\\(\\(['a-zA-Z0-9]+\\)\\|\\([][><=/~&+*^%!{}:-]+\\)\\)\\(_+\\(\\(['a-zA-Z0-9]+\\)\\|\\([][><=/~&+*^%!{}:-]+\\)\\)\\)*\\)\\|\\(\\?[0-9]+\\)" -) - - -; TODO : deal with future invisible parentheses (french guillemots) -(defun phox-pbrpm-left-paren-p (char) -"Retrun t if the character is a left parenthesis : '(' or a french guillemot '<<'" - (or - (char-equal char (int-char 40)) - (char-equal char (int-char 171))) -) - -(defun phox-pbrpm-right-paren-p (char) -"Retrun t if the character is a right parenthesis ')' or a french guillemot '>>'" - (or - (char-equal char (int-char 41)) - (char-equal char (int-char 187))) -) - - -(defun phox-pbrpm-menu-from-string (order str) - "build a menu from a string send by phox" - (setq str (proof-shell-invisible-cmd-get-result str)) - (if (string= str "") nil - (mapcar - (lambda (s) (append (list order) (split-string s "\\\\-") - (list 'phox-pbrpm-rename-in-cmd))) - (split-string str "\\\\\\\\")))) - -(defun phox-pbrpm-rename-in-cmd (cmd spans) - (let ((modified nil) (prev 0)) - (mapc (lambda (span) - (if (not (string= (span-property span 'original-text) - (span-string span))) - (setq modified (cons span modified)))) spans) - (setq modified (reverse modified)) - (if modified - (progn - (if (= 0 (span-property (car modified) 'goalnum)) - (progn - (while (and modified (= 0 (span-property (car modified) 'goalnum))) - (let ((span (pop modified))) - (setq cmd (concat cmd ";; rename " - (span-property span 'original-text) " " - (span-string span))))) - (if modified (setq cmd (concat "(" cmd ")"))))) - (if modified (setq cmd (concat cmd ";; "))) - (while modified - (let* ((span (pop modified)) - (goalnum (span-property span 'goalnum))) - (while (< (+ prev 1) goalnum) - (setq cmd (concat cmd "idt @+@ ")) - (setq prev (+ prev 1))) - (setq cmd (concat cmd "(rename " (span-property span 'original-text) " " - (span-string span))) - (setq prev goalnum) - (if (or (not modified) (< goalnum (span-property (car modified) 'goalnum))) - (setq cmd (concat cmd ") @+@ ")) - (setq cmd (concat cmd ";; "))))) - (if (> prev 0) (setq cmd (concat cmd "idt")))))) - cmd) - -(defun phox-pbrpm-get-region-name (region-info) - (if (= (nth 0 region-info) 1) (nth 1 region-info) (nth 2 region-info))) - -(defun phox-pbrpm-escape-string (str) - "add escape char '\'" - (concat "\"" (replace-regexp-in-string "\\\\" "\\\\\\\\" str) "\"")) - -(defun phox-pbrpm-generate-menu (click-infos region-infos) -"Use informations to build a list of (name , rule)" - ;click-infos = (goal-number, "whole"/hyp-name/"none", expression, depth-tree-list) - ;region-infos = idem if in the goal buffer, (0, "none", expression, nil ) if in another buffer, do not display if no region available. - - (let - ((pbrpm-rules-list nil) - (goal-prefix - (if (= (nth 0 click-infos) 1) "" - (concat "[" - (int-to-string (nth 0 click-infos)) - "] ")))) - - - ; the first goal is the selected one by default, so we prefer not to display it. - - ; if clicking in a conclusion with no selection - (if (and (string= (nth 1 click-infos) "none") (not region-infos)) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list - (list 4 (phox-lang-absurd) (concat goal-prefix "by_absurd;; elim False"))) - (phox-pbrpm-menu-from-string 0 - (concat "menu_intro " - (int-to-string (nth 0 click-infos)))) - (phox-pbrpm-menu-from-string 0 - (concat "menu_evaluate " - (int-to-string (nth 0 click-infos)))) - ); end append - );end setq - );end if - - ; if clicking a conclusion with a selection - (if (and (string= (nth 1 click-infos) "none") region-infos) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (phox-pbrpm-menu-from-string 0 - (concat "menu_intro " - (int-to-string (nth 0 click-infos)) - (let ((tmp "")) - (mapc (lambda (region-info) - (setq tmp - (concat tmp " " (phox-pbrpm-escape-string (nth 2 region-info))))) - region-infos) - tmp))) - (phox-pbrpm-menu-from-string 1 - (concat "menu_rewrite " - (int-to-string (nth 0 click-infos)) " " - (let ((tmp "")) - (mapc (lambda (region-info) - (setq tmp - (concat tmp " " (phox-pbrpm-escape-string (phox-pbrpm-get-region-name region-info))))) - region-infos) - tmp)))))) - - ; if clicking in an hypothesis with no selection - (if (and - (not (or (string= (nth 1 click-infos) "none") - (string= (nth 1 click-infos) "whole"))) - (or (string= "" (nth 2 click-infos)) (not (char= (string-to-char (nth 2 click-infos)) ??))) - (not region-infos)) - (let ((r (proof-shell-invisible-cmd-get-result (concat "is_hypothesis " - (int-to-string (nth 0 click-infos)) - " " - (phox-pbrpm-escape-string (nth 1 click-infos)))))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (if (char= (string-to-char r) ?t) - (list - (list 9 (phox-lang-suppress (nth 1 click-infos)) - (concat "[" (int-to-string (nth 0 click-infos)) "] " - "rmh " (nth 1 click-infos)))) - nil) - (phox-pbrpm-menu-from-string 1 - (concat "menu_elim " - (int-to-string (nth 0 click-infos)) " " - (nth 1 click-infos))) - (phox-pbrpm-menu-from-string 1 - (concat "menu_evaluate_hyp " - (int-to-string (nth 0 click-infos)) " " - (nth 1 click-infos))) - (phox-pbrpm-menu-from-string 0 - (concat "menu_left " - (int-to-string (nth 0 click-infos)) - " " - (nth 1 click-infos))))))) - - ; if clicking on an hypothesis with a selection - (if (and - (not (or (string= (nth 1 click-infos) "none") - (string= (nth 1 click-infos) "whole"))) - region-infos) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (phox-pbrpm-menu-from-string 1 - (concat "menu_apply " - (int-to-string (nth 0 click-infos)) " " - (nth 1 click-infos) - (let ((tmp "")) - (mapc (lambda (region-info) - (setq tmp - (concat tmp " " (phox-pbrpm-escape-string (nth 2 region-info))))) - region-infos) - tmp))) - (phox-pbrpm-menu-from-string 1 - (concat "menu_rewrite_hyp " - (int-to-string (nth 0 click-infos)) " " - (nth 1 click-infos) - (let ((tmp "")) - (mapc (lambda (region-info) - (setq tmp - (concat tmp " " (phox-pbrpm-escape-string (phox-pbrpm-get-region-name region-info))))) - region-infos) - tmp)))))) - - (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??) - region-infos (not (cdr region-infos))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 0 (concat - (phox-lang-instance (nth 2 click-infos)) - (nth 2 (car region-infos))) - (concat - "instance " - (nth 2 click-infos) - " " - (nth 2 (car region-infos)))))))) - - (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??) - (not region-infos)) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 0 (concat - (phox-lang-open-instance (nth 2 click-infos))) - (concat - "instance " - (nth 2 click-infos) - " ") - (lambda (cmd spans) - (let ((span (pop spans))) - (concat cmd " " (span-string span))))))))) - - ; is clicking on a token with no selection - (if (and (not region-infos) (not (string= (nth 2 click-infos) ""))) - (let ((r (proof-shell-invisible-cmd-get-result (concat "is_definition " - (int-to-string (nth 0 click-infos)) - " " - (phox-pbrpm-escape-string (nth 2 click-infos))))) - (ri (proof-shell-invisible-cmd-get-result (concat "is_definition " - (int-to-string (nth 0 click-infos)) - " " - (phox-pbrpm-escape-string (concat "$" (nth 2 click-infos))))))) - (if (or (char= (string-to-char r) ?t) (char= (string-to-char ri) ?t)) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 1 (concat - (phox-lang-opendef) - (nth 2 click-infos)) - (concat - goal-prefix - (if (or (string= (nth 1 click-infos) "none") - (string= (nth 1 click-infos) "whole")) - "unfold -ortho " - (concat "unfold_hyp " (nth 1 click-infos) " -ortho ")) - "$" - (nth 2 click-infos)))))) - (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??)) - (let ((r (proof-shell-invisible-cmd-get-result (concat "is_locked " - (nth 2 click-infos))))) - (if (char= (string-to-char r) ?t) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 0 (phox-lang-unlock (nth 2 click-infos)) - (concat - goal-prefix - "unlock " - (nth 2 click-infos)))))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 0 (phox-lang-lock (nth 2 click-infos)) - (concat - goal-prefix - "lock " - (nth 2 click-infos)))))))))))) - - (let ((arg (if (and region-infos (not (cdr region-infos))) (nth 2 (car region-infos)) " "))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list - (list 10 "Trivial ?" (concat goal-prefix "trivial")) - (list 10 (phox-lang-prove arg) (concat goal-prefix "prove") - (lambda (cmd spans) - (let ((span (pop spans))) - (concat cmd " " (span-string span))))) - (list 10 (phox-lang-let arg) (concat goal-prefix "local") - (lambda (cmd spans) - (let ((span1 (pop spans)) (span2 (pop spans))) - (concat cmd " " (span-string span1) " = "(span-string span2))))))))) - - pbrpm-rules-list -)) - - -;;--------------------------------------------------------------------------;; -;; phox specific functions -;;--------------------------------------------------------------------------;; - -(defalias 'proof-pbrpm-generate-menu 'phox-pbrpm-generate-menu) -(defalias 'proof-pbrpm-left-paren-p 'phox-pbrpm-left-paren-p) -(defalias 'proof-pbrpm-right-paren-p 'phox-pbrpm-right-paren-p) - -;;--------------------------------------------------------------------------;; - -(require 'phox-lang) -(provide 'phox-pbrpm) -;; phox-pbrpm ends here diff --git a/phox/phox-sym-lock.el b/phox/phox-sym-lock.el deleted file mode 100644 index ef3a9273..00000000 --- a/phox/phox-sym-lock.el +++ /dev/null @@ -1,401 +0,0 @@ -;; phox-sym-lock.el --- Extension of Font-Lock mode for symbol fontification. - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Copyright © 1997-1998 Albert Cohen, all rights reserved. -;; Copying is covered by the GNU General Public License. -;; -;; This program is free software; you can redistribute it and/or modify -;; it under the terms of the GNU General Public License as published by -;; the Free Software Foundation; either version 2 of the License, or -;; (at your option) any later version. -;; -;; This program is distributed in the hope that it will be useful, -;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -;; GNU General Public License for more details. - -(require 'proof-compat) ; avoid compile warnings - -(defcustom phox-sym-lock-enabled t - "*Whether to use yum symbol or not." - :type 'boolean - :group 'phox) - -;; DA: I have crudely hacked this file so that it compiles cleanly. -;; It won't work now, but I hope we can use Unicode Tokens instead. - -(declare-function map-extents "nofile") -(declare-function extent-face "nofile") -(declare-function face-property "nofile") -(declare-function set-extent-endpoints "nofile") -(declare-function extent-start-position "nofile") -(declare-function extent-end-position "nofile") -(declare-function set-extent-property "nofile") -(declare-function face-font-name "nofile") -(declare-function font-name "nofile") -(declare-function char-int "nofile") -(declare-function obj "nofile") -(declare-function set-face-property "nofile") -(declare-function add-menu-button "nofile") - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; History -;; -;; first prototype by wg <wg@cs.tu-berlin.de> 5-96 -;; tweaked by Steve Dunham <dunham@gdl.msu.edu> 5-96 -;; rewritten and enhanced by Albert Cohen <Albert.Cohen@prism.uvsq.fr> 3-97 -;; new symbol-face format and ergonomy improvement by Albert Cohen 2-98 -;; major step towards portability and customization by Albert Cohen 5-98 -;; removed bug with multiple appends in hook by Albert Cohen 3-99 -;; removed phox-sym-lock-face&atom which where not working by C Raffalli 4-2000 - -;; more about symbol font ? check out: xfd -fn '-adobe-symbol-*--12-*' - -(require 'font-lock) -(if (featurep 'xemacs) - (require 'atomic-extents)) ;; not available on GNU Emacs - -(defvar phox-sym-lock-sym-count 0 - "Counter for internal symbols.") - -(defvar phox-sym-lock-ext-start nil "Temporary for atomicization.") -(make-variable-buffer-local 'phox-sym-lock-ext-start) -(defvar phox-sym-lock-ext-end nil "Temporary for atomicization.") -(make-variable-buffer-local 'phox-sym-lock-ext-end) - -(defvar phox-sym-lock-font-size nil - "Default size for Phox-Sym-Lock symbol font.") -(make-variable-buffer-local 'phox-sym-lock-font-size) -(put 'phox-sym-lock-font-size 'permanent-local t) - -(defvar phox-sym-lock-keywords nil - "Similar to `font-lock-keywords'.") -(make-variable-buffer-local 'phox-sym-lock-keywords) -(put 'phox-sym-lock-keywords 'permanent-local t) - -(defvar phox-sym-lock-enabled nil - "Phox-Sym-Lock switch.") -(make-variable-buffer-local 'phox-sym-lock-enabled) -(put 'phox-sym-lock-enabled 'permanent-local t) - -(defvar phox-sym-lock-color (face-foreground 'default) - "*Phox-Sym-Lock default color in `font-lock-use-colors' mode.") -(make-variable-buffer-local 'phox-sym-lock-color) -(put 'phox-sym-lock-color 'permanent-local t) - -(defvar phox-sym-lock-mouse-face 'default - "*Face for symbols when under mouse.") -(make-variable-buffer-local 'phox-sym-lock-mouse-face) -(put 'phox-sym-lock-mouse-face 'permanent-local t) - -(defvar phox-sym-lock-mouse-face-enabled t - "Mouse face switch.") -(make-variable-buffer-local 'phox-sym-lock-mouse-face-enabled) -(put 'phox-sym-lock-mouse-face-enabled 'permanent-local t) - -(defconst phox-sym-lock-with-mule (featurep 'mule) - "Are we using Mule Xemacs ?") - -(defun phox-sym-lock-gen-symbol (&optional prefix) - "Generate a new internal symbol." - ;; where is the standard function to do this ? - (setq phox-sym-lock-sym-count (+ phox-sym-lock-sym-count 1)) - (intern (concat "phox-sym-lock-gen-" (or prefix "") - (int-to-string phox-sym-lock-sym-count)))) - - -(defun phox-sym-lock-make-symbols-atomic (&optional begin end) - "Function to make symbol faces atomic." - (if phox-sym-lock-enabled - (map-extents - (lambda (extent maparg) - (let ((face (extent-face extent)) (ext)) - (if (and face (setq ext (face-property face 'phox-sym-lock-remap))) - (progn - (if (numberp ext) - (set-extent-endpoints - extent (- (extent-start-position extent) ext) - (extent-end-position extent))) - (if ext - (progn - (if phox-sym-lock-mouse-face-enabled - (set-extent-property extent 'mouse-face - phox-sym-lock-mouse-face)) - (set-extent-property extent 'atomic t) - (set-extent-property extent 'start-open t)))))) - nil) - (current-buffer) - (if begin (save-excursion (goto-char begin) (beginning-of-line) (point)) - (point-min)) - (if end (save-excursion (goto-char end) (end-of-line) (point)) - (point-max)) - nil nil))) - -(defun phox-sym-lock-compute-font-size () - "Computes the size of the \"better\" symbol font." - (let ((font-reg (if proof-running-on-win32 - "[^:]*:[^:]*:\\([^:]*\\):[^:]*:[^:]*" - "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*")) - (font-pat (if proof-running-on-win32 - "Symbol:Regular:*::Symbol" - "-adobe-symbol-medium-r-normal--*"))) - (let ( -; face-height is not very good on win32. Why ? - (num (if (and (not proof-running-on-win32) (fboundp 'face-height)) - (face-height 'default) - (let ((str (face-font-name 'default))) - (if - (string-match font-reg str) - (string-to-number (substring str (match-beginning 1) - (match-end 1))))))) - (maxsize 100) (size) (oldsize) - (lf (and (fboundp 'list-fonts) ; da: what is this function? not defined - (list-fonts font-pat)))) - (while (and lf maxsize) - (if - (string-match font-reg - (car lf)) - (let ((str-size (substring (car lf) (match-beginning 1) - (match-end 1)))) - ; test for variable size fonts. Hope it is generic ? - (if (or (equal str-size "*")(equal str-size "")) - (progn - (setq oldsize num) - (setq lf nil)) - (setq size (string-to-number str-size)) - (if (and (> size num) (< size maxsize)) - (setq lf nil) - (setq oldsize size))))) - (setq lf (cdr lf))) - (number-to-string (if (and oldsize (< oldsize maxsize)) oldsize num))))) - -(defvar phox-sym-lock-font-name - (if window-system - (if proof-running-on-win32 - (concat "Symbol:Regular:" - (if phox-sym-lock-font-size phox-sym-lock-font-size - (phox-sym-lock-compute-font-size)) - "::Symbol") - (concat "-adobe-symbol-medium-r-normal--" - (if phox-sym-lock-font-size phox-sym-lock-font-size - (phox-sym-lock-compute-font-size)) - "-*-*-*-p-*-adobe-fontspecific")) - "") - "Name of the font used by Phox-Sym-Lock.") -(make-variable-buffer-local 'phox-sym-lock-font-name) -(put 'phox-sym-lock-font-name 'permanent-local t) - -(make-face 'phox-sym-lock-adobe-symbol-face) -; DA: DISABLED THIS top level form (PG 4.0) -;; (if phox-sym-lock-with-mule -;; (progn -;; (make-charset 'phox-sym-lock-cset-left "Char set for symbol font" -;; (list 'registry "adobe-fontspecific" -;; 'dimension 1 -;; 'chars 94 -;; ;; 'final 53 -;; ;; DA PG 3.7: above line doesn't work on XEmacs 21.5b28, gives -;; ;; Character set already defined for this DIMENSION/CHARS/FINAL/DIRECTION combo (indian-is13194) -;; ;; DA: Will 55 work? -;; 'final 55 -;; 'graphic 0)) -;; (make-charset 'phox-sym-lock-cset-right "Char set for symbol font" -;; (list 'registry "adobe-fontspecific" -;; 'dimension 1 -;; 'chars 94 -;; 'final 54 -;; 'graphic 1)) -;; (set-face-property 'phox-sym-lock-adobe-symbol-face -;; 'font phox-sym-lock-font-name nil -;; ;; DA: removed next line, it breaks "make magic" in doc -;; ;; '(mule-fonts) 'prepend, -;; )) -;; (set-face-font 'phox-sym-lock-adobe-symbol-face phox-sym-lock-font-name 'global)) - -(defun phox-sym-lock-set-foreground () - "Set foreground color of Phox-Sym-Lock faces." - (if (and (boundp 'phox-sym-lock-defaults) phox-sym-lock-defaults) - (let ((l (car phox-sym-lock-defaults)) - (color (if (and (boundp 'font-lock-use-fonts) font-lock-use-fonts) - (face-foreground 'default) phox-sym-lock-color))) - (if (and (consp l) (eq (car l) 'quote)) (setq l (eval l))) - (if (symbolp l) (setq l (eval l))) - (dolist (c l) - (setq c (nth 2 c)) - (if (consp c) (setq c (eval c))) - (if (string-match "-adobe-symbol-" (font-name (face-font c))) - (set-face-foreground c color)))))) - -(defun phox-sym-lock-translate-char (char) - (if phox-sym-lock-with-mule - (let ((code (if (integerp char) char (char-int char)))) - (with-no-warnings ;; da: dynamic scope obj - (if (< code 128) - (make-char 'phox-sym-lock-cset-left obj) - (make-char 'phox-sym-lock-cset-right (- obj 128))))) - char)) - -(defun phox-sym-lock-translate-char-or-string (obj) - (if (stringp obj) - (if phox-sym-lock-with-mule - (concat (mapcar 'phox-sym-lock-translate-char obj)) - (obj)) - (make-string 1 (phox-sym-lock-translate-char obj)))) - -(defun phox-sym-lock-remap-face (pat pos obj atomic) - "Make a temporary face which remaps the POS char of PAT to the -given OBJ under `phox-sym-lock-adobe-symbol-face' and all other characters to -the empty string. OBJ may either be a string or a character." - (let* ((name (phox-sym-lock-gen-symbol "face")) - (table (make-display-table)) - (tface (make-face name))) - (fillarray table "") - (aset table (string-to-char (substring pat (1- pos) pos)) - (phox-sym-lock-translate-char-or-string obj)) - (set-face-foreground tface (if (and (boundp 'font-lock-use-fonts) - font-lock-use-fonts) - (face-foreground 'default) phox-sym-lock-color)) - (set-face-property tface 'display-table table) - (set-face-property tface 'font (face-font 'phox-sym-lock-adobe-symbol-face)) - (set-face-property tface 'phox-sym-lock-remap atomic) ; mark it - tface ; return face value and not face name - ; the temporary face would be otherwise GCed - )) - -(defvar phox-sym-lock-clear-face - (let* ((name (phox-sym-lock-gen-symbol "face")) - (table (make-display-table)) - (tface (make-face name))) - (fillarray table "") - (set-face-property tface 'display-table table) - (set-face-property tface 'phox-sym-lock-remap 1) ; mark it - tface - ;; return face value and not face name - ;; the temporary face would be otherwise GCed - )) - -(defun phox-sym-lock (fl) - "Create font-lock table entries from a list of (PAT NUM POS OBJ) where -PAT (at NUM) is substituted by OBJ under `phox-sym-lock-adobe-symbol-face'. The -face's extent will become atomic." - (message "Computing Phox-Sym-Lock faces...") - (setq phox-sym-lock-keywords (phox-sym-lock-rec fl)) - (setq phox-sym-lock-enabled t) - (message "Computing Phox-Sym-Lock faces... done.")) - -(defun phox-sym-lock-rec (fl) - (let ((f (car fl))) - (if f - (cons (apply 'phox-sym-lock-atom-face f) - (phox-sym-lock-rec (cdr fl)))))) - -(defun phox-sym-lock-atom-face (pat num pos obj &optional override) - "Define an entry for the font-lock table which substitutes PAT (at NUM) by -OBJ under `phox-sym-lock-adobe-symbol-face'. The face extent will become atomic." - (list pat num (phox-sym-lock-remap-face pat pos obj t) override)) - -(defun phox-sym-lock-pre-idle-hook-first () - ;; da: XEmacs isms - ;; (condition-case nil - ;; (if (and phox-sym-lock-enabled font-lock-old-extent) - ;; (setq phox-sym-lock-ext-start (extent-start-position font-lock-old-extent) - ;; phox-sym-lock-ext-end (extent-end-position font-lock-old-extent)) - ;; (setq phox-sym-lock-ext-start nil)) - ;; (error (setq phox-sym-lock-ext-start nil)))) -) - -(defun phox-sym-lock-pre-idle-hook-last () - (condition-case nil - (if (and phox-sym-lock-enabled phox-sym-lock-ext-start) - (phox-sym-lock-make-symbols-atomic phox-sym-lock-ext-start phox-sym-lock-ext-end)) - (error (warn "Error caught in `phox-sym-lock-pre-idle-hook-last'")))) - -(add-hook 'font-lock-after-fontify-buffer-hook - 'phox-sym-lock-make-symbols-atomic) - -(defun phox-sym-lock-enable () - "Enable Phox-Sym-Lock on this buffer." - (interactive) - (if (not phox-sym-lock-keywords) - (error "No Phox-Sym-Lock keywords defined!") - (setq phox-sym-lock-enabled t) - (if font-lock-mode - (progn -; (setq font-lock-keywords nil) ; Font-Lock explicit-defaults bug! - (font-lock-set-defaults) - (font-lock-fontify-buffer))) - (message "Phox-Sym-Lock enabled."))) - -(defun phox-sym-lock-disable () - "Disable Phox-Sym-Lock on this buffer." - (interactive) - (if (not phox-sym-lock-keywords) - (error "No Phox-Sym-Lock keywords defined!") - (setq phox-sym-lock-enabled nil) - (if font-lock-mode - (progn -; (setq font-lock-keywords nil) ; Font-Lock explicit-defaults bug! - (font-lock-set-defaults) - (font-lock-fontify-buffer))) - (message "Phox-Sym-Lock disabled."))) - -(defun phox-sym-lock-mouse-face-enable () - "Enable special face for symbols under mouse." - (interactive) - (setq phox-sym-lock-mouse-face-enabled t) - (if phox-sym-lock-enabled - (font-lock-fontify-buffer))) - -(defun phox-sym-lock-mouse-face-disable () - "Disable special face for symbols under mouse." - (interactive) - (setq phox-sym-lock-mouse-face-enabled nil) - (if phox-sym-lock-enabled - (font-lock-fontify-buffer))) - -(defun phox-sym-lock-font-lock-hook () - "Function called by `font-lock-mode' for initialization purposes." - (add-hook 'pre-idle-hook 'phox-sym-lock-pre-idle-hook-first) - (add-hook 'pre-idle-hook 'phox-sym-lock-pre-idle-hook-last t) - (add-menu-button '("Options" "Syntax Highlighting") - ["Phox-Sym-Lock" - (if phox-sym-lock-enabled (phox-sym-lock-disable) (phox-sym-lock-enable)) - :style toggle :selected phox-sym-lock-enabled - :active phox-sym-lock-keywords] "Automatic") - (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled - font-lock-defaults (boundp 'phox-sym-lock-keywords)) - (progn - (phox-sym-lock-patch-keywords) - (phox-sym-lock-set-foreground)))) - -(defun font-lock-set-defaults (&optional explicit-defaults) - (when - (and - (featurep 'font-lock) - ;; da: font-lock has changed: - ;; (if font-lock-auto-fontify - ;; (not (memq major-mode font-lock-mode-disable-list)) - ;; (memq major-mode font-lock-mode-enable-list)) - ;; (font-lock-set-defaults-1 explicit-defaults) - (phox-sym-lock-patch-keywords)) - (turn-on-font-lock))) - -(defun phox-sym-lock-patch-keywords () - (if (and font-lock-keywords phox-sym-lock-enabled - (boundp 'phox-sym-lock-keywords) - (listp (car font-lock-keywords)) - (listp (cdar font-lock-keywords)) - (listp (cddar font-lock-keywords)) - (or (listp (caddar font-lock-keywords)) - (not (string-match - "phox-sym-lock" - (symbol-name - (face-name (cadr (cdar - font-lock-keywords)))))))) - (setq font-lock-keywords (append phox-sym-lock-keywords - font-lock-keywords))) t) - -(add-hook 'font-lock-mode-hook 'phox-sym-lock-font-lock-hook) - -(provide 'phox-sym-lock) diff --git a/phox/phox-tags.el b/phox/phox-tags.el deleted file mode 100644 index 73ed659b..00000000 --- a/phox/phox-tags.el +++ /dev/null @@ -1,92 +0,0 @@ -;; $State$ $Date$ $Revision$ -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; gestion des TAGS -;;--------------------------------------------------------------------------;; - -; sous xemacs, visit-tags-table n'a pas d'argument optionnel. Sous gnu emacs : - -; Normally M-x visit-tags-table sets the global value of `tags-file-name'. -; With a prefix arg, set the buffer-local value instead. - -; mieux vaut sous gnu emacs gérer la variable tags-table-list, qui -; n'existe pas sous xemacs. -; Sous xemacs il faut gérer la variable tag-table-alist qui n'existe pas -; sous gnu emacs. - - -(require 'etags) - -(eval-when-compile - (defvar phox-doc-dir) - (defvar phox-lib-dir) - (defvar phox-etags)) - - -(defun phox-tags-add-table(table) - "add tags table" - (interactive "D directory, location of a file named TAGS to add : ") - (if (not (boundp 'tags-table-list)) (setq tags-table-list nil)) - (if (member table tags-table-list) - (message "%s already loaded." table) - ;; (make-local-variable 'tags-table-list) ; ne fonctionne pas - (setq tags-table-list (cons table tags-table-list)))) - -(defun phox-tags-reset-table() - "Set tags-table-list to nil." - (interactive) - (setq tags-table-list nil)) - -(defun phox-tags-add-doc-table() - "Add tags in text documentation." - (interactive) - (phox-tags-add-table (concat phox-doc-dir "/text/TAGS")) - ) - -(defun phox-tags-add-lib-table() - "Add tags in libraries." - (interactive) - (phox-tags-add-table (concat phox-lib-dir "/TAGS")) - ) - -(defun phox-tags-add-local-table() - "Add the tags table created with function phox-create-local-table." - (interactive) - (phox-tags-add-table (concat buffer-file-name "TAGS")) - ) - -(defun phox-tags-create-local-table() - "create table on local buffer" - (interactive) - (shell-command (concat phox-etags - " -o " - (file-name-nondirectory (buffer-file-name)) - "TAGS " - (file-name-nondirectory (buffer-file-name)))) - ) - - -(defun phox-complete-tag() - "Complete symbol using tags table." - (interactive) - (complete-tag)) - -;; menu - -(defvar phox-tags-menu - '("Tags" - ["create a tags table for local buffer" phox-tags-create-local-table t] - ["------------------" nil nil] - ["add table" phox-tags-add-table t] - ["add local table" phox-tags-add-local-table t] - ["add table for libraries" phox-tags-add-lib-table t] - ["add table for text doc" phox-tags-add-doc-table t] - ["reset tags table list" phox-tags-reset-table t] - ["------------------" nil nil] - ["Find theorem, definition ..." find-tag t] - ["complete theorem, definition ..." phox-complete-tag t] - ) -"Phox menu for dealing with tags" -) - -(provide 'phox-tags) diff --git a/phox/phox.el b/phox/phox.el index 79b8e747..53a82a55 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -1,231 +1,141 @@ -;; $State$ $Date$ $Revision$ - -(require 'proof) ; load generic parts - - -;; Adjust toolbar entries. (Must be done before proof-toolbar is -;; loaded). - -(eval-when-compile - (defvar phox-toolbar-entries)) - -(eval-after-load "pg-custom" - '(setq phox-toolbar-entries - (assq-delete-all 'context phox-toolbar-entries))) - - -;; ======== User settings for PhoX ======== -;; -;; Defining variables using customize is pretty easy. -;; You should do it at least for your prover-specific user options. -;; -;; proof-site provides us with two customization groups -;; automatically: (based on the name of the assistant) -;; -;; 'phox - User options for PhoX Proof General -;; 'phox-config - Configuration of PhoX Proof General -;; (constants, but may be nice to tweak) -;; -;; The first group appears in the menu -;; ProofGeneral -> Customize -> PhoX -;; The second group appears in the menu: -;; ProofGeneral -> Internals -> PhoX config -;; - -(defcustom phox-prog-name "phox -pg" - "*Name of program to run PhoX." - :type 'file - :group 'phox) - -(defcustom phox-web-page - "http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html" - "URL of web page for PhoX." - :type 'string - :group 'phox-config) - -(defcustom phox-doc-dir - "/usr/local/doc/phox" - "The name of the root documentation directory for PhoX." - :type 'string - :group 'phox-config) - -(defcustom phox-lib-dir - "/usr/local/lib/phox" - "The name of the root directory for PhoX libraries." - :type 'string - :group 'phox-config) - -(defcustom phox-tags-program - (concat phox-doc-dir "/tools/phox_etags.sh") - "Program to run to generate TAGS table for proof assistant." - :type 'string - :group 'phox-config) - -(defcustom phox-tags-doc - t - "*If non nil, tags table for PhoX text documentation is loaded." - :type 'boolean - :group 'phox-config) - -(defcustom phox-etags - (concat phox-doc-dir "/tools/phox_etags.sh") - "Command to build tags table." - :type 'string - :group 'phox-config) - -(require 'phox-fun) -(require 'phox-font) -(require 'phox-extraction) -(require 'phox-tags) -(require 'phox-outline) -(require 'phox-pbrpm) - -;; default for tags [da: moved here to fix compilation 15/02/03] - -(if phox-tags-doc - (add-hook 'phox-mode-hook 'phox-tags-add-doc-table)) - - -;; ----- PhoX specific menu - -(defpgdefault menu-entries - (cons - phox-state-menu - (cons - phox-tags-menu - (cons - phox-extraction-menu - nil))) -) - -;; -;; ======== Configuration of generic modes ======== -;; - -(defun phox-config () - "Configure Proof General scripting for PhoX." - (if phox-sym-lock-enabled - (phox-sym-lock-start)) - (setq - proof-prog-name phox-prog-name - proof-prog-name-guess t - proof-prog-name-ask nil - proof-terminal-string "." ; ends every command - proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)" - proof-script-comment-start "(*" - proof-script-comment-end "*)" - proof-goal-command-regexp - "\\`\\(Local[ \t\n\r]+\\)?\\(goal[ \t\n\r]\\|pro\\(p\\(osition\\)?\\|ve_claim\\)\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)" - proof-save-command-regexp "\\`save" - proof-goal-with-hole-regexp - (concat - "\\`\\(Local[ \t\n\r]+\\)?\\(pro\\(p\\(osition\\)?\\|ve_claim\\)\\(osition\\)?\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)" - phox-strict-comments-regexp - phox-ident-regexp) - proof-goal-with-hole-result 16 - proof-save-with-hole-regexp - (concat - "\\`save" - phox-strict-comments-regexp - phox-ident-regexp) - proof-save-with-hole-result 8 - proof-ignore-for-undo-count "\\`\\(constraints\\|flag\\|goals\\|pri\\(nt\\(_sort\\)?\\|ority\\)\\|eshow\\|search\\|depend\\|menu_\\|is_\\)" - proof-non-undoables-regexp "\\`\\(undo\\|abort\\)" - proof-shell-error-regexp "^\\([^ \n\t\r]* \\)?\\(\\(e\\|E\\)rror\\)\\|\\(\\(f\\|F\\)ailure\\)" - proof-goal-command "goal %s." - proof-save-command "save %s." - proof-kill-goal-command "abort." - proof-showproof-command "goals." - proof-undo-n-times-cmd "undo %s." - proof-find-and-forget-fn 'phox-find-and-forget - proof-find-theorems-command "search \"%s\"." - proof-auto-multiple-files nil - font-lock-keywords phox-font-lock-keywords +;; phox.el + +(require 'proof-site) +(proof-ready-for-assistant 'phox) + +(require 'proof) +(require 'proof-easy-config) ; easy configure mechanism + +(defconst phox-goal-regexp + "\\(prop\\(osition\\)?\\)\\|\\(lem\\(ma\\)?\\)\\|\\(fact\\)\\|\\(cor\\(ollary\\)?\\)\\(theo\\(rem\\)?\\)") + +(proof-easy-config + 'phox "PhoX" + proof-prog-name "phox" + proof-terminal-string "." + proof-script-command-end-regexp"[.][ \n\t\r]" + proof-script-comment-start "(*" + proof-script-comment-end "*)" + proof-script-syntax-table-entries + '(?( "()1" + ?) ")(4" + ?* ". 23" + ?$ "w" + ?_ "w" + ?. "w") + proof-shell-syntax-table-entries + '(?( "()1" + ?) ")(4" + ?* ". 23" + ?$ "w" + ?_ "w" + ?. "w") + proof-goal-command-regexp (concat "^" phox-goal-regexp) + proof-save-command-regexp "^save" + proof-goal-with-hole-regexp (concat "^" phox-goal-regexp "\\(\\([a-zA-Z0-9_$]*\\)\\) ") + proof-save-with-hole-regexp "save \\(\\([a-zA-Z0-9_$]*\\)\\).[ \n\t\r]" + proof-non-undoables-regexp "\\(undo\\)\\|\\(abort\\)\\|\\(show\\)\\(.*\\)[ \n\t\r]" + proof-goal-command "fact \"%s\"." + proof-save-command "save \"%s\"." + proof-kill-goal-command "abort." + proof-showproof-command "show." + proof-undo-n-times-cmd "undo %s." + proof-auto-multiple-files t + proof-shell-cd-cmd "cd \"%s\"." + proof-shell-interrupt-regexp "Interrupt." + proof-shell-start-goals-regexp "goal [0-9]+/[0-9]+" + proof-shell-end-goals-regexp "%PhoX%" + proof-shell-quit-cmd "quit." + proof-assistant-home-page "http://www.lama.univ-savoie.fr/~raffalli/phox.html" + proof-shell-annotated-prompt-regexp "^\\(>PhoX>\\)\\|\\(%PhoX%\\) " +; proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " + proof-shell-init-cmd "" +; proof-shell-proof-completed-regexp "^No subgoals!" + proof-script-font-lock-keywords + '("Cst" "Import" "Use" "Sort" + "new_intro" "new_elim" "new_rewrite" + "add_path" "author" "cd" + "claim" "close_def" "def" "del" "documents" + "depend" "elim_after_intro" "export" + "edel" "eshow" "flag" "goal" "include" + "institute" "path" "print_sort" "priority" + "quit" "save" "search" "tex" "tex_syntax" "title" + "proposition" "prop" "lemma" "lem" "fact" "corollary" "cor" + "theorem" "theo" + ; proof command, FIXME: another color + "abort" "absurd" "apply" "axiom" "constraints" + "elim" "from" "goals" "intros" "intro" "instance" + "local" "lefts" "left" "next" "rewrite" "rewrite_hyp" + "rename" "rmh" "trivial" "slh" "use" "undo" "unfold" + "unfold_hyp") ) - (phox-init-syntax-table) - (setq pbp-goal-command "intro %s;") - (setq pbp-hyp-command "elim %s;")) - -(defun phox-shell-config () - "Configure Proof General shell for PhoX." - (setq - ;proof-shell-cd-cmd "cd \"%s\"" - proof-shell-annotated-prompt-regexp "\\(>phox> \\)\\|\\(%phox% \\)" - proof-shell-interrupt-regexp "Interrupt" - proof-shell-start-goals-regexp "^\\(Here \\(are\\|is\\) the goal\\)\\|\\([0-9]+ new goals?\\)\\|\\([0-9]+ goals? possibly instanced\\)" - proof-shell-end-goals-regexp "^End of goals." - proof-shell-quit-cmd "quit." - proof-shell-restart-cmd "restart." - proof-shell-proof-completed-regexp "^.*^proved" - )) - - -;; -;; ======== Defining the derived modes ======== -;; - -;; The name of the script mode is always <proofsym>-script, -;; but the others can be whatever you like. -;; -;; The derived modes set the variables, then call the -;; <mode>-config-done function to complete configuration. - -(define-derived-mode phox-mode proof-mode - "PhoX script" - "Major mode for PhoX proofs. - -\\{phox-mode-map}" - (phox-config) - (proof-config-done) - (phox-setup-outline) - (define-key phox-mode-map [(control j)] - 'phox-assert-next-command-interactive) - ;; with the previous binding, - ;; it is nice to do : xmodmap -e "keysym KP_Enter = Linefeed" - - (define-key phox-mode-map [(control c) (meta d)] - 'phox-delete-symbol-on-cursor)) - -(define-derived-mode phox-shell-mode proof-shell-mode - "PhoX shell" nil - (phox-shell-config) - (proof-shell-config-done)) - -(define-derived-mode phox-response-mode proof-response-mode - "PhoX response" nil - (setq proof-response-font-lock-keywords phox-font-lock-keywords) - (phox-sym-lock-start) - (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled) - (add-hook 'proof-shell-handle-delayed-output-hook - 'phox-sym-lock-font-lock-hook) - ) - (proof-response-config-done)) - -(define-derived-mode phox-goals-mode proof-goals-mode - "PhoX goals" nil - (setq font-lock-keywords phox-font-lock-keywords) - (phox-sym-lock-start) - (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled) - (add-hook 'pg-before-fontify-output-hook - 'phox-sym-lock-font-lock-hook) - ) - (proof-goals-config-done)) - - -;; A more sophisticated instantiation might set font-lock-keywords to -;; add highlighting, or some of the proof by pointing markup -;; configuration for the goals buffer. - -; completions -; dans completions.el -;(setq completion-min-length 6) -;(setq completion-prefix-min-length 3) les mots de moins de 6 caractères -; ne sont pas pris en compte. Les prefixes de moins de 3 caractères ne -; sont pas non plus pris en compte. - -; (set-variable 'phox-completion-table -(defpgdefault completion-table - (append phox-top-keywords phox-proof-keywords) -) + + +;; code for sisplaying unicode borrowed from +;; Erik Parmann, PÃ¥l Drange latex-pretty-symbol + +(require 'cl-lib) + +(defun substitute-pattern-with-unicode-symbol (pattern symbol) + "Add a font lock hook to replace the matched part of PATTERN with the Unicode +symbol SYMBOL. +Symbol can be the symbol directly, no lookup needed." + (interactive) + (font-lock-add-keywords + nil + `((,pattern + (0 (progn + (compose-region (match-beginning 1) (match-end 1) + ,symbol + 'decompose-region) + nil)))))) + +(defun substitute-patterns-with-unicode-symbol (patterns) + "Mapping over PATTERNS, calling SUBSTITUTE-PATTERN-WITH-UNICODE for each of the patterns." + (mapcar #'(lambda (x) + (substitute-pattern-with-unicode-symbol (car x) + (cl-second x))) + patterns)) + +(defun phox-symbol-regex (str) + "Gets a string, e.g. Alpha, returns the regexp matching the escaped +version of it in Phox code, with no chars in [a-z0-9A-Z] after it." + (interactive "MString:") + (concat "[^!%&*+,-/:;≤=>@\\^`#|~]\\(" str "\\)[^!%&*+,-/:;≤=>@\\^`#|~]")) + +(defun phox-word-regex (str) + "Gets a string, e.g. Alpha, returns the regexp matching the escaped +version of it in Phox code, with no chars in [a-z0-9A-Z] after it." + (interactive "MString:") + (concat "\\b\\(" str "\\)\\b")) + + +;;Goto http://www.fileformat.info/info/unicode/block/mathematical_operators/list.htm and copy the needed character +(defun phox-unicode-simplified () + "Adds a bunch of font-lock rules to display phox commands as +their unicode counterpart" + (interactive) + (substitute-patterns-with-unicode-symbol + (list + ;;These need to be on top, before the versions which are not subscriptet + (list (phox-symbol-regex "<=")"≤") + (list (phox-symbol-regex ">=")"≥") + (list (phox-symbol-regex "!=")"≠") + (list (phox-symbol-regex ":<")"∈") + (list (phox-symbol-regex ":") "∈") + (list (phox-symbol-regex "/\\\\")"∀") + (list (phox-symbol-regex "\\\\/")"∃") + (list (phox-symbol-regex "<->")"↔") + (list (phox-symbol-regex "-->")"⟶") + (list (phox-symbol-regex "->")"→") + (list (phox-symbol-regex "~")"¬") + (list (phox-symbol-regex "&")"∧") + (list (phox-word-regex "or")"∨") + ))) + +(add-hook 'phox-mode-hook 'phox-unicode-simplified) +(add-hook 'phox-goals-mode-hook 'phox-unicode-simplified) +(add-hook 'phox-response-mode-hook 'phox-unicode-simplified) + (provide 'phox) diff --git a/phox/sqrt2.phx b/phox/sqrt2.phx new file mode 100644 index 00000000..0f08dd55 --- /dev/null +++ b/phox/sqrt2.phx @@ -0,0 +1,253 @@ +tex + title = "Proof that square root of 2 is not rational" + author = "Christophe Raffalli, Paul Rozière" + institute = "LAMA, Universit\\'e de Savoie, PPS, Universit\\'e Paris VII" + documents = math +. + +Import nat. + +flag auto_lvl 2. +flag auto_type true. + + +(*! math +\section{The library.} + + +There are two proof rules used \underline{explicitely} from the library : + +\begin{itemize} +\item \verb#elim (N n) with [case].# case reasonning on integers, +using \[ $$case.N \]. +\item \verb#elim (N n) with [wf]#: well founded induction for the natural order + on integers, using \[ $$well_founded.N \]. +\end{itemize} + +and the followings theorems. + +\begin{itemize} +\item \verb#demorganl# a set of rewrite rules for Demorgan's law. +\item \verb#calcul.N# a set of rewrite rules for natural numbers. +\item \verb#odd_or_even.N#: \[ $$odd_or_even.N \]. +\item \verb#lesseq.case1.N#: \[ $$lesseq.case1.N \]. +\item \verb#lesseq.imply.not.greater.N#: \[ $$lesseq.imply.not.greater.N \]. +\end{itemize} + + + +Comments: As the default elimination rule on integers is structural +induction, it is natural to use explicitly these two rules. The first +three theorems are also natural to use explicitly. The last + could probably be removed by adding some \verb#new_intro# or +\verb#new_elim# in the library. \verb#lesseq.case1.N# is more +problematic, It would require to extend the system with some kind of +binary elimination rule (with two principal premices ?). + +\section{Some basic lemmas.} + +They should be included in the library ? +*) + +lemma not_odd_and_even.N /\y,z:N( N2 * y != N1 + N2 * z). +(*! math +\begin{lemma}\label{not_odd_and_even.N} +An integer can not be odd and even: +$$ \[ $0 \] $$ +\end{lemma} +\begin{proof} +By induction over \[ y \] , then by case over \[ z \] . +\end{proof} +*) +intro 2. +(* induction over y *) +elim H. +(* y := 0 *) + trivial. +(* y0 -> S y0 *) + intros. + (* case over z *) + elim H2 with [case]. + (* z := 0 *) + trivial. + (* z := S y1 *) + intro. + prove N2 + N2 * y0 = N2 + N1 + N2 * y1. + from N2 * S y0 = N1 + N2 + N2 * y1. + from N2 * S y0 = N1 + (N2 + N2 * y1). + from H5. + lefts G. + elim H1 with H6. +save. + + + +fact sum_square.N /\x,y:N (x + y)^N2 = x^N2 + N2*x*y + y^N2. +(*! math +\begin{lemma}\label{sum_square.N} +$$ \[ $0 \] $$ +\end{lemma} +\begin{proof} +Easy. +\end{proof} +*) +intros. +rewrite calcul.N mul.left.distributive.N mul.right.distributive.N add.associative.N. +intro. +save. + + +fact less.exp.N /\n,x,y:N( x <= y -> x^n <= y^n). +(*! math +\begin{lemma}\label{less.exp.N} +$$ \[ $0 \] $$ +\end{lemma} +\begin{proof} +By induction over \[ n \]. +\end{proof} +*) +intros. +elim H. +trivial. +rewrite calcul.N. +trivial. +save. + +fact less_r.exp.N /\n,x,y:N( x^n < y^n -> x < y). +(*! math +\begin{lemma}\label{less_r.exp.N} +$$ \[ $0 \] $$ +\end{lemma} +\begin{proof} +Follows from lemma \ref{less.exp.N}. +\end{proof} +*) +intros. +elim lesseq.case1.N with y and x. +apply less.exp.N with n and H3. +elim lesseq.imply.not.greater.N with y^n and x^n. +save. + +fact less.ladd.N /\x,y:N (N0 < y -> x < x + y). +(*! math +\begin{lemma}\label{less.ladd.N} +$$ \[ $0 \] $$ +\end{lemma} +\begin{proof} +Easy induction over \[ x \]. +\end{proof} +*) +intros. +trivial. +(* +elim H. + trivial. + trivial. +*) +save. + + +(*! math +\section{The proof itself} +*) + +(** The proof itself. *) + +theorem n.square.pair /\n:N /\p:N( n^N2=N2*p -> \/q:N n=N2*q). +(*! math +\begin{lemma}\label{n.square.pair} + If the square of \[ n \] is even then \[ n \] is even: +$$ \[ $0 \] $$ +\end{lemma} +\begin{proof} +*) +intros. +apply odd_or_even.N with H. +lefts G $\/ $& $or. +(*! math +We assume \[ $$H1 \] ( \[ H1 \] ). +We distinguish two cases. If \[ n \] is even we get what we want. +*) +trivial. +(*! math +If \[ n \] is odd we have \[ $$H3 \] +*) +prove n^N2 = N1 + N2*(N2*y^N2+N2*y). +(*! math +which implies \[ $0 \] +*) + rewrite H3 sum_square.N. + from N1+(N2*(N2*y)+ N2*(y *(N2*y)))= N1+N2 * ?1. + intro. +(*! math +and this gives a contradiction by lemma \ref{not_odd_and_even.N} using ( \[ H1 \] ). +\end{proof} +*) +rewrite_hyp G H1. +elim not_odd_and_even.N with G. +save. + +lem decrease /\m,n : N (m^ N2 = N2 * n^ N2 -> N0 < n -> n < m). +(*! math +\begin{lemma}\label{decrease} +$$ \[ $0 \] $$ +\end{lemma} +\begin{proof} +Using lemma \ref{less_r.exp.N} and lemma \ref{less.ladd.N}. +\end{proof} +*) +intros. +elim less_r.exp.N with N2. +prove m^N2 = n^N2 + n^N2. axiom H1. (* fonctionne sans *) +elim less.ladd.N. +trivial =H0 H2. +save. + +theorem square2_irrat /\m,n : N (m^ N2 = N2 * n^ N2 -> m = N0 & n = N0). +(*! math +\begin{theorem} The square-root of 2 is irrational. For this we just need to prove the following: +$$ \[ $0 \] $$ +\end{theorem} +\begin{proof} +*) +intro 2. +elim H with [wf]. +(*! math +We prove \[ $0 \] by well founded induction over \[ m \]. Induction hypothesis is +\[ H1 \] : \[ $$H1 \]. *) +intros. +elim H2 with [case]. +(* cas n=0 *) + intro. + rewrite_hyp H3 H4 calcul.N. + trivial. +(*! math +if \[ n = N0 \] the result is trivial. Suppose now that \[ n > N0 \]. +*) +(* cas n > 0 *) + apply decrease with H3 and N0 < n. + trivial. +(*! math +Using lemma \ref{decrease} we get \[ $$G \]. +*) + elim n.square.pair with H3. + left H6. +(*! math +Using lemma \ref{n.square.pair} we get \[ q \] such that \[ $$H7 \] +*) +(*! math +The result follow by using induction hypothesis \[ H1 \] , +*) + elim H1 with G then q. + rewrite_hyp H3 H7. +(*! math +using \[ $0 \] which follows from \[$$H3 \]. +*) + prove N2 * (N2 * q ^N2) = N2 * n ^ N2. + from H3. + left G0. + trivial 0. +(*! math +\end{proof} +*) +save. diff --git a/phox/square-root-2.phx b/phox/square-root-2.phx deleted file mode 100644 index 92a888b3..00000000 --- a/phox/square-root-2.phx +++ /dev/null @@ -1,368 +0,0 @@ -tex - title = "Proof that square root of 2 is not rational" - author = "Christophe Raffalli, Paul Rozière" - institute = "LAMA, Universit\\'e de Savoie, PPS, Universit\\'e Paris VII" - documents = math -. - -Import nat. - -flag auto_lvl 1. - -(* Cette preuve est à peu près celle envoyée à F. Wiedijk -- Nijmegen --- The Fifteen Provers of the World -- - http://www.cs.kun.nl/~freek/comparison/index.html -Voir une preuve plus simple : sqrt2.phx -*) - -(*! math -\section{The library:} - -The theorem used \underline{explicitely} from the library are - -\begin{itemize} -\item \verb#demorganl# a set of rewrite rules for Demorgan's law. -\item \verb#calcul.N# a set of rewrite rules for natural numbers. -\item \verb#well_founded.N#: \[ $$well_founded.N \]. -\item \verb#odd_or_even.N#: \[ $$odd_or_even.N \]. -\item \verb#lesseq.case1.N#: \[ $$lesseq.case1.N \]. -\item \verb#neq.less_or_sup.N#: \[ $$neq.less_or_sup.N \]. -\item \verb#not.lesseq.imply.less.N#: \[ $$not.lesseq.imply.less.N \]. -\item \verb#lesseq.imply.not.greater.N#: \[ $$lesseq.imply.not.greater.N \]. -\end{itemize} - -Comments: The first four are natural to use explicitely. The last two -could probably be removed by adding some \verb#new_intro# or -\verb#new_elim# in the library. \verb#lesseq.case1.N# and -\verb#neq.less_or_sup.N# are more problematic, they would require to -extend the system with some kind of binary elimination rule (with two -principal premices ?). - -\section{Some basic lemmas.} - -They should be included in the library ? -*) - -theorem minimal.element /\X (\/n:N X n -> \/n:N (X n & /\p:N (X p -> n <= p))). -(*! math -\begin{lemma}\label{minimal.element} -Every non empty subset \[ X \] of \[ N \] admits a minimal element: -$$ \[ $0 \] $$ -\end{lemma} -*) -intro 2. -by_absurd. -rewrite_hyp H0 demorganl. -(*! math -\begin{proof} -We assume \[ $$H \] and \[ $$H0 \] ( \[ H0 \] ). -*) -use /\n:N ~ X n. -(*! math -We get a contradiction from \[ $$G \] which is proven by well founded induction: -*) -trivial. -intros. -elim well_founded.N with H1. -intros. -(*! math -we assume \[ $$H3 \] and must prove \[ $0 \]. -*) -intro. -apply H0 with H4. -lefts G $& $\/. -(*! math -Assuming \[ $$H4 \] and using ( \[ H0 \] ) we get an integer \[ x \] such that -\[ $$H6 \] and \[ $$H7 \]. This gives a contradiction with \[ $$H3 \]. -\end{proof} -*) -elim H3 with H5. -elim not.lesseq.imply.less.N. -save. - -theorem not_odd_and_even.N /\x,y,z:N (~ (x = N2 * y & x = N1 + N2 * z)). -(*! math -\begin{lemma}\label{not_odd_and_even.N} -An integer can not be odd and even: -$$ \[ $0 \] $$ -\end{lemma} -\begin{proof} -By induction over \[ x \]. -\end{proof} -*) -intro 2. -elim H. -trivial 6. -intros. -intro. -left H4. -elim H2 with [case]. -trivial =H0 H4 H6. -elim H1. -axiom H3. -axiom H6. -intro. -rmh H4. -left H5. -rmh H5. -rewrite_hyp H4 H7 calcul.N. -left H4. -axiom H4. -save. - -theorem sum_square.N /\x,y:N (x + y)^N2 = x^N2 + N2*x*y + y^N2. -(*! math -\begin{lemma}\label{sum_square.N} -$$ \[ $0 \] $$ -\end{lemma} -\begin{proof} -Easy. -\end{proof} -*) -intros. -rewrite calcul.N mul.left.distributive.N mul.right.distributive.N add.associative.N. -intro. -save. - - -fact less.exp.N /\n,x,y:N( x <= y -> x^n <= y^n). -(*! math -\begin{lemma}\label{less.exp.N} -$$ \[ $0 \] $$ -\end{lemma} -\begin{proof} -By induction on \[ n \]. -\end{proof} -*) -intros. -elim H. -trivial. -rewrite calcul.N. -trivial. -save. - -fact less_r.exp.N /\n,x,y:N( x^n < y^n -> x < y). -(*! math -\begin{lemma}\label{less_r.exp.N} -$$ \[ $0 \] $$ -\end{lemma} -\begin{proof} -Follows from lemma \ref{less.exp.N}. -\end{proof} -*) -intros. -elim lesseq.case1.N with y and x. -apply less.exp.N with n and H3. -elim lesseq.imply.not.greater.N with y^n and x^n ;; Try intros. -save. - -fact less.ladd.N /\x,y:N (N0 < y -> x < x + y). -(*! math -\begin{lemma}\label{less.ladd.N} -$$ \[ $0 \] $$ -\end{lemma} -\begin{proof} -Easy induction over \[ x \]. -\end{proof} -*) -intros. -elim H. -rewrite calcul.N. -trivial. -save. - - -(*! math -\section{The proof itself} -*) - -theorem n.square.pair /\n:N (\/p:N n^N2=N2*p -> \/q:N n=N2*q). -(*! math -\begin{lemma}\label{n.square.pair} - If the square of \[ n \] is even then \[ n \] is even: -$$ \[ $0 \] $$ -\end{lemma} -\begin{proof} -*) -intros. -lefts H0 $\/ $&. -apply odd_or_even.N with H. -lefts G $\/ $& $or. -(*! math -We assume \[ $$H1 \] ( \[ H1 \] ). -We distinguish two cases. If \[ n \] is even we get what we want. -*) -trivial. -(*! math -If \[ n \] is odd we have \[ $$H3 \] -*) -prove n^N2 = N2*(N2*y^N2+N2*y) + N1. -(*! math -which implies \[ $0 \] -*) -rewrite H3 sum_square.N. -rewrite add.associative.N mul.associative.N mul.left.distributive.N. -from N1 + N4 * y + (N2 * y) ^ N2 = N1 + N4 * y + N4 * y ^ N2. -intro. -(*! math -and this gives a contradiction by lemma \ref{not_odd_and_even.N} using ( \[ H1 \] ) -\end{proof} -*) -elim not_odd_and_even.N with N (n^N2). -intros. -select 3. -intro. -axiom H1. -axiom G. -axiom H0. -intros. -save. - -lem decrease /\m,n : N (m^ N2 = N2 * n^ N2 -> N0 < n -> n < m). -(*! math -\begin{lemma}\label{decrease} -$$ \[ $0 \] $$ -\end{lemma} -\begin{proof} -Using lemma \ref{less_r.exp.N} and lemma \ref{less.ladd.N} -\end{proof} -*) -intros. -elim less_r.exp.N with N2 ;; Try intros. -prove m^N2 = n^N2 + n^N2. axiom H1. -elim less.ladd.N ;; Try intros. -trivial. -trivial. -trivial =H0 H2. -save. - -lem sup_zero /\m,n : N (m^ N2 = N2 * n^ N2 -> N0 < m -> N0 < n). -(*! math -\begin{lemma}\label{sup_zero} -$$ \[ $0 \] $$ -\end{lemma} -\begin{proof} -Using lemma \[ $$ neq.less_or_sup.N \] from the library. -\end{proof} -*) -intros. -elim neq.less_or_sup.N with N0 and n ;; Try intros. -rewrite_hyp H1 H3 calcul.N. -trivial. -trivial. -save. - -def Q m = m > N0 & \/n:N (m^ N2 = N2 * n^ N2). -(*! math -\begin{definition} -We define \[ Q m = $$Q m \]. -\end{definition} -*) - -lem dec /\m:N (Q m -> \/m':N (Q m' & m' < m)). -(*! math -\begin{lemma}\label{dec} -$$ \[ $0 \] $$ -\end{lemma} -\begin{proof} -*) -intros. -lefts H0 $Q $\/ $&. -(*! math -We assume that \[ $$H0 \] and \[ $$H2 \] (\[ H2 \]) and we must prove \[ $0 \]. -*) -apply sup_zero with H2 and H0. -(*! math -By lemma \ref{sup_zero} we get \[ $$G \]. We show that \[ n \] is the integer we are looking for. -*) -intro. -instance ?1 n. -intros. -intros. -trivial. -(*! math -We just need to prove \[ $0 \] and \[1 $0 \]. -*) -prove \/p:N (m ^ N2 = N2 * p). -intro. -instance ?2 n^N2. -trivial. -apply n.square.pair with G0. -lefts G1 $& $\/. -(*! math -Using lemma \ref{n.square.pair} we get \[ q \] such that \[ $$H4 \] -*) -prove n ^N2 = N2 * q ^N2. -rewrite_hyp H2 H4. -prove N2 * (N2 * q ^N2) = N2 * n ^ N2. -from H2. -left G1. -intro. -(*! math -and then \[ $$G1 \]. -*) -trivial =H3 G1. -(*! math -Finally \[ $0 \] follows from lemma \ref{decrease}. -\end{proof} -*) -elim decrease. -save. - -lem sq2_irrat /\m:N ~Q m. -(*! math -\begin{lemma}\label{sq2_irrat} -$$ \[ $0 \] $$ -\end{lemma} -\begin{proof} -Follows from the previous lemma by selecting the minimal element in \[ Q \] (using lemme \ref{minimal.element}) and getting a contradiction. -\end{proof} -*) -intros. -intro. -elim minimal.element with Q. -intros $\/ $&. -axiom H. -axiom H0. -lefts H1. -elim dec with H2. -lefts H4. -apply H3 with H5. -elim lesseq.imply.not.greater.N with n and m'. -save. - -theorem square2_irrat /\m,n : N (m^ N2 = N2 * n^ N2 -> m = N0 & n = N0). -(*! math -\begin{theorem} The square-root of 2 is irrational. For this we just need to prove the following: -$$ \[ $0 \] $$ -\end{theorem} -\begin{proof} -*) -intros. -apply sq2_irrat with H. -(*! math -We assume \[ $$H1 \]. -By the previous lemma we have \[ $$G \]. -*) -elim H with [case]. -intro. -intro. -(*! math -If \[ $$H2 \] we easely get \[ $0 \]. -*) -elim H0 with [case]. -intro. -rewrite_hyp H1 H2 H4 calcul.N. -left H1;; intros. -prove Q m. -(*! math -If \[ m > N0 \] then we have \[ Q m \] and a contradiction. -\end{proof} -*) -intros $Q $\/ $&. -trivial. -select 2. -axiom H1. -trivial. -elim G. -save. |