src/Sequents/LK/hardquant.ML
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 7119 02d94b69ae04
permissions -rw-r--r--
converted to Isar theory format;
wenzelm@6252
     1
(*  Title:      LK/ex/hard-quant
wenzelm@6252
     2
    ID:         $Id$
wenzelm@6252
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@6252
     4
    Copyright   1992  University of Cambridge
wenzelm@6252
     5
wenzelm@6252
     6
Hard examples with quantifiers.  Can be read to test the LK system.
wenzelm@6252
     7
From  F. J. Pelletier,
wenzelm@6252
     8
  Seventy-Five Problems for Testing Automatic Theorem Provers,
wenzelm@6252
     9
  J. Automated Reasoning 2 (1986), 191-216.
wenzelm@6252
    10
  Errata, JAR 4 (1988), 236-236.
wenzelm@6252
    11
wenzelm@6252
    12
Uses pc_tac rather than fast_tac when the former is significantly faster.
wenzelm@6252
    13
*)
wenzelm@6252
    14
wenzelm@17481
    15
context (theory "LK");
paulson@7119
    16
paulson@7119
    17
Goal "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
paulson@7119
    18
by (Fast_tac 1);
wenzelm@17481
    19
result();
wenzelm@6252
    20
paulson@7119
    21
Goal "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
paulson@7119
    22
by (Fast_tac 1);
wenzelm@17481
    23
result();
wenzelm@6252
    24
paulson@7119
    25
Goal "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
paulson@7119
    26
by (Fast_tac 1);
wenzelm@17481
    27
result();
wenzelm@6252
    28
paulson@7119
    29
Goal "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
paulson@7119
    30
by (Fast_tac 1);
wenzelm@17481
    31
result();
wenzelm@6252
    32
wenzelm@6252
    33
writeln"Problems requiring quantifier duplication";
wenzelm@6252
    34
paulson@7119
    35
(*Not provable by Fast_tac: needs multiple instantiation of ALL*)
paulson@7119
    36
Goal "|- (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
wenzelm@6252
    37
by (best_tac LK_dup_pack 1);
wenzelm@6252
    38
result();
wenzelm@6252
    39
wenzelm@6252
    40
(*Needs double instantiation of the quantifier*)
paulson@7119
    41
Goal "|- EX x. P(x) --> P(a) & P(b)";
wenzelm@6252
    42
by (fast_tac LK_dup_pack 1);
wenzelm@6252
    43
result();
wenzelm@6252
    44
paulson@7119
    45
Goal "|- EX z. P(z) --> (ALL x. P(x))";
wenzelm@6252
    46
by (best_tac LK_dup_pack 1);
wenzelm@6252
    47
result();
wenzelm@6252
    48
wenzelm@6252
    49
writeln"Hard examples with quantifiers";
wenzelm@6252
    50
wenzelm@6252
    51
writeln"Problem 18";
paulson@7119
    52
Goal "|- EX y. ALL x. P(y)-->P(x)";
wenzelm@6252
    53
by (best_tac LK_dup_pack 1);
wenzelm@17481
    54
result();
wenzelm@6252
    55
wenzelm@6252
    56
writeln"Problem 19";
paulson@7119
    57
Goal "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
wenzelm@6252
    58
by (best_tac LK_dup_pack 1);
wenzelm@6252
    59
result();
wenzelm@6252
    60
wenzelm@6252
    61
writeln"Problem 20";
paulson@7119
    62
Goal "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
wenzelm@6252
    63
\   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
wenzelm@17481
    64
by (Fast_tac 1);
wenzelm@6252
    65
result();
wenzelm@6252
    66
wenzelm@6252
    67
writeln"Problem 21";
paulson@7119
    68
Goal "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
wenzelm@6252
    69
by (best_tac LK_dup_pack 1);
wenzelm@6252
    70
result();
wenzelm@6252
    71
wenzelm@6252
    72
writeln"Problem 22";
paulson@7119
    73
Goal "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
wenzelm@17481
    74
by (Fast_tac 1);
wenzelm@6252
    75
result();
wenzelm@6252
    76
wenzelm@6252
    77
writeln"Problem 23";
paulson@7119
    78
Goal "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
wenzelm@17481
    79
by (best_tac LK_pack 1);
wenzelm@6252
    80
