test_stlc.elpi

accumulate itp.
accumulate stlc/theory.

main T S :-
    test_pair T [
        then (intro x) (
        then (intro y) (
        then andI (
        then (maptac andI [1, 2]) (
        then branch (
        then (mapp x) (
        then shift (
        then shift (
        then shift (
        then unbranch (
        then branch (
        then (mapp x) (
        then unbranch ((maptac (mapp y) [1, 2])
        )))))))))))))] S.

test_itp PTerm InScript OutScript :-
    prove (arr (arr a (arr b c)) (arr a (arr b c))) InScript PTerm OutScript.
test_itp PTerm OutScript :-
    prove (arr (arr a (arr b c)) (arr a (arr b c))) PTerm OutScript.
test_pair PTerm InScript OutScript :-
    prove (arr a (arr b (prod (prod a b) (prod b a)))) InScript PTerm OutScript.
test_pair PTerm OutScript :-
    prove (arr a (arr b (prod (prod a b) (prod b a)))) PTerm OutScript.

% (A -> (B -> C)) -> ((A & B) -> C)
% and elim test
% [intro x, intro y, app, andER y, app x, andEL y]
interactive_pairElim :- interactive_pairElim [].

interactive_pairElim InScript :-
    of X (arr (arr a (arr b c)) (arr (prod a b) c)) X',
    run_itp X InScript.

% (A & B -> C) -> (A -> B -> C)
% and intro test
% [intro x, intro y, intro z, app z, andI y x]
interactive_pairIntro :- interactive_pairIntro [].

interactive_pairIntro InScript :-
    of X (arr (arr (prod a b) c) (arr a (arr b c))) X',
    run_itp X InScript.


% (A v B) -> (A -> C) -> (B -> C) -> C
% case test
% [intro x, intro y, intro z, orE x u v, app y u, app z v]
interactive_case :- interactive_case [].

interactive_case InScript :-
    of X (arr (sum a b) (arr (arr a c) (arr (arr b c) c))) X',
    run_itp X InScript.

% suml test
interactive_suml :-
    of X (arr a (sum a b)) X',
    run_itp X InScript.