Skip to content

Major overhaul of the type system to manage typed proof search with an easier-to-maintain and less invasive API #53

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jcailler merged 8 commits into from
Mar 25, 2026
Merged

Major overhaul of the type system to manage typed proof search with an easier-to-maintain and less invasive API #53

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
b25f85e
Removal of invasive type system
jrosain Jul 20, 2025
e21b017
Updated syntax of types and reintroduced them in the internals
jrosain Jul 22, 2025
28770d4
Implementation of the new typing system
jrosain Jul 23, 2025
e4263d0
Updated gamma and delta rules to deal with type variables
jrosain Jul 26, 2025
7e47707
Manage typed proof search and add related tests
jrosain Jul 26, 2025
c4b4e6f
Fix equality of quantified formulas (forall, exists)
jrosain Jul 27, 2025
8d519f9
Add proper debugging facilities in typing rules
jrosain Jul 27, 2025
7695826
Add some basic tests on the elaboration
jrosain Jul 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions devtools/test-suite/basic/test-typing-elab-1.p
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
% should fail because $lesseq is a defined function for $int, $rat and $real but is not polymorphic
% for any type
% exit: 1

tff(ty_type, type, ty : $tType).

tff(conj, conjecture, ! [A : ty] : $lesseq(A, A)).
7 changes: 7 additions & 0 deletions devtools/test-suite/basic/test-typing-elab-2.p
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
% should fail because $quotient is a defined function for $int, $rat and $real but is not polymorphic
% for any type
% exit: 1

tff(ty_type, type, ty : $tType).

tff(conj, conjecture, ! [A : ty] : $lesseq($quotient(A, A), 1)).
4 changes: 4 additions & 0 deletions devtools/test-suite/basic/test-typing-elab-3.p
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
% quotient is defined specifically for integers
% result: NOT VALID

tff(conj, conjecture, $lesseq($quotient(2, 2), 1)).
4 changes: 2 additions & 2 deletions devtools/test-suite/basic/tf1_syntax_chk.p
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
% TODO: args -one_step and result NOT_VALID once typing is working again (this is satisfiable)
% exit: 3
% args: -one_step
% result: NOT VALID

tff(beverage_type,type,
beverage: $tType ).
Expand Down
2 changes: 1 addition & 1 deletion devtools/test-suite/basic/tfa_syntax_chk.p
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
% As arithmetic is not handled by Goeland, we simply check that parsing is OK
% args: -ari -one_step -l 1
% args: -one_step -l 1
% result: NOT VALID

tff(p_int_type,type,
Expand Down
33 changes: 33 additions & 0 deletions devtools/test-suite/bugs/bug_53-1.p
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
% args: -one_step
% exit: 1

tff(list_type,type,
list: $tType > $tType ).

tff(maybe_type,type,
maybe: $tType > $tType ).

%----Polymorphic symbols
tff(nil_type,type,
nil:
!>[A: $tType] : list(A) ).

tff(cons_type,type,
cons:
!>[A: $tType] : ( ( A * list(A) ) > list(A) ) ).

tff(none_type,type,
none:
!>[A: $tType] : maybe(A) ).

tff(some_type,type,
some:
!>[A: $tType] : ( A > maybe(A) ) ).

tff(head_type,type,
head:
!>[A: $tType] : ( list(A) > maybe(A) ) ).

%----This cannot be well typed, the last cons is not well formed
tff(solve_this,conjecture,
head($int,cons($int,1,cons($int,2,cons($int,3)))) = some($int,1) ).
28 changes: 28 additions & 0 deletions devtools/test-suite/proofs/tf1_basic_thm-2.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
[0] ALPHA_AND : ((! [A13]: ((maybe(A13) ; head(A13;nil(A13;)) = none(A13;)))) & (! [A15 X17 XS19]: ((maybe(A15) ; head(A15;cons(A15;X17, XS19)) = some(A15;X17)))) & ~((! [A21 X23 Y25 Z27]: ((maybe(A21) ; head(A21;cons(A21;X23, cons(A21;Y25, cons(A21;Z27, nil(A21;))))) = some(A21;X23))))))
-> [1] (! [A13]: ((maybe(A13) ; head(A13;nil(A13;)) = none(A13;)))), (! [A15 X17 XS19]: ((maybe(A15) ; head(A15;cons(A15;X17, XS19)) = some(A15;X17)))), ~((! [A21 X23 Y25 Z27]: ((maybe(A21) ; head(A21;cons(A21;X23, cons(A21;Y25, cons(A21;Z27, nil(A21;))))) = some(A21;X23)))))

[1] DELTA_NOT_FORALL : ~((! [A21 X23 Y25 Z27]: ((maybe(A21) ; head(A21;cons(A21;X23, cons(A21;Y25, cons(A21;Z27, nil(A21;))))) = some(A21;X23)))))
-> [2] ~((! [X23 Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;X23)))))

[2] DELTA_NOT_FORALL : ~((! [X23 Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;X23)))))
-> [3] ~((! [Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)))))

[3] DELTA_NOT_FORALL : ~((! [Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)))))
-> [4] ~((! [Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)))))

[4] DELTA_NOT_FORALL : ~((! [Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)))))
-> [5] ~((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;skolem@Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)))

