Check-in [c82ab7e9b6]

Not logged in

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

Overview
Comment:Changed the way the induction tactic handles repeated use (previous IHs are just ignored).
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:c82ab7e9b66e535198767d5b5c3640dff6d36582
User & Date: andy 2015-04-14 20:19:03
Context
2015-04-14
20:21
Added `passist` Pengine application to the server. This runs the live demo of the proof assistant. check-in: 3a093317cf user: andy tags: trunk
20:19
Changed the way the induction tactic handles repeated use (previous IHs are just ignored). check-in: c82ab7e9b6 user: andy tags: trunk
14:01
Added screenshot of the REPL UI. check-in: 2656521773 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to plsrc/checker.pl.

437
438
439
440
441
442
443
444

445
446
447
448
449
450
451
452
453
454

455
456
457
458
459

460
461



462

463
464
465
466
467
468
469
470









471
472
473
474
475
476
477
      state(Vars,Ctx,Goal),
      VOut,
      proof(Goal,Ctx,Subst,Induction)) :-
    
    nonvar(Induction),
    Induction = induction(Index,IH,Proof),

    Goal = (and(Gs) -> R),


    % Get the target of the induction
    nth0(Index,Gs,G),

    % Get the small/large versions of it
    inductify_goal(G,'\\sml',GSmall),
    inductify_goal(G,'\\big',GBig),

    % Rewrite the goal to use the big version
    replace_nth0(Gs,Index,GBig,BigGs),

    NewGoal = (and(BigGs) -> R),

    % For IH, rewrite the goal to use the small version
    replace_nth0(Gs,Index,GSmall,SmallGs),
    IH = (and(SmallGs) -> R),


    % Add IH to the program



    NewProgram = [ih('IH',R,and(SmallGs))|Program],


    % Prove recursively
    check(NewProgram,
          state(Vars,Ctx,NewGoal),
          VOut,
          Proof),

    sub(Proof,Subst).










% IH:
% Backchain on the IH
check(Program,
      state(Vars,Ctx,Goal),
      VOut,
      proof(Goal,Ctx,Subst,IHProof)) :-







|
>





|
|



>
|



|
>

|
>
>
>
|
>







|
>
>
>
>
>
>
>
>
>







437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
      state(Vars,Ctx,Goal),
      VOut,
      proof(Goal,Ctx,Subst,Induction)) :-
    
    nonvar(Induction),
    Induction = induction(Index,IH,Proof),

    % Get the premises and goal of the induction hypothesis
    get_ind_premises(Goal, Gs, R),

    % Get the target of the induction
    nth0(Index,Gs,G),

    % Get the small/large versions of it
    inductify_goal('\\sml',G,GSmall),
    inductify_goal('\\big',G,GBig),

    % Rewrite the goal to use the big version
    replace_nth0(Gs,Index,GBig,BigGs),
    andify(BigGs,AndBig),
    NewGoal = (AndBig -> R),

    % For IH, rewrite the goal to use the small version
    replace_nth0(Gs,Index,GSmall,SmallGs),
    andify(SmallGs,AndSmall),
    IH = (AndSmall -> R),

    % Add IH to the program, but only if it isn't already there.
    (member(ih(_,_,_),Program) -> 
      NewProgram = Program
    ;  
      NewProgram = [ih('IH',R,AndSmall)|Program]
    ),

    % Prove recursively
    check(NewProgram,
          state(Vars,Ctx,NewGoal),
          VOut,
          Proof),

    sub(Proof,Subst)
    .

% Helper to get the "list" of inductive premises
get_ind_premises(and(Gs) -> R, Gs, R) :- !.
get_ind_premises(G -> R, [G], R).

% Helper to do the opposite, turn a single and into itself
andify([G],G).
andify([G1,G2|Gs],and([G1,G2|Gs])).

% IH:
% Backchain on the IH
check(Program,
      state(Vars,Ctx,Goal),
      VOut,
      proof(Goal,Ctx,Subst,IHProof)) :-