Skip to content

Commit b802ed3

Browse files
lucaspenalucaspena
committed
remove coq tests besides Logic and nat_ind, add expeted output for those
1 parent 46b712b commit b802ed3

File tree

7 files changed

+114
-25
lines changed

7 files changed

+114
-25
lines changed

‎prover/t/And.v

Lines changed: 0 additions & 2 deletions
This file was deleted.

‎prover/t/AndComm.v

Lines changed: 0 additions & 10 deletions
This file was deleted.

‎prover/t/False_ind.v

Lines changed: 0 additions & 3 deletions
This file was deleted.

‎prover/t/Four.v

Lines changed: 0 additions & 7 deletions
This file was deleted.

‎prover/t/Logic.v.expected

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
<prover>
2+
<k>
3+
.CoqSentences
4+
</k>
5+
<exit-code>
6+
1
7+
</exit-code>
8+
<goals>
9+
.GoalCellSet
10+
</goals>
11+
<declarations>
12+
<declaration>
13+
axiom \equals ( AndComm , \lambda { A { Term } , B { Term } , H { Term } , .Patterns } \or ( \exists { H0 , H1 , .Patterns } \and ( \equals ( H , conj ( H0 , H1 , .Patterns ) ) , conj ( H1 , H0 , .Patterns ) , .Patterns ) , .Patterns ) )
14+
</declaration> <declaration>
15+
axiom \equals ( IF_then_else , or ( and , P , Q , .Patterns ) ( and , not , P , R , .Patterns ) )
16+
</declaration> <declaration>
17+
axiom \equals ( iff , and ( \forall { x { Term } , .Patterns } B , .Patterns ) ( \forall { y { Term } , .Patterns } A , .Patterns ) )
18+
</declaration> <declaration>
19+
axiom \equals ( not , \lambda { A { Term } , .Patterns } \forall { x { Term } , .Patterns } False )
20+
</declaration> <declaration>
21+
axiom \type ( I ( .Patterns ) , True )
22+
</declaration> <declaration>
23+
axiom \type ( S ( .Patterns ) , nat ( - , > , nat , .Patterns ) )
24+
</declaration> <declaration>
25+
axiom \type ( Z ( .Patterns ) , nat )
26+
</declaration> <declaration>
27+
axiom \type ( conj ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( and ( A , B , .Patterns ) ) )
28+
</declaration> <declaration>
29+
axiom \type ( ex_intro1 ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( ex1 ( A , P , .Patterns ) ) )
30+
</declaration> <declaration>
31+
axiom \type ( ex_intro2 ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( ex2 ( P , .Patterns ) ) )
32+
</declaration> <declaration>
33+
axiom \type ( ex_intro4 ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( ex4 ( A , .Patterns ) ( P , .Patterns ) ) )
34+
</declaration> <declaration>
35+
axiom \type ( or_introl ( .Patterns ) , \forall { x { Term } , .Patterns } ( or ( A , B , .Patterns ) ) )
36+
</declaration> <declaration>
37+
axiom \type ( or_intror ( .Patterns ) , \forall { y { Term } , .Patterns } ( or ( A , B , .Patterns ) ) )
38+
</declaration> <declaration>
39+
sort Term
40+
</declaration> <declaration>
41+
symbol AndComm ( .Sorts ) : Term
42+
</declaration> <declaration>
43+
symbol False ( .Sorts ) : Term
44+
</declaration> <declaration>
45+
symbol I ( .Sorts ) : Term
46+
</declaration> <declaration>
47+
symbol IF_then_else ( .Sorts ) : Term
48+
</declaration> <declaration>
49+
symbol S ( .Sorts ) : Term
50+
</declaration> <declaration>
51+
symbol True ( .Sorts ) : Term
52+
</declaration> <declaration>
53+
symbol Z ( .Sorts ) : Term
54+
</declaration> <declaration>
55+
symbol and ( .Sorts ) : Term
56+
</declaration> <declaration>
57+
symbol conj ( .Sorts ) : Term
58+
</declaration> <declaration>
59+
symbol ex1 ( .Sorts ) : Term
60+
</declaration> <declaration>
61+
symbol ex2 ( .Sorts ) : Term
62+
</declaration> <declaration>
63+
symbol ex4 ( .Sorts ) : Term
64+
</declaration> <declaration>
65+
symbol ex_intro1 ( .Sorts ) : Term
66+
</declaration> <declaration>
67+
symbol ex_intro2 ( .Sorts ) : Term
68+
</declaration> <declaration>
69+
symbol ex_intro4 ( .Sorts ) : Term
70+
</declaration> <declaration>
71+
symbol iff ( .Sorts ) : Term
72+
</declaration> <declaration>
73+
symbol nat ( .Sorts ) : Term
74+
</declaration> <declaration>
75+
symbol not ( .Sorts ) : Term
76+
</declaration> <declaration>
77+
symbol or ( .Sorts ) : Term
78+
</declaration> <declaration>
79+
symbol or_introl ( .Sorts ) : Term
80+
</declaration> <declaration>
81+
symbol or_intror ( .Sorts ) : Term
82+
</declaration>
83+
</declarations>
84+
</prover>

‎prover/t/Or.v

Lines changed: 0 additions & 3 deletions
This file was deleted.

‎prover/t/nat_ind.v.expected

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<prover>
2+
<k>
3+
.CoqSentences
4+
</k>
5+
<exit-code>
6+
1
7+
</exit-code>
8+
<goals>
9+
.GoalCellSet
10+
</goals>
11+
<declarations>
12+
<declaration>
13+
axiom \equals ( nat_ind , \lambda { P { Term } , f { Term } , f0 { Term } , .Patterns } \mu { F {{ Term }} , .Patterns } \lambda { n { Term } , .Patterns } \or ( \exists { .Patterns } \and ( \equals ( n , Z ) , f , .Patterns ) , \exists { n0 , .Patterns } \and ( \equals ( n , S ( n0 , .Patterns ) ) , f0 ( n0 , F , n0 , .Patterns ) , .Patterns ) , .Patterns ) )
14+
</declaration> <declaration>
15+
axiom \type ( S ( .Patterns ) , \forall { x { Term } , .Patterns } nat )
16+
</declaration> <declaration>
17+
axiom \type ( Z ( .Patterns ) , nat )
18+
</declaration> <declaration>
19+
sort Term
20+
</declaration> <declaration>
21+
symbol S ( .Sorts ) : Term
22+
</declaration> <declaration>
23+
symbol Z ( .Sorts ) : Term
24+
</declaration> <declaration>
25+
symbol nat ( .Sorts ) : Term
26+
</declaration> <declaration>
27+
symbol nat_ind ( .Sorts ) : Term
28+
</declaration>
29+
</declarations>
30+
</prover>

0 commit comments

Comments
 (0)