% ENKITEI % Interactive proof system for natural deduction % with inductive definitions % % The present file implements the interactive proof system Enkitei % that extends classical natural deduction (NK) with definitions, % including inductive definitions. For the latter, the system can % derive an induction principle and apply it. We illustrate Enkitei % on tutorial examples of inductive proofs; we conclude by % proving the mirror involution theorem for binary trees. % % Enkitei is an interactive system: it displays the current judgements % and lets the user apply deduction steps by entering various tactics. % A tactic can prove the current judgement, produce a new one, or split % the current judgements into sub-judgements. The proof concludes % when there are no more judgements. % % Classical Natural Deduction (NK) deals with `judgments', of the form % Hs |- G % where G is the first-order logic formula to prove (the `goal') % and Hs is the possibly empty list of first-order logic formulas % (assumptions, or hypothesis). % The goal G is considered proved from assumptions Hs when the % judgment Hs |- G is valid: that is, it has the form G1 |- G1 for some G1, % or it can be obtained from valid judgements by a sequence of inference % rules on NK. % Enkitei takes as input a judgement Hs |- G (which is often just [] |- G), % and tries to prove it valid (or, `prove it', for short) % by finding, with user's help, a way to reduce the problem judgement % to valid judgements. % % Although Enkitei is written in Prolog (the present file is the complete % implementation), we cannot use Prolog directly to prove judgements. % First of all, we deal with arbitrary first-order logic formulas, % not restricted at all to Horn clauses. All in all, Enkitei had % to solve the following problems: % -- incorporating definitions into NK; % -- integrating the global environment -- Prolog's database % of facts and clauses -- with local assumptions of a judgement; % -- choosing the `right' eigen-variables; % -- recognizing inductive definitions and introducing inductive % hypotheses. % % We extensively rely on Prolog's meta-call facilities. One may regard % Enkitei as a greatly extended, stepping meta-circular Prolog interpreter. % The code contains many tests and examples, including inductive proofs % from Pierce's Software Foundations course. % * Local assumptions % % Let's consider the judgement % [] |- (p(0); p(1)) -> p(0) % where (G1;G2) means the disjunction of formulas G1 and G2 and % G1->G2 denotes implication. % To decide the validity of the judgement, we convert it to the following, % relying on the implication introduction rule of NK: % (p(0); p(1)) |- p(0) % The implication introduction rule of NK licences the conversion. % If one thinks of local assumptions naively, as facts to % assert when proving a goal, one would be tempted to answer the % validity question by the Prolog query % ?- assert(p(0)), assert(p(1)), p(0). % assert-ing the assumed disjunction (p(0); p(1)) as two facts % in the Prolog database. The query succeeds, seemingly letting us % conclude that the judgment, and hence the original implication % (p(0); p(1)) -> p(0) is valid. That would be wrong! In a model in which % only p(1) is true, the antecedent of the implication will be true % whereas the conclusion will be false. Our implication formula is % not true in all models and hence cannot be proven. % The correct (according to the disjunction elimination rule of NK) % way of proving % (p(0); p(1)) |- p(0). % is to generate two sub-judgments: p(0) |- p(0) and p(1) |- p(0). % The former is provable but the latter is not. % We conclude that we cannot treat assumptions as a `local database' % of Prolog rules and facts subject to regular Prolog proof search rules. % The assumptions must be handled specially: see the tactics below. % * Eigenvariables % % The paper ``A proof theory for generic judgments'' by Dale Miller and % Alwen Tiu (LICS 2003) well explains two approaches to proving % a universally quantified formula % forall X. p(X) -> q(X) % with predicates p and q. % (We adapt Miller and Tiu's typed approach to the untyped setting.) % The _intensional_ approach generates a fresh constant c that has not % occurred before in the proof, and attempts to prove p(c) -> q(c). % This approach, used by Gentzen in the original presentation of % the sequent calculus, is popular in sequent and natural deduction calculi. % The fresh constant is called eigenvariable: despite its name, it truly % is a constant, not being subject to substitution. % The other, _extensional_ approach attempts to prove q(X) for all those % X for which p(X) holds. In other words, we attempt to prove q(X) for all % X in the extension of the predicate p. We pre-suppose that the extension % is tractable; for example, it is finite and small, or it is % inductively enumerable. % % Enkitei uses both approaches. We rely on the extensional approach % when p is (inductively) defined. We use the intensional approach % otherwise. It is difficult to tell off-hand which of the two % approaches turns out helpful in proving a given universally % quantified formula. To analyze the body of the formula however, we must % remove the quantifier first. If we replace the quantified variable with the % fresh constant right away, we commit to the intensional approach, forgoing % the extensional one. To keep our choice, we delay our commitment to either % approach. We remove the universal quantifier, replacing the quantified % variable with a fresh Prolog _variable_. We keep track of such % eigen-_variables_, attaching them to the current judgement and carrying % along through the proof process. Right before we attempt to prove a goal % by a tactic that may match a goal against an assumption or a definition, % we instantiate all attached eigen-variables with fresh constants. That is, % we commit to the intensional approach. On the other hand, tactics that % unfold definitions within assumptions (such as destruct or induction) % are free to instantiate eigen-variables with the values of the domain % of the defined predicate. % * Definitions % % Enkitei uses global Prolog database of facts and clauses as % the repository of _definitions_. Suppose the global database % contains two facts: % bool(0). bool(1). % which are equivalent to the clause % bool(X) :- (X = 0; X = 1). % That is, bool(X) is provable if X is 0 or X is 1. In the % closed-world view of the global database -- standard in Prolog -- % there are no other ways of proving bool(X). The closed-world view % thus justifies strengthening of the implication to the equality: % bool(X) := (X = 0; X = 1). % We take this equality to be a _definitional equality_. Any appearance % of a formula bool(t) with some term t can be replaced with % formula (t=0; t=1), by unfolding the definition of bool. % % Definitions thus play the role of data-type declarations. In Haskell-like % notation, the definition of bool can be written as % data Bool = 0 | 1 % with the predicate bool akin to a data-type predicate, whose % extension is comprised of 0 and 1. The latter may be regarded as % data constructors of bool. Unlike Haskell or Coq, our data constructors % are not unique to the data type and can be shared among different % data types. The sharing simplifies the code but precludes the use % of the inversion principle (see however inductive definitions below). % % The tactic 'destruct' unfolds a definition for a formula in the assumptions % of a judgement. This unfolding may instantiate eigen-variables. % The tactic 'constructor n' applies to a goal, unfolding the n-th % clause of the definition for the goal predicate (compare with the % disjunction introduction rule of NK). The clause number can be regarded as % a `constructor number'. The number n may be omitted; the tactic will % unfold the first fitting clause. The tactic 'simpl' iteratively % unfolds definitions within a goal, using Prolog's built-in proof search. % For goals, unfolding of definitions must not instantiate eigen-variables. % Therefore, the tactics simpl and constructor first instantiate % eigen-variables with fresh constants. % % We do not impose any constraints on the form of definitions. For example, % bar(X). % is an admissible definition, stating that bar(X) holds for any X. Therefore, % if bar(t), for some term t, appears in assumptions, the tactic destruct % will remove the assumption since it has been asserted as an axiom. % If bar(t) is the goal, the tactic simpl will prove it. % The definition % baz(Z) :- baz(Z). % is too an admissible, albeit useless, definition. Tactics destruct % or constructor will replace any occurrence of baz(t) with itself -- % the expected, but not productive result. % % ** A few other examples of definitions % If the global database contains % nat(z). nat(s(N)) :- nat(N). % and nat(X) is an assumption, the destruct tactic will replace the % assumption with % (X=z; exists(N,(nat(N),X=s(N)))) % Actually, the destruct tactic will also apply the disjunction and % existential elimination rules of NK. % Thus, given a judgement % nat(X), Hs |- G % the tactic destruct produces two judgements % Hs |- G with all occurrences of X replaced with z % nat(N), Hs |- G with all occurrences of X replaced with s(N) % and N being the eigenvariable. % We should contrast this outcome with the application of the tactic % 'induction' to the same judgment, see below. % % The disjunction of formulas could have been introduced by defining % disj(X,Y) :- X. disj(X,Y) :- Y. % The tactics left and right (disjunction introduction) % become equivalent to 'constructor 1' and 'constructor 2' respectively. % The tactic hintro (disjunction elimination) becomes an instance of % 'destruct'. % % For more information about constructive definitions, see Sec 4.5 of % http://coq.inria.fr/V8.1/refman/Reference-Manual006.html % Since we do not impose any constraints on definitions, injectivity % does not generally hold. We cannot implement Coq's inversion % tactic. % * Inductive definitions % % Inductive definitions are the definitions of a (very) restricted form. % The predicate must have arity 1. If a definition clause has the body, % the head of the clause must be of the form pred(t) where t is not % a variable, and all goals in the body must have the form pred(X) % where X is a variable that occurs in t. % % The restrictions are overly draconian and can be relaxed, for example, % for mutual recursion. Nevertheless, the restriction admits % popular inductive data types such as natural numbers, lists, % and trees. Here are sample inductive definitions, to be used in % the examples below. nat(z). nat(s(N)) :- nat(N). % A bad definition of nat: cannot be used for induction nat_bad(s(N)) :- nat_bad(s(N)). % another bad definition of nat: cannot be used for induction nat_bad1(N) :- nat_bad1(N). % Heterogeneous list list(nil). list(cons(_,T)) :- list(T). % For binary trees, see below. % For inductive definitions, the tactic 'induction' can derive % an inductive hypothesis and apply it to a judgement. The tactic first % verifies that the definition satisfies the constraints for inductive % definitions. % For example, given a judgement % nat(X) |- (Hs -> G) % the tactic induction produces two judgements: % [] |- (Hs{X:=z} -> G{X:=z}) % (Hs{X:=N} -> G{X:=N}), nat(N) |- (Hs{X:=s(N)} -> G{X:=s(N)}) % where N being an eigenvariable. % Here G{X:=z} means substitution of z for X in G. %======================================================================== % Implementation notes % Formulas: % atomic formulas are Prolog atoms, or terms whose functor is other than % ',', ';', '->', 'not', forall, exists. % If G1 and G2 are formulas, so are the following: % conjunction: G1, G2 % disjunction: G1; G2 % implication: G1 -> G2 % negation: not(G1) % existential: exists(X,G1) % universal: forall(X,G1) % % A judgement in Enkitei has the form % j(Hs,G,Vs) % where Hs is the (possibly empty) list of assumptions, G is the goal, % Vs is the list of (usually unground) terms -- eigenvariables. % Eigenvariables have been explained in the introduction. % % Since proving G may involve proving proving several sub-goals, % Enkitei deals with the list of judgements. When the goal in a judgement % is proved, the judgement is eliminated from the list. When the list % becomes empty, the overall proof succeeds. %======================================================================== % Tactics % A basic tactic is a predicate % tactic +Name +J -Js % that takes a judgement and returns a list of new judgements. % The list Js may be empty if the judgement J has been proven. % We justify the tactics by relating them to the inference % rules of NK. % For the general reference to NK, see % http://plato.stanford.edu/entries/reasoning-automated/#6 % Tactics operating on the goal % Tactics based on the introduction rules % justification: conjunction-introduction rule of NK. tactic(intro, j(Hs,(G1,G2),Vs), [j(Hs,G1,Vs), j(Hs,G2,Vs)]). % justification: implication-introduction rule of NK. tactic(intro, j(Hs,(G1 -> G2),Vs), [j([G1|Hs],G2,Vs)]). % justification: forall-introduction rule of NK. % We add the variable X1 to the list of eigen-variables. % Unfolding of a goal must not touch eigen-variables. % See the discussion of eigen variables elsewhere. tactic(intro, j(Hs,forall(X,G),Vs), [j(Hs,G1,[X1|Vs])]) :- freshen_var(X,(X,G),(X1,G1)) . % justification: existential-introduction rule of NK. % We create the copy of G with a fresh variable X, so X can be % instantiated to any term. tactic(intro, j(Hs,exists(X,G),Vs), [j(Hs,G1,Vs)]) :- freshen_var(X,G,G1). % When it comes to disjunction, the user must specify % which branch of the disjunction to work on. % justification: disjunction-introduction rule of NK. tactic(left, j(Hs,(G1;_G2),Vs), [j(Hs,G1,Vs)]). tactic(right, j(Hs,(_G1;G2),Vs), [j(Hs,G2,Vs)]). % justification: conjunction-elimination rule of NK. % The solution must preserve the freshness of eigen-variables. tactic(assumption, j(Hs,G,Vs), []) :- instantiate(Vs), memberchk(G,Hs). % Try to solve the goal using global environment. % The solution must preserve the freshness of eigen-variables. % justification: conjunction-elimination rule of NK, applied to the % global environment. tactic(simpl, j(_Hs,G,Vs), []) :- instantiate(Vs), G. % constructor(n) tries to unroll the n-th clause in the definition % of the predicate, which is the functor of the goal. % The numbering is 1-based. % Just 'constructor' chooses the first appropriate clause. % Eigen-variables must be freshened. tactic(constructor, J, Js) :- once(tactic(constructor(_),J,Js)). tactic(constructor(N), j(Hs,G,Vs), Js) :- defined(G), % first try the expansion instantiating Vs copy_term( (G,Vs), (Gf,Vsf) ), instantiate(Vsf), apply_clause(N,Gf,_), % now apply again, using the same N. % We are certain that instantiatedness is preserved apply_clause(N,G,G1), Js = [j(Hs,G1,Vs)]. % Tactics operating on the list of assumptions, usually on the first % assumption of the list. % move the hypothesis number N to the head of the hypothesis list. % The numbering of hypotheses starts with 1. % Just 'move' is the same as move(2), exchanging the two top tactics. % justification: in classical logic, the order of assumptions does not matter tactic(move(N), j(Hs,G,Vs), [j(Hs1,G,Vs)]) :- move_list(N,Hs,Hs1). tactic(move, j(Hs,G,Vs), [j(Hs1,G,Vs)]) :- move_list(2,Hs,Hs1). % justification: disjunction-elimination rule of NK. tactic(hintro, j([(H1;H2)|Hs],G,Vs), [j([H1|Hs],G,Vs), j([H2|Hs],G,Vs)]). % The list of assumptions is implicitly conjoined. tactic(hintro, j([(H1,H2)|Hs],G,Vs), [j([H1,H2|Hs],G,Vs)]). % justification: forall-elimination rule of NK plus cut (i.e., % implication elimination) % We create the copy of H with a fresh variable X, so X can be % instantiated to any term. tactic(hintro, j([forall(X,H)|Hs],G,Vs), [j([H1, forall(X,H)|Hs],G,Vs)]) :- freshen_var(X,H,H1). % justification: exists-elimination rule of NK. % We add the variable X1 to the list of eigen-variables. tactic(hintro, j([exists(X,H)|Hs],G,Vs), [j([H1|Hs],G,[X1|Vs])]) :- freshen_var(X,(X,H),(X1,H1)) . % justification: implication elimination % Or: convert X-> (X->Y) -> G to the normal form and simplify. tactic(cut, j([H1->G1|Hs],G,Vs), [j(Hs,H1,Vs), j([G1|Hs],G,Vs)]). % Tactics dealing with definitions % If there is a definition for the top hypothesis, unfold the definition. tactic(destruct, j([H|Hs],G,Vs), Js) :- defined(H), (bagof(J, H^Hs^G^Vs^expand_def(j([H|Hs],G,Vs),J), Js); Js = []). % prove by contradiction tactic(induction, j([H|Hs],G,Vs), Js) :- check_inductive(H), make_implications(Hs,G,G1), bagof(J, H^G1^Vs^induction_def(H,G1,Vs,J), Js). %% Yet to do %% negation introduction and elimination % Composite tactics, added for convenience. % Apply the intro tactic as far as possible. It never fails. tactic(intros, J, Js) :- tactic(intro, J, [J1|Js1]), tactic(intros, J1, Js2), append(Js2,Js1,Js). tactic(intros, J, [J]). % auxiliary predicates % rotate a list, shifting the first element to the end of the list rotate([],[]). rotate([H|T],L) :- append(T,[H],L). % move_list +N +List1 -List2 % brings the element number N to the top. % The numbering starts with 1. move_list(1,L,L). move_list(N,[H|T],[H1,H|T1]) :- N > 1, N1 is N-1, move_list(N1,T,[H1|T1]). % delete an element from a list, using physical equality. % remq +List1 +Elem -List2 remq([X|T],Y,T) :- X == Y. remq([H|T],Y,[H|T1]) :- remq(T,Y,T1). % memq +X +List % Membership test according to physical equality. memq(X,[H|_]) :- X == H. memq(X,[_|T]) :- memq(X,T). % diff_list_q +List1 +List2 -List3 % List3 contains all elements of List1 which are not in List2 % We use physical equality, to be able to compare variables diff_list_q([],_,[]). diff_list_q([H|T],L2,T1) :- once(memq(H,L2)), diff_list_q(T,L2,T1). diff_list_q([H|T],L2,[H|T1]) :- diff_list_q(T,L2,T1). % freshen_var +Var +Term1 -Term2 % Term2 is a copy of Term1 such that the variable Var is fresh freshen_var(X,G,G1) :- term_variables(G,VGX), once(remq(VGX,X,VG)), copy_term((G,VG), (G1,VG)). eigen(X) :- gensym(e,X). % Ground a term, instantiating all of its variables to fresh constants instantiate(T) :- term_variables(T,Vars), maplist(eigen,Vars). % defined +Atom % holds if there is a fact or a clause whose head predicate is % the same as the head predicate of Atom. defined(A) :- nth_clause(A,_,_) *-> true; format('No definition for ~w~n',A), false. % conj_list +Goal_conj -Goal_list % Convert a clause body (the conjunction) to a list of goals conj_list(G,Gs) :- G = (G1,G2) *-> Gs = [G1|Grest], conj_list(G2,Grest); Gs = [G]. % expand_def j([H|Hs],G,Vs) -Jexpanded % expands H against one clause of its definition; builds a new judgement. % The expansion may cause variables in Hs, G and even Vs to be % instantiated. expand_def(j([H|Hs],G,Vs), J) :- nth_clause(H,_,Ref), clause(H,B,Ref), (B = true *-> J = j(Hs,G,Vs); % No body term_variables(B,BVs), term_variables(H,HVs), once(diff_list_q(BVs,HVs,EVs)), conj_list(B,Bs), append(Bs,Hs,Hs1), append(EVs,Vs,Vs1), J = j(Hs1,G,Vs1)). % Apply the N-th clause in the definition of G to produce G1. apply_clause(N,G,B) :- nth_clause(G,N,Ref), clause(G,B,Ref). % make_implications +HS +G1 -G2 % converts Hs |- G1 to [] |- G2 % introducing implications. make_implications([],G,G). make_implications([H|Hs],G,(H->G1)) :- make_implications(Hs,G,G1). % contains +Term1 +Term2 % holds if Term2 is contained in Term1 contains(T1,T2) :- T1 == T2. contains(T1,_) :- var(T1), !, fail. contains([T1|_],T2) :- contains(T1,T2). contains([_|T1],T2) :- contains(T1,T2). contains(T1,T2) :- T1 =.. [_|Args], contains(Args,T2). % check_inductive +Atom % Given an atom, check to see it has a definition and the definition % is inductive. check_inductive(A) :- A =.. [Pred,VA], % must be an unary predicate var(VA), bagof((H,B), I^Ref^(nth_clause(A,I,Ref),clause(H,B,Ref)), Cs), maplist(check_inductive(Pred),Cs), !. check_inductive(A) :- format('Predicate ~w is not inductive~n',A), fail. check_inductive(_Pred,(_,true)). % no body check_inductive(Pred,(H,B)) :- B =.. [Pred,X], H =.. [_,HT], var(X), \+ var(HT), contains(HT,X). check_inductive(Pred,(H,(B1,B2))) :- check_inductive(Pred,(H,B1)), check_inductive(Pred,(H,B2)). % Assume that H and B are of the form pred(t) and pred(X) % (see the restriction on the inductive data type). % Unify t = X and return Gout that is the instance of G upon the % unification. subst(H,G,B,Gout) :- copy_term((H,G),(Hout,Gout)), Hout = B. % Generate an inductive hypothesis from a clause of an % inductive definition for H, and form a new judgement whose goal is G. induction_def(H,G,Vs,J) :- copy_term((H,G),(Hfresh,Gfresh)), nth_clause(H,_,Ref), clause(H,B,Ref), (B = true *-> J = j([],G,Vs); % No body, no hypothesis % subst(Hfresh,Gfresh) is a closure! % This is because maplist uses call internally. See the % variadic call: help(call). conj_list(B,Bs), maplist(subst(Hfresh,Gfresh),Bs,IGs), append(IGs,Bs,IHs), J = j(IHs,G,Vs)). %------------------------------------------------------------------------ % Interactive shell portray(j(Hs,G,Vs)) :- maplist(format('~w~n'),Hs), write('eigenvars: '), print(Vs), write('\n================\n'), print(G), write('\n\n'). interact([]) :- write('QED\n'). interact(Js) :- write('\n\nJudgements:\n'), maplist(print,Js), write('\nCommand >'), read(T), (T = end_of_file *-> true; process(T,Js,Jout), interact(Jout)). interact(Js) :- interact(Js). process(Verb,[J|Js],Jout) :- once(tactic(Verb,J,J1)), append(J1,Js,Jout). process(Verb,_,_) :- write('failed or unknown tactic: '), print(Verb), fail. main(G) :- interact([j([],G,[])]). % set_input % call_cleanup %======================================================================== % Tests and examples % Simple tests ex1 :- main(p(0)->p(0)). % intro. assumption. % testing eigen-variables and the intensional approach to proving % universally quantified formulas. ex2 :- main(forall(X,p(X)->p(X))). % intros. assumption. ex3 :- main(forall(X,p(X)->p(0))). % cannot be proven % After intros, we get stuck. ex4 :- main(exists(X,p(X)->p(0))). % intros. assumption. ex5 :- main(forall(X,exists(Y,p(Y) -> p(X)))). % intros. assumption. ex6 :- main(forall(X,exists(Y,p(X) -> p(Y)))). % intros. assumption. ex7 :- main(forall(X,eq(X,X))->forall(X,exists(Y,eq(X,Y)))). % intros. hintro. assumption. ex8 :- main(forall(X,eq(X,X))->forall(X,forall(Y,eq(X,Y)))). % intros. % but now assumption fails. % From Miller and Tiu's paper, end of Sec 1 ex9 :- main( forall(X,forall(Y,p(X,Y))) -> forall(Z,p(Z,Z)) ). % intros. hintro. hintro. assumption. ex9r :- main( forall(Z,p(Z,Z)) -> forall(X,forall(Y,p(X,Y))) ). % The converse is unprovable: we are stuck after % intros. hintro. exEE :- main( exists(X,p(X)) -> exists(Y,p(Y)) ). % intros. hintro. assumption. exEU :- main( exists(X,p(X)) -> forall(X,p(X)) ). % intros. hintro. % and then we get stuck on assumption. exUE :- main( forall(X,p(X)) -> exists(Y,p(Y)) ). % intros. hintro. assumption. exUU :- main( forall(X,p(X)) -> forall(X,p(X)) ). % intros. hintro. assumption. % Unrolling definitions. bool(true). bool(false). exb0 :- main( forall(X, p(X) -> (X=true; X=false)) ). % Cannot apply destruct because p/1 is not defined. exb1 :- main( forall(X, bool(X) -> (X=true; X=false)) ). % intros. destruct. simpl. simpl. % Use prove by contradiction: the assumption bool(xxx) is unsatisfiable exb2 :- main( bool(xxx) -> forall(X, bool(X) -> (X=true; X=false)) ). % intros. move. % brings bool(xxx) into focus % destruct. % gives the contradiction, and the proof. exb3 :- main( bool(true) -> forall(X, bool(X) -> X=true) ). % intros. move. % destruct. % eliminates bool(true). % destruct. % two judgements. % simpl. % proves first, with the goal true=true. % there remains another judgement, with the goal true=false % It is not provable. exi1 :- main( forall(X, nat(X) -> nat(s(X)) ) ). % intros. Then destruct applies, but makes bigger goals. % intros. constructor. assumption. works exi2 :- main( forall(X, nat_bad(X) -> nat_bad(s(X)) ) ). % intros. Then destruct applies, but leaves the judgement the same. exi3 :- main( forall(X, nat_bad1(X) -> nat_bad1(s(X)) ) ). % intros. Then destruct applies, but leaves the judgement the same. % Inductive proofs % From Pierce's lectures. plus(z,N,N). plus(s(N),M,s(R)) :- plus(N,M,R). % Zero is the right unit of plus exi_pz :- main( forall(N, nat(N) -> plus(N,z,N)) ). % intros. induction. simpl. % constructor. assumption. exi_pz1 :- main( forall(N, nat_bad(N) -> plus(N,z,N)) ). exi_pz2 :- main( forall(N, nat_bad1(N) -> plus(N,z,N)) ). % Addition is commutative exi_pcomm :- main( forall(N, nat(N) -> forall(M, nat(M) -> forall(R, nat(R) -> plus(N,M,R) -> plus(M,N,R)))) ). % evenb n = negb (evenb (S n)). % 3-star exercises beq_nat(z,z,true). beq_nat(z,s(_),false). beq_nat(s(_),z,false). beq_nat(s(N),s(M),R) :- beq_nat(N,M,R). ex_beqn1 :- main( forall(N, beq_nat(z,s(N),false)) ). % intros. simpl. ex_beqn2 :- main( forall(N, beq_nat(s(N),z,false)) ). % intros. simpl. ex_beqn3 :- main( forall(N, nat(N) -> exists(R, (plus(N,s(z),R), beq_nat(R,z,false)))) ). % intro. intro. intro. % leave the conjunction in the goal % induction. % simpl. % hintro. % inline the conjunction in assumption % intro. % make two subgoals for the conj in the goal % constructor. assumption. % prove first goal % simpl. % prove the rest ex_beqn4 :- main( forall(N, nat(N) -> exists(R, (plus(N,s(z),R), beq_nat(z,R,false)))) ). % the same script works here ex_beqn5 :- main( forall(N, nat(N) -> beq_nat(N,N,true)) ). % intros. induction. % simpl. % base case. % constructor. assumption. % inductive case % Binary tree, defined by a predicate btree(leaf(_)). btree(node(X,Y)) :- btree(X), btree(Y). mirror(leaf(X),leaf(X)). mirror(node(X,Y),node(Y1,X1)) :- mirror(X,X1), mirror(Y,Y1). %% define a sample tree btree1(node(node(leaf(0),leaf(1)),leaf(2))). % mirror the btree once and twice. Check that mirroring twice gives % back the original tree -- at least for the particular case of % btree1. ?- btree1(B), mirror(B,B1), mirror(B1,B). %% The query results in: %% B = node(node(leaf(0), leaf(1)), leaf(2)), %% B1 = node(leaf(2), node(leaf(1), leaf(0))). % The theorem: mirror is involutive thm(BT) :- mirror(BT,BT1), mirror(BT1,BT). prove_mirror :- main( forall(B, btree(B) -> thm(B)) ). % intros. % induction. % simpl. % destruct. move(3). destruct. % constructor. % intros. % constructor. % intros. % assumption. assumption. % constructor. intros. assumption. assumption.