[5] GAMMA_FORALL : (! [A13]: ((maybe(A13) ; head(A13;nil(A13;)) = none(A13;))))
-> [6] (maybe(A13_1) ; head(A13_1;nil(A13_1;)) = none(A13_1;))

[6] GAMMA_FORALL : (! [A15 X17 XS19]: ((maybe(A15) ; head(A15;cons(A15;X17, XS19)) = some(A15;X17))))
-> [7] (! [X17 XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X17, XS19)) = some(skoTy;X17))))

[7] GAMMA_FORALL : (! [X17 XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X17, XS19)) = some(skoTy;X17))))
-> [8] (! [XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, XS19)) = some(skoTy;skolem@X23))))

[8] GAMMA_FORALL : (! [XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, XS19)) = some(skoTy;skolem@X23))))
-> [9] (maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;skolem@Z27, nil(skoTy;))))) = some(skoTy;skolem@X23))

[9] CLOSURE : (maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;skolem@Z27, nil(skoTy;))))) = some(skoTy;skolem@X23))
40 changes: 40 additions & 0 deletions devtools/test-suite/proofs/tf1_basic_thm-2.p
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
% args: -proof -no_id
% result: VALID

tff(list_type,type,
list: $tType > $tType ).

tff(maybe_type,type,
maybe: $tType > $tType ).

%----Polymorphic symbols
tff(nil_type,type,
nil:
!>[A: $tType] : list(A) ).

tff(cons_type,type,
cons:
!>[A: $tType] : ( ( A * list(A) ) > list(A) ) ).

tff(none_type,type,
none:
!>[A: $tType] : maybe(A) ).

tff(some_type,type,
some:
!>[A: $tType] : ( A > maybe(A) ) ).

tff(head_type,type,
head:
!>[A: $tType] : ( list(A) > maybe(A) ) ).

%----Use of polymorphic symbols
tff(head_nil,axiom,
! [A: $tType] : ( head(A,nil(A)) = none(A) )).

tff(head_cons,axiom,
! [A: $tType,X : A,XS : list(A)] : ( head(A,cons(A,X,XS)) = some(A,X) ) ).

%----With integers
tff(solve_this,conjecture,
! [A: $tType,X : A,Y : A,Z : A] : ( head(A,cons(A,X,cons(A,Y,cons(A,Z,nil(A))))) = some(A,X) ) ).
16 changes: 16 additions & 0 deletions devtools/test-suite/proofs/tf1_basic_thm.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
[0] ALPHA_AND : ((! [A14]: ((maybe(A14) ; head(A14;nil(A14;)) = none(A14;)))) & (! [A16 X18 XS20]: ((maybe(A16) ; head(A16;cons(A16;X18, XS20)) = some(A16;X18)))) & ~((maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1))))
-> [1] (! [A14]: ((maybe(A14) ; head(A14;nil(A14;)) = none(A14;)))), (! [A16 X18 XS20]: ((maybe(A16) ; head(A16;cons(A16;X18, XS20)) = some(A16;X18)))), ~((maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1)))

[1] GAMMA_FORALL : (! [A14]: ((maybe(A14) ; head(A14;nil(A14;)) = none(A14;))))
-> [2] (maybe(A14_1) ; head(A14_1;nil(A14_1;)) = none(A14_1;))

[2] GAMMA_FORALL : (! [A16 X18 XS20]: ((maybe(A16) ; head(A16;cons(A16;X18, XS20)) = some(A16;X18))))
-> [3] (! [X18 XS20]: ((maybe($int) ; head($int;cons($int;X18, XS20)) = some($int;X18))))

[3] GAMMA_FORALL : (! [X18 XS20]: ((maybe($int) ; head($int;cons($int;X18, XS20)) = some($int;X18))))
-> [4] (! [XS20]: ((maybe($int) ; head($int;cons($int;1, XS20)) = some($int;1))))

[4] GAMMA_FORALL : (! [XS20]: ((maybe($int) ; head($int;cons($int;1, XS20)) = some($int;1))))
-> [5] (maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1))

[5] CLOSURE : (maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1))
40 changes: 40 additions & 0 deletions devtools/test-suite/proofs/tf1_basic_thm.p
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
% args: -proof -no_id
% result: VALID

tff(list_type,type,
list: $tType > $tType ).

tff(maybe_type,type,
maybe: $tType > $tType ).

%----Polymorphic symbols
tff(nil_type,type,
nil:
!>[A: $tType] : list(A) ).

tff(cons_type,type,
cons:
!>[A: $tType] : ( ( A * list(A) ) > list(A) ) ).

tff(none_type,type,
none:
!>[A: $tType] : maybe(A) ).

tff(some_type,type,
some:
!>[A: $tType] : ( A > maybe(A) ) ).

tff(head_type,type,
head:
!>[A: $tType] : ( list(A) > maybe(A) ) ).

%----Use of polymorphic symbols
tff(head_nil,axiom,
! [A: $tType] : ( head(A,nil(A)) = none(A) )).

tff(head_cons,axiom,
! [A: $tType,X : A,XS : list(A)] : ( head(A,cons(A,X,XS)) = some(A,X) ) ).

%----With integers
tff(solve_this,conjecture,
head($int,cons($int,1,cons($int,2,cons($int,3,nil($int))))) = some($int,1) ).
Loading
Loading