result();
wenzelm@6252
    81
wenzelm@6252
    82
writeln"Problem 24";
paulson@7119
    83
Goal "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
wenzelm@6252
    84
\    ~(EX x. P(x)) --> (EX x. Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
wenzelm@6252
    85
\   --> (EX x. P(x)&R(x))";
wenzelm@6252
    86
by (pc_tac LK_pack 1);
wenzelm@6252
    87
result();
wenzelm@6252
    88
wenzelm@6252
    89
writeln"Problem 25";
paulson@7119
    90
Goal "|- (EX x. P(x)) &  \
wenzelm@6252
    91
\       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
wenzelm@6252
    92
\       (ALL x. P(x) --> (M(x) & L(x))) &   \
wenzelm@6252
    93
\       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
wenzelm@6252
    94
\   --> (EX x. Q(x)&P(x))";
wenzelm@17481
    95
by (best_tac LK_pack 1);
wenzelm@6252
    96
result();
wenzelm@6252
    97
wenzelm@6252
    98
writeln"Problem 26";
paulson@7119
    99
Goal "|- ((EX x. p(x)) <-> (EX x. q(x))) &       \
wenzelm@6252
   100
\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
wenzelm@6252
   101
\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
wenzelm@6252
   102
by (pc_tac LK_pack 1);
wenzelm@6252
   103
result();
wenzelm@6252
   104
wenzelm@6252
   105
writeln"Problem 27";
paulson@7119
   106
Goal "|- (EX x. P(x) & ~Q(x)) &   \
wenzelm@6252
   107
\             (ALL x. P(x) --> R(x)) &   \
wenzelm@6252
   108
\             (ALL x. M(x) & L(x) --> P(x)) &   \
wenzelm@6252
   109
\             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
wenzelm@6252
   110
\         --> (ALL x. M(x) --> ~L(x))";
wenzelm@17481
   111
by (pc_tac LK_pack 1);
wenzelm@6252
   112
result();
wenzelm@6252
   113
wenzelm@6252
   114
writeln"Problem 28.  AMENDED";
paulson@7119
   115
Goal "|- (ALL x. P(x) --> (ALL x. Q(x))) &   \
wenzelm@6252
   116
\       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
wenzelm@6252
   117
\       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
wenzelm@6252
   118
\   --> (ALL x. P(x) & L(x) --> M(x))";
wenzelm@17481
   119
by (pc_tac LK_pack 1);
wenzelm@6252
   120
result();
wenzelm@6252
   121
wenzelm@6252
   122
writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
paulson@7119
   123
Goal "|- (EX x. P(x)) & (EX y. Q(y))  \
wenzelm@6252
   124
\   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
wenzelm@6252
   125
\        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
wenzelm@17481
   126
by (pc_tac LK_pack 1);
wenzelm@6252
   127
result();
wenzelm@6252
   128
wenzelm@6252
   129
writeln"Problem 30";
paulson@7119
   130
Goal "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \
wenzelm@6252
   131
\       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
wenzelm@6252
   132
\   --> (ALL x. S(x))";
wenzelm@17481
   133
by (Fast_tac 1);
wenzelm@6252
   134
result();
wenzelm@6252
   135
wenzelm@6252
   136
writeln"Problem 31";
paulson@7119
   137
Goal "|- ~(EX x. P(x) & (Q(x) | R(x))) & \
wenzelm@6252
   138
\       (EX x. L(x) & P(x)) & \
wenzelm@6252
   139
\       (ALL x. ~ R(x) --> M(x))  \
wenzelm@6252
   140
\   --> (EX x. L(x) & M(x))";
paulson@7119
   141
by (Fast_tac 1);
wenzelm@6252
   142
result();
wenzelm@6252
   143
wenzelm@6252
   144
writeln"Problem 32";
paulson@7119
   145
Goal "|- (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
wenzelm@6252
   146
\       (ALL x. S(x) & R(x) --> L(x)) & \
wenzelm@6252
   147
\       (ALL x. M(x) --> R(x))  \
wenzelm@6252
   148
\   --> (ALL x. P(x) & M(x) --> L(x))";
wenzelm@6252
   149
by (best_tac LK_pack 1);
wenzelm@6252
   150
result();
wenzelm@6252
   151
wenzelm@6252
   152
writeln"Problem 33";
paulson@7119
   153
Goal "|- (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
wenzelm@6252
   154
\    (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
paulson@7119
   155
by (Fast_tac 1);
wenzelm@6252
   156
result();
wenzelm@6252
   157
paulson@7119
   158
writeln"Problem 34  AMENDED (TWICE!!)";
wenzelm@6252
   159
(*Andrews's challenge*)
paulson@7119
   160
Goal "|- ((EX x. ALL y. p(x) <-> p(y))  <->              \
wenzelm@6252
   161
\              ((EX x. q(x)) <-> (ALL y. p(y))))     <->        \
wenzelm@6252
   162
\             ((EX x. ALL y. q(x) <-> q(y))  <->                \
wenzelm@6252
   163
\              ((EX x. p(x)) <-> (ALL y. q(y))))";
paulson@7119
   164
by (best_tac LK_dup_pack 1); (*10 secs!*)
wenzelm@6252
   165
result();
wenzelm@6252
   166
wenzelm@6252
   167
wenzelm@6252
   168
writeln"Problem 35";
paulson@7119
   169
Goal "|- EX x y. P(x,y) -->  (ALL u v. P(u,v))";
paulson@7119
   170
by (best_tac LK_dup_pack 1);
wenzelm@6252
   171
result();
wenzelm@6252
   172
wenzelm@6252
   173
writeln"Problem 36";
paulson@7119
   174
Goal "|- (ALL x. EX y. J(x,y)) & \
paulson@7119
   175
\        (ALL x. EX y. G(x,y)) & \
paulson@7119
   176
\        (ALL x y. J(x,y) | G(x,y) -->   \
paulson@7119
   177
\        (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
paulson@7119
   178
\        --> (ALL x. EX y. H(x,y))";
paulson@7119
   179
by (Fast_tac 1);
wenzelm@6252
   180
result();
wenzelm@6252
   181
wenzelm@6252
   182
writeln"Problem 37";
paulson@7119
   183
Goal "|- (ALL z. EX w. ALL x. EX y. \
wenzelm@6252
   184
\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
wenzelm@6252
   185
\       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
wenzelm@6252
   186
\       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
wenzelm@6252
   187
\   --> (ALL x. EX y. R(x,y))";
wenzelm@6252
   188
by (pc_tac LK_pack 1);
wenzelm@6252
   189
result();
wenzelm@6252
   190
wenzelm@6252
   191
writeln"Problem 38";
paulson@7119
   192
Goal "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
paulson@7119
   193
\                (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->         \
paulson@7119
   194
\        (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
paulson@7119
   195
\                (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
paulson@7119
   196
\                (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
wenzelm@6252
   197
by (pc_tac LK_pack 1);
wenzelm@6252
   198
result();
wenzelm@6252
   199
wenzelm@6252
   200
writeln"Problem 39";
paulson@7119
   201
Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
paulson@7119
   202
by (Fast_tac 1);
wenzelm@6252
   203
result();
wenzelm@6252
   204
wenzelm@6252
   205
writeln"Problem 40.  AMENDED";
paulson@7119
   206
Goal "|- (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
paulson@7119
   207
\        ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
paulson@7119
   208
by (Fast_tac 1);
wenzelm@6252
   209
result();
wenzelm@6252
   210
wenzelm@6252
   211
writeln"Problem 41";
paulson@7119
   212
Goal "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))      \
paulson@7119
   213
\        --> ~ (EX z. ALL x. f(x,z))";
paulson@7119
   214
by (Fast_tac 1);
wenzelm@6252
   215
result();
wenzelm@6252
   216
wenzelm@6252
   217
writeln"Problem 42";
paulson@7119
   218
Goal "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))";
wenzelm@6252
   219
wenzelm@6252
   220
writeln"Problem 43  NOT PROVED AUTOMATICALLY";
paulson@7119
   221
Goal "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \
wenzelm@6252
   222
\         --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))";
wenzelm@6252
   223
wenzelm@6252
   224
writeln"Problem 44";
paulson@7119
   225
Goal "|- (ALL x. f(x) -->                                        \
paulson@7119
   226
\                (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
paulson@7119
   227
\        (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
paulson@7119
   228
\        --> (EX x. j(x) & ~f(x))";
paulson@7119
   229
by (Fast_tac 1);
wenzelm@6252
   230
result();
wenzelm@6252
   231
wenzelm@6252
   232
writeln"Problem 45";
paulson@7119
   233
Goal "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))        \
wenzelm@6252
   234
\                     --> (ALL y. g(y) & h(x,y) --> k(y))) &    \
wenzelm@6252
   235
\     ~ (EX y. l(y) & k(y)) &                                   \
wenzelm@6252
   236
\     (EX x. f(x) & (ALL y. h(x,y) --> l(y))                    \
wenzelm@6252
   237
\                  & (ALL y. g(y) & h(x,y) --> j(x,y)))         \
wenzelm@6252
   238
\     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
wenzelm@17481
   239
by (best_tac LK_pack 1);
wenzelm@6252
   240
result();
wenzelm@6252
   241
wenzelm@6252
   242
paulson@7119
   243
writeln"Problems (mainly) involving equality or functions";
paulson@7119
   244
paulson@7119
   245
writeln"Problem 48";
paulson@7119
   246
Goal "|- (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
paulson@7119
   247
by (fast_tac (pack() add_safes [subst]) 1);
paulson@7119
   248
result();
paulson@7119
   249
wenzelm@17481
   250
writeln"Problem 50";
paulson@7119
   251
Goal "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
wenzelm@6252
   252
by (best_tac LK_dup_pack 1);
wenzelm@6252
   253
result();
wenzelm@6252
   254
paulson@7119
   255
writeln"Problem 51";
paulson@7119
   256
Goal "|- (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
paulson@7119
   257
\        (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)";
paulson@7119
   258
by (fast_tac (pack() add_safes [subst]) 1);
paulson@7119
   259
result();
paulson@7119
   260
paulson@7119
   261
writeln"Problem 52";
paulson@7119
   262
(*Almost the same as 51. *)
paulson@7119
   263
Goal "|- (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
paulson@7119
   264
\        (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)";
paulson@7119
   265
by (fast_tac (pack() add_safes [subst]) 1);
paulson@7119
   266
result();
paulson@7119
   267
paulson@7119
   268
writeln"Problem 56";
paulson@7119
   269
Goal "|- (ALL x.(EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
paulson@7119
   270
by (best_tac (pack() add_unsafes [symL, subst]) 1);
paulson@7119
   271
(*requires tricker to orient the equality properly*)
paulson@7119
   272
result();
paulson@7119
   273
wenzelm@6252
   274
writeln"Problem 57";
paulson@7119
   275
Goal "|- P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
paulson@7119
   276
\        (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
paulson@7119
   277
by (Fast_tac 1);
paulson@7119
   278
result();
paulson@7119
   279
paulson@7119
   280
writeln"Problem 58!";
paulson@7119
   281
Goal "|- (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
paulson@7119
   282
by (fast_tac (pack() add_safes [subst]) 1);
wenzelm@6252
   283
result();
wenzelm@6252
   284
wenzelm@6252
   285
writeln"Problem 59";
wenzelm@6252
   286
(*Unification works poorly here -- the abstraction %sobj prevents efficient
wenzelm@6252
   287
  operation of the occurs check*)
wenzelm@17481
   288
Unify.trace_bound := !Unify.search_bound - 1;
paulson@7119
   289
Goal "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
wenzelm@6252
   290
by (best_tac LK_dup_pack 1);
wenzelm@6252
   291
result();
wenzelm@6252
   292
wenzelm@6252
   293
writeln"Problem 60";
paulson@7119
   294
Goal "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
paulson@7119
   295
by (Fast_tac 1);
paulson@7119
   296
result();
paulson@7119
   297
paulson@7119
   298
writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
paulson@7119
   299
Goal "|- (ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->     \
paulson@7119
   300
\     (ALL x. (~p(a) | p(x) | p(f(f(x)))) &                      \
paulson@7119
   301
\             (~p(a) | ~p(f(x)) | p(f(f(x)))))";
paulson@7119
   302
by (Fast_tac 1);
wenzelm@6252
   303
result();
wenzelm@6252
   304
wenzelm@6252
   305
(*18 June 92: loaded in 372 secs*)
wenzelm@6252
   306
(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
wenzelm@6252
   307
(*29 June 92: loaded in 370 secs*)
wenzelm@17481
   308
(*18 September 2005: loaded in 1.809 secs*)