Instantly share code, notes, and snippets.

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

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).
 /** * 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).
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
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.