Check-in [c4c963bcde]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Fixed a bug in proofs that involve backchaining on the IH.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:c4c963bcde15c563a67f32328eca4950ce557b00
User & Date: andy 2015-04-18 16:44:51
Context
2015-04-18
18:45
Fixed a bug in the checker, context was not being initialized to [] which made goals succeed once and then enter an infinite loop. check-in: f931058aa9 user: andy tags: trunk
16:44
Fixed a bug in proofs that involve backchaining on the IH. check-in: c4c963bcde user: andy tags: trunk
16:44
Fixed the body of the hard-coded IH to be a conjunction, as required by the (current) call expansion predicate. check-in: 95a716e7e5 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to plsrc/checker.pl.

3
4
5
6
7
8
9

10
11
12
13
14
15
16
...
243
244
245
246
247
248
249

250
251
252
253
254
255
256
...
299
300
301
302
303
304
305




306
307
308
309
310
311
312
...
509
510
511
512
513
514
515
516

517
518
519
520
521
522
523
%%% Prototype proof checker (in Prolog). 
%%% This only exists to make sure we have the logic right, before implementing
%%% everything in Arend.
%%%

:- module(checker, [
    check/3,

    proof/1,
    elaborate/6,
    proof_complete/1
]).

:- use_module(['program', 'subst', 'util']).

................................................................................

% elaborate_node(Goal,Ctx,What,Data,Elaboration)
% Elaborating a single node is just a matter of applying the translation from
% figs. 3 and 4 in the report. `What` tells us what to elaborate on:
% either `goal` or `ctx`
elaborate_node(true,        _, goal,_,  trivial).
elaborate_node(_ = _,       _, goal,_,  unify(_,_)).

elaborate_node(_ -> _,      _, goal,_,  implies(proof(_,_,_,hole))).
elaborate_node(forall(_,_), _, goal,_,  generic(proof(_,_,_,hole))).
elaborate_node(exists(_,_), _, goal,_,  instan(_,proof(_,_,_,hole))).
elaborate_node(and(Ps),     _, goal,_,  product(Holes)) :-
    length(Ps,N), fill(Holes,proof(_,_,_,hole),N).

elaborate_node(or(_),       _, goal,N,  choice(N,proof(_,_,_,hole))).
................................................................................
proof_complete(case(forall_left(_),_,_,[Proof])) :- proof_complete(Proof).
proof_complete(case(exists_left,_,_,[Proof])) :- proof_complete(Proof).
proof_complete(case(unify_left,_,_,[Proof])) :- proof_complete(Proof).
proof_complete(case(goal_left,_,_,[Proof])) :- proof_complete(Proof).

%%% ---------------------------------------------------------------------------





% check(Program, Goal, Proof)
% Check the Proof of Goal, in Program.

check(Program,Goal,proof(Goal,Ctx,Subst,Proof)) :-
  get_vars(Goal,Vars),
  % Ctx = [],
  check(Program,state(Vars,Ctx,Goal),_,proof(Goal,Ctx,Subst,Proof)).
................................................................................
    Rule = rule(Name,Head,Body),

    % From here on out it's very similar to backchaining on a normal goal
    get_vars(Goal,NVars),
    union(Vars,NVars,V2),

    % "Call" (expand) the Goal in the program consisting only of the IH
    program:call_clauses(V2,Goal,[Rule],Expansion),


    get_vars(Expansion,V3),
    union(V2,V3,V4),

    % Prove recursively on the expansion
    check(Program,
          state(V4,Ctx,Expansion),







>







 







>







 







>
>
>
>







 







|
>







3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
...
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
...
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
...
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
%%% Prototype proof checker (in Prolog). 
%%% This only exists to make sure we have the logic right, before implementing
%%% everything in Arend.
%%%

:- module(checker, [
    check/3,
    check/2,
    proof/1,
    elaborate/6,
    proof_complete/1
]).

:- use_module(['program', 'subst', 'util']).

................................................................................

% elaborate_node(Goal,Ctx,What,Data,Elaboration)
% Elaborating a single node is just a matter of applying the translation from
% figs. 3 and 4 in the report. `What` tells us what to elaborate on:
% either `goal` or `ctx`
elaborate_node(true,        _, goal,_,  trivial).
elaborate_node(_ = _,       _, goal,_,  unify(_,_)).
elaborate_node(_,           _, goal,asm,ctxmem(_)).
elaborate_node(_ -> _,      _, goal,_,  implies(proof(_,_,_,hole))).
elaborate_node(forall(_,_), _, goal,_,  generic(proof(_,_,_,hole))).
elaborate_node(exists(_,_), _, goal,_,  instan(_,proof(_,_,_,hole))).
elaborate_node(and(Ps),     _, goal,_,  product(Holes)) :-
    length(Ps,N), fill(Holes,proof(_,_,_,hole),N).

elaborate_node(or(_),       _, goal,N,  choice(N,proof(_,_,_,hole))).
................................................................................
proof_complete(case(forall_left(_),_,_,[Proof])) :- proof_complete(Proof).
proof_complete(case(exists_left,_,_,[Proof])) :- proof_complete(Proof).
proof_complete(case(unify_left,_,_,[Proof])) :- proof_complete(Proof).
proof_complete(case(goal_left,_,_,[Proof])) :- proof_complete(Proof).

%%% ---------------------------------------------------------------------------

check(Program,Proof) :-
  Proof = proof(Goal,_,_,_),
  check(Program,Goal,Proof).

% check(Program, Goal, Proof)
% Check the Proof of Goal, in Program.

check(Program,Goal,proof(Goal,Ctx,Subst,Proof)) :-
  get_vars(Goal,Vars),
  % Ctx = [],
  check(Program,state(Vars,Ctx,Goal),_,proof(Goal,Ctx,Subst,Proof)).
................................................................................
    Rule = rule(Name,Head,Body),

    % From here on out it's very similar to backchaining on a normal goal
    get_vars(Goal,NVars),
    union(Vars,NVars,V2),

    % "Call" (expand) the Goal in the program consisting only of the IH
    program:call_goal([Rule],V2,Goal,Expansion),
    Proof = proof(Expansion,_,_,_),

    get_vars(Expansion,V3),
    union(V2,V3,V4),

    % Prove recursively on the expansion
    check(Program,
          state(V4,Ctx,Expansion),