Skip to content

Instantly share code, notes, and snippets.

@jburse jburse/fixpoint3.p
Last active Aug 29, 2015

Embed
What would you like to do?
Proof verifyer based on holes, implicit, normalization and type checking. Connectives, Quantifiers and Higher Order.
/**
* Tarski Fixpoint Theorems. We show that a lfp and gfp are minimal
* resp. maximal lower resp. upper pre-fixpoints, independent of
* whether f is montone or not. Then if f is monotone we can also
* show that lfp and gfp are fixpoints itself.
*
* We use here the mini isabelle clone with holes and implicits.
* And we use a HOL sequent calculus. Solution is a compromise
* in some parts since our debruijn solver is still weak and
* there are no powerful tactics yet around.
*
* Copyright 2015, XLOG Technologies GmbH, Switzerland
* Jekejeke Prolog 1.0.5 (a fast and small prolog interpreter)
*/
:- use_module(implicit2).
:- use_module(seq_implicit2).
:- op(200, yf, set).
:- op(700, xfx, ⊆).
:- op(200, fy, ∪).
:- op(200, fy, ∩).
:- op(200, yf, map).
/***************************************************************************************/
/* Lattice definition. */
/***************************************************************************************/
:- fun (set) :: sort -> sort by
u set = (u=>prop).
:- fun ∪(u) :: u set set -> u set by
∪ a = {x\(∃ y\(y ∈ a & x ∈ y))}.
:- fun ∩(u) :: u set set -> u set by
∩ a = {x\(∀ y\(y ∈ a ==> x ∈ y))}.
:- fun ⊆(u) :: u set -> u set -> prop by
(a ⊆ b) = (∀ x\(x ∈ a ==> x ∈ b)).
:- fun =(u) :: u set -> u set -> prop by
(a = b) = (∀ x\(x ∈ a <=> x ∈ b)).
:- lemma lemma_1_1(u,b:u set,a) :: ∀ x\(x ∈ a ==> b ⊆ x) ==> b ⊆ ∩ a by
ruleR, ruleR, ruleR, ruleR, ruleR, ruleR, ruleL(x6,x3), ruleL(x8),
rule(x7), ruleL(x4,x9), ruleL(x10), rule(x5), rule(x11).
:- lemma lemma_1_2(u,b:u set,a) :: ∀ x\(x ∈ a ==> x ⊆ b) ==> ∪ a ⊆ b by
ruleR, ruleR, ruleR, ruleL(x5), ruleL(x6), ruleL(x8), ruleL(x7,x3),
ruleL(x11), rule(x9), ruleL(x4,x12), ruleL(x13), rule(x10), rule(x14).
:- lemma lemma_2(u,a:u set,b,c) :: a ⊆ b & b ⊆ c ==> a ⊆ c by
ruleR, ruleR, ruleR, ruleL(x4), ruleL(_,x7), rule(x5), ruleL(_,x8),
rule(x5), ruleL(x10), ruleL(x9), rule(x6), rule(x11), rule(x11).
:- lemma lemma_3(u,a:u set,b) :: a ⊆ b & b ⊆ a ==> a = b by
ruleR, ruleR, ruleR, ruleR, ruleR, ruleL(x3), ruleL(_,x6), rule(x4),
ruleL(x8), rule(x5), rule(x9), ruleR, ruleL(x3), ruleL(_,x7),
rule(x4), ruleL(x8), rule(x5), rule(x9).
:- lemma lemma_4_1(u,a:u set,b) :: a = b ==> a ⊆ b by
ruleR, ruleR, ruleR, ruleL(_,x3), rule(x4), ruleL(x6), ruleL(x7),
ruleL(x8), rule(x5), rule(x10).
:- lemma lemma_4_2(u,a:u set,b) :: a = b ==> b ⊆ a by
ruleR, ruleR, ruleR, ruleL(_,x3), rule(x4), ruleL(x6), ruleL(x7),
ruleL(x9), rule(x5), rule(x10).
/***************************************************************************************/
/* Minimality resp. Maximality of Lfp & Gfp */
/***************************************************************************************/
:- fun (map) :: u\(u set -> sort) by
(map) = u\(u set -> u set).
:- fun lfp(u) :: u map -> u set by
lfp(f) ={a\(f(a) ⊆ a)}.
:- fun gfp(u) :: u map -> u set by
gfp(f) ={a\(a ⊆ f(a))}.
:- lemma lemma_5_1(u,a:u set,f) :: f(a) ⊆ a ==> lfp(f) ⊆ a by
ruleR, ruleR, ruleR, ruleL(x5), ruleL(a,x6), ruleL(x7),
ruleR, rule(x3), rule(x8).
:- lemma lemma_5_2(u,a:u set,f) :: a ⊆ f(a) ==> a ⊆ gfp(f) by
ruleR, ruleR, ruleR, ruleR, ruleR(a), ruleR, ruleR,
rule(x3), rule(x5).
:- theorem min_lfp(u,a:u set,f) :: f(a) = a ==> lfp(f) ⊆ a by
ruleR, ruleL(lemma_4_1), rule(x3), ruleL(of(lemma_5_1,_,a,f)),
rule(x4), rule(x5).
:- theorem max_gfp(u,a:u set,f) :: f(a) = a ==> a ⊆ gfp(f) by
ruleR, ruleL(lemma_4_2), rule(x3), ruleL(of(lemma_5_2,_,a,f)),
rule(x4), rule(x5).
/***************************************************************************************/
/* Fixpointness of Lfp & Gfp */
/***************************************************************************************/
:- fun mono(u) :: u map -> prop by
mono(f) = (∀ x\(∀ y\(x ⊆ y ==> f(x) ⊆ f(y)))).
:- lemma lemma_6_1(u,f:u map) :: mono(f) ==> f(lfp(f)) ⊆ lfp(f) by
ruleR, ruleL(of(lemma_1_1,_,f(lfp(f)), {a\(f(a) ⊆ a)})),
prefer(2), rule(x3), ruleR, ruleR, ruleR,
ruleL(x4), ruleL(x5,x6), ruleL(of(lemma_5_1,_,x3,f)), rule(x6), ruleL(lfp(f),x2),
ruleL(x3,x9), ruleL(x10), rule(x8), ruleR, ruleL(x5,x11),
ruleL(x13), rule(x12), ruleL(x7), rule(x14), rule(x15).
:- lemma lemma_6_2(u,f:u map) :: mono(f) ==> gfp(f) ⊆ f(gfp(f)) by
ruleR, ruleL(of(lemma_1_2,_,f(gfp(f)), {a\(a ⊆ f(a))})),
prefer(2), rule(x3), ruleR, ruleR, ruleR,
ruleL(x4), ruleL(x5,x6), ruleL(of(lemma_5_2,_,x3,f)), rule(x6), ruleL(x3,x2),
ruleL(gfp(f),x9), ruleL(x10), rule(x8), ruleR, ruleL(x5,x11),
ruleL(x13), ruleL(x7), rule(x12), rule(x14), rule(x14).
:- lemma lemma_7_1(u,f:u map) :: mono(f) ==> lfp(f) ⊆ f(lfp(f)) by
ruleR, ruleL(of(lemma_5_1,_,f(lfp(f)),f)), prefer(2),
rule(x3), ruleL(f(lfp(f)),x2), ruleL(lfp(f),x3), ruleL(x4), prefer(2),
rule(x5), ruleL(of(lemma_6_1,_,f)), prefer(2), rule(x5), rule(x2).
:- lemma lemma_7_2(u,f:u map) :: mono(f) ==> f(gfp(f)) ⊆ gfp(f) by
ruleR, ruleL(of(lemma_5_2,_,f(gfp(f)),f)), prefer(2),
rule(x3), ruleL(gfp(f),x2), ruleL(f(gfp(f)),x3), ruleL(x4), prefer(2),
rule(x5), ruleL(of(lemma_6_2,_,f)), prefer(2), rule(x5), rule(x2).
:- theorem fp_lfp(u,f:u map) :: mono(f) ==> f(lfp(f)) = lfp(f) by
ruleR, ruleR, ruleR, ruleR, ruleL(of(lemma_6_1,_,f)), rule(x2),
ruleL(x3,x4), rule(x5), ruleL(of(lemma_7_1,_,f)),
rule(x2), ruleL(x3,x4), rule(x5).
:- theorem fp_gfp(u,f:u map) :: mono(f) ==> f(gfp(f)) = gfp(f) by
ruleR, ruleR, ruleR, ruleR, ruleL(of(lemma_7_2,_,f)), rule(x2),
ruleL(x3,x4), rule(x5), ruleL(of(lemma_6_2,_,f)),
rule(x2), ruleL(x3,x4), rule(x5).
/**
* Prolog code for some constraint solving helpers.
*
* Copyright 2015, XLOG Technologies GmbH, Switzerland
* Jekejeke Prolog 1.0.5 (a fast and small prolog interpreter)
*/
:- module(helper, []).
:- use_module(library(minimal/assume)).
:- use_module(library(minimal/hypo)).
:- use_module(library(minimal/delta)).
:- use_module(library(system/trail)).
:- use_module(library(advanced/sets)).
/*******************************************************/
/* Subject to Occurs Check Hook */
/*******************************************************/
% sto_hook(+Var, +Term)
sto_hook(V, T) :-
term_variables(T, L),
(contains(V, L) -> fail; sto_list(L)).
% sto_list(+List)
sto_list([X|Y]) :-
sys_ensure_attr(X),
sys_ensure_hook(X, sto_hook),
sto_list(Y).
sto_list([]).
/*******************************************************/
/* General wakeup hook. */
/*******************************************************/
% sys_guard(+Var, +Term)
sys_guard(V, W) :- var(W), !,
sys_freeze_var(V, R),
sys_freeze_var(W, S),
<= +sys_wakeup(R, S).
sys_guard(V, T) :-
sys_freeze_var(V, R),
sys_freeze_var(W, S),
W = T,
<= +sys_wakeup(R, S).
% sys_wakeup(+Warp, +Wrap)
:- thread_local sys_wakeup/2.
:- forward sys_wakeup/3.
:- multifile sys_wakeup/3.
unit <=
=sys_wakeup(_, _).
/*******************************************************/
/* Some post extensions. */
/*******************************************************/
% minimal/hypo:post_impl(+Event)
:- multifile minimal/hypo:post_impl/1.
:- static minimal/hypo:post_impl/1.
:- discontiguous minimal/hypo:post_impl/1.
minimal/hypo:post_impl(sys_redo_eq(X, Y)) :- !,
sys_melt_var(X, U),
sys_melt_var(Y, T),
U = T.
minimal/hypo:post_impl(sys_fresh_var(A)) :- !,
sys_freeze_var(_, A).
% sys_melt_equal(+Ref, +Ref)
sys_melt_equal(X, Y) :-
sys_melt_var(X, A),
sys_melt_var(Y, B),
A == B.
/*******************************************************/
/* Custom constraint display. */
/*******************************************************/
/**
* cust_show_vars:
* Will show all constraints.
*/
% cust_show_vars
:- public cust_show_vars/0.
cust_show_vars :-
findall(E, cust_current_eq(E), L),
cust_unwrap_eq_list(L, H),
sys_filter_eq_trivial(H, R),
sys_show_eq_list(R).
% cust_unwrap_eq_list(+List, -List)
:- private cust_unwrap_eq_list/2.
cust_unwrap_eq_list([F|G], [X|Y]) :-
cust_unwrap_eq(F, X),
cust_unwrap_eq_list(G, Y).
cust_unwrap_eq_list([], []).
/**
* cust_current_eq(E):
* The predicate succeeds for each current equation handle that unifies with E.
*/
% cust_current_eq(-Handle)
:- public cust_current_eq/1.
:- multifile cust_current_eq/1.
:- meta_predicate cust_current_eq(0).
cust_current_eq(X = U) :-
sys_get_variable_names(V),
sys_member(X = Y, V),
sys_wrap_term(Y, U).
/**
* cust_unwrap_eq(E, F):
* The predicate unwraps the equation handle E into the term F.
*/
% cust_unwrap_eq(+Goal, -Goal)
:- public cust_unwrap_eq/2.
:- multifile cust_unwrap_eq/2.
:- meta_predicate cust_unwrap_eq(0, 0).
cust_unwrap_eq(X = U, X = T) :-
sys_unwrap_term(U, T).
/**
* Prolog code for debruijn indexes with holes and implicits.
* Using debruijn indexes here assures automatic alpha conversion.
* Holes allow the end-user to leave terms unspecified. Implicits
* automatize argument holes.
*
* We call nominal terms those lambda expressions that use
* ordinary variable names. We call indexed terms those lambda
* expressions that use debruijn indexes. In our iconic logic
* framework there is no distinction between abstraction terms
* and product types. Therefore the data structures are as
* follows:
*
* Nominal Term:
* c : A defined constant.
* n : A nominal variable.
* app(s,t) : An application term.
* n:s\t : An abstraction term.
*
* Indexed Term:
* c : A defined constant.
* i : A debruijn index.
* app(s,t) : An application term.
* lam(s,t) : An abstraction term.
*
* To help the end-user input/output of nominal terms, there is
* an extended syntax of nominal terms. This data structure has the
* following additional elements:
*
* Extended Nominal Term:
* s->t : An implication term, short hand for n:s\t
* where n does not occur in t.
* n\t : An abstraction term with a hole,
* short hand for n:_\t.
* f(t1,..,tn) : A compound term with implicit,
* short hand for
* app(..app(app(f..,_),t1)..,tn)
* of(f,t1,..,tn) : An implicit escape,
* short hand for
* app( app(app(f,t1)..,tn)..,_).
* g(s,t) : An implication like term,
* short hand for h(s,s->t).
*
* The following commands are supported:
* axiom C(X1:T1,..,Xn:Tn) :: A
* type T
* lemma C(X1:T1,..,Xn:Tn) :: A by W
* theorem C(X1:T1,..,Xn:Tn) :: A by W
* fun C(X1:T1,..,Xn:Tn) :: A by W
* show C
* value T
*
* The following proof steps are supported:
* C(X1:T1,..,Xn:Tn) = A
* rule(A)
* prefer(N)
*
* Copyright 2011-2015, XLOG Technologies GmbH, Switzerland
* Jekejeke Prolog 1.0.7 (a fast and small prolog interpreter)
*/
:- use_module(library(basic/lists)).
:- use_module(library(minimal/assume)).
:- use_module(library(minimal/hypo)).
:- use_module(library(minimal/delta)).
:- use_module(library(system/trail)).
:- use_module(helper).
:- op(650, xfy, \).
:- set_oper_property(infix(\), nspl).
:- set_oper_property(infix(\), nspr).
:- op(1150, fx, axiom).
:- op(1150, fx, type).
:- op(1150, fx, lemma).
:- op(1150, fx, theorem).
:- op(1125, xfx, by).
:- op(1100, xfx, ::).
:- op(1150, fx, fun).
:- op(1150, fx, show).
:- op(1150, fx, value).
:- meta_predicate \(0,0,?).
:- meta_predicate ::(0,0).
:- meta_predicate \(0,0).
/***************************************************************************************/
/* Convert an extended nominal term to an indexed term. */
/***************************************************************************************/
% like(+ProductAtom, -ImplicationAtom)
:- multifile like/2.
:- static like/2.
/**
* typ(C, P, N):
* Stores the type P in normal form for the constant C.
* N gives the number of implicit arguments.
*/
% typ(+Atom, -Indexed, -Integer)
:- dynamic typ/3.
/**
* def(C, T, N):
* Stores the term T for the constant C. The term T need
* not be in normal form.
* N gives the number of implicit arguments.
*/
% def(+Atom, -Indexed, -Integer)
:- dynamic def/3.
% sys_convert(+Ref, +Ref, +Ref)
:- thread_local sys_convert/3.
:- forward sys_convert/4.
sys_redo_eq(Z, V) <=
=sys_convert(X, Y, Z), sys_convert(X, U, V), sys_melt_equal(Y, U), !.
sys_redo_eq(Z, V) <=
=sys_convert(Z, Y, X), sys_convert(V, U, X), sys_melt_equal(Y, U), !.
% helper:cust_current_eq(-Goal)
:- multifile helper:cust_current_eq/1.
helper:cust_current_eq(convert(X, Y, Z)) :-
sys_convert(X, Y, Z).
% helper:cust_unwrap_eq(+Goal, -Goal)
:- multifile helper:cust_unwrap_eq/2.
:- discontiguous helper:cust_unwrap_eq/2.
helper:cust_unwrap_eq(convert(X, Y, Z), convert(U, V, W)) :-
sys_melt_var(X, U),
sys_melt_var(Y, V),
sys_melt_var(Z, W).
% convert(+Nominal, +Context, -Indexed)
convert(V, C, W) :-
var(V), var(W), !,
sys_ensure_attr(V),
sys_ensure_hook(V, sys_guard),
sys_freeze_var(V, P),
sys_ensure_attr(W),
sys_ensure_hook(W, sys_guard),
sys_freeze_var(W, Q),
sys_freeze_var(A, T),
A = C,
<= +sys_convert(P, T, Q).
convert(V, C, W) :-
var(V), !,
reconst(W, C, V).
convert((V:F\G), C, W) :- var(V), !,
length(C, N),
makesym(N, V),
convert(F, C, X),
convert(G, [V|C], Y),
W = lam(X,Y).
convert((V:F\G), C, W) :- !,
convert(F, C, X),
convert(G, [V|C], Y),
W = lam(X,Y).
convert(app(U,V), C, W) :- !,
convert(U, C, X),
convert(V, C, Y),
W = app(X,Y).
convert((F->G), C, W) :- !,
convert((_:F\G), C, W).
convert((V\G), C, W) :- !,
convert((V:_\G), C, W).
convert(F, C, W) :-
F =.. [of,V|L],
typ(V, _, N),
length(L, M),
M =< N, !,
convert_list(L, cst(V), C, H),
K is N-M,
wildcard(K, H, C, W).
convert(F, C, W) :-
F =.. [of,V|L],
def(V, _, N),
length(L, M),
M =< N, !,
convert_list(L, cst(V), C, H),
K is N-M,
wildcard(K, H, C, W).
convert(U, C, R) :- U =.. [G,S,T], like(H, G), !,
W =.. [H,S,(S->T)],
convert(W, C, R).
convert(H, C, R) :- H =.. [V,S|L], !,
convert(V, C, X),
convert_list([S|L], X, C, R).
convert(V, C, W) :-
nth0(I, C, V), !,
W = idx(I).
convert(V, C, W) :-
typ(V, _, N), !,
wildcard(N, cst(V), C, W).
convert(V, C, W) :-
def(V, _, N), !,
wildcard(N, cst(V), C, W).
convert(V, _, _) :-
sys_throw_error(syntax_error(undef_var,V)).
% convert_list(+ListExtendedNominal, +Indexed, +Context, -Indexed)
convert_list([S|L], V, C, R) :-
convert(S, C, U),
convert_list(L, app(V,U), C, R).
convert_list([], V, _, V).
% wildcard(+Nat, +Atomic, +Context, -Indexed)
wildcard(0, V, _, W) :- !,
W = V.
wildcard(N, V, C, W) :-
convert(_, C, U),
M is N-1,
wildcard(M, V, C, X),
W = app(X,U).
% minimal/hypo:post_impl(+Event)
:- multifile minimal/hypo:post_impl/1.
:- discontiguous minimal/hypo:post_impl/1.
minimal/hypo:post_impl(sys_redo_convert(X, Y, Z)) :- !,
sys_melt_var(X, U),
sys_melt_var(Y, V),
sys_melt_var(Z, W),
convert(U, V, W).
% sys_wakeup(+Warp, +Wrap)
:- multifile helper:sys_wakeup/3.
:- discontiguous helper:sys_wakeup/3.
sys_redo_convert(T, Y, Z) <=
+(helper:sys_wakeup(X, T)), -sys_convert(X, Y, Z).
sys_redo_convert(X, Y, T) <=
+(helper:sys_wakeup(Z, T)), -sys_convert(X, Y, Z), X \== Z.
% makesym(+Nat, -Atom)
makesym(N, S) :-
number_codes(N, L),
atom_codes(S, [120|L]).
/***************************************************************************************/
/* Convert an indexed term to a nominal term. */
/***************************************************************************************/
% reconst(+Indexed, +Nat, -Nominal)
reconst(V, C, W) :- var(V), var(W), !,
sys_ensure_attr(V),
sys_ensure_hook(V, sys_guard),
sys_freeze_var(V, P),
sys_ensure_attr(W),
sys_ensure_hook(W, sys_guard),
sys_freeze_var(W, Q),
sys_freeze_var(A, T),
A = C,
<= +sys_convert(Q, T, P).
reconst(V, C, W) :- var(V), !,
convert(W, C, V).
reconst(app(F,G), C, W) :-
reconst(F, C, X),
reconst(G, C, Y),
W = app(X,Y).
reconst(lam(F,G), C, W) :-
reconst(F, C, X),
length(C, N),
makesym(N, U),
reconst(G, [U|C], Y),
W = (U:X\Y).
reconst(idx(I), C, W) :-
nth0(I, C, V), !,
W = V.
reconst(cst(C), _, W) :-
W = C.
/***************************************************************************************/
/* Convert a nominal term to an extended nominal term. */
/***************************************************************************************/
% pretty(+Nominal, -ExtendedNominal)
pretty(V, V) :- var(V), !.
pretty(app(A,B), W) :- nonvar(A), nonvar(B),
A = app(H,P), B = (N:S\T),
P == S, like(H, G), \+ varof(N, T), !,
pretty(app(app(G,S),T), W).
pretty(app(S,T), R) :- pretty_list(S, [V], L), !,
pretty(T, V),
unimplicit(L, M),
R =.. M.
pretty(app(S,T), app(U,V)) :- !,
pretty(S, U),
pretty(T, V).
pretty((N:S\T), (U->V)) :- \+ varof(N, T), !,
pretty(S, U),
pretty(T, V).
pretty((N:S\T), (N:U\V)) :- !,
pretty(S, U),
pretty(T, V).
pretty(F, F) :- atom(F).
% pretty_list(+Nominal, -ListExtendedNominal, -ListExtendedNominal)
pretty_list(V, _, _) :- var(V), !, fail.
pretty_list(app(S,T), I, O) :- pretty_list(S, [V|I], O), pretty(T, V).
pretty_list(F, I, [F|I]) :- atom(F).
% varof(+Atom, +Nominal)
varof(_, V) :- var(V), !.
varof(N, app(S,_)) :- varof(N, S).
varof(N, app(_,T)) :- varof(N, T).
varof(N, (_:S\_)) :- varof(N, S).
varof(N, (M:_\T)) :- M \== N, varof(N, T).
varof(N, M) :- M == N.
% unimplicit(+ListNominal, -ListNominal)
unimplicit([C|L], [C|R]) :-
typ(C, _, N), !,
unwildcard(N, L, R).
unimplicit([C|L], [C|R]) :-
def(C, _, N), !,
unwildcard(N, L, R).
unimplicit(L, L).
% unwildcard(+Nat, +ListNominal, -ListNominal)
unwildcard(0, L, L) :- !.
unwildcard(M, [_|L], R) :-
N is M-1,
unwildcard(N, L, R).
/***************************************************************************************/
/* Constraint on shifted variable pairs. */
/* Since there is a 1-1 relationship we wakeup on both variables. */
/***************************************************************************************/
% sys_shift(+Ref, +Nat, +Nat, +Ref)
:- thread_local sys_shift/4.
:- forward sys_shift/5.
sys_redo_eq(X, Y) <=
=sys_shift(X, _, 0, Y), !.
sys_redo_eq(Y, Z) <=
=sys_shift(X, I, J, Y), sys_shift(X, I, J, Z), !.
sys_redo_eq(X, Z) <=
=sys_shift(X, I, J, Y), sys_shift(Z, I, J, Y), !.
% helper:cust_current_eq(-Goal)
:- multifile helper:cust_current_eq/1.
:- discontiguous helper:cust_current_eq/1.
helper:cust_current_eq(shift(X, I, J, Y)) :-
sys_shift(X, I, J, Y).
% helper:cust_unwrap_eq(+Goal, -Goal)
helper:cust_unwrap_eq(shift(X, I, J, Y), shift(U, I, J, T)) :-
sys_melt_var(X, U),
sys_melt_var(Y, T).
% shift(+Indexed, +Nat, +Nat, -Indexed)
shift(V, I, J, W) :- var(V), var(W), !,
sys_ensure_attr(V),
sys_ensure_hook(V, sys_guard),
sys_freeze_var(V, U),
sys_ensure_attr(W),
sys_ensure_hook(W, sys_guard),
sys_freeze_var(W, T),
<= +sys_shift(U, I, J, T).
shift(V, I, J, T) :- var(V), !,
unshift(T, I, J, V).
shift(app(F,G), I, J, W) :- !,
shift(F, I, J, X),
shift(G, I, J, Y),
W = app(X,Y).
shift(lam(F,G), I, J, W) :- !,
shift(F, I, J, X),
K is I+1,
shift(G, K, J, Y),
W = lam(X,Y).
shift(idx(I), J, L, W) :- I >= J, !, K is I+L, W = idx(K).
shift(idx(I), _, _, idx(I)).
shift(cst(C), _, _, cst(C)).
% unshift(+Indexed, +Nat, +Nat, -Indexed)
unshift(W, I, J, V) :- var(V), var(W), !,
sys_ensure_attr(V),
sys_ensure_hook(V, sys_guard),
sys_freeze_var(V, U),
sys_ensure_attr(W),
sys_ensure_hook(W, sys_guard),
sys_freeze_var(W, T),
<= +sys_shift(U, I, J, T).
unshift(T, I, J, V) :- var(T), !,
shift(V, I, J, T).
unshift(app(F,G), I, J, W) :- !,
unshift(F, I, J, X),
unshift(G, I, J, Y),
W = app(X,Y).
unshift(lam(F,G), I, J, W) :- !,
unshift(F, I, J, X),
K is I+1,
unshift(G, K, J, Y),
W = lam(X,Y).
unshift(idx(I), J, L, W) :- I-L >= J, !, K is I-L, W = idx(K).
unshift(idx(I), J, _, idx(I)) :- I < J.
unshift(cst(C), _, _, cst(C)).
% minimal/hypo:post_impl(+Event)
minimal/hypo:post_impl(sys_redo_shift(X, I, J, Y)) :- !,
sys_melt_var(X, U),
sys_melt_var(Y, T),
shift(U, I, J, T).
sys_redo_shift(V, I, J, T) <=
+(helper:sys_wakeup(U, V)), -sys_shift(U, I, J, T).
sys_redo_shift(U, I, J, V) <=
+(helper:sys_wakeup(T, V)), -sys_shift(U, I, J, T), U \== T.
/***************************************************************************************/
/* Constraint on substituted variable pairs. */
/***************************************************************************************/
% sys_subst(+Ref, +Nat, +Ref, +Ref)
:- thread_local sys_subst/4.
:- forward sys_subst/5.
+sys_shift(U, I, L, Z) <=
=sys_subst(X, K, _, Z), sys_shift(U, I, J, X), I =< K, K < I+J, !, L is J-1.
+sys_shift(U, I, L, Z) <=
+sys_shift(U, I, J, X), -sys_subst(X, K, _, Z), I =< K, K < I+J, L is J-1.
% helper:cust_current_eq(-Goal)
:- multifile helper:cust_current_eq/1.
:- discontiguous helper:cust_current_eq/1.
helper:cust_current_eq(subst(X, I, Y, Z)) :-
sys_subst(X, I, Y, Z).
% helper:cust_unwrap_eq(+Goal, -Goal)
helper:cust_unwrap_eq(subst(X, I, Y, Z), subst(U, I, T, S)) :-
sys_melt_var(X, U),
sys_melt_var(Y, T),
sys_melt_var(Z, S).
% subst(+Indexed, +Nat, +Indexed, -Indexed)
subst(V, I, W, X) :- var(V), var(X), !,
sys_ensure_attr(V),
sys_ensure_hook(V, sys_guard),
sys_freeze_var(V, U),
sys_freeze_var(A, T),
A = W,
sys_ensure_attr(X),
sys_ensure_hook(X, sys_guard),
sys_freeze_var(X, S),
<= +sys_subst(U, I, T, S).
subst(V, I, W, X) :- var(V), !,
sys_ensure_attr(V),
sys_ensure_hook(V, sys_guard),
sys_freeze_var(V, U),
sys_freeze_var(A, T),
A = W,
sys_freeze_var(B, S),
B = X,
<= +sys_subst(U, I, T, S).
subst(app(F,G), I, T, Z) :-
subst(F, I, T, X),
subst(G, I, T, Y),
reduce(X, Y, Z).
subst(lam(F,G), I, T, W) :-
subst(F, I, T, X),
J is I+1,
subst(G, J, T, Y),
W = lam(X,Y).
subst(idx(I), I, T, S) :- !, shift(T, 0, I, S).
subst(idx(I), J, _, W) :- I > J, !, K is I-1, W = idx(K).
subst(idx(I), _, _, idx(I)).
subst(cst(C), _, _, cst(C)).
% minimal/hypo:post_impl(+Event)
minimal/hypo:post_impl(sys_redo_subst(X, I, Y, Z)) :- !,
sys_melt_var(X, U),
sys_melt_var(Y, T),
sys_melt_var(Z, S),
subst(U, I, T, S).
sys_redo_subst(V, I, T, S) <=
+(helper:sys_wakeup(U, V)), -sys_subst(U, I, T, S).
sys_redo_subst(U, I, T, V) <=
+(helper:sys_wakeup(S, V)), -sys_subst(U, I, T, S), U \== S.
/***************************************************************************************/
/* Constraint on type checked variables. */
/***************************************************************************************/
% sys_typeof(+Ref, +Ref, +Ref)
:- thread_local sys_typeof/3.
:- forward sys_typeof/4.
% C=D --> typeof(X,C) = typeof(X,D).
sys_redo_eq(P, Q) <=
=sys_typeof(X, C, P), sys_typeof(X, D, Q), sys_melt_equal(C, D), !.
% helper:cust_current_eq(-Goal)
:- multifile helper:cust_current_eq/1.
:- discontiguous helper:cust_current_eq/1.
helper:cust_current_eq(typeof(X, Y, Z)) :-
sys_typeof(X, Y, Z).
% helper:cust_unwrap_eq(+Goal, -Goal)
helper:cust_unwrap_eq(typeof(X, Y, Z), typeof(U, V, W)) :-
sys_melt_var(X, U),
sys_melt_var(Y, V),
sys_melt_var(Z, W).
/**
* typeof(T, C, P):
* Computes the type P in normal form of the term T
* in the normal form context C. The term T itself need
* not be in normal form.
*/
% typeof(+Indexed, +Context, -Indexed)
typeof(V, W, X) :- var(V), !,
sys_ensure_attr(V),
sys_ensure_hook(V, sys_guard),
sys_freeze_var(V, U),
sys_freeze_var(A, T),
A = W,
sys_freeze_var(B, S),
B = X,
<= +sys_typeof(U, T, S).
typeof(app(F,G), C, D) :-
typeof(F, C, H),
H = lam(A,B),
valueof(G, C, Y, K),
K = A,
subst(B, 0, Y, D).
typeof(lam(F,G), C, W) :-
valueof(F, C, X, _),
typeof(G, [X|C], B),
W = lam(X,B).
typeof(idx(I), C, B) :-
nth0(I, C, A), !,
J is I+1,
shift(A, 0, J, B).
typeof(cst(V), _, W) :-
typ(V, X, _), !,
W = X.
typeof(cst(V), C, X) :-
def(V, F, _),
typeof(F, C, X).
% minimal/hypo:post_impl(+Event)
minimal/hypo:post_impl(sys_redo_typeof(X, Y, Z)) :- !,
sys_melt_var(X, U),
sys_melt_var(Y, V),
sys_melt_var(Z, W),
typeof(U, V, W).
sys_redo_typeof(V, T, S) <=
+(helper:sys_wakeup(U, V)), -sys_typeof(U, T, S).
/***************************************************************************************/
/* Constraint on normalized variables. */
/***************************************************************************************/
% sys_reduce(+Ref, +Ref, +ßRef)
:- thread_local sys_reduce/3.
:- forward sys_reduce/4.
sys_fresh_var(A) /\ sys_redo_subst(Z, I, J, A) /\
sys_fresh_var(B) /\ sys_redo_subst(T, I, J, B) /\
sys_redo_reduce(A, B, Y) <=
=sys_subst(X, I, J, Y), sys_reduce(Z, T, X), !.
sys_fresh_var(A) /\ sys_redo_subst(Z, I, J, A) /\
sys_fresh_var(B) /\ sys_redo_subst(T, I, J, B) /\
sys_redo_reduce(A, B, Y) <=
+sys_reduce(Z, T, X), -sys_subst(X, I, J, Y).
% helper:cust_current_eq(-Goal)
:- multifile helper:cust_current_eq/1.
:- discontiguous helper:cust_current_eq/1.
helper:cust_current_eq(reduce(X, Y, T)) :-
sys_reduce(X, Y, T).
% helper:cust_unwrap_eq(+Goal, -Goal)
helper:cust_unwrap_eq(reduce(X, Y, T), reduce(S, U, W)) :-
sys_melt_var(X, S),
sys_melt_var(Y, U),
sys_melt_var(T, W).
/**
* valueof(T, C, N, P):
* Computes the type P in normal form and the normal form N
* of the term T in the normal form context C. The term T
* itself need not be in normal form.
*/
% valueof(+Indexed, +Context, -Indexed, -Indexed)
valueof(V, W, K, X) :- var(V), !,
V = K,
sys_ensure_attr(V),
sys_ensure_hook(V, sys_guard),
sys_freeze_var(V, U),
sys_freeze_var(A, T),
A = W,
sys_freeze_var(B, S),
B = X,
<= +sys_typeof(U, T, S).
valueof(app(F,G), C, Z, X) :-
valueof(F, C, N, H),
H = lam(A,B),
valueof(G, C, Y, K),
K = A,
subst(B, 0, Y, X),
reduce(N, Y, Z).
valueof(lam(F,G), C, V, W) :-
valueof(F, C, X, _),
valueof(G, [X|C], N, B),
V = lam(X,N),
W = lam(X,B).
valueof(idx(I), C, V, B) :-
nth0(I, C, A), !,
J is I+1,
shift(A, 0, J, B),
V = idx(I).
valueof(cst(V), _, U, W) :-
typ(V, X, _), !,
U = cst(V),
W = X.
valueof(cst(V), C, Z, X) :-
def(V, F, _),
valueof(F, C, Z, X).
% reduce(+Indexed, +Indexed, -Indexed)
reduce(X, Y, T) :- var(X), var(T), !,
sys_ensure_attr(X),
sys_ensure_hook(X, sys_guard),
sys_freeze_var(X, S),
sys_freeze_var(A, U),
A = Y,
sys_ensure_attr(T),
sys_ensure_hook(T, sys_guard),
sys_freeze_var(T, W),
<= +sys_reduce(S, U, W).
reduce(X, Y, T) :- var(X), !,
sys_ensure_attr(X),
sys_ensure_hook(X, sys_guard),
sys_freeze_var(X, S),
sys_freeze_var(A, U),
A = Y,
sys_freeze_var(C, W),
C = T,
<= +sys_reduce(S, U, W).
reduce(lam(_,B), J, X) :- !,
subst(B, 0, J, X).
reduce(X, Y, app(X,Y)).
% minimal/hypo:post_impl(+Event)
minimal/hypo:post_impl(sys_redo_reduce(X, Y, T)) :- !,
sys_melt_var(X, S),
sys_melt_var(Y, U),
sys_melt_var(T, W),
reduce(S, U, W).
sys_redo_reduce(T, U, W) <=
+(helper:sys_wakeup(S, T)), -sys_reduce(S, U, W).
sys_redo_reduce(S, U, T) <=
+(helper:sys_wakeup(W, T)), -sys_reduce(S, U, W), S \== W.
/***************************************************************************************/
/* Term builder commands. */
/***************************************************************************************/
/**
* rule(N):
* Extendes the first open hole in the current incomplete
* proof by the nominal term N.
*/
% rule(+Nominal, +List, -List)
rule(X, [X|L], R) :-
term_variables([X|L], R).
/**
* C(X1:T1,..,Xn:Tn) = A:
* Extendes the first open hole in the current incomplete
* proof by the nominal term X1:T1\..\Xn:Tn\A.
* A type annotations :Ti is optional when it can be infered.
*/
% =(+Compound, +Nominal, +List, -List)
=(U, A, [X|S], R) :-
U =.. [_|L],
quant(L, A, X),
term_variables([X|S], R).
/**
* prefer(I):
* Moves the I-th open hole in the current incomplete proof
* to the front.
*/
% prefer(+Nat, +List, -List)
prefer(N, S, [X|R]) :-
nth1(N, S, X, R).
/**
* size(N):
* Retrieve the number of open holes in the current incomplete
* proof.
*/
size(N, L, L) :-
length(L, N).
/**
* pick(V):
* Enumerates the variables identifiying the premisses in the
* first open hold in the current incomplete proof.
*/
% pick(-Nominal, +List, -List)
pick(Y, [X|L], [X|L]) :-
sys_freeze_var(X, K),
sys_convert(K, A, _),
sys_melt_var(A, H),
member(Y, H).
% write_var(+Term)
write_var(X) :-
sys_get_variable_names(V),
write_term(X, [quoted(true),context(0),variable_names(V),format(newline),ignore_mod(true)]).
% quant(+List, +Nominal, -Nominal)
quant([V|L], A, V\B) :-
quant(L, A, B).
quant([], A, A).
/***************************************************************************************/
/* Problem diagnositics I */
/***************************************************************************************/
% pretty(+ListIndexed, +Indexed, +ListAtom, -Nominal, +Nat)
pretty(L, X, R, (Y::H), S) :-
reconst(X, R, E),
pretty(E, H),
extend(L, R, true, Y, S).
% extend(+ListIndexed, +ListAtom, +Nominal, -Nominal, +Nat)
extend([F|L], [U|R], Y, B, S) :-
length([F|L], T), T > S, !,
reconst(F, R, E),
pretty(E, X),
makeand(U:X, Y, Z),
extend(L, R, Z, B, S).
extend(_, _, Y, Y, _).
% makeand(+Nominal, +Nominal, -Nominal)
makeand(X, true, X) :- !.
makeand(X, Y, (X,Y)).
% write_goal_vars(+List, +Nat, +Atom, +Nat)
write_goal_vars([X|Y], N, G, S) :-
M is N+1,
sys_freeze_var(X, K),
sys_convert(K, A, J),
sys_typeof(J, B, C), !,
sys_melt_var(A, R),
sys_melt_var(B, L),
sys_melt_var(C, T),
pretty(L, T, R, P, S),
write('-- '), write(G), write(' '), write(M), write(' --'), nl,
write_var(P), nl,
write_goal_vars(Y, M, G, S).
write_goal_vars([_|Y], N, G, S) :-
M is N+1,
write('-- '), write(G), write(' '), write(M), write( '--'), nl,
write('-- Problem --'), nl,
write_goal_vars(Y, M, G, S).
write_goal_vars([], _, _, _).
/***************************************************************************************/
/* Problem diagnositics. */
/***************************************************************************************/
% show_rest(+List, +Nat)
show_rest(C, S) :-
write_goal_vars(C, 0, 'Goal', S),
sys_freeze_list(C, D),
findall(X, (sys_convert(X, _, Y), sys_typeof(Y, _, _), \+ member(X, D)), L),
sys_melt_list(L, R),
length(C, N),
write_goal_vars(R, N, 'Rest', S).
% sys_melt_list(+List, -List)
sys_melt_list([F|G], [X|Y]) :-
sys_melt_var(F, X),
sys_melt_list(G, Y).
sys_melt_list([], []).
% sys_freeze_list(+List, -List)
sys_freeze_list([F|G], [X|Y]) :-
sys_freeze_var(F, X),
sys_freeze_list(G, Y).
sys_freeze_list([], []).
/***************************************************************************************/
/* Type check commands language. */
/***************************************************************************************/
:- assertz(typ(sort, cst(kind), 0)).
/**
* axiom C(X1:T1,..,Xn:Tn) :: A
* Adds a new constant C and its type X1:T1\..\Xn:Tn\A.
* This might change the logic.
* A type annotations :Ti is optional when it can be infered.
*/
% axiom +Compound :: +Nominal
axiom U :: _ :-
U =.. [C|_],
typ(C, _, _), sys_throw_error(permission_error(already_defined,C)).
axiom U :: _ :-
U =.. [C|_],
def(C, _, _), sys_throw_error(permission_error(already_defined,C)).
axiom U :: V :-
U =.. [C|L],
quant(L, V, A),
convert(A, [], H),
valueof(H, [], B, _), !,
axiom1(C, B, L).
axiom _ :: _ :-
sys_throw_error(domain_error(head_failed)).
axiom _ :-
sys_throw_error(syntax_error(illegal_argument)).
% axiom1(+Atom, +Indexed, +List)
axiom1(_, _, L) :-
current_prolog_flag(sys_context, user),
cust_current_eq(E),
E \= (_ = _), !,
length(L, S),
show_rest([], S).
axiom1(_, _, _) :-
cust_current_eq(E),
E \= (_ = _), !,
sys_throw_error(domain_error(body_eqs)).
axiom1(C, B, L) :-
length(L, N),
sys_replace_site(F, C, typ(C, B, N)),
assertz(F).
/**
* type T:
* Displays the type P in normal form of the term T.
* The extended nominal form is displayed.
*/
% type +Nominal
type T :-
convert(T, [], J),
typeof(J, [], S),
reconst(S, [], E),
pretty(E, P),
write_var(P), nl,
show_rest([], 0).
/**
* lemma C(X1:T1,..,Xn:Tn) :: A by W:
* Adds a new constant C and its type X1:T1\..\Xn:Tn\A. The
* type X1:T1\..\Xn:Tn\A is verified by the proof steps W.
* This does not change the logic.
* A type annotations :Ti is optional when it can be infered.
*/
% lemma +Compound :: +Nominal by +Script
lemma U :: _ by _ :-
U =.. [C|_],
typ(C, _, _), sys_throw_error(permission_error(already_defined,C)).
lemma U :: _ by _ :-
U =.. [C|_],
def(C, _, _), sys_throw_error(permission_error(already_defined,C)).
lemma U :: V by W :-
U =.. [C|L],
quant(L, V, A),
quant(L, _, T),
convert(A, [], H),
valueof(H, [], B, _), !,
convert(T, [], J),
typeof(J, [], S),
S = B,
term_variables(T, K),
phrase(W, K, R),
lemma1(R, C, B, L).
lemma _ :: _ by _ :-
sys_throw_error(domain_error(head_failed)).
lemma _ :-
sys_throw_error(syntax_error(illegal_argument)).
% lemma1(+List, +Atomic, +Indexed, +List)
lemma1([], C, B, L) :- !,
lemma2(C, B, L).
lemma1(R, _, _, L) :-
current_prolog_flag(sys_context, user), !,
length(L, S),
show_rest(R, S).
lemma1(_, _, _, _) :-
sys_throw_error(domain_error(body_vars)).
% lemma2(+Atom, +Indexed, +List)
lemma2(_, _, L) :-
current_prolog_flag(sys_context, user),
cust_current_eq(E),
E \= (_ = _), !,
length(L, S),
show_rest([], S).
lemma2(_, _, _) :-
cust_current_eq(E),
E \= (_ = _), !,
sys_throw_error(domain_error(body_eqs)).
lemma2(C, B, L) :-
length(L, N),
sys_replace_site(F, C, typ(C, B, N)),
assertz(F).
/**
* theorem C(X1:T1,..,Xn:Tn) :: A by W:
* The type X1:T1\..\Xn:Tn\A is verified by the proof steps W.
* A type annotations :Ti is optional when it can be infered.
*/
% theorem +Compound :: +Nominal by +Script
theorem U :: V by W :-
U =.. [C|L],
quant(L, V, A),
quant(L, _, T),
convert(A, [], H),
valueof(H, [], B, _), !,
convert(T, [], J),
typeof(J, [], S),
S = B,
term_variables(T, K),
phrase(W, K, R),
theorem1(R, C, L).
theorem _ :: _ by _ :-
sys_throw_error(domain_error(head_failed)).
theorem _ :-
sys_throw_error(syntax_error(illegal_argument)).
% theorem1(+List, +Atomic, +List)
theorem1([], C, L) :- !,
theorem2(C, L).
theorem1(R, _, L) :-
current_prolog_flag(sys_context, user), !,
length(L, S),
show_rest(R, S).
theorem1(_, _, _) :-
sys_throw_error(domain_error(body_vars)).
% theorem2(+Atomic, +List)
theorem2(_, L) :-
current_prolog_flag(sys_context, user),
cust_current_eq(E),
E \= (_ = _), !,
length(L, S),
show_rest([], S).
theorem2(_, _) :-
cust_current_eq(E),
E \= (_ = _), !,
sys_throw_error(domain_error(body_eqs)).
theorem2(C, _) :-
write('Theorem '), write(C), write(' verified.'), nl.
/***************************************************************************************/
/* Normalization commands language. */
/***************************************************************************************/
/**
* fun C(X1:T1,..,Xn:Tn) :: A by W:
* Adds a new constant C and its type X1:T1\..\Xn:Tn\A. The
* type X1:T1\..\Xn:Tn\A is verified by the proof steps W.
* This does not change the logic.
* A type annotations :Ti is optional when it can be infered.
*/
% fun +Compound :: +Nominal by +Script
fun U :: _ by _ :-
U =.. [C|_],
typ(C, _, _), sys_throw_error(permission_error(already_defined,C)).
fun U :: _ by _ :-
U =.. [C|_],
def(C, _, _), sys_throw_error(permission_error(already_defined,C)).
fun U :: V by W :-
U =.. [C|L],
quant(L, V, A),
quant(L, _, T),
convert(A, [], H),
valueof(H, [], B, _), !,
convert(T, [], J),
typeof(J, [], S),
S = B,
term_variables(T, K),
phrase(W, K, R),
fun1(R, C, J, L).
fun _ :: _ by _ :-
sys_throw_error(domain_error(head_failed)).
fun _ :-
sys_throw_error(syntax_error(illegal_argument)).
% fun1(+List, +Atomic, +Indexed, +List)
fun1([], C, J, L) :- !,
fun2(C, J, L).
fun1(R, _, _, L) :-
current_prolog_flag(sys_context, user), !,
length(L, S),
show_rest(R, S).
fun1(_, _, _, _) :-
sys_throw_error(domain_error(body_vars)).
% fun2(+Atom, +Indexed, +List)
fun2(_, _, L) :-
current_prolog_flag(sys_context, user),
cust_current_eq(E),
E \= (_ = _), !,
length(L, S),
show_rest([], S).
fun2(_, _, _) :-
cust_current_eq(E),
E \= (_ = _), !,
sys_throw_error(domain_error(body_eqs)).
fun2(C, J, L) :-
length(L, N),
sys_replace_site(F, C, def(C, J, N)),
assertz(F).
/**
* show C:
* Display the term T of the constant C.
* The extended nominal form is displayed.
*/
% show +Atom
show C :-
def(C, F),
reconst(F, [], G),
pretty(G, T),
write_var(T), nl.
/**
* value T:
* Displays the normal form N of the term T.
* The extended nominal form is displayed.
*/
% value +Nominal
value T :-
convert(T, [], H),
valueof(H, [], E, _),
reconst(E, [], F),
pretty(F, N),
write_var(N), nl,
show_rest([]).
/**
* Natural deduction based on holes, type checking and normalization.
* - We make use of curry style abstraction and leave the
* type infered by the constraint solver.
* - We make use of wildcard arguments and leave the form
* parameters infered by the constraint solver.
*
* Copyright 2014, XLOG Technologies GmbH, Switzerland
* Jekejeke Prolog 1.0.5 (a fast and small prolog interpreter)
*/
:- use_module(implicit2).
:- op(1050, xfy, ==>).
:- op(1000, xfy, &).
:- op(1050, xfy, <=>).
:- op(900, fy, ∀).
:- op(900, fy, ∃).
:- op(1050, xfy, =>).
:- op(700, xfx, ∈).
:- meta_predicate ==>(0,0).
:- meta_predicate &(0,0).
:- meta_predicate <=>(0,0).
:- meta_predicate ∀(1).
:- meta_predicate ∃(1).
:- meta_function '{}'(1).
/***************************************************************/
/* Implication, Conjunction and Bi-Implication */
/***************************************************************/
:- axiom prop :: sort.
:- theorem ex0(a:prop, b:prop) :: a->(a->b)->b by
rule(x\_),
rule(y\_),
rule(y(x)).
/*
:- theorem ex0(a:prop, b:prop) :: a->(a->b)->b by
ex0 = x\y\y(x).
*/
:- axiom (==>) :: prop -> prop -> prop.
:- axiom (&) :: prop -> prop -> prop.
:- axiom (<=>) :: prop -> prop -> prop.
:- axiom ('|') :: prop -> prop -> prop.
:- axiom ifI(x,y) :: (x -> y) -> (x ==> y).
:- axiom ifE(x,y) :: x -> (x ==> y) -> y.
:- axiom andI(x,y) :: x -> y -> x & y.
:- axiom andE1(x,y) :: x & y -> x.
:- axiom andE2(x,y) :: x & y -> y.
:- axiom iffI(x,y) :: (x ==> y) & (y ==> x) -> (x <=> y).
:- axiom iffE(x,y) :: (x <=> y) -> (x ==> y) & (y ==> x).
:- axiom orI1(x,y) :: x -> (x | y).
:- axiom orI2(x,y) :: y -> (x | y).
:- axiom orE(x,y,z:prop) :: (x | y) -> (x -> z) -> (y -> z) -> z.
:- theorem ex1(a,b) :: a==>(a==>b)==>b by
rule(ifI(x\_)),
rule(ifI(y\_)),
rule(ifE(x,y)).
:- theorem ex2(a,b) :: a&(a==>b)==>b by
rule(ifI(x\_)),
rule(ifE(_,_)),
rule(andE1(x)),
rule(andE2(x)).
:- theorem ex3(a) :: a<=>a by
rule(iffI(_)),
rule(andI(_,_)),
rule(ifI(x\x)),
rule(ifI(x\x)).
/*
:- theorem ex1(a, b) :: a==>(a==>b)==>b by
ex1 = ifI(x\ifI(y\ifE(x,y))).
:- theorem ex2(a, b) :: a&(a==>b)==>b by
ex2 = ifI(x\ifE(andE1(x),andE2(x))).
:- theorem ex3(a) :: a<=>a by
ex3 = iffI(andI(ifI(x\x),ifI(x\x))).
*/
/***************************************************************/
/* Universal and Existential Quantifier */
/***************************************************************/
:- axiom nat :: sort.
:- theorem ex4(p:(nat->prop)) :: s\(t\p(t)->p(s)) by
rule(x\_),
rule(y\_),
rule(y(x)).
/*
:- theorem ex4(p:(nat->prop)) :: s\(t\p(t)->p(s)) by
ex4 = x\y\y(x).
*/
:- axiom ∀(x:sort) :: (x -> prop) -> prop.
:- axiom ∃(x:sort) :: (x -> prop) -> prop.
:- axiom allI(x,y) :: z:x\y(z) -> ∀ y.
:- axiom allE(x,y) :: z:x\(∀ y -> y(z)).
:- axiom exI(x,y) :: z:x\(y(z) -> ∃ y).
:- axiom exE(x,y,c:prop) :: ∃ y -> z:x\(y(z) -> c) -> c.
:- theorem ex5(p:(nat->prop)) :: ∀ s\(∀ t\p(t)==>p(s)) by
rule(allI(x\_)),
rule(ifI(y\_)),
rule(allE(x,y)).
:- theorem ex6(p:(nat->prop),q:(nat->prop)) :: ∃ s\(p(s)&q(s))==> ∃ t\p(t) by
rule(ifI(z\_)),
rule(exE(z,y\x\_)),
rule(exI(y,_)),
rule(andE1(x)).
/***************************************************************/
/* Higher Order */
/***************************************************************/
:- axiom (=>) :: sort -> sort -> sort.
:- axiom '{}'(x,y) :: (x -> y) -> (x => y).
:- axiom ∈(x,y) :: x -> (x => y) -> y.
:- axiom lamI(z,t,x:z,y:(z->t)) :: y(x) -> x ∈ {y}.
:- axiom lamE(z,t,x:z,y:(z->t)) :: x ∈ {y} -> y(x).
:- lemma lemma1(u,y:u,z) :: y ∈ {z}==>z(y) by
rule(ifI(x\_)),
rule(lamE(x)).
:- lemma lemma2(u,y:u,z) :: z(y)==>y ∈ {z} by
rule(ifI(x\_)),
rule(lamI(x)).
:- lemma lemma3(u,y:u,z) :: y ∈ {z}<=>z(y) by
rule(iffI(_)),
rule(andI(_,_)),
rule(lemma1),
rule(lemma2).
:- lemma lemma4(u,z) :: (∀ y:u\(y ∈ {z}<=>z(y))) by
rule(allI(y\_)),
rule(lemma3).
:- theorem ex7(u,z) :: ∃ t\(∀ y:u\(y ∈ t<=>z(y))) by
rule(exI({z},_)),
rule(lemma4).
/**
* Sequent calculus based only on holes and type checking:
* - We make use of curry style abstraction and leave the
* type infered by the constraint solver.
* - We make use of wildcard arguments and leave the form
* parameters infered by the constraint solver.
*
* Copyright 2014, XLOG Technologies GmbH, Switzerland
* Jekejeke Prolog 1.0.5 (a fast and small prolog interpreter)
*/
:- use_module(library(advanced/arith)).
:- use_module(implicit2).
:- op(1050, xfy, ==>).
:- op(1000, xfy, &).
:- op(1050, xfy, <=>).
:- op(900, fy, ∀).
:- op(900, fy, ∃).
:- op(1050, xfy, =>).
:- op(700, xfx, ∈).
:- meta_predicate ==>(0,0).
:- meta_predicate &(0,0).
:- meta_predicate <=>(0,0).
:- meta_predicate ∀(1).
:- meta_predicate ∃(1).
:- meta_function '{}'(1).
/***************************************************************/
/* Implication, Conjunction and Bi-Implication */
/***************************************************************/
:- axiom prop :: sort.
:- theorem ex0(a:prop,b:prop) :: a->(a->b)->b by
rule(x\_),
rule(y\_),
rule(app(z\z,y(x))).
:- axiom (==>) :: prop -> prop -> prop.
:- axiom (&) :: prop -> prop -> prop.
:- axiom (<=>) :: prop -> prop -> prop.
:- axiom ('|') :: prop -> prop -> prop.
:- axiom ifR(x,y) :: (x -> y) -> (x ==> y).
:- axiom ifL(x,y,z:prop) :: x -> (y -> z) -> (x ==> y) -> z.
:- axiom andR(x,y) :: x -> y -> x & y.
:- axiom andL(x,y,z:prop) :: (x -> y -> z) -> x & y -> z.
:- axiom iffR(x,y) :: (x==>y)&(y==>x) -> (x<=>y).
:- axiom iffL(x,y,z:prop) :: ((x==>y)&(y==>x) -> z) -> (x<=>y) -> z.
:- axiom orR1(x,y) :: x -> (x | y).
:- axiom orR2(x,y) :: y -> (x | y).
:- axiom orL(x,y,z:prop) :: (x -> z) -> (y -> z) -> (x | y) -> z.
/***************************************************************/
/* Universal and Existential Quantifier */
/***************************************************************/
:- axiom nat :: sort.
:- theorem ex4(p:(nat->prop)) :: s\(t\p(t)->p(s)) by
rule(x\_),
rule(y\_),
rule(app(z\z,y(x))).
:- axiom ∀(x:sort) :: (x -> prop) -> prop.
:- axiom ∃(x:sort) :: (x -> prop) -> prop.
:- axiom allR(x,y) :: z:x\y(z) -> ∀ y.
:- axiom allL(x,y,c:prop) :: z:x\((y(z) -> c) -> ∀ y -> c).
:- axiom exR(x,y) :: z:x\(y(z) -> ∃ y).
:- axiom exL(x,y,c:prop) :: z:x\(y(z) -> c) -> ∃ y -> c.
/***************************************************************/
/* Higher Order */
/***************************************************************/
:- axiom (=>) :: sort -> sort -> sort.
:- axiom '{}'(x,y) :: (x -> y) -> (x => y).
:- axiom ∈(x,y) :: x -> (x => y) -> y.
:- axiom lamR(z,t,x:z,y:(z->t)) :: y(x) -> x ∈ {y}.
:- axiom lamL(z,t,x:z,y:(z->t),c:t) :: (y(x) -> c) -> x ∈ {y} -> c.
/***************************************************************/
/* Point and Go Rules */
/***************************************************************/
/* Pick the right side of the sequent. No need to indicate
which conclusion is meant. */
% ruleR
:- multifile ruleR/2.
/* propositional */
ruleR --> rule(ifR(_:_\_)).
ruleR --> rule(andR(_,_)).
ruleR --> rule(iffR(_)).
ruleR --> rule(orR1(_)).
ruleR --> rule(orR2(_)).
/* FOL */
ruleR --> rule(allR(_:_\_)).
/* HOL */
ruleR --> rule(lamR(_)).
/* Pick the right side of the sequent and specify a term. No need
to indicate which conclusion is meant. */
% ruleR(+Nominal)
:- multifile ruleR/3.
/* FOL */
ruleR(T) --> rule(exR(T,_)).
/* Pick the left side of the sequent. Need to specify which
premisse is meant. */
% ruleL(+Nominal)
:- multifile ruleL/3.
/* propositional */
ruleL(Y) --> rule(ifL(_,_:_\_,Y)).
ruleL(Y) --> rule(andL(_:_\_:_\_,Y)).
ruleL(Y) --> rule(iffL(_:_\_,Y)).
ruleL(Y) --> rule(orL(_:_\_,_:_\_,Y)).
/* FOL */
ruleL(Y) --> rule(exL(_:_\_:_\_,Y)).
/* HOL */
ruleL(Y) --> rule(lamL(_:_\_,Y)).
/* Pick the left side of the sequent and specify a term. Need to
specify which premisse is meant. */
% ruleL(+Nominal,+Nominal)
:- multifile ruleL/4.
/* FOL */
ruleL(T,Y) --> rule(allL(T,_:_\_,Y)).
/***************************************************************/
/* Iterative Deepenig Strategy */
/***************************************************************/
/**
* step:
* Automatically pick a right side or left side of the
* sequent, or try closing a sequent. Don't specify any
* term, leave it to the constraint solver.
*/
% step
step -->
ruleR.
step -->
ruleR(_).
step -->
pick(X), ruleL(X).
step -->
pick(X), ruleL(_,X).
step -->
pick(X), rule(X).
/**
* step(N,B):
* Stop if the size was reduced compared to B. Otherwise
* continue picking sequent sides for the maximal given
* number of steps N.
*/
% stzeps(+Nat, +Nat)
steps(_, B) -->
size(C), {C < B}, !.
steps(N, B) -->
{N > 0, M is N-1}, prefer(_), step, steps(M, B).
/**
* search:
* Iteratively deepen the number of steps that are tried.
*/
search -->
size(B), {between(1, 10, N)}, steps(N, B).
/***************************************************************/
/* Some Example Proofs */
/***************************************************************/
:- theorem ex1(a,b) :: a==>(a==>b)==>b by
search.
:- theorem ex2(a,b) :: a&(a==>b)==>b by
search.
:- theorem ex3(a) :: a<=>a by
search.
:- theorem ex5(p:(nat->prop)) :: ∀ s\(∀ t\p(t)==>p(s)) by
search.
:- theorem ex6(p:(nat->prop),q:(nat->prop)) :: ∃ s\(p(s)&q(s))==> ∃ t\p(t) by
search.
/**
* Search does not yet work on the following example,
* crashes, most likely because of a cyclic term.
*/
:- theorem ex7(u,z:(u->prop)) :: ∃ t\(∀ y:u\(y ∈ t<=>z(y))) by
ruleR({z}), ruleR, ruleR, ruleR, ruleR, ruleL(x3), rule(x4),
ruleR, ruleR, rule(x3).
@jburse

This comment has been minimized.

Copy link
Owner Author

jburse commented Feb 2, 2015

Literature:

Induction principles formalized in
the Calculus of Constructions (1988)
Gérard Huet, Programming of Future Generation Computers. Elsevier
http://yquem.inria.fr/~huet/PUBLIC/induction.pdf

Residual Theory in λ-calculus
A Formal Development, Gerard Huet, 1998
http://pauillac.inria.fr/~huet/PUBLIC/residuals.pdf

@jburse

This comment has been minimized.

Copy link
Owner Author

jburse commented Feb 4, 2015

Relies on the Jekejeke Minlog Forward Chaining and Attribute Variables, downloadable from:
http://www.jekejeke.ch/

Using another constraint solver framework would need some severe adaptation.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.