Check-in [4a035bbfc0]

Not logged in

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

Overview
Comment:Added a specialized version of the nat specification, for demonstration purposes.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:4a035bbfc05f9fd88446fedc8f16e450b575b42e
User & Date: andy 2015-04-14 20:21:57
Context
2015-04-14
20:49
Added support for rendering inductive goals with the up/down arrows. check-in: 98ef3fd317 user: andy tags: trunk
20:21
Added a specialized version of the nat specification, for demonstration purposes. check-in: 4a035bbfc0 user: andy tags: trunk
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
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Added plsrc/nat_spec_demo.pl.



























































































>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
%%%
%%% nat_spec_demo.pl
%%% Sample specification for natural numbers, but modified to work with the
%%% demo. 
%%%

:- module(nat_spec_demo, [spec/1]).

spec([

    % Due to an oversight on my part, the way we handle inductive proofs, 
    % although correct, will not work with the kind of incremental proofs
    % construction we are aiming to do. More permanent solutions will have to
    % come later, but for now we hard-code the IH into the specification.
    % (Which, yes, means that you can only prove one thing by induction!)
    ih('IH',         add(' x', z, ' x'), 'nat\\sml'(' x')),

    % Nat formation rules
    rule('Nat-z',    nat(z),       and([true])),
    rule('Nat-succ', nat(s(' n')), and([nat(' n')])),

    % Addition rules
    rule('Add-z',    add(z,' x', ' x'),         and([true])),
    rule('Add-succ', add(s(' x'),' y',s(' z')), and([add(' x',' y',' z')])),

    % Greater-than rules
    rule('GT-z',    (s(' _') > z),    and([true])),
    rule('GT-succ', (s(' x') > s(' y')), and([' x' > ' y'])),

    % Natlist formation rules
    rule('NL-nil', natlist(nil),       and([true])),
    rule('NL-cons',natlist(cons(' n',' l')), and([nat(' n'), natlist(' l')])),

    % List concatenation
    rule('Cat-nil', cat(nil,' l',' l'),                 and([true])),
    rule('Cat-cons',cat(cons(' n',' l'),' l1',cons(' n',' l2')), and([cat(' l',' l1',' l2')])),

    % List length
    rule('Len-nil', nlen(nil,z),          and([true])),
    rule('Len-cons',nlen(cons(' _',' l'),s(' m')), and([nlen(' l',' m')])),

    % List membership
    rule('Elem-cons', elem(' e',cons(' e', ' _')), and([true])),
    rule('Elem-tail', elem(' e',cons(' _', ' l')), and([elem(' e', ' l')]))
]).