1 % Implementation of a Sequent Prover
2 % where we can use the ProB animator to perform proof steps
3 % proof rules taken/adapted from https://wiki.event-b.org/index.php/Inference_Rules
4 % rewrite rules taken/adapted from https://wiki.event-b.org/index.php/All_Rewrite_Rules
5 % the term representation is the one from ProB's well_definedness prover
6
7 :- use_module(library(lists)).
8
9 % ------------------------
10
11
12 % for ProB XTL Mode:
13 % specifying the start state:
14 start(sequent(SHyps,Goal,success)) :- start2(Hyps,Goal), sort(Hyps,SHyps).
15
16 start2([equal('$'(x),2)],
17 conjunct(equal('$'(y),'$'(y)),equal('$'(x),2))).
18 start2([equal('$'(x),2)],
19 implication(equal('$'(y),'$'(x)),equal('$'(y),2))).
20 start2([equal('$'(x),2)],
21 disjunct(negation(equal('$'(y),'$'(x))),equal('$'(y),2))).
22 % SKS 24/25 sheet 10:
23 start2(
24 [equal(intersection(set_extension(['$'(red)]),set_extension(['$'(green)])),empty_set),
25 member('$'(peds_colour),set_extension(['$'(red),'$'(green)])), % inv2,2
26 equal('$'(peds_go),convert_bool(equal('$'(peds_colour),'$'(green)))), % inv2,4
27 member('$'(new_colour),set_extension(['$'(red),'$'(green),'$'(yellow),'$'(redyellow)])), %grd1
28 implication(disjunct(equal('$'(new_colour),'$'(green)),
29 disjunct(equal('$'(new_colour),'$'(yellow)),
30 equal('$'(new_colour),'$'(redyellow)))),
31 equal('$'(peds_colour),'$'(red))),
32 equal('$'(new_value),convert_bool(disjunct(equal('$'(new_colour),'$'(green)),
33 disjunct(equal('$'(new_colour),'$'(yellow)),
34 equal('$'(new_colour),'$'(redyellow))))))
35 ],
36 implication(equal('$'(new_value),boolean_true),equal('$'(peds_go),boolean_false))
37 ).
38 % SKS 24/25 sheet 11:
39 start2(
40 [member('$'(n),natural1_set),
41 member('$'(arr),total_function(interval(1,'$'(n)),natural1_set)),
42 member('$'(mxi),interval(1,'$'(n))),
43 forall(['$'(j)],member('$'(j),interval(1,'$'(n))),greater_equal(function('$'(arr),['$'(mxi)]),function('$'(arr),['$'(j)])))
44 ],
45 conjunct(conjunct(conjunct(
46 member('$'(arr),partial_function(interval(1,'$'(n)),natural1_set)),
47 member('$'(mxi),domain('$'(arr)))),
48 not_equal(range('$'(arr)),empty_set)),
49 exists(['$'(b)],forall(['$'(x)],member('$'(x),range('$'(arr))),greater_equal('$'(b),'$'(x)))))
50 ).
51 %start2(Hyps,Goal) :- % automatic import from PO file
52 % load_from_po_file('/Users/jangruteser/Desktop/find_ctx_ctx.pl',Hyps,Goal).%,
53 % print(goal(Goal)), nl,
54 % format('hyps: ~w',[Hyps]), nl.
55
56 get_normalised_bexpr(Expr,NormExpr) :-
57 translate:transform_raw(Expr,TExpr),
58 well_def_hyps:normalize_predicate(TExpr,NormExpr).
59
60 %:- get_normalised_bexpr(conjunct(none,greater(none,integer(none,4),integer(none,5)),truth(none)),NormExpr), print(NormExpr), nl.
61
62 :- use_module(disproversrc(disprover_test_runner),[load_po_file/1,get_disprover_po/6]).
63 load_from_po_file(File,Hyps,Goal) :-
64 disprover_test_runner:load_po_file(File),
65 disprover_test_runner:get_disprover_po(_PO,_Context,RawGoal,_RawAllHyps,RawSelHyps,_RodinStatus),
66 get_normalised_bexpr(RawGoal,Goal),
67 maplist(get_normalised_bexpr,RawSelHyps,Hyps).
68
69 % ------------------------
70
71 % specifying properties that appear in the State Properties view:
72 prop(success,goal).
73 prop(sequent(_,X,_), 'GOAL'(XS)) :- translate_term(X,XS).
74 prop(sequent(Hyps,_,_),'HYP'(Nr,XS)) :- nth1(Nr,Hyps,X),
75 translate_term(X,XS).
76 prop(sequent(_,_,Cont),'='('CONTINUATION',P)) :- cont_length(Cont,P).
77 prop(X,X).
78
79 translate_term(Term,Str) :-
80 catch(well_def_hyps:translate_norm_expr_with_limit(Term,300,Str), % probably only works when ProB is run from source
81 _Exc,Str=Term).
82
83 cont_length(sequent(_,_,C),R) :- !, cont_length(C,R1), R is R1+1.
84 cont_length(_,0).
85
86 % ------------------------
87
88 % specifying the next state relation using proof rules:
89 trans(Rule,sequent(Hyps,Goal,Cont),Cont) :- axiom(Rule,Hyps,Goal).
90 trans(simplify_goal(Rule),sequent(Hyps,Goal,Cont),sequent(Hyps,NewGoal,Cont)) :-
91 simp_rule(Goal,Hyps,NewGoal,Rule).
92 trans(simplify_hyp(Rule),sequent(Hyps,Goal,Cont),sequent(SHyps,Goal,Cont)) :-
93 select(Hyp,Hyps,NewHyp,NewHyps),
94 simp_rule(Hyp,NewHyp,Rule),
95 sort(NewHyps,SHyps).
96 trans(dbl_hyp,sequent(Hyps,Goal,Cont),sequent(SHyps,Goal,Cont)) :-
97 % not really necessary if we use sort on Hyps everywhere else
98 sort(Hyps,SHyps), SHyps \= Hyps.
99 trans(and_l,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
100 select(conjunct(P,Q),Hyps,Hyps0),
101 sort([P,Q|Hyps0],Hyps1).
102 trans(or_r,sequent(Hyps,disjunct(GA,GB),Cont),sequent(Hyps1,GA,Cont)) :-
103 negate(GB,NotGB), % we could also negate GA and use GB as goal
104 sort([NotGB|Hyps],Hyps1).
105 trans(imp_l1,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
106 select(implication(P,Q),Hyps,implication(NewP,Q),Hyps1),
107 select_conjunct(PP,P,NewP),
108 member(PP,Hyps).
109 trans(mon_deselect(Nr),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
110 nth1(Nr,Hyps,_,Hyps1).
111 trans(imp_r,sequent(Hyps,implication(G1,G2),Cont),
112 sequent(Hyps1,G2,Cont)) :-
113 add_hyp(G1,Hyps,Hyps1).
114 trans(and_r,sequent(Hyps,conjunct(G1,G2),Cont),
115 sequent(Hyps,G1,sequent(Hyps,G2,Cont))).
116 trans(eq(Dir,X,Y),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,Cont)) :- select(equal(X,Y),Hyps,Hyps0),
117 (Dir=lr,
118 maplist(rewrite(X,Y),Hyps0,Hyps1),
119 rewrite(X,Y,Goal,Goal1)
120 ; Dir=rl,
121 maplist(rewrite(Y,X),Hyps0,Hyps1),
122 rewrite(Y,X,Goal,Goal1)).
123 trans(upper_bound_l,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(Set),Cont)) :-
124 Goal = exists([B],forall([X],member(X,Set),greater_equal(B,X))). % TODO: Set must not contain any bound variable
125 trans(exists_inst(Inst),sequent(Hyps,Goal,Cont),sequent(Hyps,Goal1,Cont1)) :-
126 % TODO: WD(Inst)
127 (Inst = function('$'(arr),[1]), Cont1 = sequent(Hyps,conjunct(member('$'(arr),partial_function(interval(1,'$'(n)),natural1_set)),member(1,domain('$'(arr)))),Cont)
128 ; Inst = 1, Cont1 = sequent(Hyps,truth,Cont)), % TODO: user selection
129 Goal = exists([X],Pred),
130 rewrite(X,Inst,Pred,Goal1).
131 trans(fin_fun_dom,sequent(Hyps,finite(Fun),Cont),sequent(Hyps,truth,Cont1)) :-
132 member_hyps(member(Fun,FunType),Hyps),
133 is_fun(FunType,_,Dom,_),
134 (member_hyps(finite(Dom),Hyps)
135 -> Cont1 = Cont
136 ; Cont1 = sequent(Hyps,finite(Dom),Cont)).
137
138 add_hyp(Hyp,Hyps,NewHyps) :- sort([Hyp|Hyps],NewHyps).
139
140 member_disjunct(X,disjunct(A,B)) :- el_of_disjunct(A,X) ; el_of_disjunct(B,X).
141 el_of_disjunct(disjunct(A,B),X) :- !, (el_of_disjunct(A,X) ; el_of_disjunct(B,X)).
142 el_of_disjunct(P,P).
143
144 member_conjunct(X,conjunct(A,B)) :- !, member_conjunct(X,A) ; member_conjunct(X,B).
145 member_conjunct(X,X).
146
147 % select and remove a conjunct:
148 select_conjunct(X,conjunct(A,B),Rest) :- !,
149 (select_conjunct(X,A,RA), conjoin(RA,B,Rest)
150 ;
151 select_conjunct(X,B,RB), conjoin(A,RB,Rest)).
152 select_conjunct(X,X,truth).
153
154 conjoin(truth,X,R) :- !, R=X.
155 conjoin(X,truth,R) :- !, R=X.
156 conjoin(X,Y,conjunct(X,Y)).
157
158 negate(truth,Res) :- !, Res=falsity.
159 negate(falsity,Res) :- !, Res=truth.
160 negate(equal(X,Y),R) :- !, R=not_equal(X,Y).
161 negate(not_equal(X,Y),R) :- !, R=equal(X,Y).
162 negate(disjunct(X,Y),R) :- !, R=conjunct(NX,NY), negate(X,NX), negate(Y,NY).
163 negate(conjunct(X,Y),R) :- !, R=disjunct(NX,NY), negate(X,NX), negate(Y,NY).
164 negate(implication(X,Y),R) :- !, R=conjunct(X,NY), negate(Y,NY).
165 negate(negation(X),R) :- !, R=X.
166 negate(P,negation(P)).
167
168 is_fun(partial_function(DOM,RAN),partial,DOM,RAN).
169 is_fun(partial_injection(DOM,RAN),partial,DOM,RAN).
170 is_fun(partial_surjection(DOM,RAN),partial,DOM,RAN).
171 is_fun(partial_bijection(DOM,RAN),partial,DOM,RAN).
172 is_fun(total_function(DOM,RAN),total,DOM,RAN).
173 is_fun(total_injection(DOM,RAN),total,DOM,RAN).
174 is_fun(total_surjection(DOM,RAN),total,DOM,RAN).
175 is_fun(total_bijection(DOM,RAN),total,DOM,RAN).
176
177 % rewrite X to E
178 rewrite(X,Y,E,NewE) :- X=E,!, NewE=Y.
179 rewrite(X,Y,E,NewE) :- atomic(E),!, NewE=E.
180 rewrite(X,Y,'$'(E),NewE) :- atomic(E),!, NewE='$'(E).
181 rewrite(X,Y,C,NewC) :- C=..[Op|Args],
182 maplist(rewrite(X,Y), Args,NewArgs),
183 NewC =.. [Op|NewArgs].
184
185
186 % axioms: proof rules without antecedent, discharging goal directly
187 axiom(hyp,Hyps,Goal) :- member_hyps(Goal,Hyps).
188 axiom(hyp_or,Hyps,Goal) :- member_disjunct(P,Goal), member_hyps(P,Hyps).
189 axiom(false_hyp,Hyps,_Goal) :- member_hyps(falsity,Hyps).
190 axiom(true_goal,_,truth).
191 axiom(Rule,_Hyps,Goal) :- axiom_wo_hyps(Goal,Rule).
192 axiom(fun_goal(F),Hyps,member(F,PFType)) :-
193 is_fun(PFType,partial,_,_),
194 member_hyps(member(F,FType),Hyps),
195 is_fun(FType,_,_,_).
196
197 axiom_wo_hyps(true,true_goal).
198 axiom_wo_hyps(eq(E,E),eql).
199
200 member_hyps(Goal,Hyps) :-
201 ? (member(Goal,Hyps) -> true
202 ; equiv(Goal,G2), member(G2,Hyps) -> true).
203
204 % replace by normalisation
205 equiv(equal(A,B),equal(B,A)).
206 equiv(not_equal(A,B),not_equal(B,A)).
207 equiv(greater(A,B),less(B,A)).
208 equiv(less(A,B),greater(B,A)).
209 equiv(greater_equal(A,B),less_equal(B,A)).
210 equiv(less_equal(A,B),greater_equal(B,A)).
211
212
213 % Goal Simplification Rules
214 simp_rule(Goal,_Hyps,NewGoal,Rule) :-
215 ? simp_rule(Goal,NewGoal,Rule).
216
217 % rules that do not require hyps:
218 simp_rule(equal(L,L),truth,'SIMP_MULTI_EQUAL').
219 simp_rule(not_equal(L,L),falsity,'SIMP_MULTI_NOTEQUAL').
220 simp_rule(less_equal(E,E),truth,'SIMP_MULTI_LE').
221 simp_rule(less_equal(I,J),Res,'SIMP_LIT_LE') :- number(I), number(J), I =< J -> Res=truth ; Res=falsity. % where I and J are literals
222 simp_rule(not_equal(L,R),negation(equal(L,R)),'SIMP_NOTEQUAL').
223 simp_rule(negation(equal(Set,empty_set)),exists(['$'(x)],member('$'(x),Set)),'DEF_SPECIAL_NOT_EQUAL'). % TODO: get free identifier?
224 simp_rule(Eq,P,'SIMP_LIT_EQUAL_KBOOL_TRUE') :- is_equality(Eq,convert_bool(P),boolean_true).
225 simp_rule(Eq,negation(P),'SIMP_LIT_EQUAL_KBOOL_FALSE') :- is_equality(Eq,convert_bool(P),boolean_false).
226 simp_rule(implication(truth,P),P,'SIMP_SPECIAL_IMP_BTRUE_L').
227 simp_rule(implication(P,falsity),negation(P),'SIMP_SPECIAL_IMP_BFALSE_R').
228 simp_rule(Eq,negation(member(A,SetB)),'SIMP_BINTER_SING_EQUAL_EMPTY') :-
229 ? is_equality(Eq,Inter,empty_set),
230 is_inter(Inter,SetA,SetB),
231 singleton_set(SetA,A).
232 simp_rule(member(X,SetA),equal(X,A),'SIMP_IN_SING') :-
233 singleton_set(SetA,A).
234 simp_rule(member(X,total_function(Dom,Ran)),conjunct(Conj1,Conj2),'DEF_IN_TFCT') :-
235 Conj1 = member(X,partial_function(Dom,Ran)),
236 Conj2 = equal(domain(X),Dom).
237 simp_rule(member(R,range(F)),exists(['$'(x)],member(couple('$'(x),R),F)),'DEF_IN_RAN'). % TODO: get free identifier?
238 simp_rule(member(couple(E,function(F,[E])),F),truth,'SIMP_IN_FUNIMAGE').
239 simp_rule(member(LB,interval(LB,_)),truth,'lower_bound_in_interval'). % own rule: lower bound in interval
240 simp_rule(member(E,interval(L,R)),conjunct(less_equal(L,E),less_equal(E,R)),'DEF_IN_UPTO').
241 simp_rule(finite(range(F)),finite(F),'FIN_REL_RAN_R').
242 simp_rule(finite(interval(_,_)),truth,'SIMP_FINITE_UPTO').
243 % allow simplifications deeper inside the term:
244 simp_rule(negation(P),negation(Q),Rule) :- simp_rule(P,Q,Rule).
245 ?simp_rule(conjunct(P,R),conjunct(Q,R),Rule) :- simp_rule(P,Q,Rule).
246 ?simp_rule(conjunct(R,P),conjunct(R,Q),Rule) :- simp_rule(P,Q,Rule).
247 simp_rule(disjunct(P,R),disjunct(Q,R),Rule) :- simp_rule(P,Q,Rule).
248 simp_rule(disjunct(R,P),disjunct(R,Q),Rule) :- simp_rule(P,Q,Rule).
249 simp_rule(implication(P,R),implication(Q,R),Rule) :- simp_rule(P,Q,Rule).
250 simp_rule(implication(R,P),implication(R,Q),Rule) :- simp_rule(P,Q,Rule).
251 simp_rule(negation(P),Q,'Propagate negation') :- negate(P,Q), Q \= negation(_). % De-Morgan and similar rules to propagate negation
252
253 %simp_rule(X,X,'EQ'(F,N,X)) :- functor(X,F,N).
254
255 is_equality(equal(A,B),A,B).
256 is_equality(equal(B,A),A,B).
257
258 is_inter(intersection(A,B),A,B). % TODO: extend to nested inter
259 is_inter(intersection(B,A),A,B).
260
261 singleton_set(set_extension([X]),X).
262
263 animation_function_result(success,[((1,1),'Proof succeeded.')]).
264 animation_function_result(State,Matrix) :-
265 State = sequent(_,_,Cont),
266 cont_length(Cont,LCont),
267 findall(((RowNr,ColNr),Cell), (cell_content(RowNr,ColNr,State,Cell,LCont)), Matrix).
268
269 cell_content(Row,1,sequent(Hyps,_,_),Cell,_) :- nth1(Row,Hyps,RowHyp), translate_term(RowHyp,Cell).
270 cell_content(Row,1,sequent(Hyps,_,_),'---------------------',_) :- length(Hyps,LHyps), Row is LHyps + 1.
271 cell_content(Row,1,sequent(Hyps,Goal,_),Cell,_) :- length(Hyps,LHyps), Row is LHyps + 2, translate_term(Goal,Cell).
272
273 cell_content(Row,Col,Sequent,Cell,LCont) :-
274 extract_continuations(Sequent,LCont,Cont,Col),
275 cell_content(Row,_,Cont,Cell,LCont).
276
277 extract_continuations(sequent(_,_,Cont),LCont,Cont,ColNr) :-
278 cont_length(Cont,ActualLCont),
279 ColNr is LCont - ActualLCont + 2.
280 extract_continuations(sequent(_,_,Cont),LCont,FoundCont,ColNr) :-
281 extract_continuations(Cont,LCont,FoundCont,ColNr).