595 Up 596
597 598 604 605 Klaus Grue 606 607 " end text ,, 608 609 610 611 text "page.bib" : ""-""; 612 613 @article {berline97, 614 author = {C. Berline and K. Grue}, 615 title = {A $\kappa$-denotational semantics for {M}ap {T}heory 616 in {ZFC+SI}}, 617 journal = TCS, 618 year = {1997}, 619 volume = {179}, 620 number = {1--2}, 621 pages = {137--202}, 622 month = {jun}} 623 624 @inproceedings{Logiweb, 625 author = {K. Grue}, 626 title = {Logiweb}, 627 editor = {Fairouz Kamareddine}, 628 booktitle = {Mathematical Knowledge Management Symposium 2003}, 629 publisher = {Elsevier}, 630 series = {Electronic Notes in Theoretical Computer Science}, 631 volume = {93}, 632 year = {2004}, 633 pages = {70--101}} 634 635 @Book {Mendelson, 636 author = {E. Mendelson}, 637 title = {Introduction to Mathematical Logic}, 638 publisher = {Wadsworth and Brooks}, 639 year = {1987}, 640 edition = {3.}} 641 642 @techreport{chores, 643 author = {K. Grue}, 644 year = {2006}, 645 title = {A Logiweb proof checker - chores}, 646 institution={Logiweb}, 647 note = 648 {\href{\lgwBlockRelay \lgwBlockThis /page/appendix.pdf}{% 649 \lgwBreakRelay \lgwBreakThis /page/appendix.pdf}}} 650 651 @techreport{base, 652 author = {K. Grue}, 653 year = {2006}, 654 title = {A Logiweb base page}, 655 institution={Logiweb}, 656 note = 657 {\href{\lgwBlockRelay \lgwBlockbase /page/index.html}{% 658 \lgwBreakRelay \lgwBreakbase /page/index.html}}} 659 660 " end text ,, 661 662 663 664 text "page.tex" : ""-""; 665 666 \documentclass[fleqn]{article} 667 668 % Include definitions generated by the Logiweb compiler 669 \input{lgwinclude} 670 671 % Make latexsym characters available 672 \usepackage{latexsym} 673 674 % Ensure reasonable rendering of strings 675 \everymath{\rm} 676 \everydisplay{\rm} 677 678 % Enable generation of an index 679 \usepackage{makeidx} 680 \makeindex 681 \newcommand{\intro}[1]{\emph{#1}} 682 \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} 683 684 % Enable generation of a bibliography 685 \bibliographystyle{plain} 686 687 % Enable hyperlinks 688 \usepackage[dvipdfm=true]{hyperref} 689 \hypersetup{pdfpagemode=UseNone} 690 \hypersetup{pdfstartpage=1} 691 \hypersetup{pdfstartview=FitBH} 692 \hypersetup{pdfpagescrop={120 80 490 730}} 693 \hypersetup{pdftitle=A Logiweb proof checker} 694 \hypersetup{colorlinks=true} 695 696 % Construct for listing statements with associated explanations 697 \newenvironment{statements}{\begin{list}{}{ 698 \setlength{\leftmargin}{5em} 699 \setlength{\itemindent}{-5em}}}{\end{list}} 700 701 \begin{document} 702 \title{A Logiweb proof checker} 703 \author{Klaus Grue} 704 \maketitle 705 \tableofcontents 706 707 "[ make macro expanded version ragged right ]" 708 "[ prepare proof indentation ]" 709 710 711 712 \section{Introduction} 713 714 \indexintro{Logiweb} \cite{Logiweb} is an open source system available under GNU GPL for distribution of mathematical definitions, lemmas, and proofs. 715 716 The present document is part of a \index{page, Logiweb}\indexintro{Logiweb page}. A Logiweb page is a cluster of documents which has been submitted to the Logiweb system. Such a cluster typically consists of a main document like the present one plus a number of electronic appendices. 717 718 The present Logiweb page (i.e.\ the document cluster to which the present document belongs) defines a general purpose proof checker. 719 720 721 722 \subsection{Electronic appendices} 723 724 The present Logiweb page comprises one html and two PDF files, located the following places: 725 726 \begin{itemize} 727 \item \href{\lgwBlockRelay \lgwBlockThis /page/page.pdf}{% 728 \lgwBreakRelay \lgwBreakThis /page/page.pdf} 729 \item \href{\lgwBlockRelay \lgwBlockThis /page/chores.pdf}{% 730 \lgwBreakRelay \lgwBreakThis /page/chores.pdf} \cite{chores} 731 \item \href{\lgwBlockRelay \lgwBlockThis /page/index.html}{% 732 \lgwBreakRelay \lgwBreakThis /page/index.html} 733 \end{itemize} 734 735 The first link points to the present paper. The second link points to an electronic appendix with definitions that would bore most readers (such as definitions of how each construct should be rendered). The second link is included in the \textsc{Bib}\TeX\ bibliography \cite{chores} for easy reference. The third link points to a table of contents. 736 737 738 739 \subsection{Referenced Logiweb pages} 740 741 The present Logiweb page references the following other Logiweb page: 742 743 \begin{itemize} 744 \item \href{\lgwBlockRelay \lgwBlockbase /page/chores.pdf}{% 745 \lgwBreakRelay \lgwBreakbase /page/chores.pdf} \cite{base} 746 \end{itemize} 747 748 749 750 \subsection{Bed page} 751 752 The present page may be used as `bed' page, i.e.\ as the first reference of other pages. Pages which use the present page as bed page and which do not define a verifier of their own use the verifier of the present page: 753 754 "[[[ verifier test1 &c proofcheck end verifier ]]]" 755 756 \noindent The verifier is a conjunction of "[[ proofcheck ]]" which is the proof checker defined on the present page and "[[ test1 ]]" which is defined on the bed page of the present page. The "[[ test1 ]]" verifier executes test suites and supports testing of computable functions. 757 758 Pages which use the present page as bed page and which do not define a macro expander of their own use the macro expander of the present page: 759 760 "[[[ expander macro1 end expander ]]]" 761 762 \noindent The expander is nothing but a reexport of the expander defined on the bed page of the present page. 763 764 765 766 \section{Terms} 767 768 \subsection{Aspect declarations} 769 770 We shall use several user aspects for implementing the proof checker. 771 772 Logiweb has a list of predefined aspects like `value', `name', `use', and so on. Predefined aspects are built up from small letters and space characters. The list of predefined aspects may grow with time, so user defined aspects must contain at least one character which is neither a small letter, nor a space character. 773 774 Furthermore, to reduce the risk of name conflicts, one should give any user aspect a personal touch. The aspects defined in the following all end with a slash and the initials of the present author. If two authors use the same aspect for different things, then a third author may run into trouble when referencing both of the two first authors. 775 776 Logiweb has means for defining guaranteed unique aspects, but we shall not use that here. The aspects to be used are: 777 778 \begin{statements} 779 780 \item "[[ eager message define statement as "statement/kg" end define ]]"\index{statement} defines `"[[ statement ]]"' to represent the \index{aspect, statement}\indexintro{statement aspect}. The present page uses the statement aspect for expressing lemmas, theories, axioms, inference rules, and conjectures. 781 782 \item "[[ eager message define proof as "proof/kg" end define ]]"\index{proof} defines `"[[ proof ]]"' to represent the \index{aspect, proof}\index{proof aspect}\intro{proof} user aspect. The present page uses the proof aspect for expressing formal proofs. 783 784 \item "[[ eager message define meta as "meta/kg" end define ]]"\index{meta} defines `"[[ meta ]]"' to represent the \index{aspect, meta}\index{meta aspect}\intro{meta} user aspect. The present page uses the meta aspect for declaring constructs to be meta-variables, meta-quantifiers and sequent operators. 785 786 \item "[[ eager message define math as "math/kg" end define ]]"\index{math} defines `"[[ math ]]"' to represent the \index{aspect, math}\index{math aspect}\intro{math} user aspect. The semantics of this aspect is defined by individual axiomatic systems, the intension being that definition of new function letters are done using this aspect. 787 788 \item "[[ eager message define tactic as "tactic/kg" end define ]]"\index{tactic} defines `"[[ tactic ]]"' to represent the \index{aspect, tactic}\index{tactic aspect}\intro{tactic} user aspect. The present page uses the tactic aspect for specifying how proofs should be translated into sequent terms. 789 790 \item "[[ eager message define unitac as "unitac/kg" end define ]]"\index{unitac} defines `"[[ unitac ]]"' to represent the \index{aspect, unitac}\index{unitac aspect}\intro{unitac} user aspect. The unitac aspect defines a special kind of tactic which may occur inside arguments of the `unification tactic'. The unification tactic is described later. 791 792 \item "[[ eager message define locate as "locate/kg" end define ]]"\index{locate} defines `"[[ locate ]]"' to represent the \index{aspect, locate}\index{locate aspect}\intro{locate} user aspect. The present page uses the locate aspect for locating the source of errors for the sake of diagnostic messages. 793 794 \end{statements} 795 796 797 798 \subsection{Definition constructs} 799 800 The following constructs allow to define various aspects of a construct "[[ x ]]". 801 802 \begin{statements} 803 804 \item "[[ macro define statement define x as y end define as define statement of x as y end define end define ]]". 805 806 \item "[[ macro define proof define x as y end define as define proof of x as y end define end define ]]". 807 808 \item "[[ macro define meta define x as y end define as define meta of x as y end define end define ]]". 809 810 \item "[[ macro define math define x as y end define as define math of x as y end define end define ]]". 811 812 \item "[[ macro define tactic define x as y end define as define tactic of x as y end define end define ]]". 813 814 \item "[[ macro define unitac define x as y end define as define unitac of x as y end define end define ]]". 815 816 \item "[[ macro define locate define x as y end define as define locate of root protect x end protect as y end define end define ]]". 817 818 \end{statements} 819 820 In `locate' definitions, the construct being defined is protected against macro expansion. This is important because errors are located in the body of a page, i.e.\ in the page before macro expansion whereas locate definitions are interpretted after macro expansion. So protection is needed in cases where one needs to assign a locate aspect to some construct which also has a macro definition. 821 822 823 824 \subsection{Axioms, rules, theories, and lemmas} 825 826 Axioms, inference rules, theories, and lemmas are all represented by statement definitions. As an example, a lemma "[[ L ]]" saying that any statement infers itself could read 827 828 "[ hide lemma L : #a infer #a end lemma end hide ]" 829 830 \noindent which is simply shorthand for "[[ hide statement define L as #a infer #a end define end hide ]]". The lemma construct is defined thus: "[[ macro define lemma x : y end lemma as ensure math statement define x as y end define end math end define ]]". 831 832 A theory "[[ T ]]" comprising an inference rule named "[[ p.MP ]]" and three axioms "[[ p.A1 ]]", "[[ p.A2 ]]", and "[[ p.A3 ]]" could read 833 834 "[ hide theory T : p.MP oplus p.A1 oplus p.A2 oplus p.A3 end theory end hide ]" 835 836 \noindent which is shorthand for "[[ hide statement define T as p.MP oplus p.A1 oplus p.A2 oplus p.A3 end define end hide ]]". The theory construct is defined thus: "[[ macro define theory x : y end theory as ensure math define statement of x as y end define end math end define ]]". 837 838 An axiom "[[ p.A1 ]]" which says that "[[ #a p.imply #b p.imply #a ]]" for all terms "[[ #a ]]" and "[[ #b ]]" could read 839 840 "[ hide axiom p.A1 : All #a ,, #b : A p.imply B p.imply A end axiom end hide ]" 841 842 \noindent This is shorthand for "[[ hide statement define p.A1 as All #a ,, #b : #a p.imply #b p.imply #a end define end hide ]]" plus one more definition. The second definition is a unitac definition which explains how to prove the axiom. This may seem strange since, from a human point of view, axioms are assumed rather than proved. But in the present system, axioms actually do have to be proved, and the proof even depends on context. As an example, if axiom "[[ p.A1 ]]" occurs in a proof which is relative to the theory "[[ T ]]" above, then the proof of "[[ p.A1 ]]" will be one which accesses the second element of "[[ T ]]". In a proof relative to "[[ p.A1 oplus p.A2 oplus p.A3 oplus p.MP ]]", the proof would be one which accesses the first element. 843 844 A working logician need not care about how axioms are proved backstage. And need not even know that axioms do have to be proved. The working logician just needs to state proofs in a style close to that of \cite{Mendelson} and the definitions on the present page will take care of the rest. 845 846 The axiom construct is defined thus: 847 848 "[[[ macro define axiom x : y end axiom as ensure math define statement of x as y end define,unitac define x as \ u . unitac-rule ( u ) end define end math end define ]]]" 849 850 When an axiom like "[[ p.A1 ]]" occurs in a proof line which is expanded using the unification tactic, then the unification tactic evaluates "[[ unitac-rule ( << t ,, s ,, c >> ) ]]" where "[[ t ]]" is "[[ p.A1 ]]", "[[ s ]]" is a `state' which contains local information, and "[[ c ]]" is the cache of the page on which the proof occurs. Among other, the state "[[ s ]]" contains information about which theories may be used and which hypotheses have been assumed. The value of "[[ unitac-rule ( << t ,, s ,, c >> ) ]]" is a proof of "[[ All #a ,, #b : #a p.imply #b p.imply #a ]]" which the unification tactic will then try to instantiate suitably. 851 852 From the point of view of the proof checker, there is no difference between axioms and inference rules: 853 854 "[[[ macro define rule x : y end rule as ensure math define statement of x as y end define,unitac define x as \ u . unitac-rule ( u ) end define end math end define ]]]" 855 856 857 858 \subsection{Meta variables} 859 860 We use the meta aspect to declare that a construct is a meta variable. In general, several aspects are used when finding out what a construct means: Constructs which have a meta aspect mean whatever that aspect says they mean. Constructs without a meta aspect mean whatever the value aspect says they mean. Constructs with neither meta nor value aspect mean whatever the def aspect says they mean. Constructs with no meta, value, or def aspect are considered to be object variables. So e.g.\ "[[ a ]]", "[[ X ]]", and "[[ beta ]]" are object variables. 861 862 A construct is a meta variable if its "[[ meta ]]" aspect equals "[[ show "var" end show ]]". The following construct allows to declare meta variables: 863 864 "[[[ macro define metadeclare x as meta define x as "var" end define end define ]]]" 865 866 To have an arsenal of meta variables, we declare "[[ #a ]]", "[[ #b ]]", and so on to be meta variables: 867 "[[ metadeclare #a ]]", 868 "[[ metadeclare #b ]]", 869 "[[ metadeclare #c ]]", 870 "[[ metadeclare #d ]]", 871 "[[ metadeclare #e ]]", 872 "[[ metadeclare #f ]]", 873 "[[ metadeclare #g ]]", 874 "[[ metadeclare #h ]]", 875 "[[ metadeclare #i ]]", 876 "[[ metadeclare #j ]]", 877 "[[ metadeclare #k ]]", 878 "[[ metadeclare #l ]]", 879 "[[ metadeclare #m ]]", 880 "[[ metadeclare #n ]]", 881 "[[ metadeclare #o ]]", 882 "[[ metadeclare #p ]]", 883 "[[ metadeclare #q ]]", 884 "[[ metadeclare #r ]]", 885 "[[ metadeclare #s ]]", 886 "[[ metadeclare #t ]]", 887 "[[ metadeclare #u ]]", 888 "[[ metadeclare #v ]]", 889 "[[ metadeclare #w ]]", 890 "[[ metadeclare #x ]]", 891 "[[ metadeclare #y ]]", and 892 "[[ metadeclare #z ]]". 893 894 A term is a meta variable, if the "[[ meta ]]" aspect of the root of the term equals "[[ show "var" end show ]]". As an example of use, we declare the unary construct "[[ x# ]]" to be a meta variable: 895 896 "[[[ metadeclare x# ]]]" 897 898 \noindent The construct above allows to use e.g.\ "[[ a# ]]", "[[ beta# ]]", "[[ c prime# ]]", and "[[ d _ { 5 }# ]]" as meta variables. 899 900 Two meta variable are identical if they are identical as terms (i.e.\ w.r.t.\ "[[ x t= y ]]"). As a peculiarity this entails that "[[ ( 2 + 2 )# ]]" and "[[ 4# ]]" are distinct meta variables. 901 902 We shall need two more indexed meta variables: "[[ metadeclare tacfresh ( x ) ]]" and "[[ metadeclare unifresh ( x , y ) ]]". The unification tactic defined later uses these indexed meta variables to generate variables that are supposed to be `fresh'. If you use these indexed meta variables in proofs, you ask for trouble. 903 904 905 906 \subsection{Cache accessors} 907 908 Given a construct "[[ x ]]" and a cache "[[ c ]]", the following functions return various information about "[[ x ]]". The last construct below decides whether or not a construct "[[ x ]]" is a meta variable. 909 910 \begin{statements} 911 912 \item "[[ eager define x plist ( c ) as c [[ x ref ]] [[ "codex" ]] [[ x ref ]] [[ x idx ]] [[ 0 ]] end define ]]". Given a symbol "[[ x ]]", this construct looks up an array which maps strings to the associated aspects. 913 914 \item "[[ eager define x def ( c , a ) as x plist ( c ) [[ a ]] end define ]]". Look up aspect "[[ a ]]" of symbol "[[ x ]]". 915 916 \item "[[ eager define x lhs ( c , a ) as x def ( c , a ) second end define ]]". Look up the left hand side of the aspect "[[ a ]]" definition of symbol "[[ x ]]". 917 918 \item "[[ eager define x rhs ( c , a ) as x def ( c , a ) third end define ]]". Look up the right hand side of the aspect "[[ a ]]" definition of symbol "[[ x ]]". 919 920 \item "[[ eager define x metadef ( c ) as x rhs ( c , meta ) idx end define ]]". Look up the meta definition of symbol "[[ x ]]". 921 922 \item "[[ eager define x metavar ( c ) as x metadef ( c ) = "var" end define ]]". True if "[[ x ]]" is a meta variable. 923 924 \item "[[ eager define x stmt-rhs ( c ) as x rhs ( c , statement ) end define ]]". Look up the statement definition of symbol "[[ x ]]". 925 926 \item "[[ eager define x proof-rhs ( c ) as x rhs ( c , proof ) end define ]]". Look up the statement definition of symbol "[[ x ]]". 927 928 \item "[[ eager define x tactic-rhs ( c ) as x rhs ( c , tactic ) end define ]]". Look up the statement definition of symbol "[[ x ]]". 929 930 \item "[[ eager define x unitac-rhs ( c ) as x rhs ( c , unitac ) end define ]]". Look up the statement definition of symbol "[[ x ]]". 931 932 \item "[[ eager define x locate-rhs ( c ) as x rhs ( c , locate ) end define ]]". Look up the statement definition of symbol "[[ x ]]". 933 934 \end{statements} 935 936 937 938 \subsection{Meta operators} 939 940 In addition to meta variables, the five operators for building meta terms of the Logiweb sequent calculus are: 941 942 \begin{statements} 943 944 \item "[[ meta define x infer y as "infer" end define ]]". States that provability of "[[ x ]]" implies provability of "[[ y ]]". 945 946 \item "[[ meta define x endorse y as "endorse" end define ]]" States that if "[[ x ]]" evaluates to "[[ true ]]" then "[[ y ]]" is provable. 947 948 \item "[[ meta define x oplus y as "plus" end define ]]" States that both "[[ x ]]" and "[[ y ]]" are provable. 949 950 \item "[[ meta define All x : y as "all" end define ]]". States that "[[ y ]]" is provable for all "[[ x ]]" 951 952 \item "[[ meta define False as "false" end define ]]". Expresses absurdity. One may disprove "[[ x ]]" is by proving "[[ x infer False ]]" 953 954 \end{statements} 955 956 957 958 \subsection{Meta constructs} 959 960 We shall say that a construct is a \index{construct, meta}\indexintro{meta construct} iff the construct has a meta definition. In other words we shall say that a construct "[[ x ]]" is a meta construct iff "[[ x metadef ( self ) != true ]]". 961 962 We shall say that a meta construct is a \index{variable, meta}\indexintro{meta variable} iff it is meta defined as "[[ show "var" end show ]]". In other words, "[[ x ]]" is a meta variable iff "[[ x metadef ( self ) = "var" ]]". 963 964 We shall say that a meta construct "[[ x ]]" is a \index{binder, meta}\indexintro{meta binder} iff "[[ x metadef ( self ) = "all" ]]". 965 966 We shall say that a meta construct is a \index{operator, meta}\indexintro{meta operator} if it is neither a meta variable nor a meta binder. 967 968 969 970 \subsection{Object constructs} 971 972 We shall say that a construct is an \index{construct, object}\indexintro{object construct} iff it is not a meta construct. So "[[ x ]]" is an object construct iff "[[ x metadef ( self ) = true ]]" 973 974 We shall say that an object construct is an \index{binder, object}\indexintro{object binder} if the construct is declared to denote lambda abstraction. So "[[ x ]]" is an object binder iff "[[ self [[ x ref ]] [[ "code" ]] [[ x idx ]] = 0 ]]". 975 976 We shall say that an object construct "[[ x ]]" is a \indexintro{quote} if the construct is declared to denote quoting. So "[[ x ]]" is a quote iff "[[ self [[ x ref ]] [[ "code" ]] [[ x idx ]] = 1 ]]". 977 978 We shall say that an object construct is an \index{variable, object}\indexintro{object variable} if it neither has a value nor a math definition. 979 980 We shall say that object constructs other than object variables, object binders, and quotes are \index{operator, object}\index{object operator}\intro{object operators}. 981 982 983 984 \subsection{Object terms} 985 986 We shall say that a term is an \index{term, object}\indexintro{object term} if it is built up from the following: 987 988 \begin{itemize} 989 990 \item object operators applied to object terms. 991 992 \item quotes applied to arbitrary terms. 993 994 \item object variables applied to arbitrary terms (i.e.\ object variables with arbitrary indices). 995 996 \item object binders applied to an object or meta variable and an object term in that order. 997 998 \item meta variables applied to arbitrary terms (i.e.\ meta variables with arbitrary indices). 999 1000 \end{itemize} 1001 1002 In other words, a term "[[ x ]]" is an object term iff "[[ x objectterm ( self ) ]]" where we define "[[ x objectterm ( c ) ]]" in the following. 1003 1004 \begin{statements} 1005 1006 \item "[[ eager define x valuedef ( c ) as c [[ x ref ]] [[ "code" ]] [[ x idx ]] end define ]]". The value definition of "[[ x ]]". This is "[[ 0 ]]" for lambda abstractions, "[[ 1 ]]" for quotes, and "[[ true ]]" for constructs with no value definition. 1007 1008 \item "[[ eager define x mathdef ( c ) as x rhs ( c , math ) idx end define ]]". The math definition of "[[ x ]]". This is "[[ true ]]" for constructs with no math definition. 1009 1010 \item "[[ eager define x objectvar ( c ) as x metadef ( c ) = true .and. x valuedef ( c ) = true .and. x mathdef ( c ) = true end define ]]". This is true if "[[ x ]]" is an object variable. 1011 1012 \item "[[ eager define x objectlambda ( c ) as x metadef ( c ) = true .and. x valuedef ( c ) = 0 end define ]]". This is true if "[[ x ]]" is a lambda abstraction. 1013 1014 \item "[[ eager define x objectquote ( c ) as x metadef ( c ) = true .and. x valuedef ( c ) = 1 end define ]]". This is true if "[[ x ]]" is a lambda abstraction. 1015 1016 \item "[[ eager define x objectterm ( c ) as newline 1017 1018 let d = x metadef ( c ) in newline 1019 1020 if d = "var" then true else newline 1021 1022 if d != true then false else newline 1023 1024 let d = x valuedef ( c ) in newline 1025 1026 if d = 0 then ( x first objectvar ( c ) .or. x first metavar ( c ) ) .and. x second objectterm ( c ) else newline 1027 1028 if d = 1 then true else 1029 1030 if d .and. x mathdef ( c ) then true else x tail objectterm* ( c ) end define ]]" 1031 1032 \item "[[ eager define x objectterm* ( c ) as x atom .or. x head objectterm ( c ) .and. x tail objectterm* ( c ) end define ]]". 1033 1034 \end{statements} 1035 1036 1037 1038 \subsection{Meta terms} 1039 1040 We shall say that a term is a \index{term, meta}\indexintro{meta term} if it is built up from the following: 1041 1042 \begin{itemize} 1043 1044 \item object terms. 1045 1046 \item meta operators applied to meta terms. 1047 1048 \item meta binders applied to a meta variable and a meta term in that order. 1049 1050 \end{itemize} 1051 1052 In other words, a term "[[ x ]]" is a meta term iff "[[ x metaterm ( self ) ]]" where we define "[[ x metaterm ( c ) ]]" in the following. 1053 1054 \begin{statements} 1055 1056 \item "[[ eager define x metaterm ( c ) as newline 1057 1058 let d = x metadef ( c ) in newline 1059 1060 if d = "var" then true else newline 1061 1062 if d = "all" then x first metavar ( c ) .and. x second metaterm ( c ) else newline 1063 1064 if d != true then x tail metaterm* ( c ) else x objectterm ( c ) end define ]]" 1065 1066 \item "[[ eager define x metaterm* ( c ) as x atom .or. x head metaterm ( c ) .and. x tail metaterm* ( c ) end define ]]" 1067 1068 \end{statements} 1069 1070 1071 1072 \subsection{Avoidance} 1073 1074 We shall say that a variable "[[ x ]]" \index{avoid}\intro{avoids} a term "[[ t ]]" if "[[ x ]]" does not occur free in "[[ t ]]". The meta version of avoidance is defined thus: 1075 1076 \begin{statements} 1077 1078 \item "[[ eager define x metaavoid ( c ) y as x metavar ( c ) .and. metaavoid1 ( x , y , c ) end define ]]". True if "[[ x ]]" is a meta variable and "[[ x ]]" does not occur free in the meta term "[[ y ]]". 1079 1080 \item "[[ eager define x metaavoid* ( c ) y as newline 1081 1082 if y atom then true else newline 1083 1084 if x metaavoid ( c ) ( y head ) then x metaavoid* ( c ) ( y tail ) else y head end define ]]". True if "[[ x ]]" does not occur free in any element of the list "[[ y ]]" of meta terms. Otherwise returns the first element of "[[ y ]]" in which "[[ x ]]" occurs free. 1085 1086 \item "[[ eager define metaavoid1 ( x , y , c ) as newline 1087 1088 let d = y metadef ( c ) in newline 1089 1090 if d = "var" then .not. x t= y else newline 1091 1092 if d = "all" then x t= y first .or. metaavoid1 ( x , y second , c ) else newline 1093 1094 if d != true then metaavoid1* ( x , y tail , c ) else newline 1095 1096 let d = y valuedef ( c ) in newline 1097 1098 if d = 1 then true else metaavoid1* ( x , y tail , c ) end define ]]" 1099 1100 \item "[[ eager define metaavoid1* ( x , y , c ) as y atom .or. metaavoid1 ( x , y head , c ) .and. metaavoid1* ( x , y tail , c ) end define ]]" 1101 1102 \end{statements} 1103 1104 The object version of avoidance is defined in the following. We define a construct "[[ x objectavoid* ( c ) y ]]" which is true if "[[ x ]]" is a list of distinct object variables all of which avoid the term "[[ y ]]". 1105 1106 \begin{statements} 1107 1108 \item "[[ eager define distinctvar ( x , c ) as x atom .or. x head objectvar ( c ) .and. .not. x head member x tail .and. distinctvar ( x tail , c ) end define ]]". True if "[[ x ]]" is a list of distinct meta variables. 1109 1110 \item "[[ eager define x objectavoid* ( c ) y as distinctvar ( x , c ) .and. ( objectavoid1 ( x , y , c , true ) catch tail ) end define ]]". True if "[[ x ]]" is a list of object variables none of which occur free in the meta term "[[ y ]]". If some element of "[[ x ]]" definitely occur free in "[[ y ]]" then the function returns "[[ false ]]". If the term contains meta variables then the function returns a list of meta variables which the variables in "[[ x ]]" must avoid in order to avoid "[[ y ]]". 1111 1112 \item "[[ eager define x objectavoid ( c ) y as << x >> objectavoid* ( c ) y end define ]]". Same as above except that "[[ x ]]" is a term rather than a list of terms. 1113 1114 \item "[[ eager define objectavoid1 ( x , y , c , r ) as newline 1115 1116 if x = <<>> then r else newline 1117 1118 let d = y metadef ( c ) in newline 1119 1120 if d = "var" then r set+ y else newline 1121 1122 let d = y valuedef ( c ) in newline 1123 1124 if d = true then if y member x then false raise else r else newline 1125 1126 if d = 0 then objectavoid1 ( x set- y first , y second , c , r ) else newline 1127 1128 if d = 1 then r else newline 1129 1130 objectavoid1* ( x , y tail , c , r ) end define ]]" 1131 1132 \item "[[ eager define objectavoid1* ( x , y , c , r ) as if y atom then r else objectavoid1* ( x , y tail , c , objectavoid1 ( x , y head , c , r ) ) end define ]]" 1133 1134 \end{statements} 1135 1136 1137 1138 \subsection{Substitution freeness} 1139 1140 We shall say that a substitution is \index{free substitution}\index{substitution, free}\intro{free} if one can perform the substitution without renaming. The meta and object versions of freeness are defined in the following. 1141 1142 \begin{statements} 1143 1144 \item "[[ eager define metafree ( x , y , z , c ) as newline 1145 1146 let d = x metadef ( c ) in newline 1147 1148 if d = "var" then true else newline 1149 1150 if d = true then z objectterm ( c ) .or. y metaavoid ( c ) x else newline 1151 1152 if d != "all" then metafree* ( x tail , y , z , c ) else newline 1153 1154 if y t= x first then true else newline 1155 1156 if y metaavoid ( c ) x second then true else newline 1157 1158 x first metaavoid ( c ) z .and. metafree ( x second , y , z , c ) end define ]]". True if one can freely replace the meta variable "[[ y ]]" by the meta term "[[ z ]]" in the meta term "[[ x ]]". 1159 1160 \item "[[ eager define metafree* ( x , y , z , c ) as x atom .or. metafree ( x head , y , z , c ) .and. metafree* ( x tail , y , z , c ) end define ]]" True if one can freely replace the meta variable "[[ y ]]" by the meta term "[[ z ]]" in any element of the list "[[ x ]]" of meta terms. 1161 1162 \item "[[ eager define objectfree ( x , y , z , c ) as newline 1163 1164 if x metadef ( c ) != true then false else newline 1165 1166 let d = x valuedef ( c ) in newline 1167 1168 if d = true then true else newline 1169 1170 if d = 1 then true else newline 1171 1172 if d != 0 then objectfree* ( x tail , y , z , c ) else newline 1173 1174 if y t= x first then true else newline 1175 1176 if y objectavoid ( c ) x second then true else newline 1177 1178 x first objectavoid ( c ) z .and. objectfree ( x second , y , z , c ) end define ]]". True if one can freely replace the object variable "[[ y ]]" by the object term "[[ z ]]" in the object term "[[ x ]]". 1179 1180 \item "[[ eager define objectfree* ( x , y , z , c ) as x atom .or. objectfree ( x head , y , z , c ) .and. objectfree* ( x tail , y , z , c ) end define ]]". True if one can freely replace the object variable "[[ y ]]" by the object term "[[ z ]]" in any element of the list "[[ x ]]" of object terms. 1181 1182 \end{statements} 1183 1184 1185 1186 \subsection{Substitution} 1187 1188 The function "[[ metasubst ( x , s , c ) ]]" defined in the following substitutes variables with terms as specified in the association list "[[ s ]]". Only free occurences of variables in "[[ x ]]" are replaced. The function performs substitution without renaming of free variables and does not check whether or not the substitution if free. Substitution is parallel so that one may use e.g.\ "[[ s = << quote x end quote :: quote y end quote ,, quote y end quote :: quote x end quote >> ]]" to swap "[[ x ]]" and "[[ y ]]". 1189 1190 \begin{statements} 1191 1192 \item "[[ eager define metasubst ( x , s , c ) as newline 1193 1194 let d = x metadef ( c ) in newline 1195 1196 if d = "var" then lookup ( x , s , x ) else newline 1197 1198 if d != "all" then x head :: metasubst* ( x tail , s , c ) else newline 1199 1200 let s = remove ( x first , s ) in newline 1201 1202 << x head ,, x first ,, metasubst ( x second , s , c ) >> end define ]]". 1203 1204 \item "[[ eager define metasubst* ( x , s , c ) as newline 1205 1206 if x atom then true else newline 1207 1208 metasubst ( x head , s , c ) :: metasubst* ( x tail , s , c ) end define ]]" 1209 1210 \end{statements} 1211 1212 The following function is like "[[ metasubst ( x , s , c ) ]]" but also checks that the substitution is free, that "[[ z ]]" is a metaterm, and that if "[[ x ]]" is a metaterm then so is the return value. Returns "[[ true ]]" on error. 1213 1214 \begin{statements} 1215 1216 \item "[[ eager define metasubstc ( x , s , c ) as metasubstc1 ( x , s , true , c ) end define ]]" 1217 1218 \item "[[ eager define metasubstc1 ( x , s , b , c ) as newline 1219 1220 let d = x metadef ( c ) in newline 1221 1222 if d = "var" then metasubstc3 ( x , s , b , c ) else newline 1223 1224 if d then metasubstc2 ( x , s , b , c ) else newline 1225 1226 if d != "all" then x head :: metasubstc1* ( x tail , s , b , c ) else newline 1227 1228 let s = remove ( x first , s ) in newline 1229 1230 << x head ,, x first ,, metasubstc1 ( x second , s , x first :: b , c ) >> end define ]]". 1231 1232 \item "[[ eager define metasubstc1* ( x , s , b , c ) as newline 1233 1234 if x atom then true else newline 1235 1236 metasubstc1 ( x head , s , b , c ) :: metasubstc1* ( x tail , s , b , c ) end define ]]" 1237 1238 \item "[[ eager define metasubstc2 ( x , s , b , c ) as newline 1239 1240 let d = x metadef ( c ) in newline 1241 1242 if d then x head :: metasubstc2* ( x tail , s , b , c ) else newline 1243 1244 let v = lookup ( x , s , true ) in newline 1245 1246 if v then x else newline 1247 1248 let d = v metadef ( c ) in newline 1249 1250 if .not. d .and. d != "var" then newline 1251 1252 error ( x , 1253 LocateProofLine ( x , c ) 1254 diag ( "Substitution of" ) 1255 disp ( x ) 1256 diag ( "with" ) 1257 disp ( v ) 1258 diag ( "produces non-meta-term" ) 1259 end diagnose ) else newline 1260 1261 if metaavoid2* ( b , v , c ) then v else newline 1262 1263 error ( x , 1264 LocateProofLine ( x , c ) 1265 diag ( "At-seqop used for non-free substitution. Attempt to instantiate" ) 1266 disp ( x ) 1267 diag ( "with" ) 1268 disp ( v ) 1269 end diagnose ) end define ]]" 1270 1271 \item "[[ eager define metasubstc2* ( x , s , b , c ) as newline 1272 1273 if x atom then true else newline 1274 1275 metasubstc2 ( x head , s , b , c ) :: metasubstc2* ( x tail , s , b , c ) end define ]]" 1276 1277 \item "[[ eager define metaavoid2* ( x , y , c ) as x .or. x head metaavoid ( c ) y .and. metaavoid2* ( x tail , y , c ) end define ]]" 1278 1279 \item "[[ eager define metasubstc3 ( x , s , b , c ) as newline 1280 1281 let v = lookup ( x , s , true ) in newline 1282 1283 if v then x else newline 1284 1285 if metaavoid2* ( b , v , c ) then v else newline 1286 1287 error ( x , 1288 LocateProofLine ( x , c ) 1289 diag ( "At-seqop used for non-free substitution. Attempt to instantiate" ) 1290 disp ( x ) 1291 diag ( "with" ) 1292 disp ( v ) 1293 end diagnose ) end define ]]" 1294 1295 \item "[[ eager define remove ( x , s ) as newline 1296 1297 if s atom then s else newline 1298 1299 if x t= s head head then remove ( x , s tail ) else newline 1300 1301 s head :: remove ( x , s tail ) end define ]]" 1302 1303 \end{statements} 1304 1305 1306 1307 \subsection{Quantifiers} 1308 1309 The following macro definition allows to write e.g.\ "[[ All #x ,, #y ,, #z : #a ]]" instead of "[[ All #x : All #y : All #z : #a ]]". 1310 1311 \begin{statements} 1312 1313 \item "[[ Macro define All u : v as \ x . expand-All ( x ) end define ]]" 1314 1315 \item "[[ eager define expand-All ( x ) as newline 1316 1317 let << t ,, s ,, c >> = x in newline 1318 1319 let << true ,, u ,, v >> = t in newline 1320 1321 let u = stateexpand ( u , s , c ) in newline 1322 1323 let v = stateexpand ( v , s , c ) in newline 1324 1325 expand-All1 ( t , u , v ) end define ]]" 1326 1327 \item "[[ eager define expand-All1 ( t , u , v ) as newline 1328 1329 if .not. u r= quote x ,, y end quote then back t quote All u unquote : v unquote end quote else newline 1330 1331 expand-All1 ( t , u first , expand-All1 ( t , u second , v ) ) end define ]]" 1332 1333 \end{statements} 1334 1335 1336 1337 \section{Sequents} 1338 1339 \subsection{Term sets}\label{sec:TermSets} 1340 1341 We represent sets of terms by tuples of terms without repetitions so that no two elements "[[ x ]]" and "[[ y ]]" of the tuple satisfy "[[ x t= y ]]". 1342 1343 \begin{statements} 1344 1345 \item "[[ eager define x member y as if y atom then false else x t= y head .or. x member y tail end define ]]". Membership of a set of terms. 1346 1347 \item "[[ eager define x set+ y as if y member x then x else y :: x end define ]]". Add the term "[[ y ]]" to the set "[[ x ]]" of terms. 1348 1349 \item "[[ eager define x set- y as if y member x then x set-- y else x end define ]]". Remove the term "[[ y ]]" from the set "[[ x ]]" of terms. 1350 1351 \item "[[ eager define x set-- y as if x atom then true else if x head t= y then x tail else x head :: x tail set-- y end define ]]" 1352 1353 \item "[[ eager define x subset y as if x atom then true else x head member y .and. x tail subset y end define ]]" 1354 1355 \item "[[ eager define x union y as if x atom then y else x tail union ( y set+ x head ) end define ]]" 1356 1357 \item "[[ eager define x set= y as x subset y .and. y subset x end define ]]" 1358 1359 \end{statements} 1360 1361 1362 1363 \subsection{Sequents} 1364 1365 The sequents of Logiweb sequent calculus have form "[[ << P ,, C ,, R >> ]]" where "[[ P ]]" is a pool of premisses, "[[ C ]]" is a pool of condition (i.e.\ side conditions), and "[[ R ]]" is a result which holds if the given premisses and conditions hold. "[[ P ]]" and "[[ C ]]" are sets of meta terms (c.f. Section \ref{sec:TermSets}) and "[[ R ]]" is a meta term. 1366 1367 \begin{statements} 1368 1369 \item "[[ eager define x sequent= y as x zeroth set= y zeroth .and. x first set= y first .and. x second t= y second end define ]]" 1370 1371 \end{statements} 1372 1373 1374 1375 \subsection{Sequent operators} 1376 1377 The thirteen sequent operators of the Logiweb sequent calculus are: 1378 1379 \begin{statements} 1380 1381 \item "[[ meta define x Init as "Init" end define ]]". Allows to build a sequent with "[[ x ]]" as both premise and result. 1382 1383 \item "[[ meta define x Ponens as "Ponens" end define ]]". Allows to move a premise from result to premise pool. 1384 1385 \item "[[ meta define x Probans as "Probans" end define ]]". Allows to move a condition from result to condition pool. 1386 1387 \item "[[ meta define x Verify as "Verify" end define ]]". Allows to evaluate and remove a condition from the result. 1388 1389 \item "[[ meta define x Curry as "Curry" end define ]]". Allows to change a result from "[[ x oplus y infer z ]]" to "[[ x infer y infer z ]]". 1390 1391 \item "[[ meta define x Uncurry as "Uncurry" end define ]]". Allows to change a result from "[[ x infer y infer z ]]" to "[[ x oplus y infer z ]]" 1392 1393 \item "[[ meta define x Deref as "Dereference" end define ]]". Allows to change the name of a result to the result itself. 1394 1395 \item "[[ meta define x at y as "at" end define ]]". Allows to instantiate a meta quantifier. 1396 1397 \item "[[ meta define x infer y as "infer" end define ]]". Allows to move a premise from premise pool to result. 1398 1399 \item "[[ meta define x endorse y as "endorse" end define ]]". Allows to move a condition from condition pool to result. 1400 1401 \item "[[ meta define x id est y as "id est" end define ]]". Allows to change the result of "[[ x ]]" to the name "[[ y ]]" for the result. 1402 1403 \item "[[ meta define All x : y as "all" end define ]]". Allows to perform meta generalization. 1404 1405 \item "[[ meta define x ;; y as "cut" end define ]]". Allows to perform a cut operation. 1406 1407 \end{statements} 1408 1409 The operators "[[ x infer y ]]", "[[ x endorse y ]]", and "[[ All x : y ]]" may be used both as meta and as sequent operators. Whether they denote the one or the other depends on context. 1410 1411 1412 1413 \subsection{Sequent pseudo operators} 1414 1415 In addition to the genuine sequent operators the following pseudo operators allow to build up the body of a proof. The pseudo operators disappear during unification. 1416 1417 \begin{statements} 1418 1419 \item "[[ meta define x ponens y as "ponens" end define ]]". Same as "[[ x Ponens ]]" but "[[ y ]]" specifies what the moved premise looks like as an aid to unification. 1420 1421 \item "[[ meta define x probans y as "probans" end define ]]". Same as "[[ x Probans ]]" but "[[ y ]]" specifies what the moved condition looks like as an aid to unification. 1422 1423 \item "[[ meta define x verify y as "verify" end define ]]". Same as "[[ x Verify ]]" but "[[ y ]]" specifies what the verified condition looks like as an aid to unification. 1424 1425 \item "[[ meta define x conclude y as "conclude" end define ]]". Same as "[[ x ]]" but "[[ y ]]" specifies what "[[ x ]]" is supposed to prove as an aid to unification. 1426 1427 \item "[[ meta define x At as "At" end define ]]". Same as "[[ x at y ]]" but leaves it to unification to determine "[[ y ]]". 1428 1429 \item "[[ meta define x Infer as "Infer" end define ]]". Same as "[[ y infer x ]]" but leaves it to unification to determine "[[ y ]]". 1430 1431 \item "[[ meta define x Endorse as "Endorse" end define ]]". Same as "[[ y endorse x ]]" but leaves it to unification to determine "[[ y ]]". 1432 1433 \item "[[ meta define x All as "All" end define ]]". Same as "[[ All y : x ]]" but leaves it to unification to determine "[[ y ]]". 1434 1435 \item "[[ meta define x Conclude as "Conclude" end define ]]". Add as many "[[ x at y ]]", "[[ x Ponens ]]", and "[[ x Verify ]]" operations as possible in an attempt to make "[[ x ]]" prove an object term. 1436 1437 \end{statements} 1438 1439 1440 1441 \subsection{Counting of sequent operators} 1442 1443 The following function can be used for profiling tactics in that it returns the number of tactic operators in the term t. 1444 1445 "[[ eager define seqcnt ( t , c ) as newline 1446 1447 if t r= quote x Init end quote then 1 else newline 1448 1449 if t r= quote x Ponens end quote then 1 + seqcnt ( t first , c ) else newline 1450 1451 if t r= quote x Probans end quote then 1 + seqcnt ( t first , c ) else newline 1452 1453 if t r= quote x Verify end quote then 1 + seqcnt ( t first , c ) else newline 1454 1455 if t r= quote x Curry end quote then 1 + seqcnt ( t first , c ) else newline 1456 1457 if t r= quote x Uncurry end quote then 1 + seqcnt ( t first , c ) else newline 1458 1459 if t r= quote x Deref end quote then 1 + seqcnt ( t first , c ) else newline 1460 1461 if t r= quote x at y end quote then 1 + seqcnt ( t first , c ) else newline 1462 1463 if t r= quote x infer y end quote then 1 + seqcnt ( t second , c ) else newline 1464 1465 if t r= quote x endorse y end quote then 1 + seqcnt ( t second , c ) else newline 1466 1467 if t r= quote x id est y end quote then 1 + seqcnt ( t first , c ) else newline 1468 1469 if t r= quote All x : y end quote then 1 + seqcnt ( t second , c ) else newline 1470 1471 if t r= quote x ;; y end quote then 1 + seqcnt ( t first , c ) + seqcnt ( t second , c ) else newline 1472 1473 error ( t , 1474 LocateProofLine ( t , c ) 1475 diag ( "In seqcnt: Unknown seqop in root of" ) 1476 disp ( t ) 1477 end diagnose ) 1478 1479 end define ]]" 1480 1481 1482 1483 \subsection{Error message construct} 1484 1485 The "[[ eager define error ( x , y ) as ( dbug ( x ) y ) raise end define ]]" construct is useful for signaling errors. The construct signals that an error has occurred by raising an exception. Exceptions take one parameter, and "[[ error ( x , y ) ]]" raises an exception with parameter "[[ y ]]". That parameter is supposed to be a term which, when typeset, explains to a human reader what went wrong. 1486 1487 If the term "[[ y ]]" contains no useful ``debugging information'' then "[[ error ( x , y ) ]]" takes the debugging information from "[[ x ]]". At the time of writing, the debugging information is not used. As an example of use, a Logiweb browser could have a button for moving to the proof line in error. As another example, a custom renderer could add a hypertarget to the line in error such that one could navigate to it using an ordinary web browser. 1488 1489 1490 1491 \subsection{Pattern recognition} 1492 1493 The `mismatch' construct defined in the following is such that e.g.\ "[[ mismatch ( quote x infer y end quote , R , c ) ]]" is false if "[[ R ]]" has form "[[ x infer y ]]". 1494 1495 \begin{statements} 1496 1497 \item "[[ eager define mismatch ( x , y , c ) as newline 1498 1499 let a = x metadef ( c ) in newline 1500 1501 if a = true then false else newline 1502 1503 if a != y metadef ( c ) then true else mismatch* ( x tail , y tail , c ) end define ]]" 1504 1505 1506 1507 \item "[[ eager define mismatch* ( x , y , c ) as newline 1508 1509 if x atom .and. y atom then false else newline 1510 1511 if x atom .or. y atom then true else newline 1512 1513 mismatch ( x head , y head , c ) .or. mismatch* ( x tail , y tail , c ) end define ]]" 1514 1515 \end{statements} 1516 1517 1518 1519 \subsection{Sequent evaluator} 1520 1521 "[[ seqeval ( t , c ) ]]" evaluates the sequent term "[[ t ]]". The result is either an exception or a valid sequent "[[ s ]]". In the latter case, "[[ t ]]" is said to be a sequent proof of "[[ s ]]". 1522 1523 \vspace{\abovedisplayskip} 1524 1525 \noindent "[[ eager define seqeval ( t , c ) as newline 1526 1527 "";timer ( "seqeval" ) .then. newline 1528 1529 if t r= quote x Init end quote then eval-Init ( t first , c ) else newline 1530 1531 if t r= quote x Ponens end quote then eval-Ponens ( seqeval ( t first , c ) , t first , c ) else newline 1532 1533 if t r= quote x Probans end quote then eval-Probans ( seqeval ( t first , c ) , t first , c ) else newline 1534 1535 if t r= quote x Verify end quote then eval-Verify ( seqeval ( t first , c ) , t first , c ) else newline 1536 1537 if t r= quote x Curry end quote then eval-Curry ( seqeval ( t first , c ) , t first , c ) else newline 1538 1539 if t r= quote x Uncurry end quote then eval-Uncurry ( seqeval ( t first , c ) , t first , c ) else newline 1540 1541 if t r= quote x Deref end quote then eval-Deref ( seqeval ( t first , c ) , t first , c ) else newline 1542 1543 if t r= quote x at y end quote then eval-at ( t , true , c ) else newline 1544 1545 if t r= quote x infer y end quote then eval-infer ( t first , seqeval ( t second , c ) , t second , c ) else newline 1546 1547 if t r= quote x endorse y end quote then eval-endorse ( t first , seqeval ( t second , c ) , t second , c ) else newline 1548 1549 if t r= quote x id est y end quote then eval-ie ( seqeval ( t first , c ) , t second , t first , c ) else newline 1550 1551 if t r= quote All x : y end quote then eval-all ( t first , seqeval ( t second , c ) , t second , c ) else newline 1552 1553 if t r= quote x ;; y end quote then eval-cut ( seqeval ( t first , c ) , seqeval ( t second , c ) , c ) else newline 1554 1555 error ( t , 1556 LocateProofLine ( t , c ) 1557 diag ( "Unknown seqop in root of" ) 1558 disp ( t ) 1559 end diagnose ) 1560 1561 end define ]]" 1562 1563 1564 1565 \subsection{Definitions of sequent operators} 1566 1567 The individual sequent operators of the Logiweb sequent calculus are defined as follows: 1568 1569 \begin{statements} 1570 1571 \item "[[ eager define eval-Init ( x , c ) as newline 1572 1573 "";timer ( "eval-Init" ) .then. newline 1574 1575 if x metaterm ( c ) then << << x >> ,, <<>> ,, x >> else newline 1576 1577 error ( x , 1578 LocateProofLine ( x , c ) 1579 diag ( "Init-seqop used on non-meta term:" ) 1580 disp ( x ) 1581 end diagnose ) 1582 1583 end define ]]" 1584 1585 1586 1587 \item "[[ eager define eval-Ponens ( x , d , c ) as newline 1588 1589 "";timer ( "eval-Ponens" ) .then. newline 1590 1591 let << P ,, C ,, R >> = x in newline 1592 1593 if mismatch ( quote x infer y end quote , R , c ) then newline 1594 1595 error ( d , 1596 LocateProofLine ( d , c ) 1597 diag ( "Ponens-seqop used on non-inference:" ) 1598 disp ( R ) 1599 end diagnose ) else newline 1600 1601 let << true ,, P prime ,, R prime >> = R in newline 1602 1603 << P set+ P prime ,, C ,, R prime >> end define ]]" 1604 1605 1606 1607 \item "[[ eager define eval-Probans ( x , d , c ) as newline 1608 1609 "";timer ( "eval-Probans" ) .then. newline 1610 1611 let << P ,, C ,, R >> = x in newline 1612 1613 if mismatch ( quote x endorse y end quote , R , c ) then newline 1614 1615 error ( d , 1616 LocateProofLine ( d , c ) 1617 diag ( "Probans-seqop used on non-endorsement:" ) 1618 disp ( R ) 1619 end diagnose ) else newline 1620 1621 let << true ,, C prime ,, R prime >> = R in newline 1622 1623 << P ,, C set+ C prime ,, R prime >> end define ]]" 1624 1625 1626 1627 \item "[[ eager define eval-Verify ( x , d , c ) as newline 1628 1629 "";timer ( "eval-Verify" ) .then. newline 1630 1631 let << P ,, C ,, R >> = x in newline 1632 1633 if mismatch ( quote x endorse y end quote , R , c ) then newline 1634 1635 error ( d , 1636 LocateProofLine ( d , c ) 1637 diag ( "Verify-seqop used on non-endorsement:" ) 1638 disp ( R ) 1639 end diagnose ) else newline 1640 1641 let << true ,, C prime ,, R prime >> = R in newline 1642 1643 if ( eval ( C prime , true , c ) apply c maptag ) untag catch = false :: true then << P ,, C ,, R prime >> else newline 1644 1645 error ( d , 1646 LocateProofLine ( d , c ) 1647 diag ( "Verify-seqop used on false condition:" ) 1648 disp ( C prime ) 1649 end diagnose ) 1650 1651 end define ]]" 1652 1653 1654 1655 \item "[[ eager define eval-Curry ( x , d , c ) as newline 1656 1657 "";timer ( "eval-Curry" ) .then. newline 1658 1659 let << P ,, C ,, R >> = x in newline 1660 1661 if mismatch ( quote ( x oplus y ) infer z end quote , R , c ) then newline 1662 1663 error ( d , 1664 LocateProofLine ( d , c ) 1665 diag ( "Curry-seqop used on unfit argument:" ) 1666 disp ( R ) 1667 end diagnose ) else newline 1668 1669 let back true quote ( X unquote oplus Y unquote ) infer Z unquote end quote = R in newline 1670 1671 << P ,, C ,, back R quote X unquote infer Y unquote infer Z unquote end quote >> end define ]]" 1672 1673 1674 1675 \item "[[ eager define eval-Uncurry ( x , d , c ) as newline 1676 1677 "";timer ( "eval-Uncurry" ) .then. newline 1678 1679 let << P ,, C ,, R >> = x in newline 1680 1681 if mismatch ( quote x infer y infer z end quote , R , c ) then newline 1682 1683 error ( d , 1684 LocateProofLine ( d , c ) 1685 diag ( "Uncurry-seqop used on unfit argument:" ) 1686 disp ( R ) 1687 end diagnose ) else newline 1688 1689 let back true quote X unquote infer Y unquote infer Z unquote end quote = R in newline 1690 1691 << P ,, C ,, back R quote ( X unquote oplus Y unquote ) infer Z unquote end quote >> end define ]]" 1692 1693 1694 1695 \item "[[ eager define eval-Deref ( x , d , c ) as newline 1696 1697 "";timer ( "eval-Deref" ) .then. newline 1698 1699 let << P ,, C ,, R >> = x in newline 1700 1701 let R prime = R stmt-rhs ( c ) in newline 1702 1703 if R prime = true then newline 1704 1705 error ( d , 1706 LocateProofLine ( d , c ) 1707 diag ( "Deref-seqop used on undefined statement:" ) 1708 disp ( R ) 1709 end diagnose ) else newline 1710 1711 if R prime metaterm ( c ) then << P ,, C ,, R prime >> else newline 1712 1713 error ( d , 1714 LocateProofLine ( d , c ) 1715 diag ( "Deref-seqop applied to" ) 1716 disp ( R ) 1717 diag ( "produced non-meta term:" ) 1718 disp ( R prime ) 1719 end diagnose ) 1720 1721 end define ]]" 1722 1723 1724 1725 \item "[[ eager define eval-at ( x , v , c ) as newline 1726 1727 "";timer ( "eval-at" ) .then. newline 1728 1729 if .not. x r= quote x at y end quote then 1730 1731 let << P ,, C ,, R >> = seqeval ( x , c ) in newline 1732 1733 << P ,, C ,, eval-at1 ( R , v , true , x , c ) >> else newline 1734 1735 if x second metaterm ( c ) then eval-at ( x first , x second :: v , c ) else newline 1736 1737 error ( x , 1738 LocateProofLine ( x , c ) 1739 diag ( "At-seqop used on non-meta-term:" ) 1740 disp ( x second ) 1741 end diagnose ) end define ]]" 1742 1743 \item "[[ eager define eval-at1 ( R , v , s , d , c ) as newline 1744 1745 if v then metasubstc ( R , s , c ) else newline 1746 1747 if mismatch ( quote All x : y end quote , R , c ) then 1748 1749 error ( d , 1750 LocateProofLine ( d , c ) 1751 diag ( "At-seqop used on non-quantifier:" ) 1752 disp ( R ) 1753 end diagnose ) else newline 1754 1755 eval-at1 ( R second , v tail , ( R first :: v head ) :: s , d , c ) end define ]]" 1756 1757 1758 1759 \item "[[ eager define eval-infer ( x , y , d , c ) as newline 1760 1761 "";timer ( "eval-infer" ) .then. newline 1762 1763 if .not. x metaterm ( c ) then newline 1764 1765 error ( d , 1766 LocateProofLine ( d , c ) 1767 diag ( "Infer-seqop used on non-meta term:" ) 1768 disp ( x ) 1769 end diagnose ) else newline 1770 1771 let << P ,, C ,, R >> = y in newline 1772 1773 << P set- x ,, C ,, back R quote x unquote infer R unquote end quote >> 1774 1775 end define ]]" 1776 1777 1778 1779 \item "[[ eager define eval-endorse ( x , y , d , c ) as newline 1780 1781 "";timer ( "eval-endorse" ) .then. newline 1782 1783 if .not. x metaterm ( c ) then newline 1784 1785 error ( d , 1786 LocateProofLine ( d , c ) 1787 diag ( "Endorse-seqop used on non-meta term:" ) 1788 disp ( x ) 1789 end diagnose ) else newline 1790 1791 let << P ,, C ,, R >> = y in newline 1792 1793 << P ,, C set- x ,, back R quote x unquote endorse R unquote end quote >> 1794 1795 end define ]]" 1796 1797 1798 1799 \item "[[ eager define eval-ie ( x , y , d , c ) as newline 1800 1801 "";timer ( "eval-ie" ) .then. newline 1802 1803 let << P ,, C ,, R >> = x in newline 1804 1805 if R t= y stmt-rhs ( c ) then newline 1806 1807 << P ,, C ,, y >> else newline 1808 1809 error ( d , 1810 LocateProofLine ( d , c ) 1811 diag ( "IdEst-seqop used on non-matching result. Attempt to match" ) 1812 disp ( y ) 1813 diag ( "with" ) 1814 disp ( R ) 1815 end diagnose ) 1816 1817 end define ]]" 1818 1819 1820 1821 \item "[[ eager define eval-all ( x , y , d , c ) as newline 1822 1823 "";timer ( "eval-all" ) .then. newline 1824 1825 let << P ,, C ,, R >> = y in newline 1826 1827 if .not. x metaavoid* ( c ) P then newline 1828 1829 error ( d , 1830 LocateProofLine ( d , c ) 1831 diag ( "All-seqop catches variable" ) 1832 disp ( x ) 1833 diag ( "which is free in the following premise:" ) 1834 disp ( x metaavoid* ( c ) P ) 1835 end diagnose ) else newline 1836 1837 if .not. x metaavoid* ( c ) C then newline 1838 1839 error ( d , 1840 LocateProofLine ( d , c ) 1841 diag ( "All-seqop catches variable" ) 1842 disp ( x ) 1843 diag ( "which is free in the following condition:" ) 1844 disp ( x metaavoid* ( c ) C ) 1845 end diagnose ) else newline 1846 1847 << P ,, C ,, back R quote All x unquote : R unquote end quote >> end define ]]" 1848 1849 1850 1851 \item "[[ eager define eval-cut ( x , y , c ) as newline 1852 1853 "";timer ( "eval-cut" ) .then. newline 1854 1855 let << P ,, C ,, R >> = x in newline 1856 1857 let << P prime ,, C prime ,, R prime >> = y in newline 1858 1859 << P union ( P prime set- R ) ,, C union C prime ,, R prime >> end define ]]" 1860 1861 \end{statements} 1862 1863 1864 1865 \section{Proof construction} 1866 1867 \subsection{Location information} 1868 1869 \begin{statements} 1870 1871 \item "[[ locate define proof of x : y as "proof" :: 1 end define ]]". State that the given construct defines a proof and that the name of the proof is the first argument. 1872 1873 \item "[[ locate define x proof of y : z as "proof" :: 2 end define ]]". State that the given construct defines a proof and that the name of the proof is the second argument. 1874 1875 \item "[[ locate define proof define x as y end define as "proof" :: 1 end define ]]". State that the given construct defines a proof and that the name of the proof is the first argument. 1876 1877 \item "[[ locate define line asterisk : asterisk >> asterisk ; asterisk as "line" :: 1 end define ]]". State that the given construct defines a proof line and that the name of the proof line is the first argument. 1878 1879 \item "[[ locate define line asterisk : asterisk >> asterisk ; as "line" :: 1 end define ]]" 1880 1881 \item "[[ locate define line asterisk : asterisk >> asterisk qed as "line" :: 1 end define ]]" 1882 1883 \item "[[ locate define line asterisk : Premise >> asterisk ; asterisk as "line" :: 1 end define ]]" 1884 1885 \item "[[ locate define line asterisk : Condition >> asterisk ; asterisk as "line" :: 1 end define ]]" 1886 1887 \item "[[ locate define line asterisk : Arbitrary >> asterisk ; asterisk as "line" :: 1 end define ]]" 1888 1889 \item "[[ locate define line asterisk : Local >> asterisk = asterisk ; asterisk as "line" :: 1 end define ]]" 1890 1891 \item "[[ locate define line asterisk : Block >> Begin ; asterisk line asterisk : Block >> End ; asterisk as "line" :: 3 end define ]]" 1892 1893 \end{statements} 1894 1895 1896 1897 \subsection{Error message generation} 1898 1899 \begin{statements} 1900 1901 \item "[[ eager define make-string ( d , x ) as << << 0 ,, x ,, d >> >> end define ]]". Convert the string "[[ x ]]" to a tree which represents the term 1902 1903 \item "[[ eager define dbug ( x ) y as newline 1904 1905 if y debug != true then y else newline 1906 1907 make-root ( x , y ) :: dbug* ( x ) y tail 1908 1909 end define ]]" 1910 1911 \item "[[ eager define dbug* ( x ) y as if y then true else ( dbug ( x ) y head ) :: dbug* ( x ) y tail end define ]]" 1912 1913 \item "[[ eager define glue ( x ) y as << make-root ( true , show quote glue' ( x ) y end quote end show ) ,, make-string ( true , x ) ,, y >> end define ]]" 1914 1915 \item "[[ eager define diag ( x ) y as << make-root ( true , show quote diag' ( x ) y end quote end show ) ,, make-string ( true , x ) ,, y >> end define ]]" 1916 1917 \item "[[ eager define disp ( x ) y as << make-root ( true , show quote disp' ( x ) y end quote end show ) ,, x ,, y >> end define ]]" 1918 1919 \item "[[ eager define form ( x ) y as << make-root ( true , show quote form' ( x ) y end quote end show ) ,, x ,, y >> end define ]]" 1920 1921 \item "[[ eager define end diagnose as make-string ( true , show "". end show ) end define ]]" 1922 1923 \end{statements} 1924 1925 1926 1927 \subsection{Error location} 1928 1929 \begin{statements} 1930 1931 \item "[[ eager define Locate ( t , s , c ) as newline 1932 1933 let true :: d = reverse ( t debug head ) catch in newline 1934 1935 let e :: v = Locate1 ( d tail , c [[ d head ]] [[ "body" ]] , s , true , c ) catch in newline 1936 1937 if e then exception else v 1938 1939 end define ]]". "[[ t ]]" is supposed to be a term which has been macro expanded. If macro expansion has been set up properly, then it is possible to locate where "[[ t ]]" came from before macro expansion. "[[ d ]]" is set to that location encoded as a list "[[ << r ,, i _ { 0 } ,, *** ,, i _ { n } >> ]]" where "[[ r ]]" is the reference of the page where the term occurred and "[[ i _ { 0 } ,, *** ,, i _ { n } ]]" is a path from the root of that page to the term. That path is traversed and for each symbol on the path, the locate aspect is looked up. The locate aspect is supposed to be a pair of a string and a value. If the string equals "[[ s ]]" then a pair of the symbol with subtrees and the value is returned. If more than one node matches, the last one (the one closest to "[[ t ]]") is returned. If no nodes match, then "[[ true ]]" is returned. 1940 1941 \item "[[ eager define Locate1 ( d , t , s , r , c ) as newline 1942 1943 if t then r else newline 1944 1945 let v = t locate-rhs ( c ) in newline 1946 1947 let v = if v then true else eval ( v , true , c ) untag in newline 1948 1949 let r = if v head = s then t :: v tail else r in newline 1950 1951 if d atom then r else newline 1952 1953 Locate1 ( d tail , nth ( d head , t tail ) , s , r , c ) 1954 1955 end define ]]" 1956 1957 \item "[[ eager define LocateProofLine ( v , c ) y as newline 1958 1959 let p = Locate ( v , "proof" , c ) in newline 1960 1961 let l = Locate ( v , "line" , c ) in newline 1962 1963 if .not. p .and. .not. l then newline 1964 1965 dbug ( v ) 1966 diag ( "Line" ) 1967 form ( nth ( l tail , l head ) ) 1968 diag ( "in proof of" ) 1969 form ( nth ( p tail , p head ) ) 1970 glue ( ":\newline " ) 1971 y else newline 1972 1973 if .not. p then newline 1974 1975 dbug ( v ) 1976 diag ( "In proof of" ) 1977 form ( nth ( p tail , p head ) ) 1978 glue ( ":\newline " ) 1979 y else newline 1980 1981 dbug ( v ) 1982 diag ( "Cannot locate error." ) 1983 diag ( "Look at ``macro'' and ``locate'' definitions." ) 1984 diag ( "". ) 1985 y 1986 1987 end define ]]" 1988 1989 \end{statements} 1990 1991 1992 1993 \subsection{Proof checker} 1994 1995 \begin{statements} 1996 1997 \item "[[ eager define claiming ( x , y ) as newline 1998 1999 if .not. y r= quote u &c v end quote then x t= y else newline 2000 2001 claiming ( x , y first ) .or. claiming ( x , y second ) end define ]]". 2002 2003 True if "[[ x ]]" is among the conjuncts of a term "[[ y ]]" built up from conjunctions and "[[ u &c v ]]". 2004 2005 \item "[[ value define proofcheck as \ c . proofcheck1 ( c ) end define ]]". 2006 2007 Suited as conjunct in the claim of a page. 2008 2009 \item "[[ verifier test1 &c proofcheck end verifier ]]". 2010 2011 Use both proofcheck and test1 as verifiers. 2012 2013 \item "[[ eager define proofcheck1 ( c ) as newline 2014 2015 let e :: v = proofcheck2 ( c ) catch in newline 2016 2017 "";timer ( true ) .then. newline 2018 2019 if v != true then diagnose v end diagnose else newline 2020 2021 if .not. e then true else newline 2022 2023 diagnose show quote "In proof checker: unprocessed exception" end quote end show end diagnose end define ]]". 2024 2025 Proofcheck page. Errors are reported as exceptions whose value is a term to be typeset as diagnose and for which the debugging information of the root indicates the location of the error. 2026 2027 \item "[[ eager define proofcheck2 ( c ) as newline 2028 2029 let r = c [[ 0 ]] in newline 2030 2031 "";timer ( "seqeval*" ) .then. newline 2032 2033 let a = seqeval* ( c [[ r ]] [[ "codex" ]] [[ r ]] , c ) in newline 2034 2035 "";timer ( "circularitycheck1" ) .then. newline 2036 2037 let x = circularitycheck1 ( r , c , a , a ) in true end define ]]". 2038 2039 Check all proofs on the page using "[[ seqeval* ( a , c ) ]]", then check that the proofs do not reference each other in a circular way. 2040 2041 \item "[[ eager define seqeval* ( a , c ) as newline 2042 2043 if a = true then true else newline 2044 2045 let x :: y = a in newline 2046 2047 if .not. x intp then seqeval* ( x , c ) :: seqeval* ( y , c ) else newline 2048 2049 let d = y [[ 0 ]] [[ proof ]] in 2050 2051 if d = true then true else newline 2052 2053 "";timer ( d second ) .then. newline 2054 2055 print ( d second rhs ( c , !"name" ) idx :: LF ) .then. newline 2056 2057 "";timer ( "tactic" ) .then. newline 2058 2059 let e :: p = ( eval ( d third , true , c ) apply d maptag apply c maptag ) untag [[ hook-arg ]] catch in newline 2060 2061 "";timer ( true ) .then. newline 2062 2063 if e .and. p then 2064 error ( d second , 2065 diag ( "Malformed proof of" ) 2066 form ( d second ) 2067 end diagnose ) else newline 2068 2069 if e then p raise else newline 2070 2071 "";timer ( "seqeval" ) .then. newline 2072 2073 let e :: S = seqeval ( p , c ) catch in newline 2074 2075 "";timer ( true ) .then. newline 2076 2077 if e .and. S then 2078 error ( d second , 2079 diag ( "Malformed sequent proof of" ) 2080 form ( d second ) 2081 end diagnose ) else newline 2082 2083 if e then S raise else newline 2084 2085 let << P ,, C ,, R >> = S in newline 2086 2087 if C != <<>> then 2088 error ( d second , 2089 diag ( "In proof of" ) 2090 form ( d second ) 2091 glue ( ":\newline " ) 2092 diag ( "Unchecked sidecondition:" ) 2093 disp ( C head ) 2094 end diagnose ) else newline 2095 2096 let l = y [[ 0 ]] [[ statement ]] in newline 2097 2098 if l = true then 2099 error ( d second , 2100 diag ( "Proof of non-existent lemma:" ) 2101 disp ( d second ) 2102 end diagnose ) else newline 2103 2104 if .not. l third t= R then newline 2105 2106 error ( d , 2107 diag ( "The proof of" ) 2108 disp ( d second ) 2109 diag ( "does not prove what the lemma says." ) 2110 diag ( "After macro expansion, the lemma says:" ) 2111 disp ( l third ) 2112 diag ( "After macro, tactic, and sequent expansion, the proof concludes:" ) 2113 disp ( R ) 2114 end diagnose ) else newline 2115 2116 premisecheck* ( P , c ) .and. x :: S end define ]]". 2117 2118 Sequent evaluate all proofs in the array "[[ a ]]" and return an array of sequents. Proofs are tactic evaluated first end the resulting sequents are checked for everything except circularities. 2119 2120 \item "[[ eager define premisecheck* ( P , c ) as newline 2121 2122 if P atom then true else premisecheck ( P head , c ) .and. premisecheck* ( P tail , c ) end define ]]". 2123 2124 Check each premise in the list "[[ P ]]" of premisses. 2125 2126 \item "[[ eager define checked ( r , c ) as newline 2127 2128 let x = c [[ r ]] [[ "codex" ]] [[ r ]] [[ 0 ]] [[ 0 ]] [[ "claim" ]] third in newline 2129 2130 if claiming ( quote proofcheck end quote , x ) then true else newline 2131 2132 if .not. x then false else newline 2133 2134 let r = c [[ r ]] [[ "bibliography" ]] first in newline 2135 2136 if r then false else newline 2137 2138 let x = c [[ r ]] [[ "codex" ]] [[ r ]] [[ 0 ]] [[ 0 ]] [[ "claim" ]] third in newline 2139 2140 claiming ( quote proofcheck end quote , x ) end define ]]". True if the page with reference "[[ r ]]" has been checked by "[[ proofcheck ]]". 2141 2142 \item "[[ eager define premisecheck ( P , c ) as newline 2143 2144 let r = P ref in let i = P idx in newline 2145 2146 if r != c [[ 0 ]] .and. c [[ r ]] [[ "diagnose" ]] untag != true then newline 2147 2148 error ( P , 2149 diag ( "Lemma" ) 2150 disp ( P ) 2151 diag ( "occurs on a page with a non-empty diagnose." ) 2152 diag ( "Avoid referencing that lemma." ) 2153 end diagnose ) else newline 2154 2155 if .not. checked ( r , c ) then newline 2156 2157 error ( P , 2158 diag ( "Lemma" ) 2159 disp ( P ) 2160 diag ( "occurs on a page which has not been checked" ) 2161 diag ( "by the present proof checker." ) 2162 diag ( "Avoid referencing that lemma." ) 2163 end diagnose ) else newline 2164 2165 if P proof-rhs ( c ) then newline 2166 2167 error ( P , 2168 LocateProofLine ( P , c ) 2169 diag ( "Lemma" ) 2170 disp ( P ) 2171 diag ( "has no proof. Avoid referencing that lemma." ) 2172 end diagnose ) else true end define ]]". 2173 2174 Check that a referenced lemma occurs on a correct page ("[[ "diagnose" = true ]]"), has been checked (claim contains verifier), and has been proved (has non-empty proof aspect). 2175 2176 \item "[[ eager define circularitycheck1 ( r , c , a , q ) as newline 2177 2178 if a = true then q else newline 2179 2180 let x :: y = a in newline 2181 2182 if x intp then circularitycheck2 ( r , c , x , q ) else 2183 2184 circularitycheck1 ( r , c , y , circularitycheck1 ( r , c , x , q ) ) end define ]]". 2185 2186 Check all indices in "[[ a ]]" for circularities. "[[ q ]]" is an array of sequents. The elements of "[[ q ]]" are set to "[[ 0 ]]" while they are being checked for circularities and are set to "[[ 1 ]]" when it has been verified that they are not circular. 2187 2188 \item "[[ eager define circularitycheck2 ( r , c , i , q ) as newline 2189 2190 let v = q [[ i ]] in newline 2191 2192 if v = 0 then newline 2193 2194 let n = c [[ r ]] [[ "codex" ]] [[ r ]] [[ i ]] [[ 0 ]] [[ proof ]] second in newline 2195 2196 error ( n , 2197 diag ( "Circular proof. The vicious circle includes lemma" ) 2198 disp ( n ) 2199 end diagnose ) else newline 2200 2201 if v = 1 then q else newline 2202 2203 circularitycheck2* ( r , c , v head , q [[ i -> 0 ]] ) [[ i -> 1 ]] end define ]]". 2204 2205 Check the proof with index "[[ i ]]" for circularities. 2206 2207 \item "[[ eager define circularitycheck2* ( r , c , l , q ) as newline 2208 2209 if l atom then q else newline 2210 2211 let p :: l = l in newline 2212 2213 let q = circularitycheck2* ( r , c , l , q ) in newline 2214 2215 if r != p ref then q else 2216 2217 circularitycheck2 ( r , c , p idx , q ) end define ]]". 2218 2219 Check all proofs in the list "[[ l ]]" of terms for circularity. 2220 2221 \item "[[ statement define lemma1 as All #x : All #y : #x infer #y infer #x end define ]]". 2222 2223 Manually stated lemma for testing. 2224 2225 \item "[[ proof define lemma1 as \ p . \ c . true [[ hook-arg -> quote All #x : All #y : #x infer #y infer #x Init end quote ]] end define ]]". 2226 2227 Manually stated proof for testing. 2228 2229 \end{statements} 2230 2231 2232 2233 \subsection{Conversions from values to terms} 2234 2235 The following are useful for constructing indexed variables: 2236 2237 \begin{statements} 2238 2239 \item "[[ eager define int2string ( t , v ) as newline 2240 2241 if v > 0 then << 0 :: int2string1 ( v , "". ) :: t debug >> else newline 2242 2243 if v = 0 then << 0 :: "0" :: t debug >> else newline 2244 2245 << 0 :: 256 * int2string1 ( - v , "". ) + logand ( "-" , 255 ) :: t debug >> end define ]]" 2246 2247 \item "[[ eager define int2string1 ( v , r ) as newline 2248 2249 if v = 0 then r else newline 2250 2251 let z = logand ( "0" , 255 ) in newline 2252 2253 let x :: y = floor ( v , 10 ) in newline 2254 2255 int2string1 ( x , 256 * r + z + y ) end define ]]" 2256 2257 \item "[[ eager define val2term ( t , v ) as newline 2258 2259 if v = true then back t quote true end quote else newline 2260 2261 if v = false then back t quote false end quote else newline 2262 2263 if v pairp then back t quote val2term ( t , v head ) unquote :: val2term ( t , v tail ) unquote end quote else newline 2264 2265 if v mapp then back t quote map ( *** ) end quote else newline 2266 2267 if v objectp then back t quote object ( val2term ( t , destruct ( v ) ) unquote ) end quote else 2268 2269 if v = 0 then back t quote 0 end quote else newline 2270 2271 if v < 0 then back t quote - card2term ( t , - v ) unquote end quote else newline 2272 2273 card2term ( t , v ) end define ]]" 2274 2275 \item "[[ eager define card2term ( t , v ) as newline 2276 2277 if v = 0 then back t quote %% end quote else newline 2278 2279 if evenp ( v ) 2280 then back t quote card2term ( t , half ( v ) ) unquote %0 end quote 2281 else back t quote card2term ( t , half ( v ) ) unquote %1 end quote end define ]]". 2282 2283 \end{statements} 2284 2285 2286 2287 \subsection{Unification} 2288 2289 \begin{statements} 2290 2291 \item "[[ eager define univar ( t , v , i ) as 2292 back t quote unifresh ( v unquote , int2string ( t , i ) unquote ) end quote end define ]]" 2293 2294 \item "[[ eager define pterm ( t , c ) as pterm1 ( t , true , 1 , c ) end define ]]". 2295 2296 We shall refer to terms in which some of the bound meta variables are replaced by fresh variables indexed by numbers as \index{term, parameter}\index{parameter term}\intro{parameter terms}. "[[ pterm ( t , c ) ]]" replaces meta variables bound at the top level in "[[ t ]]". The function is used e.g.\ on instances of lemmas in proofs before unification. That allows to recognize instantiable meta variables after their associated quantifiers have been removed. "[[ c ]]" should be the cache of the page. 2297 2298 \item "[[ eager define pterm1 ( t , s , n , c ) as newline 2299 2300 let d = t metadef ( c ) in newline 2301 2302 if d != "all" then pterm2 ( t , s , c ) else newline 2303 2304 let v = univar ( t first , t first , n ) in newline 2305 2306 let t prime = pterm1 ( t second , ( t first :: v ) :: s , n + 1 , c ) in newline 2307 2308 back t quote All v unquote : t prime unquote end quote end define ]]". 2309 2310 \item "[[ eager define pterm2 ( t , s , c ) as newline 2311 2312 let d = t metadef ( c ) in newline 2313 2314 let s = if d = "all" then ( t first :: t first ) :: s else s in newline 2315 2316 if d != "var" then t head :: pterm2* ( t tail , s , c ) else newline 2317 2318 let n = lookup ( t , s , true ) in newline 2319 2320 if n = true then t else n end define ]]" 2321 2322 \item "[[ eager define pterm2* ( t , s , c ) as newline 2323 2324 if t atom then true else newline 2325 2326 pterm2 ( t head , s , c ) :: pterm2* ( t tail , s , c ) end define ]]" 2327 2328 \item "[[ eager define inst ( t , d , a ) as newline 2329 2330 if .not. t r= quote unifresh ( true , true ) end quote then ( t ref :: t idx :: d debug ) :: inst* ( t tail , d , a ) else newline 2331 2332 let u = a [[ t second idx ]] in 2333 2334 if u != true then inst ( u , d , a ) else newline 2335 2336 error ( d , 2337 diag ( "Incomplete unification. Uninstantiated variable:" ) 2338 disp ( t ) 2339 end diagnose ) end define ]]". 2340 2341 Instantiate the parameter term "[[ t ]]" as specified by the array "[[ a ]]". May loop indefinitely. As an example, a substitution which maps "[[ #x ]]" to "[[ #x :: #x ]]" will keep expanding "[[ #x ]]" forever. We shall say that a substitution is \index{circular substitution}\index{substitution, circular}\intro{circular} if there exists a term "[[ t ]]" for which "[[ inst ( t , d , x ) ]]" loops indefinitely. 2342 2343 \item "[[ eager define inst* ( t , d , a ) as if t atom then true else inst ( t head , d , a ) :: inst* ( t tail , d , a ) end define ]]". 2344 2345 \item "[[ eager define occur ( t , u , s ) as newline 2346 2347 if u r= quote unifresh ( true , true ) end quote then t t= u .or. occur ( t , s [[ u second idx ]] , s ) else newline 2348 2349 occur* ( t , u tail , s ) end define ]]". 2350 2351 True if "[[ t ]]" occurs in "[[ inst ( u , d , s ) ]]". May loop indefinitely if "[[ s ]]" is circular. 2352 2353 \item "[[ eager define occur* ( t , u , s ) as newline 2354 2355 if u atom then false else occur ( t , u head , s ) .or. occur* ( t , u tail , s ) end define ]]". 2356 2357 \item "[[ eager define unify ( t , u , s ) as newline 2358 2359 if t r= quote unifresh ( true , true ) end quote then unify2 ( t , u , s ) else newline 2360 2361 if u r= quote unifresh ( true , true ) end quote then unify2 ( u , t , s ) else newline 2362 2363 if t r= u then unify* ( t tail , u tail , s ) else newline 2364 2365 error ( t , 2366 diag ( "Unable to unify" ) 2367 disp ( t ) 2368 diag ( "with" ) 2369 disp ( u ) 2370 end diagnose ) 2371 2372 end define ]]". 2373 2374 If possible, return the `smallest' substitution which contains "[[ s ]]" and unifies the parameter terms "[[ t ]]" and "[[ u ]]", i.e.\ a substitution which, if applied to "[[ t ]]" and "[[ u ]]" yield identical terms. Raise an exception if unification is impossible. 2375 2376 \item "[[ eager define unify* ( t , u , s ) as newline 2377 2378 if t atom then s else newline 2379 2380 unify* ( t tail , u tail , unify ( t head , u head , s ) ) end define ]]". 2381 2382 \item "[[ eager define unify2 ( t , u , s ) as newline 2383 2384 if t t= u then s else newline 2385 2386 let t prime = s [[ t second idx ]] in newline 2387 2388 if t prime != true then unify ( t prime , u , s ) else newline 2389 2390 if occur ( t , u , s ) then exception else s [[ t second idx -> u ]] end define ]]". 2391 2392 Does the same as "[[ unify ( t , u , s ) ]]" but only when "[[ t ]]" is a number. 2393 2394 \end{statements} 2395 2396 2397 2398 \subsection{Hooks for the tactic state} 2399 2400 \begin{statements} 2401 2402 \item "[[ eager define hook-arg as "arg" end define ]]" 2403 2404 Argumentation hook. States returned from tactic or unitac evaluation contain the returned argumentation on this hook. 2405 2406 \item "[[ eager define hook-res as "con" end define ]]" 2407 2408 Result hook. States returned from tactic or unitac evaluation contain the expected conclusion on this hook. 2409 2410 \item "[[ eager define hook-idx as "idx" end define ]]" 2411 2412 Index hook. During unitac evaluation, the index hook contains an accumulating index used for generating fresh variables. 2413 2414 \item "[[ eager define hook-uni as "uni" end define ]]" 2415 2416 Unification hook. During unitac evaluation, the result of unification is accumulated here. 2417 2418 \item "[[ eager define hook-pre as "pre" end define ]]" 2419 2420 Premise hook. Premises are stacked here during tactic evaluation. Premises may be explicitly assumed premises, the conclusion of the left hand side of a cut, or a theory assumed at the beginning of a proofs. Elements of the premise hook have form "[[ l :: p :: x ]]" where "[[ l ]]" is a label for referring to the premise, "[[ p ]]" is the premise itself, and "[[ x ]]" may be used by individual tactics. 2421 2422 \item "[[ eager define hook-cond as "cond" end define ]]" 2423 2424 Condition hook. Side conditions are stacked here during tactic evaluation. 2425 2426 \item "[[ eager define hook-parm as "parm" end define ]]" 2427 2428 Parameter hook. Tactic evaluation of "[[ x at y ]]" stacks "[[ y ]]" on the parameter hook. Tactic evaluation of "[[ All x : y ]]" unstacks. Useful for parameterized tactics. 2429 2430 \end{statements} 2431 2432 2433 2434 \subsection{Tactic evaluation} 2435 2436 \begin{statements} 2437 2438 \item "[[ eager define taceval ( t , s , c ) as newline 2439 2440 let d = t tactic-rhs ( c ) in newline 2441 2442 if .not. d then ( eval ( d , true , c ) apply << t ,, s ,, c >> maptag ) untag else newline 2443 2444 let << r ,, a >> = lookup ( t , s [[ hook-pre ]] , true ) in newline 2445 2446 if .not. a then s [[ hook-res -> r ]] [[ hook-arg -> a ]] else newline 2447 2448 error ( t , newline 2449 diag ( "Unknown tactic operator in root of argumentation:" ) newline 2450 disp ( t ) 2451 end diagnose ) end define ]]". 2452 2453 Evaluate the `tactic' aspect of "[[ t ]]". 2454 2455 \item "[[ eager define tactic-push ( n , v , s ) as newline 2456 2457 s [[ n -> v :: s [[ n ]] ]] end define ]]" 2458 2459 Push the value "[[ v ]]" onto the stack named "[[ n ]]" in the tactic state "[[ s ]]". 2460 2461 \item "[[ eager define tactic-pop ( n , s ) as newline 2462 2463 s [[ n -> s [[ n ]] tail ]] end define ]]" 2464 2465 Pop a value from the stack named "[[ n ]]" in the tactic state "[[ s ]]" and return the new state (not the popped value). 2466 2467 \item "[[ eager define taceval1 ( t , p , c ) as newline 2468 2469 let d = t tactic-rhs ( c ) in newline 2470 2471 let t = back t quote t unquote infer p unquote end quote in newline 2472 2473 if d then taceval ( t , tacstate0 , c ) else newline 2474 2475 ( eval ( d , true , c ) apply << t ,, tacstate0 ,, c >> maptag ) untag end define ]]" 2476 2477 Evaluate the `tactic' aspect of "[[ t infer p ]]" using the tactic definition of "[[ t ]]". If "[[ t ]]" has no tactic definition then use taceval. 2478 2479 \end{statements} 2480 2481 2482 2483 \subsection{Proof macros} 2484 2485 \begin{statements} 2486 2487 \item "[[ macro define x lemma y : z end lemma as ensure math statement define y as x infer z end define,unitac define y as \ u . unitac-lemma ( u ) end define end math end define ]]". 2488 2489 A lemma declaration is the same as a statement definition plus a unitac definition which says how to sequent-prove a lemma plus what the lemma concludes. 2490 2491 \item "[[ macro define proof of x : y as ensure math define proof of x as \ p . \ c . taceval ( quote y end quote , tacstate0 , c ) end define end math end define ]]". 2492 2493 A proof is the same as a proof definition. 2494 2495 \item "[[ macro define x proof of y : z as ensure math define proof of y as \ p . \ c . taceval1 ( quote x end quote , quote z end quote , c ) end define end math end define ]]". 2496 2497 Assume "[[ x ]]", then prove "[[ y ]]" using the proof "[[ z ]]". If "[[ x ]]" has a tactic definition then that tactic is applied to the entire proof. 2498 2499 \end{statements} 2500 2501 2502 2503 \subsection{Proof line macros} 2504 2505 \begin{statements} 2506 2507 \item "[[ macro define line l : a >> x ; as a conclude x end define ]]" 2508 2509 \item "[[ macro define line l : a >> x qed as a conclude x end define ]]" 2510 2511 \item "[[ macro define line l : Arbitrary >> x ; n as All x : n end define ]]" 2512 2513 \item "[[ macro define line l : Local >> x = y ; n as let x := y in n end define ]]" 2514 2515 \end{statements} 2516 2517 2518 2519 \section{Tactic definitions of sequent operators} 2520 2521 \subsection{Init tactic} 2522 2523 \begin{statements} 2524 2525 \item "[[ tactic define x Init as \ u . tactic-Init ( u ) end define ]]". 2526 2527 \item "[[ eager define tactic-Init ( u ) as newline 2528 2529 let << t ,, s ,, c >> = u in newline 2530 2531 let << true ,, x >> = t in newline 2532 2533 s [[ hook-arg -> t ]] [[ hook-res -> x ]] end define ]]" 2534 2535 \end{statements} 2536 2537 2538 2539 \subsection{Ponens tactic} 2540 2541 \begin{statements} 2542 2543 \item "[[ tactic define x Ponens as \ u . tactic-Ponens ( u ) end define ]]". 2544 2545 \item "[[ eager define tactic-Ponens ( u ) as newline 2546 2547 let << t ,, s ,, c >> = u in newline 2548 2549 let << true ,, x >> = t in newline 2550 2551 let s = taceval ( x , s , c ) in newline 2552 2553 let a = back t quote s [[ hook-arg ]] unquote Ponens end quote in newline 2554 2555 let r = s [[ hook-res ]] in newline 2556 2557 if mismatch ( quote x infer y end quote , r , c ) then newline 2558 2559 error ( t , 2560 diag ( "Ponens tactic used on non-inference:" ) 2561 disp ( r ) 2562 end diagnose ) else newline 2563 2564 s [[ hook-arg -> a ]] [[ hook-res -> r second ]] end define ]]" 2565 2566 \end{statements} 2567 2568 2569 2570 \subsection{Probans tactic} 2571 2572 \begin{statements} 2573 2574 \item "[[ tactic define x Probans as \ u . tactic-Probans ( u ) end define ]]". 2575 2576 \item "[[ eager define tactic-Probans ( u ) as newline 2577 2578 let << t ,, s ,, c >> = u in newline 2579 2580 let << true ,, x >> = t in newline 2581 2582 let s = taceval ( x , s , c ) in newline 2583 2584 let a = back t quote s [[ hook-arg ]] unquote Probans end quote in newline 2585 2586 let r = s [[ hook-res ]] in newline 2587 2588 if mismatch ( quote x endorse y end quote , r , c ) then newline 2589 2590 error ( t , 2591 diag ( "Probans tactic used on non-endorsement:" ) 2592 disp ( r ) 2593 end diagnose ) else newline 2594 2595 s [[ hook-arg -> a ]] [[ hook-res -> r second ]] end define ]]" 2596 2597 \end{statements} 2598 2599 2600 2601 \subsection{Verify tactic} 2602 2603 \begin{statements} 2604 2605 \item "[[ tactic define x Verify as \ u . tactic-Verify ( u ) end define ]]". 2606 2607 \item "[[ eager define tactic-Verify ( u ) as newline 2608 2609 let << t ,, s ,, c >> = u in newline 2610 2611 let << true ,, x >> = t in newline 2612 2613 let s = taceval ( x , s , c ) in newline 2614 2615 let a = back t quote s [[ hook-arg ]] unquote Verify end quote in newline 2616 2617 let r = s [[ hook-res ]] in newline 2618 2619 if mismatch ( quote x endorse y end quote , r , c ) then newline 2620 2621 error ( t , 2622 diag ( "Verify tactic used on non-endorsement:" ) 2623 disp ( r ) 2624 end diagnose ) else newline 2625 2626 s [[ hook-arg -> a ]] [[ hook-res -> r second ]] end define ]]" 2627 2628 \end{statements} 2629 2630 2631 2632 \subsection{Curry tactic} 2633 2634 \begin{statements} 2635 2636 \item "[[ tactic define x Curry as \ u . tactic-Curry ( u ) end define ]]". 2637 2638 \item "[[ eager define tactic-Curry ( u ) as newline 2639 2640 let << t ,, s ,, c >> = u in newline 2641 2642 let << true ,, x >> = t in newline 2643 2644 let s = taceval ( x , s , c ) in newline 2645 2646 let a = back t quote s [[ hook-arg ]] unquote Curry end quote in newline 2647 2648 let r = s [[ hook-res ]] in newline 2649 2650 if mismatch ( quote ( x oplus y ) infer z end quote , r , c ) then newline 2651 2652 error ( t , 2653 diag ( "Curry tactic used on unfit argument:" ) 2654 disp ( r ) 2655 end diagnose ) else newline 2656 2657 let r = back r quote r first first unquote infer r first second unquote infer r second unquote end quote in newline 2658 2659 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 2660 2661 \end{statements} 2662 2663 2664 2665 \subsection{Uncurry tactic} 2666 2667 \begin{statements} 2668 2669 \item "[[ tactic define x Uncurry as \ u . tactic-Uncurry ( u ) end define ]]". 2670 2671 \item "[[ eager define tactic-Uncurry ( u ) as newline 2672 2673 let << t ,, s ,, c >> = u in newline 2674 2675 let << true ,, x >> = t in newline 2676 2677 let s = taceval ( x , s , c ) in newline 2678 2679 let a = back t quote s [[ hook-arg ]] unquote Uncurry end quote in newline 2680 2681 let r = s [[ hook-res ]] in newline 2682 2683 if mismatch ( quote x infer y infer z end quote , r , c ) then newline 2684 2685 error ( t , 2686 diag ( "Uncurry tactic used on unfit argument:" ) 2687 disp ( r ) 2688 end diagnose ) else newline 2689 2690 let r = back r quote ( r first unquote oplus r second first unquote ) infer r second second unquote end quote in newline 2691 2692 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 2693 2694 \end{statements} 2695 2696 2697 2698 \subsection{Deref tactic} 2699 2700 \begin{statements} 2701 2702 \item "[[ tactic define x Deref as \ u . tactic-Deref ( u ) end define ]]". 2703 2704 \item "[[ eager define tactic-Deref ( u ) as newline 2705 2706 let << t ,, s ,, c >> = u in newline 2707 2708 let << true ,, x >> = t in newline 2709 2710 let s = taceval ( x , s , c ) in newline 2711 2712 let a = back t quote s [[ hook-arg ]] unquote Deref end quote in newline 2713 2714 let r = s [[ hook-res ]] in newline 2715 2716 let r prime = r stmt-rhs ( c ) in newline 2717 2718 if r prime = true then newline 2719 2720 error ( t , 2721 diag ( "Deref tactic used on undefined statement:" ) 2722 disp ( r ) 2723 end diagnose ) else newline 2724 2725 s [[ hook-arg -> a ]] [[ hook-res -> r prime ]] end define ]]" 2726 2727 \end{statements} 2728 2729 2730 2731 \subsection{At tactic} 2732 2733 Accumulate instantiations on the ``parameters'' stack. To do multiple instantiations in parallel, "[[ tactic-at1 ( t , s , v , c ) ]]" accumulates instantiations on the "[[ v ]]" list and then "[[ tactic-at2 ( t , s , v , s prime , c ) ]]" accumulates instantiations on the "[[ s prime ]]" association list of substitutions to be performed in parallel. 2734 2735 \begin{statements} 2736 2737 \item "[[ tactic define x at y as \ u . tactic-at ( u ) end define ]]". 2738 2739 \item "[[ eager define tactic-at ( u ) as newline 2740 2741 let << t ,, s ,, c >> = u in tactic-at1 ( t , s , true , c ) end define 2742 ]]" 2743 2744 \item "[[ eager define tactic-at1 ( t , s , v , c ) as newline 2745 2746 if mismatch ( quote x at y end quote , t , c ) then newline 2747 2748 tactic-at2 ( t , taceval ( t , s , c ) , v , true , c ) else newline 2749 2750 let << true ,, x ,, y >> = t in newline 2751 2752 let s = tactic-push ( hook-parm , y , s ) in newline 2753 2754 tactic-at1 ( x , s , y :: v , c ) end define ]]" 2755 2756 \item "[[ eager define tactic-at2 ( t , s , v , s prime , c ) as newline 2757 2758 if v then s [[ hook-res -> metasubst ( s [[ hook-res ]] , s prime , c ) ]] else newline 2759 2760 let y :: v = v in newline 2761 2762 let a = back t quote s [[ hook-arg ]] unquote at y unquote end quote in newline 2763 2764 let r = s [[ hook-res ]] in newline 2765 2766 if mismatch ( quote All x : y end quote , r , c ) then newline 2767 2768 error ( t , 2769 diag ( "At tactic used on non-quantifier:" ) 2770 disp ( r ) 2771 end diagnose ) else newline 2772 2773 let s = s [[ hook-arg -> a ]] [[ hook-res -> r second ]] in newline 2774 2775 tactic-at2 ( t , s , v , ( r first :: y ) :: s prime , c ) end define ]]" 2776 2777 \end{statements} 2778 2779 2780 2781 \subsection{Infer tactic} 2782 2783 Accumulate premises on the ``premises'' stack. 2784 2785 \begin{statements} 2786 2787 \item "[[ tactic define x infer y as \ u . tactic-infer ( u ) end define ]]". 2788 2789 \item "[[ eager define tactic-infer ( u ) as newline 2790 2791 let << t ,, s ,, c >> = u in newline 2792 2793 let << true ,, x ,, y >> = t in newline 2794 2795 let s = tactic-push ( hook-pre , << true ,, x ,, back x quote x unquote Init end quote >> , s ) in newline 2796 2797 let s = taceval ( y , s , c ) in newline 2798 2799 let a = back t quote x unquote infer s [[ hook-arg ]] unquote end quote in newline 2800 2801 let r = back t quote x unquote infer s [[ hook-res ]] unquote end quote in newline 2802 2803 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 2804 2805 \end{statements} 2806 2807 2808 2809 \subsection{Endorse tactic} 2810 2811 Accumulate side conditions on the ``conditions'' stack. 2812 2813 \begin{statements} 2814 2815 \item "[[ tactic define x endorse y as \ u . tactic-endorse ( u ) end define ]]". 2816 2817 \item "[[ eager define tactic-endorse ( u ) as newline 2818 2819 let << t ,, s ,, c >> = u in newline 2820 2821 let << true ,, x ,, y >> = t in newline 2822 2823 let s = taceval ( y , tactic-push ( hook-cond , << true ,, x >> , s ) , c ) in newline 2824 2825 let a = back t quote x unquote endorse s [[ hook-arg ]] unquote end quote in newline 2826 2827 let r = back t quote x unquote endorse s [[ hook-res ]] unquote end quote in newline 2828 2829 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 2830 2831 \end{statements} 2832 2833 2834 2835 \subsection{Id est tactic} 2836 2837 \begin{statements} 2838 2839 \item "[[ tactic define x id est y as \ u . tactic-ie ( u ) end define ]]". 2840 2841 \item "[[ eager define tactic-ie ( u ) as newline 2842 2843 let << t ,, s ,, c >> = u in newline 2844 2845 let << true ,, x ,, y >> = t in newline 2846 2847 let s = taceval ( x , s , c ) in newline 2848 2849 let a = back t quote s [[ hook-arg ]] unquote id est y unquote end quote in newline 2850 2851 s [[ hook-arg -> a ]] [[ hook-res -> y ]] end define ]]" 2852 2853 \end{statements} 2854 2855 2856 2857 \subsection{All tactic} 2858 2859 Pop instantiations from the ``parameters'' stack. 2860 2861 \begin{statements} 2862 2863 \item "[[ tactic define All x : y as \ u . tactic-all ( u ) end define ]]". 2864 2865 \item "[[ eager define tactic-all ( u ) as newline 2866 2867 let << t ,, s ,, c >> = u in newline 2868 2869 let << true ,, x ,, y >> = t in newline 2870 2871 let s = taceval ( y , tactic-pop ( hook-parm , s ) , c ) in newline 2872 2873 let a = back t quote All x unquote : s [[ hook-arg ]] unquote end quote in newline 2874 2875 let r = back t quote All x unquote : s [[ hook-res ]] unquote end quote in newline 2876 2877 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 2878 2879 \end{statements} 2880 2881 2882 2883 \subsection{Cut tactic} 2884 2885 Accumulate conclusions of left hand sides of cuts on the ``premises'' stack. 2886 2887 \begin{statements} 2888 2889 \item "[[ tactic define x ;; y as \ u . tactic-cut ( u ) end define ]]". 2890 2891 \item "[[ eager define tactic-cut ( u ) as newline 2892 2893 let << t ,, s ,, c >> = u in newline 2894 2895 let << true ,, x ,, y >> = t in newline 2896 2897 let s prime = taceval ( x , s , c ) in newline 2898 2899 let a = s prime [[ hook-arg ]] in newline 2900 2901 let r = s prime [[ hook-res ]] in newline 2902 2903 let s = tactic-push ( hook-pre , << true ,, r ,, back r quote r unquote Init end quote >> , s ) in newline 2904 2905 let s = taceval ( y , s , c ) in newline 2906 2907 let a = back t quote a unquote ;; s [[ hook-arg ]] unquote end quote in newline 2908 2909 s [[ hook-arg -> a ]] end define ]]" 2910 2911 \end{statements} 2912 2913 2914 2915 \section{Unification tactic} 2916 2917 \subsection{Main definitions} 2918 2919 \begin{statements} 2920 2921 \item "[[ tactic define a conclude a prime as \ x . unitac ( x ) end define ]]". 2922 2923 Proof tactic which tries to modify the argumentation "[[ a ]]" so that it proves the term "[[ a prime ]]". The tactic adds missing "[[ x at y ]]", "[[ x Ponens ]]", and "[[ x Verify ]]" operations and determines the "[[ y ]]" in "[[ x at y ]]" using unification. 2924 2925 2926 2927 \item "[[ eager define unitac ( x ) as newline 2928 2929 let << t ,, s ,, c >> = x in newline 2930 2931 let e :: v = unitac1 ( t , s , c ) catch in newline 2932 2933 if .not. e then v else newline 2934 2935 if .not. v then error ( t , LocateProofLine ( t , c ) v ) else newline 2936 2937 error ( t , newline 2938 LocateProofLine ( t , c ) newline 2939 diag ( "During unification: Uncaught exception" ) newline 2940 end diagnose ) 2941 2942 end define ]]" 2943 2944 Hand the term "[[ t ]]" of form "[[ a conclude a prime ]]", the tactic state "[[ s ]]", and the codex "[[ c ]]" to unitac1. Locate any errors found by unitac1. 2945 2946 2947 2948 \item "[[ eager define unitac1 ( t , s , c ) as newline 2949 2950 let s = s [[ hook-idx -> 1 ]] [[ hook-uni -> true ]] in newline 2951 2952 let s = unieval ( t , s , c ) in newline 2953 2954 let t = inst ( s [[ hook-arg ]] , t , s [[ hook-uni ]] ) in newline 2955 2956 let e :: v = taceval ( t , s , c ) catch in 2957 2958 if .not. e then v else newline 2959 2960 if .not. v then v raise else newline 2961 2962 error ( t , newline 2963 diag ( "Post unification tactic evalutation: Uncaught exception" ) newline 2964 end diagnose ) 2965 2966 end define ]]" 2967 2968 Call unieval to unitac expand the proof term "[[ t ]]" to a unification and an uninstantiated argumentation. The unification and argumentation are added to the state "[[ s ]]". "[[ c ]]" is the cache. Then instantiate the argumentation and do usual tactic expansion. 2969 2970 \end{statements} 2971 2972 2973 2974 \subsection{Adaption} 2975 2976 \begin{statements} 2977 2978 \item "[[ eager define unitac-adapt ( t , s , c ) as newline 2979 2980 if t = "var" then s else newline 2981 2982 let a = s [[ hook-arg ]] in newline 2983 2984 let r = s [[ hook-res ]] in newline 2985 2986 let d = r metadef ( c ) in newline 2987 2988 if d = "var" then s else newline 2989 2990 if d = t then s else newline 2991 2992 if d = "infer" then newline 2993 2994 unitac-adapt ( t , s [[ hook-arg -> back a quote a unquote Ponens end quote ]] [[ hook-res -> r second ]] , c ) else newline 2995 2996 if d = "endorse" then newline 2997 2998 unitac-adapt ( t , s [[ hook-arg -> back a quote a unquote Verify end quote ]] [[ hook-res -> r second ]] , c ) else newline 2999 3000 if d = "all" then newline 3001 3002 let i = s [[ hook-idx ]] in newline 3003 3004 let s = s [[ hook-idx -> i + 1 ]] in newline 3005 3006 let v = univar ( a , r first , i ) in newline 3007 3008 let r prime = metasubst ( r second , << r first :: v >> , c ) in newline 3009 3010 unitac-adapt ( t , s [[ hook-arg -> back a quote a unquote at v unquote end quote ]] [[ hook-res -> r prime ]] , c ) else newline 3011 3012 if t then s else newline 3013 3014 error ( a , newline 3015 diag ( "Cannot convert" ) 3016 disp ( r ) newline 3017 diag ( "to type ``" ) 3018 diag ( t ) 3019 diag ( "''" ) 3020 end diagnose ) end define ]]". 3021 3022 Add Ponens, Verify, and At operations to the argumentation inside "[[ s ]]" until the root of the conclusion is of type "[[ t ]]". As examples, "[[ t ]]" could be ``infer'', ``endorse'', ``all'', ``var'' or "[[ true ]]". In the latter case, a maximum of Ponens, Verify, and At operations are added. When "[[ t ]]" is ``var'', a minimum of operators are added (meaning that "[[ s ]]" is returned unchanged). 3023 3024 \end{statements} 3025 3026 3027 3028 \subsection{Unitac evaluation} 3029 3030 \begin{statements} 3031 3032 \item "[[ eager define unieval ( t , s , c ) as newline 3033 3034 let d = t unitac-rhs ( c ) in newline 3035 3036 if d then newline 3037 3038 let << r ,, a >> = lookup ( t , s [[ hook-pre ]] , true ) in newline 3039 3040 if .not. a then s [[ hook-arg -> a ]] [[ hook-res -> r ]] else newline 3041 3042 error ( t , newline 3043 diag ( "Unknown unitac operator in root of argumentation:" ) newline 3044 disp ( t ) 3045 end diagnose ) else newline 3046 3047 let e :: s = ( eval ( d , true , c ) apply << t ,, s ,, c >> maptag ) untag catch in newline 3048 3049 if .not. e then s else newline 3050 3051 if .not. s then s raise else newline 3052 3053 error ( t , newline 3054 diag ( "Exception raised by the unitac aspect of:" ) 3055 disp ( t ) 3056 end diagnose ) 3057 3058 end define ]]" 3059 3060 Unitac expand the argumentation "[[ t ]]" to a unification, an uninstantiated argumentation, and an expected conclusion. The unification, argumentation, and conclusion are added to the state "[[ s ]]" as "[[ s [[ hook-uni ]] ]]", "[[ s [[ hook-arg ]] ]]", and "[[ s [[ hook-res ]] ]]", respectively. "[[ c ]]" is the cache. 3061 3062 During unitac expansion, fresh variables are generated using "[[ univar ( t prime , v , s [[ hook-idx ]] ) ]]" where "[[ s [[ hook-idx ]] ]]" is supposed to be a unique index. "[[ v ]]" is the varible which receives the unique index and debugging information is taken from "[[ t prime ]]". The index is supposed to guarantee uniqueness in itself. The purpose of "[[ v ]]" is to make error messages more readable. 3063 3064 \end{statements} 3065 3066 3067 3068 \section{Unitac definitions} 3069 3070 \subsection{Init} 3071 3072 \begin{statements} 3073 3074 \item "[[ unitac define x Init as \ u . unitac-Init ( u ) end define ]]" 3075 3076 \item "[[ eager define unitac-Init ( u ) as newline 3077 3078 let << t ,, s ,, c >> = u in newline 3079 3080 s [[ hook-res -> t first ]] [[ hook-arg -> t ]] end define ]]" 3081 3082 If "[[ t ]]" has form "[[ r Init ]]" then the conclusion is "[[ r ]]" and the argumentation is "[[ r Init ]]". 3083 3084 \end{statements} 3085 3086 3087 3088 \subsection{Ponens} 3089 3090 \begin{statements} 3091 3092 \item "[[ unitac define x Ponens as \ u . unitac-Ponens ( u ) end define ]]" 3093 3094 \item "[[ unitac define x ponens y as \ u . unitac-ponens ( u ) end define ]]" 3095 3096 \item "[[ eager define unitac-Ponens ( u ) as newline 3097 3098 let << t ,, s ,, c >> = u in newline 3099 3100 let s = unieval ( t first , s , c ) in newline 3101 3102 let s = unitac-adapt ( "infer" , s , c ) in newline 3103 3104 let a = s [[ hook-arg ]] in newline 3105 3106 let r = s [[ hook-res ]] in newline 3107 3108 s [[ hook-arg -> back t quote a unquote Ponens end quote ]] [[ hook-res -> r second ]] end define ]]" 3109 3110 If the argumentation has form "[[ a Ponens ]]" then convert the argumentation "[[ a ]]" into something whose conclusion "[[ r ]]" is expected to be of form "[[ x infer y ]]". 3111 3112 \item "[[ eager define unitac-ponens ( u ) as newline 3113 3114 let << t ,, s ,, c >> = u in newline 3115 3116 let s = unieval ( t first , s , c ) in newline 3117 3118 let s = unitac-adapt ( "infer" , s , c ) in newline 3119 3120 let a = s [[ hook-arg ]] in newline 3121 3122 let r = s [[ hook-res ]] in newline 3123 3124 let s = unieval ( t second , s , c ) in newline 3125 3126 let s = unitac-adapt ( r first metadef ( c ) , s , c ) in newline 3127 3128 let a prime = s [[ hook-arg ]] in newline 3129 3130 let r prime = s [[ hook-res ]] in newline 3131 3132 let u = s [[ hook-uni ]] in newline 3133 3134 let u = unify ( r first , r prime , u ) in newline 3135 3136 let s = s [[ hook-uni -> u ]] in newline 3137 3138 s [[ hook-arg -> back t quote a prime unquote ;; a unquote Ponens end quote ]] [[ hook-res -> r second ]] 3139 3140 end define ]]" 3141 3142 If the argumentation has form "[[ a ponens a prime ]]" then convert "[[ a ]]" into something whose result is expected to be of form "[[ x infer y ]]". Convert "[[ a prime ]]" into something whose result is expected to be of form "[[ r prime ]]". Unify "[[ x ]]" with "[[ r prime ]]" and return argumentation "[[ ( a prime ;; a Ponens ) ]]" and conclusion "[[ y ]]". 3143 3144 \end{statements} 3145 3146 3147 3148 \subsection{Probans} 3149 3150 \begin{statements} 3151 3152 \item "[[ unitac define x Probans as \ u . unitac-Probans ( u ) end define ]]" 3153 3154 \item "[[ unitac define x probans y as \ u . unitac-probans ( u ) end define ]]" 3155 3156 \item "[[ eager define unitac-Probans ( u ) as newline 3157 3158 let << t ,, s ,, c >> = u in newline 3159 3160 let s = unieval ( t first , s , c ) in newline 3161 3162 let s = unitac-adapt ( "endorse" , s , c ) in newline 3163 3164 let a = s [[ hook-arg ]] in newline 3165 3166 let r = s [[ hook-res ]] in newline 3167 3168 s [[ hook-arg -> back t quote a unquote Probans end quote ]] [[ hook-res -> r second ]] end define ]]" 3169 3170 If the argumentation has form "[[ a probans p ]]" then convert the argumentation "[[ a ]]" into something whose conclusion "[[ r ]]" is expected to be of form "[[ x endorse y ]]". 3171 3172 \item "[[ eager define unitac-probans ( u ) as newline 3173 3174 let << t ,, s ,, c >> = u in newline 3175 3176 let s = unieval ( t first , s , c ) in newline 3177 3178 let s = unitac-adapt ( "endorse" , s , c ) in newline 3179 3180 let a = s [[ hook-arg ]] in newline 3181 3182 let r = s [[ hook-res ]] in newline 3183 3184 let u = s [[ hook-uni ]] in newline 3185 3186 let << p >> = lookup ( t second , s [[ hook-cond ]] , << t second >> ) in newline 3187 3188 let u = unify ( r first , p , u ) in newline 3189 3190 let s = s [[ hook-uni -> u ]] in newline 3191 3192 s [[ hook-arg -> back t quote a unquote Probans end quote ]] [[ hook-res -> r second ]] 3193 3194 end define ]]" 3195 3196 If the argumentation has form "[[ a probans s ]]" then convert "[[ a ]]" into something whose result is expected to be of form "[[ x endorse y ]]". Unify "[[ x ]]" with "[[ s ]]" and return argumentation "[[ a Probans ]]" and conclusion "[[ y ]]". 3197 3198 \end{statements} 3199 3200 3201 3202 \subsection{Verify} 3203 3204 \begin{statements} 3205 3206 \item "[[ unitac define x Verify as \ u . unitac-Verify ( u ) end define ]]" 3207 3208 \item "[[ unitac define x verify y as \ u . unitac-verify ( u ) end define ]]" 3209 3210 \item "[[ eager define unitac-Verify ( u ) as newline 3211 3212 let << t ,, s ,, c >> = u in newline 3213 3214 let s = unieval ( t first , s , c ) in newline 3215 3216 let s = unitac-adapt ( "endorse" , s , c ) in newline 3217 3218 let a = s [[ hook-arg ]] in newline 3219 3220 let r = s [[ hook-res ]] in newline 3221 3222 s [[ hook-arg -> back t quote a unquote Verify end quote ]] [[ hook-res -> r second ]] 3223 3224 end define ]]" 3225 3226 If the argumentation has form "[[ a Verify ]]" then convert the argumentation "[[ a ]]" into something whose conclusion "[[ r ]]" is expected to be of form "[[ x endorse y ]]". 3227 3228 \item "[[ eager define unitac-verify ( u ) as newline 3229 3230 let << t ,, s ,, c >> = u in newline 3231 3232 let s = unieval ( t first , s , c ) in newline 3233 3234 let s = unitac-adapt ( "endorse" , s , c ) in newline 3235 3236 let a = s [[ hook-arg ]] in newline 3237 3238 let r = s [[ hook-res ]] in newline 3239 3240 let u = s [[ hook-uni ]] in newline 3241 3242 let u = unify ( r first , t second , u ) in newline 3243 3244 let s = s [[ hook-uni -> u ]] in newline 3245 3246 s [[ hook-arg -> back t quote a unquote Verify end quote ]] [[ hook-res -> r second ]] 3247 3248 end define ]]" 3249 3250 If the argumentation has form "[[ a verify s ]]" then convert "[[ a ]]" into something whose result is expected to be of form "[[ x endorse y ]]". Unify "[[ x ]]" with "[[ s ]]" and return argumentation "[[ a Verify ]]" and conclusion "[[ y ]]". 3251 3252 \end{statements} 3253 3254 3255 3256 \subsection{Curry and decurry} 3257 3258 \begin{statements} 3259 3260 \item "[[ unitac define x Curry as \ u . unitac-Curry ( u ) end define ]]" 3261 3262 \item "[[ unitac define x Uncurry as \ u . unitac-Uncurry ( u ) end define ]]" 3263 3264 \item "[[ eager define unitac-Curry ( u ) as newline 3265 3266 let << t ,, s ,, c >> = u in newline 3267 3268 let s = unieval ( t first , s , c ) in newline 3269 3270 let s = unitac-adapt ( "infer" , s , c ) in newline 3271 3272 let a = s [[ hook-arg ]] in newline 3273 3274 let r = s [[ hook-res ]] in newline 3275 3276 if .not. r first r= quote x oplus y end quote then newline 3277 3278 error ( r , 3279 diag ( "Unsuited for currying:" ) 3280 disp ( r ) 3281 end diagnose ) else newline 3282 3283 let r = back r quote r first first unquote infer r first second unquote infer r second unquote end quote in newline 3284 3285 s [[ hook-arg -> back t quote a unquote Curry end quote ]] [[ hook-res -> r ]] 3286 3287 end define ]]" 3288 3289 If the argumentation has form "[[ a Curry ]]" then convert the argumentation "[[ a ]]" into something with conclusion "[[ x oplus y infer z ]]" and return conclusion "[[ x infer y infer z ]]". 3290 3291 \item "[[ eager define unitac-Uncurry ( u ) as newline 3292 3293 let << t ,, s ,, c >> = u in newline 3294 3295 let s = unieval ( t first , s , c ) in newline 3296 3297 let s = unitac-adapt ( "infer" , s , c ) in newline 3298 3299 let a = s [[ hook-arg ]] in newline 3300 3301 let r = s [[ hook-res ]] in newline 3302 3303 if .not. r second r= quote x infer y end quote then newline 3304 3305 error ( r , 3306 diag ( "Unsuited for uncurrying:" ) 3307 disp ( r ) 3308 end diagnose ) else newline 3309 3310 let r = back r quote ( r first unquote oplus r second first unquote ) infer r second second unquote end quote in newline 3311 3312 s [[ hook-arg -> back t quote a unquote Uncurry end quote ]] [[ hook-res -> r ]] 3313 3314 end define ]]" 3315 3316 If the argumentation has form "[[ a Uncurry ]]" then convert the argumentation "[[ a ]]" into something with conclusion "[[ x infer y infer z ]]" and return conclusion "[[ ( x oplus y ) infer z ]]". 3317 3318 \end{statements} 3319 3320 3321 3322 \subsection{At} 3323 3324 \begin{statements} 3325 3326 \item "[[ unitac define x At as \ u . unitac-At ( u ) end define ]]" 3327 3328 \item "[[ unitac define x at y as \ u . unitac-at ( u ) end define ]]" 3329 3330 \item "[[ eager define unitac-At ( u ) as newline 3331 3332 let << t ,, s ,, c >> = u in newline 3333 3334 let s = unieval ( t first , s , c ) in newline 3335 3336 let s = unitac-adapt ( "all" , s , c ) in newline 3337 3338 let a = s [[ hook-arg ]] in newline 3339 3340 let r = s [[ hook-res ]] in newline 3341 3342 let i = s [[ hook-idx ]] in newline 3343 3344 let s = s [[ hook-idx -> i + 1 ]] in newline 3345 3346 let v = univar ( a , r first , i ) in newline 3347 3348 let a = back t quote a unquote at v unquote end quote in newline 3349 3350 let r = metasubst ( r second , << r first :: v >> , c ) in newline 3351 3352 s [[ hook-arg -> a ]] [[ hook-res -> r ]] 3353 3354 end define ]]" 3355 3356 If the argumentation has form "[[ a At ]]" then convert "[[ a ]]" into something whose conclusion is expected to be of form "[[ All x : y ]]". Then replace "[[ x ]]" by a fresh variable "[[ v ]]" in "[[ y ]]" and return argumentation "[[ a at v ]]" and conclusion "[[ y ]]". 3357 3358 \item "[[ eager define unitac-at ( u ) as newline 3359 3360 let << t ,, s ,, c >> = u in newline 3361 3362 let s = unieval ( t first , s , c ) in newline 3363 3364 let s = unitac-adapt ( "all" , s , c ) in newline 3365 3366 let a = s [[ hook-arg ]] in newline 3367 3368 let r = s [[ hook-res ]] in newline 3369 3370 let i = s [[ hook-idx ]] in newline 3371 3372 let s = s [[ hook-idx -> i + 1 ]] in newline 3373 3374 let v = univar ( a , r first , i ) in newline 3375 3376 let a = back t quote a unquote at v unquote end quote in newline 3377 3378 let r = metasubst ( r second , << r first :: v >> , c ) in newline 3379 3380 let u = s [[ hook-uni ]] in newline 3381 3382 let u = unify ( t second , v , u ) in newline 3383 3384 let s = s [[ hook-uni -> u ]] in newline 3385 3386 s [[ hook-arg -> a ]] [[ hook-res -> r ]] 3387 3388 end define ]]" 3389 3390 If the argumentation has form "[[ a at a prime ]]" then convert "[[ a ]]" into something whose conclusion is expected to be of form "[[ All x : y ]]". Then replace "[[ x ]]" by a fresh variable "[[ v ]]" in "[[ y ]]", unify "[[ v ]]" with "[[ a prime ]]", and return argumentation "[[ a at v ]]" and conclusion "[[ y ]]". 3391 3392 \end{statements} 3393 3394 3395 3396 \subsection{Reference and dereference} 3397 3398 \begin{statements} 3399 3400 \item "[[ unitac define x Deref as \ u . unitac-Deref ( u ) end define ]]" 3401 3402 \item "[[ eager define unitac-Deref ( u ) as newline 3403 3404 let << t ,, s ,, c >> = u in newline 3405 3406 let s = unieval ( t first , s , c ) in newline 3407 3408 let s = unitac-adapt ( true , s , c ) in newline 3409 3410 let r = s [[ hook-res ]] in newline 3411 3412 let l = r stmt-rhs ( c ) in newline 3413 3414 if l then s else newline 3415 3416 let a = s [[ hook-arg ]] in newline 3417 3418 let a = back t quote a unquote Deref end quote in newline 3419 3420 s [[ hook-arg -> a ]] [[ hook-res -> l ]] end define ]]" 3421 3422 \item Let "[[ r ]]" be the conclusion of "[[ t first ]]". "[[ r ]]" is supposed to be a lemma. Let "[[ l ]]" be the contents of that lemma. Use "[[ l ]]" as conclusion of "[[ t first Deref ]]". 3423 3424 \item "[[ unitac define x id est y as \ u . unitac-idest ( u ) end define ]]" 3425 3426 \item "[[ eager define unitac-idest ( u ) as newline 3427 3428 let << t ,, s ,, c >> = u in newline 3429 3430 let s = unieval ( t first , s , c ) in newline 3431 3432 let l = t second stmt-rhs ( c ) in newline 3433 3434 let s = unitac-adapt ( l metadef ( c ) , s , c ) in newline 3435 3436 let r = s [[ hook-res ]] in newline 3437 3438 let u = s [[ hook-uni ]] in newline 3439 3440 let u = unify ( r , l , u ) in newline 3441 3442 let s = s [[ hook-uni -> u ]] in newline 3443 3444 let a = s [[ hook-arg ]] in newline 3445 3446 let a = back t quote a unquote id est t second unquote end quote in newline 3447 3448 s [[ hook-arg -> a ]] [[ hook-res -> t second ]] end define ]]" 3449 3450 \item Let "[[ l ]]" be the contents of the lemma named "[[ t second ]]". Unify the conclusion "[[ r ]]" of "[[ t first ]]" with "[[ l ]]" and take "[[ t second ]]" to be the conclusion of "[[ t first id est t second ]]". 3451 3452 \end{statements} 3453 3454 3455 3456 \subsection{Infer} 3457 3458 \begin{statements} 3459 3460 \item "[[ unitac define x Infer as \ u . unitac-Infer ( u ) end define ]]" 3461 3462 \item "[[ eager define unitac-Infer ( u ) as newline 3463 3464 let << t ,, s ,, c >> = u in newline 3465 3466 let s = unieval ( t first , s , c ) in newline 3467 3468 let i = s [[ hook-idx ]] in newline 3469 3470 let s = s [[ hook-idx -> i + 1 ]] in newline 3471 3472 let v = univar ( t , quote cla end quote , i ) in newline 3473 3474 let r = s [[ hook-res ]] in newline 3475 3476 let a = s [[ hook-arg ]] in newline 3477 3478 let r = back t quote v unquote infer r unquote end quote in newline 3479 3480 let a = back t quote v unquote infer a unquote end quote in newline 3481 3482 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 3483 3484 \item "[[ unitac define x infer y as \ u . unitac-infer ( u ) end define ]]" 3485 3486 \item "[[ eager define unitac-infer ( u ) as newline 3487 3488 let << t ,, s ,, c >> = u in newline 3489 3490 let s = unieval ( t second , s , c ) in newline 3491 3492 let r = s [[ hook-res ]] in newline 3493 3494 let a = s [[ hook-arg ]] in newline 3495 3496 let r = back t quote t first unquote infer r unquote end quote in newline 3497 3498 let a = back t quote t first unquote infer a unquote end quote in newline 3499 3500 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 3501 3502 \end{statements} 3503 3504 3505 3506 \subsection{Endorse} 3507 3508 \begin{statements} 3509 3510 \item "[[ unitac define x Endorse as \ u . unitac-Endorse ( u ) end define ]]" 3511 3512 \item "[[ eager define unitac-Endorse ( u ) as newline 3513 3514 let << t ,, s ,, c >> = u in newline 3515 3516 let s = unieval ( t first , s , c ) in newline 3517 3518 let i = s [[ hook-idx ]] in newline 3519 3520 let s = s [[ hook-idx -> i + 1 ]] in newline 3521 3522 let v = univar ( t , quote cla end quote , i ) in newline 3523 3524 let r = s [[ hook-res ]] in newline 3525 3526 let a = s [[ hook-arg ]] in newline 3527 3528 let r = back t quote v unquote endorse r unquote end quote in newline 3529 3530 let a = back t quote v unquote endorse a unquote end quote in newline 3531 3532 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 3533 3534 \item "[[ unitac define x endorse y as \ u . unitac-endorse ( u ) end define ]]" 3535 3536 \item "[[ eager define unitac-endorse ( u ) as newline 3537 3538 let << t ,, s ,, c >> = u in newline 3539 3540 let s = unieval ( t second , s , c ) in newline 3541 3542 let r = s [[ hook-res ]] in newline 3543 3544 let a = s [[ hook-arg ]] in newline 3545 3546 let r = back t quote t first unquote endorse r unquote end quote in newline 3547 3548 let a = back t quote t first unquote endorse a unquote end quote in newline 3549 3550 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 3551 3552 \end{statements} 3553 3554 3555 3556 \subsection{All} 3557 3558 \begin{statements} 3559 3560 \item "[[ unitac define x All as \ u . unitac-All ( u ) end define ]]" 3561 3562 \item "[[ eager define unitac-All ( u ) as newline 3563 3564 let << t ,, s ,, c >> = u in newline 3565 3566 let s = unieval ( t first , s , c ) in newline 3567 3568 let i = s [[ hook-idx ]] in newline 3569 3570 let s = s [[ hook-idx -> i + 1 ]] in newline 3571 3572 let v = univar ( t , quote cla end quote , i ) in newline 3573 3574 let r = s [[ hook-res ]] in newline 3575 3576 let a = s [[ hook-arg ]] in newline 3577 3578 let r = back t quote All v unquote : r unquote end quote in newline 3579 3580 let a = back t quote All v unquote : a unquote end quote in newline 3581 3582 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 3583 3584 \item "[[ unitac define All x : y as \ u . unitac-all ( u ) end define ]]" 3585 3586 \item "[[ eager define unitac-all ( u ) as newline 3587 3588 let << t ,, s ,, c >> = u in newline 3589 3590 let s = unieval ( t second , s , c ) in newline 3591 3592 let r = s [[ hook-res ]] in newline 3593 3594 let a = s [[ hook-arg ]] in newline 3595 3596 let r = back t quote All t first unquote : r unquote end quote in newline 3597 3598 let a = back t quote All t first unquote : a unquote end quote in newline 3599 3600 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 3601 3602 \end{statements} 3603 3604 3605 3606 \subsection{Cut} 3607 3608 \begin{statements} 3609 3610 \item "[[ unitac define x ;; y as \ u . unitac-cut ( u ) end define ]]" 3611 3612 \item "[[ eager define unitac-cut ( u ) as newline 3613 3614 let << t ,, s ,, c >> = u in newline 3615 3616 let s = unieval ( t first , s , c ) in newline 3617 3618 let a prime = s [[ hook-arg ]] in newline 3619 3620 let s = unieval ( t second , s , c ) in newline 3621 3622 let r = s [[ hook-res ]] in newline 3623 3624 let a = s [[ hook-arg ]] in newline 3625 3626 let a = back t quote a prime unquote ;; a unquote end quote in newline 3627 3628 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 3629 3630 \end{statements} 3631 3632 3633 3634 \subsection{Unary conclude} 3635 3636 The "[[ x Conclude ]]" operator adds Ponens, Verify, and At operations to the argumentation inside "[[ x ]]" until all occurrences of "[[ u infer v ]]", "[[ u endorse v ]]", and "[[ All u : v ]]" have been removed. One may think of "[[ x Conclude ]]" as a unary version of "[[ x conclude y ]]" in which "[[ y ]]" is missing but for which it is known that "[[ y ]]" is an object term. 3637 3638 \begin{statements} 3639 3640 \item "[[ unitac define x Conclude as \ u . unitac-Conclude ( u ) end define ]]" 3641 3642 \item "[[ eager define unitac-Conclude ( u ) as newline 3643 3644 let << t ,, s ,, c >> = u in newline 3645 3646 let s = unieval ( t first , s , c ) in newline 3647 3648 unitac-adapt ( true , s , c ) end define ]]" 3649 3650 If "[[ t ]]" has form "[[ a Conclude ]]" then find the conclusion "[[ r ]]" of "[[ a ]]", add as many "[[ x at y ]]", "[[ x Ponens ]]", and "[[ x Verify ]]" operations as possible, and return "[[ a :: r :: u ]]". 3651 3652 \end{statements} 3653 3654 3655 3656 \section{Lemmas, rules, and proof lines} 3657 3658 Lemmas, rules, and proof lines do not always say what they seem to say. As an example, a lemma stating that "[[ x = x ]]" in Mendelsons "[[ System S ]]" does not say "[[ x = x ]]". Rather, it says "[[ System S infer x = x ]]". As another example, if one allows the use of deduction in FOL-based proofs then a proof line proving e.g. "[[ x + 1 = 0 + ( x + 1 ) ]]" under the hypothesis "[[ x = 0 + x ]]" really proves "[[ x = 0 + x p.imply x + 1 = 0 + ( x + 1 ) ]]". Or, rather, it proves "[[ System S infer x = 0 + x p.imply x + 1 = 0 + ( x + 1 ) ]]" if the proof is stated in "[[ System S ]]". 3659 3660 No single way of handling lemmas, rules, and proofs will satisfy all theories. As an example, deduction in FOL is different from deduction in map theory, and for that reason those two theories need different ways of treating proof lines in hypothetical proofs. 3661 3662 For that reason, the way lemmas, rules, and proofs are treated is embedded in the tactic state. 3663 3664 3665 3666 \subsection{The initial tactic state} 3667 3668 The initial tactic state "[[ tacstate0 ]]" contains "[[ unitac0 ]]". "[[ unitac0 ]]" in turn defines how to treat lemmas, rules, and proof lines during unitac evaluation. The definition of "[[ tacstate0 ]]" reads: 3669 3670 \begin{statements} 3671 3672 \item "[[ eager define hook-unitac as "unitac" end define ]]" 3673 3674 \item "[[ eager define tacstate0 as true [[ hook-unitac -> unitac0 ]] end define ]]" 3675 3676 \end{statements} 3677 3678 \noindent The "[[ unitac0 ]]" structure defines how to handle lemmas, rules, and proof lines during unitac evaluation. Handling of proof lines really means how to handle the conclude construct "[[ x conclude y ]]". 3679 3680 \begin{statements} 3681 3682 \item "[[ eager define hook-lemma as "lemma" end define ]]" 3683 3684 \item "[[ eager define hook-rule as "rule" end define ]]" 3685 3686 \item "[[ eager define hook-conclude as "conclude" end define ]]" 3687 3688 \item "[[ eager define unitac0 as 3689 3690 true 3691 3692 [[ hook-lemma -> quote \ u . unitac-lemma-std ( u ) end quote ]] 3693 3694 [[ hook-rule -> quote \ u . unitac-rule-std ( u ) end quote ]] 3695 3696 [[ hook-conclude -> quote \ u . unitac-conclude-std ( u ) end quote ]] end define ]]". 3697 3698 \end{statements} 3699 3700 3701 3702 \subsection{Conclude} 3703 3704 \begin{statements} 3705 3706 \item "[[ unitac define x conclude y as \ u . unitac-conclude ( u ) end define ]]" 3707 3708 \item "[[ eager define unitac-conclude ( u ) as newline 3709 3710 let << t ,, s ,, c >> = u in newline 3711 3712 let d = s [[ hook-unitac ]] [[ hook-conclude ]] in newline 3713 3714 ( eval ( d , true , c ) apply << t ,, s ,, c >> maptag ) untag end define ]]" 3715 3716 \item "[[ eager define unitac-conclude-std ( u ) as newline 3717 3718 let << t ,, s ,, c >> = u in newline 3719 3720 let s = unieval ( t first , s , c ) in newline 3721 3722 let s = unitac-adapt ( t second metadef ( c ) , s , c ) in newline 3723 3724 let u = unify ( s [[ hook-res ]] , t second , s [[ hook-uni ]] ) in newline 3725 3726 s [[ hook-uni -> u ]] [[ hook-res -> t second ]] 3727 3728 end define ]]" 3729 3730 If "[[ t ]]" has form "[[ t first conclude t second ]]" then convert "[[ t first ]]" into something whose conclusion fits "[[ t second ]]". Unify the conclusion with "[[ t second ]]" and return the resulting state "[[ s ]]". 3731 3732 \end{statements} 3733 3734 3735 3736 \subsection{Rules} 3737 3738 We define two rule tactics: "[[ x Rule ]]" for explicit use and "[[ unitac-rule ( x ) ]]" which is implicitly attached to axioms and inference rules. The ``implicit attachment'' is done by the axiom and rule macros. As an example of use, "[[ p.A1 Rule ]]" explicitly proves "[[ p.A1 ]]" whereas "[[ p.A1 ]]" implicitly proves "[[ All #a ,, #b : A p.imply B p.imply A ]]". Note that the former proves the name and the latter proves the contents of "[[ p.A1 ]]". 3739 3740 \begin{statements} 3741 3742 \item "[[ unitac define r Rule as \ u . unitac-Rule ( u ) end define ]]" 3743 3744 \item "[[ eager define unitac-Rule ( x ) as newline 3745 3746 let << t ,, s ,, c >> = x in newline 3747 3748 let r = t first in newline 3749 3750 let a = unitac-theo ( r , s , c ) in newline 3751 3752 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 3753 3754 3755 3756 \item "[[ eager define unitac-rule ( u ) as newline 3757 3758 let << t ,, s ,, c >> = u in newline 3759 3760 let d = s [[ hook-unitac ]] [[ hook-rule ]] in newline 3761 3762 ( eval ( d , true , c ) apply << t ,, s ,, c >> maptag ) untag end define ]]" 3763 3764 \item "[[ eager define unitac-rule-std ( x ) as newline 3765 3766 let << t ,, s ,, c >> = x in newline 3767 3768 let r = t stmt-rhs ( c ) in newline 3769 3770 let a = unitac-theo ( t , s , c ) in newline 3771 3772 let a = back r quote a unquote Deref end quote in newline 3773 3774 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 3775 3776 \item "[[ eager define unitac-theo ( t , s , c ) as newline 3777 3778 let p = reverse ( s [[ hook-pre ]] ) in newline 3779 3780 unitac-rule0 ( t , p , c ) end define ]]" 3781 3782 Construct a proof of the rule "[[ t ]]" assuming the premisses contained in the tactic state "[[ s ]]". Complain if no proof is found. 3783 3784 \item "[[ eager define unitac-rule0 ( r , P , c ) as newline 3785 3786 let p = unitac-rule1 ( r , P , c ) in newline 3787 3788 if .not. p then p else newline 3789 3790 if r metadef ( c ) = "plus" then unitac-rule-plus ( r , P , c ) else newline 3791 3792 let d = r stmt-rhs ( c ) in newline 3793 3794 if .not. d then unitac-rule-stmt ( d , r , P , c ) else newline 3795 3796 error ( r , newline 3797 diag ( "No locally assumed theory includes the following rule:" ) 3798 disp ( r ) newline 3799 end diagnose ) end define ]]" 3800 3801 Construct a proof of the rule "[[ r ]]" assuming the premisses "[[ P ]]". Complain if no proof is found. The function first tries to find "[[ r ]]" verbatim among the premisses (where each premise is tree searched). If no proof is found, "[[ r ]]" is decomposed. 3802 3803 \item "[[ eager define unitac-rule-plus ( R , P , c ) as newline 3804 3805 let << true ,, r ,, r prime >> = R in newline 3806 3807 let p = unitac-rule0 ( r , P , c ) in newline 3808 3809 if p then true else newline 3810 3811 let p prime = unitac-rule0 ( r prime , P , c ) in newline 3812 3813 if p prime then true else 3814 3815 back R quote p unquote ;; p prime unquote ;; ( ( r unquote oplus r prime unquote ) infer ( r unquote oplus r prime unquote ) Init ) Curry Ponens Ponens end quote end define ]]" 3816 3817 Construct a proof of the rule "[[ R ]]" of form "[[ r oplus r prime ]]" assuming the premisses "[[ P ]]". Return "[[ true ]]" if no proof is found. 3818 3819 \item "[[ eager define unitac-rule-stmt ( d , r , P , c ) as newline 3820 3821 let p = unitac-rule0 ( d , P , c ) in newline 3822 3823 if p then true else newline 3824 3825 back r quote p unquote ;; d unquote Init id est r unquote end quote end define ]]" 3826 3827 Construct a proof of the rule "[[ r ]]" with definition "[[ d ]]" assuming the premisses "[[ P ]]". Return "[[ true ]]" if no proof is found. 3828 3829 \item "[[ eager define unitac-rule1 ( r , P , c ) as newline 3830 3831 if P atom then true else newline 3832 3833 unitac-rule2 ( r , P head first , c ) .and. newline 3834 3835 unitac-rule1 ( r , P tail , c ) end define ]]" 3836 3837 Construct a proof of the rule "[[ r ]]" assuming the premisses "[[ P ]]". Return "[[ true ]]" if the rule is not found among the premisses. 3838 3839 \item "[[ eager define unitac-rule2 ( r , T , c ) as newline 3840 3841 let p = unitac-search ( r , T , c ) in newline 3842 3843 if p then true else newline 3844 3845 unitac-rule3 ( r , p ) end define ]]" 3846 3847 Construct a proof of the rule "[[ r ]]" assuming the theory "[[ T ]]". Sequent evaluating the proof gives "[[ << << T >> ,, true ,, r prime >> ]]" where "[[ r prime ]]" is what the rule with name "[[ r ]]" says. Return "[[ true ]]" if no proof is found (i.e.\ if the rule does not belong to the theory). 3848 3849 3850 3851 \item "[[ eager define unitac-search ( r , T , c ) as newline 3852 3853 unitac-search1 ( r , T , true , << T >> , c ) catch tail 3854 3855 end define ]]". 3856 3857 Search for the rule "[[ r ]]" in the theory "[[ T ]]" and return the ``path'' of "[[ r ]]". Return "[[ true ]]" is "[[ r ]]" is not found. 3858 3859 A path is a non-empty list of ``addresses''. An address is a pair of a tree and a list of ``edges''. Each edge is one of the strings ``head'' and ``tail''. As an example, the address "[[ << ( x oplus y ) oplus z ,, "head" ,, "tail" >> ]]" points out the "[[ y ]]" in the tree "[[ ( x oplus y ) oplus z ]]". 3860 3861 A path "[[ << a ,, b >> ]]" adresses some term "[[ a prime ]]" which, when dereferenced, is supposed to be the starting point of "[[ b ]]". As an example, "[[ << << p.Prop oplus p.A3 ,, "head" >> ,, << p.A1 oplus p.A2 oplus p.MP ,, "tail" ,, "head" >> >> ]]" is a path to "[[ p.A2 ]]" within "[[ p.Prop oplus p.A3 ]]". 3862 3863 The path is returned in reverse order. 3864 3865 3866 3867 \item "[[ eager define unitac-search1 ( r , T , p , a , c ) as newline 3868 3869 if r t= T then ( reverse ( a ) :: p ) raise else newline 3870 3871 let T prime = T stmt-rhs ( c ) in newline 3872 3873 if .not. T prime then unitac-search1 ( r , T prime , reverse ( a ) :: p , << T prime >> , c ) else newline 3874 3875 if T metadef ( c ) != "plus" then true else newline 3876 3877 unitac-search1 ( r , T first , p , "head" :: a , c ) .and. newline 3878 3879 unitac-search1 ( r , T second , p , "tail" :: a , c ) end define ]]". 3880 3881 Search for "[[ r ]]" in "[[ T ]]" and throw the path of "[[ r ]]" when found. Return "[[ true ]]" if "[[ r ]]" is not found. Accumulate the path in "[[ p ]]" in reverse order and the addresses in "[[ a ]]" in reverse order. The path is returned in reverse order. 3882 3883 3884 3885 \item "[[ eager define unitac-rule3 ( r , p ) as newline 3886 3887 let q = unitac-rule4 ( r , p head ) in newline 3888 3889 if p tail then q else 3890 3891 let p = unitac-rule3 ( r , p tail ) in newline 3892 3893 back r quote p unquote Deref ;; q unquote end quote end define ]]" 3894 3895 3896 3897 \item "[[ eager define unitac-rule4 ( r , a ) as newline 3898 3899 let p = unitac-rule5 ( r , a head , a tail , true ) in newline 3900 3901 back r quote p unquote Ponens end quote end define ]]". 3902 3903 Given an address "[[ T :: a ]]", construct a proof which generates the sequent "[[ << << T >> ,, true ,, a prime >> ]]" where "[[ a prime ]]" is the conjunct at address "[[ a ]]" in conjunction "[[ T ]]". 3904 3905 3906 3907 \item "[[ eager define unitac-rule5 ( r , T , a , s ) as newline 3908 3909 if a atom then newline 3910 3911 let p = unitac-stack ( r , s , back r quote T unquote Init end quote ) in 3912 3913 back r quote T unquote infer p unquote end quote else 3914 3915 let e :: a = a in newline 3916 3917 if e = "head" then newline 3918 3919 back r quote unitac-rule5 ( r , T first , a , T second :: s ) unquote Uncurry end quote else newline 3920 3921 back r quote ( T first unquote infer unitac-rule5 ( r , T second , a , s ) unquote ) Uncurry end quote end define ]]". 3922 3923 Given a conjunction "[[ T ]]" and a list "[[ a ]]" of edges, prove "[[ T infer a prime ]]" where "[[ a prime ]]" is the conjunct at address "[[ a ]]". 3924 3925 3926 3927 \item "[[ eager define unitac-stack ( r , s , t ) as newline 3928 3929 if s atom then t else newline 3930 3931 let p :: s = s in newline 3932 3933 let t = unitac-stack ( r , s , t ) in newline 3934 3935 back r quote p unquote infer t unquote end quote 3936 3937 end define ]]". 3938 3939 Add the premisses on the stack "[[ s ]]" to the term "[[ t ]]". 3940 3941 \end{statements} 3942 3943 3944 3945 \subsection{Lemmas} 3946 3947 \begin{statements} 3948 3949 \item "[[ eager define unitac-lemma ( u ) as newline 3950 3951 let << t ,, s ,, c >> = u in newline 3952 3953 let d = s [[ hook-unitac ]] [[ hook-lemma ]] in newline 3954 3955 ( eval ( d , true , c ) apply << t ,, s ,, c >> maptag ) untag end define ]]" 3956 3957 \item "[[ eager define unitac-lemma-std ( x ) as newline 3958 3959 let << t ,, s ,, c >> = x in newline 3960 3961 let << true ,, T ,, r >> = t stmt-rhs ( c ) in newline 3962 3963 let a prime = unitac-theo ( T , s , c ) in newline 3964 3965 let a = back t quote a prime unquote ;; t unquote Init Deref Ponens end quote in newline 3966 3967 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]". 3968 3969 Define how to sequent prove a lemma and what the lemma concludes. 3970 3971 \end{statements} 3972 3973 3974 3975 \section{Tactic definitions of proof line constructs} 3976 3977 \subsection{Conclude-cut lines} 3978 3979 \begin{statements} 3980 3981 \item "[[ macro define line l : a >> x ; n as Line l : a >> x ; n end define ]]" 3982 3983 \item "[[ tactic define Line l : a >> x ; n as \ u . tactic-conclude-cut ( u ) end define ]]" 3984 3985 \item "[[ eager define tactic-conclude-cut ( u ) as newline 3986 3987 let << t ,, s ,, c >> = u in newline 3988 3989 let << true ,, l ,, a ,, x ,, n >> = t in newline 3990 3991 let s prime = taceval ( back t quote a unquote conclude x unquote end quote , s , c ) in newline 3992 3993 let a prime = s prime [[ hook-arg ]] in newline 3994 3995 let r = s prime [[ hook-res ]] in newline 3996 3997 let s = tactic-push ( hook-pre , << l ,, r ,, back r quote r unquote Init end quote >> , s ) in newline 3998 3999 let s = taceval ( n , s , c ) in newline 4000 4001 let a = s [[ hook-arg ]] in newline 4002 4003 s [[ hook-arg -> back t quote a prime unquote ;; a unquote end quote ]] end define ]]" 4004 4005 \end{statements} 4006 4007 4008 4009 \subsection{Premise line} 4010 4011 \begin{statements} 4012 4013 \item "[[ macro define line l : Premise >> x ; n as Line l : Premise >> x ; n end define ]]" 4014 4015 \item "[[ tactic define Line l : Premise >> x ; n as \ u . tactic-premise-line ( u ) end define ]]" 4016 4017 \item "[[ eager define tactic-premise-line ( u ) as newline 4018 4019 let << t ,, s ,, c >> = u in newline 4020 4021 let << true ,, l ,, x ,, n >> = t in newline 4022 4023 let s = taceval ( n , tactic-push ( hook-pre , << l ,, x ,, back x quote x unquote Init end quote >> , s ) , c ) in newline 4024 4025 let a = back t quote x unquote infer s [[ hook-arg ]] unquote end quote in newline 4026 4027 let r = back t quote x unquote infer s [[ hook-res ]] unquote end quote in newline 4028 4029 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 4030 4031 \end{statements} 4032 4033 4034 4035 \subsection{Condition line} 4036 4037 \begin{statements} 4038 4039 \item "[[ macro define line l : Condition >> x ; n as Line l : Condition >> x ; n end define ]]" 4040 4041 \item "[[ tactic define Line l : Condition >> x ; n as \ u . tactic-condition-line ( u ) end define ]]" 4042 4043 \item "[[ eager define tactic-condition-line ( u ) as newline 4044 4045 let << t ,, s ,, c >> = u in newline 4046 4047 let << true ,, l ,, x ,, n >> = t in newline 4048 4049 let s = taceval ( n , tactic-push ( hook-cond , << l ,, x >> , s ) , c ) in newline 4050 4051 let a = back t quote x unquote endorse s [[ hook-arg ]] unquote end quote in newline 4052 4053 let r = back t quote x unquote endorse s [[ hook-res ]] unquote end quote in newline 4054 4055 s [[ hook-arg -> a ]] [[ hook-res -> r ]] end define ]]" 4056 4057 \end{statements} 4058 4059 4060 4061 \subsection{Blocks} 4062 4063 \begin{statements} 4064 4065 \item "[[ macro define line l : Block >> Begin ; x line k : Block >> End ; n as Line l : Block >> Begin ; x line k : Block >> End ; n end define ]]" 4066 4067 \item "[[ tactic define Line l : Block >> Begin ; x line k : Block >> End ; n as \ u . tactic-block ( u ) end define ]]" 4068 4069 \item "[[ eager define tactic-block ( u ) as newline 4070 4071 let << t ,, s ,, c >> = u in newline 4072 4073 let << true ,, l ,, x ,, k ,, n >> = t in newline 4074 4075 let s prime = taceval ( x , s , c ) in newline 4076 4077 let a prime = s prime [[ hook-arg ]] in newline 4078 4079 let r = s prime [[ hook-res ]] in newline 4080 4081 let s = tactic-push ( hook-pre , << k ,, r ,, back r quote r unquote Init end quote >> , s ) in newline 4082 4083 let s = taceval ( n , s , c ) in newline 4084 4085 let a = s [[ hook-arg ]] in newline 4086 4087 s [[ hook-arg -> back t quote a prime unquote ;; a unquote end quote ]] end define ]]" 4088 4089 \end{statements} 4090 4091 4092 4093 \section{Sample proofs} 4094 4095 \subsection{Propositional Calculus} 4096 4097 We now define Propositional Calculus ("[[ p.Prop ]]") as in \cite{Mendelson}. We also define Intuitionistic Propositional Calculus ("[[ p.IProp ]]"). 4098 4099 "[ axiom p.A1 : All #x ,, #y : #x p.imply #y p.imply #x end axiom ]" 4100 4101 "[ axiom p.A2 : All #x ,, #y ,, #z : ( #x p.imply #y p.imply #z ) p.imply ( #x p.imply #y ) p.imply #x p.imply #z end axiom ]" 4102 4103 "[ axiom p.A3 : All #x ,, #y : ( p.not #y p.imply p.not #x ) p.imply ( p.not #y p.imply #x ) p.imply #y end axiom ]" 4104 4105 "[ rule p.MP : All #x ,, #y : #x p.imply #y infer #x infer #y end rule ]" 4106 4107 "[ theory p.IProp : p.A1 oplus p.A2 oplus p.MP end theory ]" 4108 4109 "[ theory p.Prop : p.IProp oplus p.A3 end theory ]" 4110 4111 \noindent The inference rule of Modus Ponens ("[[ p.MP ]]") is typically applied to two arguments, so we introduce a macro for that: 4112 4113 "[[[ macro define x p.mp y as p.MP ponens x ponens y Conclude end define ]]]" 4114 4115 \noindent In the macro, "[[ y Conclude ]]" is argument "[[ y ]]" from which all occurences of "[[ All #u : #v ]]", "[[ #u infer #v ]]", and "[[ #u endorse #v ]]" are stripped by applications of "[[ #a at #b ]]", "[[ #a Ponens ]]", and "[[ #a Verify ]]", respectively. Stripping is done during tactic evaluation. The macro does not strip "[[ x ]]" since that happens automatically: During tactic evaluation, the "[[ p.MP ]]" rules forces "[[ x ]]" to be of form "[[ #x p.imply #y ]]" which causes "[[ x ]]" to be stripped. 4116 4117 As an example of a proof, take the first lemma proved in \cite{Mendelson}: 4118 4119 4120 4121 "[ p.Prop lemma lemma2 : All #x : #x p.imply #x end lemma ]" 4122 4123 "[ p.Prop proof of lemma2 : 4124 4125 line L01 : Arbitrary >> #x ; 4126 4127 line L02 : p.A2 >> 4128 ( #x p.imply ( #y p.imply #x ) p.imply #x ) p.imply newline 4129 ( #x p.imply #y p.imply #x ) p.imply #x p.imply #x ; 4130 4131 line L03 : p.A1 >> #x p.imply ( #y p.imply #x ) p.imply #x ; 4132 4133 line L04 : L02 p.mp L03 >> ( #x p.imply #y p.imply #x ) p.imply #x p.imply #x ; 4134 4135 line L05 : p.A1 >> #x p.imply #y p.imply #x ; 4136 4137 line L06 : L04 p.mp L05 >> #x p.imply #x qed ]" 4138 4139 \noindent We may leave more work to unification simply by omitting line "[[ L02 ]]" and "[[ L03 ]]": 4140 4141 "[ p.Prop lemma lemma2a : All #x : #x p.imply #x end lemma ]" 4142 4143 "[ p.Prop proof of lemma2a : 4144 4145 line L01 : Arbitrary >> #x ; 4146 4147 line L04 : p.A2 p.mp p.A1 >> ( #x p.imply #y p.imply #x ) p.imply #x p.imply #x ; 4148 4149 line L05 : p.A1 >> #x p.imply #y p.imply #x ; 4150 4151 line L06 : L04 p.mp L05 >> #x p.imply #x qed ]" 4152 4153 \noindent We may state the proof even shorter as follows: 4154 4155 "[ p.Prop lemma lemma2b : All #x : #x p.imply #x end lemma ]" 4156 4157 "[ p.Prop proof of lemma2b : 4158 4159 line L01 : Arbitrary >> #x ; 4160 4161 line L05 : p.A1 >> #x p.imply #y p.imply #x ; 4162 4163 line L06 : p.A2 p.mp p.A1 p.mp L05 >> #x p.imply #x qed ]" 4164 4165 \noindent It would be tempting to change the argumentation of line "[[ L06 ]]" to "[[ p.A2 p.mp p.A1 p.mp p.A1 ]]", but then unification would be unable to determine how to instantiate the second quantifier of "[[ p.A1 ]]". We may specify that instantiation explicitly, though: 4166 4167 "[ p.Prop lemma lemma2c : All #x : #x p.imply #x end lemma ]" 4168 4169 "[ p.Prop proof of lemma2c : 4170 4171 line L01 : Arbitrary >> #x ; 4172 4173 line L06 : p.A2 p.mp p.A1 p.mp ( p.A1 At at #y ) >> #x p.imply #x qed ]" 4174 4175 \noindent In the proof above, "[[ p.A1 At ]]" tells unification to instantiate the first quantifier of "[[ p.A1 ]]" suitably. "[[ p.A1 At at #y ]]" tells unification to instantiate the first quantifier suitably and to instantiate the second one to "[[ #y ]]". 4176 4177 Line "[[ L01 ]]" above applies the generalization sequent operator "[[ All #x : #y ]]" to the rest of the proof. The same effect may be achieved by putting that operator in the argumentation of line "[[ L06 ]]". But then one must also add a meta-quantifier to the conclusion of line "[[ L06 ]]". The "[[ All #x : #y ]]" construct happens to denote both the generalization sequent operator and the meta-quantifier: 4178 4179 "[ p.Prop lemma lemma2d : All #x : #x p.imply #x end lemma ]" 4180 4181 "[ p.Prop proof of lemma2d : 4182 4183 line L06 : All #x : p.A2 p.mp p.A1 p.mp ( p.A1 At at #y ) >> All #x : #x p.imply #x qed ]" 4184 4185 \noindent One may even leave to unification to guess the quantified variable: 4186 4187 "[ p.Prop lemma lemma2e : All #x : #x p.imply #x end lemma ]" 4188 4189 "[ p.Prop proof of lemma2e : 4190 4191 line L06 : ( p.A2 p.mp p.A1 p.mp ( p.A1 At at #y ) ) All >> All #x : #x p.imply #x qed ]" 4192 4193 \noindent The theory part of a lemma and a proof may be stated as a conjunction in an arbitrary order. Each conjunct may be a rule or a theory, where each theory recursively may be an arbitrary conjunction of rules and theories. As an example, "[[ p.IProp oplus p.A3 ]]" contains the rules "[[ p.A1 ]]", "[[ p.A2 ]]", "[[ p.A3 ]]", and "[[ p.MP ]]" which makes the following lemma and proof correct: 4194 4195 "[ p.IProp oplus p.A3 lemma lemma2f : All #x : #x p.imply #x end lemma ]" 4196 4197 "[ p.IProp oplus p.A3 proof of lemma2f : 4198 4199 line L01 : Arbitrary >> #x ; 4200 4201 line L06 : p.A2 p.mp p.A1 p.mp ( p.A1 At at #y ) >> #x p.imply #x qed ]" 4202 4203 4204 4205 \subsection{Blocks} 4206 4207 Blocks allow subproofs inside other proofs. The following example stress test the block concept in that it first proves that any statement "[[ #x ]]" implies itself, then applies that to the statement itself. The proof is much like applying the identity function to itself which of course yeilds the identity function. 4208 4209 "[ p.Prop lemma lemma3 : All #x : #x infer #x end lemma ]" 4210 4211 "[ p.Prop proof of lemma3 : 4212 4213 line L01 : Block >> Begin ; 4214 4215 line L02 : Arbitrary >> #x ; 4216 4217 line L03 : Premise >> #x ; 4218 4219 line L04 : L03 >> #x ; 4220 4221 line L05 : Block >> End ; 4222 4223 line L06 : L05 ponens L05 >> All #x : #x infer #x qed ]" 4224 4225 4226 4227 \subsection{System S} 4228 4229 For the sake of testing we introduce a small subset of Mendelsons System S. For historical reasons, this system is used in the Logiweb test suites. 4230 4231 "[ theory System S : S.S1 oplus S.S5 end theory ]" 4232 4233 "[ rule S.S1 : All #x ,, #y ,, #z : #x = #y infer #x = #z infer #y = #z end rule ]" 4234 4235 "[ rule S.S5 : All #x : #x + 0 = #x end rule ]" 4236 4237 "[ System S lemma S.reflexivity : All #x : #x = #x end lemma ]" 4238 4239 "[ System S proof of S.reflexivity : 4240 4241 line L01 : Arbitrary >> #x ; 4242 4243 line L02 : S.S5 >> #x + 0 = #x ; 4244 4245 line L03 : S.S1 ponens L02 ponens L02 >> #x = #x qed ]" 4246 4247 4248 4249 \subsection{Rules} 4250 4251 4252 4253 "[ p.Prop lemma lemma4a : p.IProp end lemma ]" 4254 4255 "[ p.Prop proof of lemma4a : 4256 4257 line L01 : p.IProp Rule >> p.IProp qed ]" 4258 4259 4260 4261 "[ p.Prop lemma lemma4b : p.A1 end lemma ]" 4262 4263 "[ p.Prop proof of lemma4b : 4264 4265 line L01 : p.A1 Rule >> p.A1 qed ]" 4266 4267 4268 4269 "[ p.Prop lemma lemma4c : p.A2 end lemma ]" 4270 4271 "[ p.Prop proof of lemma4c : 4272 4273 line L01 : p.A2 Rule >> p.A2 qed ]" 4274 4275 4276 4277 "[ p.Prop lemma lemma4d : p.A3 end lemma ]" 4278 4279 "[ p.Prop proof of lemma4d : 4280 4281 line L01 : p.A3 Rule >> p.A3 qed ]" 4282 4283 4284 4285 "[ p.IProp oplus p.A3 lemma lemma4e : p.Prop end lemma ]" 4286 4287 "[ p.IProp oplus p.A3 proof of lemma4e : 4288 4289 line L01 : p.Prop Rule >> p.Prop qed ]" 4290 4291 4292 4293 "[ p.IProp lemma lemma4f : p.A3 infer p.Prop end lemma ]" 4294 4295 "[ p.IProp proof of lemma4f : 4296 4297 line L01 : Premise >> p.A3 ; 4298 4299 line L02 : p.Prop Rule >> p.Prop qed ]" 4300 4301 4302 4303 "[ p.IProp lemma lemma4g : p.A3 infer x p.imply x end lemma ]" 4304 4305 "[ p.IProp proof of lemma4g : 4306 4307 line L01 : Premise >> p.A3 ; 4308 4309 line L02 : lemma2 >> x p.imply x qed ]" 4310 4311 4312 4313 \printindex 4314 4315 4316 4317 \bibliography{./page} 4318 4319 4320 4321 \end{document} 4322 " end text ,, 4323 4324 4325 4326 latex ( "page" ) ,, 4327 makeindex ( "page" ) ,, 4328 bibtex ( "page" ) ,, 4329 latex ( "page" ) ,, 4330 makeindex ( "page" ) ,, 4331 latex ( "page" ) ,, 4332 dvipdfm ( "page" ) ,, 4333 4334 4335 4336 text "chores.tex" : ""-""; 4337 4338 \documentclass[fleqn]{article} 4339 4340 % Include definitions generated by the Logiweb compiler 4341 \input{lgwinclude} 4342 4343 % Make latexsym characters available 4344 \usepackage{latexsym} 4345 4346 % Ensure reasonable rendering of strings 4347 \everymath{\rm} 4348 \everydisplay{\rm} 4349 4350 % Enable generation of an index 4351 \usepackage{makeidx} 4352 \makeindex 4353 \newcommand{\intro}[1]{\emph{#1}} 4354 \newcommand{\indexintro}[1]{\index{#1}\intro{#1}} 4355 4356 % Enable generation of a bibliography 4357 \bibliographystyle{plain} 4358 4359 % Enable hyperlinks 4360 \usepackage[dvipdfm=true]{hyperref} 4361 \hypersetup{pdfpagemode=UseNone} 4362 \hypersetup{pdfstartpage=1} 4363 \hypersetup{pdfstartview=FitBH} 4364 \hypersetup{pdfpagescrop={120 80 490 730}} 4365 \hypersetup{pdftitle=A Logiweb proof checker - chores} 4366 \hypersetup{colorlinks=true} 4367 4368 % Construct for listing statements with associated explanations 4369 \newenvironment{statements}{\begin{list}{}{ 4370 \setlength{\leftmargin}{5em} 4371 \setlength{\itemindent}{-5em}}}{\end{list}} 4372 4373 \begin{document} 4374 \title{A Logiweb proof checker - chores} 4375 \author{Klaus Grue} 4376 \maketitle 4377 \tableofcontents 4378 4379 4380 4381 \section{\TeX\ definitions} 4382 4383 \begin{statements} 4384 4385 \item "[[ tex show define alpha as " 4386 \alpha " end define ]]" 4387 4388 \item "[[ tex show define beta as " 4389 \beta " end define ]]" 4390 4391 \item "[[ tex show define gamma as " 4392 \gamma " end define ]]" 4393 4394 \item "[[ tex show define delta as " 4395 \delta " end define ]]" 4396 4397 \item "[[ tex show define epsilon as " 4398 \epsilon " end define ]]" 4399 4400 \item "[[ tex show define varepsilon as " 4401 \varepsilon " end define ]]" 4402 4403 \item "[[ tex show define zeta as " 4404 \zeta " end define ]]" 4405 4406 \item "[[ tex show define eta as " 4407 \eta " end define ]]" 4408 4409 \item "[[ tex show define theta as " 4410 \theta " end define ]]" 4411 4412 \item "[[ tex show define vartheta as " 4413 \vartheta " end define ]]" 4414 4415 \item "[[ tex show define iota as " 4416 \iota " end define ]]" 4417 4418 \item "[[ tex show define kappa as " 4419 \kappa " end define ]]" 4420 4421 \item "[[ tex show define lambda as " 4422 \lambda " end define ]]" 4423 4424 \item "[[ tex show define mu as " 4425 \mu " end define ]]" 4426 4427 \item "[[ tex show define nu as " 4428 \nu " end define ]]" 4429 4430 \item "[[ tex show define xi as " 4431 \xi " end define ]]" 4432 4433 \item "[[ tex show define pi as " 4434 \pi " end define ]]" 4435 4436 \item "[[ tex show define varpi as " 4437 \varpi " end define ]]" 4438 4439 \item "[[ tex show define rho as " 4440 \rho " end define ]]" 4441 4442 \item "[[ tex show define varrho as " 4443 \varrho " end define ]]" 4444 4445 \item "[[ tex show define sigma as " 4446 \sigma " end define ]]" 4447 4448 \item "[[ tex show define varsigma as " 4449 \varsigma " end define ]]" 4450 4451 \item "[[ tex show define tau as " 4452 \tau " end define ]]" 4453 4454 \item "[[ tex show define upsilon as " 4455 \upsilon " end define ]]" 4456 4457 \item "[[ tex show define phi as " 4458 \phi " end define ]]" 4459 4460 \item "[[ tex show define chi as " 4461 \chi " end define ]]" 4462 4463 \item "[[ tex show define psi as " 4464 \psi " end define ]]" 4465 4466 \item "[[ tex show define omega as " 4467 \omega " end define ]]" 4468 4469 \item "[[ tex show define Gamma as " 4470 \Gamma " end define ]]" 4471 4472 \item "[[ tex show define Delta as " 4473 \Delta " end define ]]" 4474 4475 \item "[[ tex show define Theta as " 4476 \Theta " end define ]]" 4477 4478 \item "[[ tex show define Lambda as " 4479 \Lambda " end define ]]" 4480 4481 \item "[[ tex show define Xi as " 4482 \Xi " end define ]]" 4483 4484 \item "[[ tex show define Pi as " 4485 \Pi " end define ]]" 4486 4487 \item "[[ tex show define Sigma as " 4488 \Sigma " end define ]]" 4489 4490 \item "[[ tex show define Upsilon as " 4491 \Upsilon " end define ]]" 4492 4493 \item "[[ tex show define Phi as " 4494 \Phi " end define ]]" 4495 4496 \item "[[ tex show define Psi as " 4497 \Psi " end define ]]" 4498 4499 \item "[[ tex show define Omega as " 4500 \Omega " end define ]]" 4501 4502 \item "[[ tex show define cla as "{\cal A}" end define ]]" 4503 4504 \item "[[ tex show define clb as "{\cal B}" end define ]]" 4505 4506 \item "[[ tex show define clc as "{\cal C}" end define ]]" 4507 4508 \item "[[ tex show define cld as "{\cal D}" end define ]]" 4509 4510 \item "[[ tex show define cle as "{\cal E}" end define ]]" 4511 4512 \item "[[ tex show define clf as "{\cal F}" end define ]]" 4513 4514 \item "[[ tex show define clg as "{\cal G}" end define ]]" 4515 4516 \item "[[ tex show define clh as "{\cal H}" end define ]]" 4517 4518 \item "[[ tex show define cli as "{\cal I}" end define ]]" 4519 4520 \item "[[ tex show define clj as "{\cal J}" end define ]]" 4521 4522 \item "[[ tex show define clk as "{\cal K}" end define ]]" 4523 4524 \item "[[ tex show define cll as "{\cal L}" end define ]]" 4525 4526 \item "[[ tex show define clm as "{\cal M}" end define ]]" 4527 4528 \item "[[ tex show define cln as "{\cal N}" end define ]]" 4529 4530 \item "[[ tex show define clo as "{\cal O}" end define ]]" 4531 4532 \item "[[ tex show define clp as "{\cal P}" end define ]]" 4533 4534 \item "[[ tex show define clq as "{\cal Q}" end define ]]" 4535 4536 \item "[[ tex show define clr as "{\cal R}" end define ]]" 4537 4538 \item "[[ tex show define cls as "{\cal S}" end define ]]" 4539 4540 \item "[[ tex show define clt as "{\cal T}" end define ]]" 4541 4542 \item "[[ tex show define clu as "{\cal U}" end define ]]" 4543 4544 \item "[[ tex show define clv as "{\cal V}" end define ]]" 4545 4546 \item "[[ tex show define clw as "{\cal W}" end define ]]" 4547 4548 \item "[[ tex show define clx as "{\cal X}" end define ]]" 4549 4550 \item "[[ tex show define cly as "{\cal Y}" end define ]]" 4551 4552 \item "[[ tex show define clz as "{\cal Z}" end define ]]" 4553 4554 \item "[[ tex show define statement as " 4555 stmt" end define ]]" 4556 4557 \item "[[ tex show define proof as " 4558 proof" end define ]]" 4559 4560 \item "[[ tex show define statement define x as y end define as " 4561 [ "[ texshow x end texshow ]" 4562 \stackrel{stmt}{=} "[ texshow y end texshow ]" 4563 ]" end define ]]" 4564 4565 \item "[[ tex show define proof define x as y end define as " 4566 [ "[ texshow x end texshow ]" 4567 \stackrel{proof}{=} "[ texshow y end texshow ]" 4568 ]" end define ]]" 4569 4570 \item "[[ tex show define meta define x as y end define as " 4571 [ "[ texshow x end texshow ]" 4572 \stackrel{meta}{=} "[ texshow y end texshow ]" 4573 ]" end define ]]" 4574 4575 \item "[[ tex show define math define x as y end define as " 4576 [ "[ texshow x end texshow ]" 4577 \stackrel{math}{=} "[ texshow y end texshow ]" 4578 ]" end define ]]" 4579 4580 \item "[[ tex show define tactic define x as y end define as " 4581 [ "[ texshow x end texshow ]" 4582 \stackrel{tactic}{=} "[ texshow y end texshow ]" 4583 ]" end define ]]" 4584 4585 \item "[[ tex show define unitac define x as y end define as " 4586 [ "[ texshow x end texshow ]" 4587 \stackrel{unitac}{=} "[ texshow y end texshow ]" 4588 ]" end define ]]" 4589 4590 \item "[[ tex show define locate define x as y end define as " 4591 [ "[ texshow x end texshow ]" 4592 \stackrel{locate}{=} "[ y ]" 4593 ]" end define ]]" 4594 4595 \item "[[ tex show define #a as " 4596 \mathsf{a}" end define ]]" 4597 4598 \item "[[ tex show define #b as " 4599 \mathsf{b}" end define ]]" 4600 4601 \item "[[ tex show define #c as " 4602 \mathsf{c}" end define ]]" 4603 4604 \item "[[ tex show define #d as " 4605 \mathsf{d}" end define ]]" 4606 4607 \item "[[ tex show define #e as " 4608 \mathsf{e}" end define ]]" 4609 4610 \item "[[ tex show define #f as " 4611 \mathsf{f}" end define ]]" 4612 4613 \item "[[ tex show define #g as " 4614 \mathsf{g}" end define ]]" 4615 4616 \item "[[ tex show define #h as " 4617 \mathsf{h}" end define ]]" 4618 4619 \item "[[ tex show define #i as " 4620 \mathsf{i}" end define ]]" 4621 4622 \item "[[ tex show define #j as " 4623 \mathsf{j}" end define ]]" 4624 4625 \item "[[ tex show define #k as " 4626 \mathsf{k}" end define ]]" 4627 4628 \item "[[ tex show define #l as " 4629 \mathsf{l}" end define ]]" 4630 4631 \item "[[ tex show define #m as " 4632 \mathsf{m}" end define ]]" 4633 4634 \item "[[ tex show define #n as " 4635 \mathsf{n}" end define ]]" 4636 4637 \item "[[ tex show define #o as " 4638 \mathsf{o}" end define ]]" 4639 4640 \item "[[ tex show define #p as " 4641 \mathsf{p}" end define ]]" 4642 4643 \item "[[ tex show define #q as " 4644 \mathsf{q}" end define ]]" 4645 4646 \item "[[ tex show define #r as " 4647 \mathsf{r}" end define ]]" 4648 4649 \item "[[ tex show define #s as " 4650 \mathsf{s}" end define ]]" 4651 4652 \item "[[ tex show define #t as " 4653 \mathsf{t}" end define ]]" 4654 4655 \item "[[ tex show define #u as " 4656 \mathsf{u}" end define ]]" 4657 4658 \item "[[ tex show define #v as " 4659 \mathsf{v}" end define ]]" 4660 4661 \item "[[ tex show define #w as " 4662 \mathsf{w}" end define ]]" 4663 4664 \item "[[ tex show define #x as " 4665 \mathsf{x}" end define ]]" 4666 4667 \item "[[ tex show define #y as " 4668 \mathsf{y}" end define ]]" 4669 4670 \item "[[ tex show define #z as " 4671 \mathsf{z}" end define ]]" 4672 4673 \item "[[ tex show define False as " 4674 \mathrel{\makebox[0mm][l]{$\bot$}\,{\bot}}" end define ]]" 4675 4676 \item "[[ tex show define p.A1 as " 4677 A1" end define ]]" 4678 4679 \item "[[ tex show define p.A2 as " 4680 A2" end define ]]" 4681 4682 \item "[[ tex show define p.A3 as " 4683 A3" end define ]]" 4684 4685 \item "[[ tex show define p.MP as " 4686 MP" end define ]]" 4687 4688 \item "[[ tex show define p.Prop as " 4689 Prop" end define ]]" 4690 4691 \item "[[ tex show define p.IProp as " 4692 IProp" end define ]]" 4693 4694 4695 4696 \item "[[ tex show define x# as "".[ x ]" 4697 {}^{\#}" end define ]]" 4698 4699 4700 4701 \item "[[ tex show define x member y as "".[ x ]" 4702 \in "[ y ]"". end define ]]" 4703 4704 4705 4706 \item "[[ tex show define p.not x as " 4707 \neg "[ x ]"". end define ]]" 4708 4709 4710 4711 \item "[[ tex show define x p.imply y as "".[ x ]" 4712 \Rightarrow "[ y ]"". end define ]]" 4713 4714 4715 4716 \item "[[ tex show define metadeclare x as " 4717 meta\ \linebreak [0]"[ x ]"". end define ]]" 4718 4719 4720 4721 \item "[[ tex show define x Init as "".[ x ]" 4722 {}^I " end define ]]" 4723 4724 \item "[[ tex show define x Ponens as "".[ x ]" 4725 {}^{\rhd} " end define ]]" 4726 4727 \item "[[ tex show define x Probans as "".[ x ]" 4728 {\makebox[0mm][l]{${}^\rhd$}\,{}^\rhd} " end define ]]" 4729 4730 \item "[[ tex show define x Verify as "".[ x ]" 4731 {}^{\ast} " end define ]]" 4732 4733 \item "[[ tex show define x Curry as "".[ x ]" 4734 {}^C " end define ]]" 4735 4736 \item "[[ tex show define x Uncurry as "".[ x ]" 4737 {}^U " end define ]]" 4738 4739 \item "[[ tex show define x Deref as "".[ x ]" 4740 {}^D " end define ]]" 4741 4742 \item "[[ tex show define x At as "".[ x ]" 4743 {}^@ " end define ]]" 4744 4745 \item "[[ tex show define x Infer as "".[ x ]" 4746 {}^{\vdash} " end define ]]" 4747 4748 \item "[[ tex show define x Endorse as "".[ x ]" 4749 {\makebox[0mm][l]{${}^\vdash$}\,{}^\vdash} " end define ]]" 4750 4751 \item "[[ tex show define x All as "".[ x ]" 4752 {}^{\Pi} " end define ]]" 4753 4754 \item "[[ tex show define x Conclude as "".[ x ]" 4755 {}^{\gg}" end define ]]" 4756 4757 4758 4759 \item "[[ tex show define x at y as "".[ x ]" 4760 \mathrel{@} "[ y ]"". end define ]]" 4761 4762 \item "[[ tex show define x ponens y as "".[ x ]" 4763 \rhd "[ y ]"". end define ]]" 4764 4765 \item "[[ tex show define x probans y as "".[ x ]" 4766 \mathrel{\makebox[0mm][l]{$\rhd$}\,{\rhd}} "[ y ]"". end define ]]" 4767 4768 \item "[[ tex show define x infer y as "".[ x ]" 4769 \vdash "[ y ]"". end define ]]" 4770 4771 \item "[[ tex show define x endorse y as "".[ x ]" 4772 \mathrel{\makebox[0mm][l]{$\vdash$}\,{\vdash}} "[ y ]"". end define ]]" 4773 4774 \item "[[ tex show define x id est y as "".[ x ]" 4775 \mathrel{ie} "[ y ]"". end define ]]" 4776 4777 \item "[[ tex show define x verify y as "".[ x ]" 4778 \mathrel{\ast} "[ y ]"". end define ]]" 4779 4780 \item "[[ tex show define x conclude y as "".[ x ]" 4781 \gg "[ y ]"". end define ]]" 4782 4783 \item "[[ tex show define x p.mp y as "".[ x ]" 4784 \unrhd "[ y ]"". end define ]]" 4785 4786 4787 4788 \item "[[ tex show define All x : y as " 4789 \Pi "[ x ]" 4790 \colon "[ y ]"". end define ]]" 4791 4792 4793 4794 \item "[[ tex show define x oplus y as "".[ x ]" 4795 \oplus "[ y ]"". end define ]]" 4796 4797 4798 4799 \item "[[ tex use define line x : y >> z ; u as " 4800 \newline% 4801 \makebox[0.1\textwidth]{}% 4802 \parbox[b]{0.4\textwidth}{\raggedright% 4803 \makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}% 4804 $"[ y ]" {} \gg {}$}% 4805 \parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}% 4806 $"[ z ]"$\hfill 4807 \makebox[0mm][l]{\quad ;}} "[ u ]"". end define ]]" 4808 4809 \item "[[ tex show define line x : y >> z ; u as " 4810 L "[ x ]" 4811 \colon "[ y ]" 4812 \gg "[ z ]" 4813 ; "[ u ]"". end define ]]" 4814 4815 \item "[[ tex use define line x : y >> z ; as " 4816 \newline% 4817 \makebox[0.1\textwidth]{}% 4818 \parbox[b]{0.4\textwidth}{\raggedright% 4819 \makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}% 4820 $"[ y ]" {} \gg {}$}% 4821 \parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}% 4822 $"[ z ]"$\hfill 4823 \makebox[0mm][l]{\quad ;}}" end define ]]" 4824 4825 \item "[[ tex show define line x : y >> z ; as " 4826 L "[ x ]" 4827 \colon "[ y ]" 4828 \gg "[ z ]" 4829 ;" end define ]]" 4830 4831 \item "[[ tex use define line x : y >> z qed as " 4832 \newline% 4833 \makebox[0.1\textwidth]{}% 4834 \parbox[b]{0.4\textwidth}{\raggedright% 4835 \makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}% 4836 $"[ y ]" {} \gg {}$}% 4837 \parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}% 4838 $"[ z ]"$\hfill 4839 \makebox[0mm][l]{\quad $\Box$}}" end define ]]" 4840 4841 \item "[[ tex show define line x : y >> z qed as " 4842 L "[ x ]" 4843 \colon "[ y ]" 4844 \gg "[ z ]" 4845 \Box" end define ]]" 4846 4847 \item "[[ tex use define line x : Premise >> z ; u as " 4848 \newline% 4849 \makebox[0.1\textwidth]{}% 4850 \parbox[b]{0.4\textwidth}{\raggedright% 4851 \makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}% 4852 $Premise {} \gg {}$}% 4853 \parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}% 4854 $"[ z ]"$\hfill 4855 \makebox[0mm][l]{\quad ;}} "[ u ]"". end define ]]" 4856 4857 \item "[[ tex show define line x : Premise >> z ; u as " 4858 L "[ x ]" 4859 \colon Premise 4860 \gg "[ z ]" 4861 ; "[ u ]"". end define ]]" 4862 4863 \item "[[ tex use define line x : Condition >> z ; u as " 4864 \newline% 4865 \makebox[0.1\textwidth]{}% 4866 \parbox[b]{0.4\textwidth}{\raggedright% 4867 \makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}% 4868 $Condition {} \gg {}$}% 4869 \parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}% 4870 $"[ z ]"$\hfill 4871 \makebox[0mm][l]{\quad ;}} "[ u ]"". end define ]]" 4872 4873 \item "[[ tex show define line x : Condition >> z ; u as " 4874 L "[ x ]" 4875 \colon Condition 4876 \gg "[ z ]" 4877 ; "[ u ]"". end define ]]" 4878 4879 \item "[[ tex use define line x : Arbitrary >> z ; u as " 4880 \newline% 4881 \makebox[0.1\textwidth]{}% 4882 \parbox[b]{0.4\textwidth}{\raggedright% 4883 \makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}% 4884 $Arbitrary {} \gg {}$}% 4885 \parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}% 4886 $"[ z ]"$\hfill 4887 \makebox[0mm][l]{\quad ;}} "[ u ]"". end define ]]" 4888 4889 \item "[[ tex show define line x : Arbitrary >> z ; u as " 4890 L "[ x ]" 4891 \colon Arbitrary 4892 \gg "[ z ]" 4893 ; "[ u ]"". end define ]]" 4894 4895 \item "[[ tex use define line x : Local >> y = z ; u as " 4896 \newline% 4897 \makebox[0.1\textwidth]{}% 4898 \parbox[b]{0.4\textwidth}{\raggedright% 4899 \makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}% 4900 $Local {} \gg {}$}% 4901 \parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}% 4902 $"[ y ]" \mathrel{\ddot{=}} "[ z ]"$\hfill 4903 \makebox[0mm][l]{\quad ;}} "[ u ]"". end define ]]" 4904 4905 \item "[[ tex show define line x : Local >> y = z ; u as " 4906 L "[ x ]" 4907 \colon Local 4908 \gg "[ y ]" \mathrel{\ddot{=}} "[ z ]" 4909 ; "[ u ]"". end define ]]" 4910 4911 \item "[[ tex use define line x : Block >> Begin ; y line z : Block >> End ; u as " 4912 \newline% 4913 \makebox[0.1\textwidth]{}% 4914 \parbox[b]{0.4\textwidth}{\raggedright% 4915 \makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]"{:}$}}% 4916 $Block {} \gg {}$}% 4917 \parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}% 4918 $Begin$\hfill 4919 \makebox[0mm][l]{\quad ;}}\addtolength{\indentation}{1em} "[ y ]" 4920 \newline\addtolength{\indentation}{-1em}% 4921 \makebox[0.1\textwidth]{}% 4922 \parbox[b]{0.4\textwidth}{\raggedright% 4923 \makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ z ]"{:}$}}% 4924 $Block {} \gg {}$}% 4925 \parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}% 4926 $End$\hfill 4927 \makebox[0mm][l]{\quad ;}} "[ u ]"". end define ]]" 4928 4929 \item "[[ tex show define line x : Block >> Begin ; y line z : Block >> End ; u as " 4930 L "[ x ]" 4931 \colon Block \gg Begin ; \quad "[ y ]" 4932 \quad L "[ z ]" 4933 \colon Block \gg End ; "[ u ]"". end define ]]" 4934 4935 \item "[[ tex use define prepare proof indentation as " 4936 \ifx\indentation\undefined 4937 \newlength{\indentation}\setlength{\indentation}{0em} 4938 \fi" end define ]]" 4939 4940 4941 4942 \item "[[ tex show define x ;; y as "".[ x ]" 4943 ; "[ y ]"". end define ]]" 4944 4945 4946 4947 \item "[[ tex use define axiom x : y end axiom as " 4948 \addvspace{\abovedisplayskip} 4949 \noindent $\mathbf{Axiom\ }"[ x ]" 4950 \colon "[ y ]" 4951 \;\Box$ 4952 4953 \addvspace{\belowdisplayskip}" end define ]]" 4954 4955 \item "[[ tex show define axiom x : y end axiom as " 4956 \mathbf{Axiom\ }"[ x ]" 4957 \colon "[ y ]" 4958 \;\Box" end define ]]" 4959 4960 \item "[[ tex use define rule x : y end rule as " 4961 \addvspace{\abovedisplayskip} 4962 \noindent $\mathbf{Rule\ }"[ x ]" 4963 \colon "[ y ]" 4964 \;\Box$ 4965 4966 \addvspace{\belowdisplayskip}" end define ]]" 4967 4968 \item "[[ tex show define rule x : y end rule as " 4969 \mathbf{Rule\ }"[ x ]" 4970 \colon "[ y ]" 4971 \;\Box" end define ]]" 4972 4973 \item "[[ tex use define theory x : y end theory as " 4974 \addvspace{\abovedisplayskip} 4975 \noindent $\mathbf{Theory\ }"[ x ]" 4976 \colon "[ y ]" 4977 \;\Box$ 4978 4979 \addvspace{\belowdisplayskip}" end define ]]" 4980 4981 \item "[[ tex show define theory x : y end theory as " 4982 \mathbf{Theory\ }"[ x ]" 4983 \colon "[ y ]" 4984 \;\Box" end define ]]" 4985 4986 \item "[[ tex use define lemma x : y end lemma as " 4987 \addvspace{\abovedisplayskip} 4988 \noindent $\mathbf{Lemma\ }"[ x ]" 4989 \colon "[ y ]" 4990 \;\Box$ 4991 4992 \addvspace{\belowdisplayskip}" end define ]]" 4993 4994 \item "[[ tex show define lemma x : y end lemma as " 4995 \mathbf{Lemma\ }"[ x ]" 4996 \colon "[ y ]" 4997 \;\Box" end define ]]" 4998 4999 \item "[[ tex use define x lemma y : z end lemma as " 5000 \addvspace{\abovedisplayskip} 5001 \noindent $"[ x ]" 5002 \mathbf{\ lemma\ }"[ y ]" 5003 \colon "[ z ]" 5004 \;\Box$ 5005 5006 \addvspace{\belowdisplayskip}" end define ]]" 5007 5008 \item "[[ tex show define x lemma y : z end lemma as "".[ x ]" 5009 \mathbf{\ lemma\ }"[ y ]" 5010 \colon "[ z ]" 5011 \;\Box" end define ]]" 5012 5013 \item "[[ tex use define proof of x : y as " 5014 \addvspace{\abovedisplayskip} 5015 \noindent $\mathbf{Proof\ of\ }"[ x ]" 5016 \colon "[ y ]"$ 5017 5018 \addvspace{\belowdisplayskip}" end define ]]" 5019 5020 \item "[[ tex show define proof of x : y as " 5021 \mathbf{Proof\ of\ }"[ x ]" 5022 \colon "[ y ]"". end define ]]" 5023 5024 \item "[[ tex use define x proof of y : z as " 5025 \addvspace{\abovedisplayskip} 5026 \noindent $"[ x ]" 5027 \mathbf{\ proof\ of\ }"[ y ]" 5028 \colon "[ z ]"$ 5029 5030 \addvspace{\belowdisplayskip}" end define ]]" 5031 5032 \item "[[ tex show define x proof of y : z as "".[ x ]" 5033 \mathbf{\ proof\ of\ }"[ y ]" 5034 \colon "[ z ]"". end define ]]" 5035 5036 5037 5038 \item "[[ tex show define glue ( x ) y as " 5039 glue\linebreak [0]\ (\linebreak [0]\ "[ texshow x end texshow ]" 5040 \linebreak [0]\ )\linebreak [0]\ "[ y ]"". end define ]]" 5041 5042 \item "[[ tex show define diag ( x ) y as " 5043 diag\linebreak [0]\ (\linebreak [0]\ "[ texshow x end texshow ]" 5044 \linebreak [0]\ )\linebreak [0]\ "[ y ]"". end define ]]" 5045 5046 \item "[[ tex use define glue' ( x ) y as "".[ x ]"".[ y ]"". end define ]]" 5047 5048 \item "[[ tex use define diag' ( x ) y as " 5049 "[ x ]" "[ y ]"". end define ]]" 5050 5051 \item "[[ tex use define disp' ( x ) y as " 5052 \begin{quotation} \noindent $ "[ x ]" 5053 $ \end{quotation} "[ y ]"". end define ]]" 5054 5055 \item "[[ tex use define form' ( x ) y as " 5056 $ "[ x ]" 5057 $"[ y ]"". end define ]]" 5058 5059 5060 5061 \end{statements} 5062 5063 5064 5065 \section{Name definitions} 5066 5067 "[[ protect ""N end protect ]]" 5068 5069 5070 5071 \section{Charge definitions} 5072 5073 "[[ protect ""C end protect ]]" 5074 5075 5076 5077 \end{document} 5078 " end text ,, 5079 5080 5081 5082 latex ( "chores" ) ,, 5083 latex ( "chores" ) ,, 5084 dvipdfm ( "chores" ) 5085 5086 5087 5088