% 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.