miz3/Samples/robbins.ml

   1 (* ======== Robbins Conjecture proof from John ============================= *)
   2
   3 hide_constant "+";;
   4 horizon := 0;;
   5 timeout := 2;; (* John apparently has a faster computer :-) *)
   6
   7 let ROBBINS = thm `;
   8
   9   let (+) be A->A->A;
  10   let n be A->A;
  11
  12   assume !x y. x+y = y+x [COM];
  13   assume !x y z. x+(y+z) = (x+y)+z [ASS];
  14   assume !a b. n(n(a+b)+n(a+n(b))) = a [ROB];
  15
  16   consider x such that x:A = x;
  17
  18   set u = n(x+n(x)) [U];
  19   set d = x+u [D];
  20   set c = x+x+x+u [C];
  21   set j = n(c+d) [J];
  22   set e = u+n(x+x)+n(c) [E];
  23
  24   n(u+n(x+x)) = x [0]
  25   proof n(u+n(x+x))
  26       = n(n(x+n(x))+n(x+x)) by U;
  27      .= x by ROB,COM;
  28   qed by -;
  29
  30   n(x+u+n(x+u+n(x+x)+n(c))) = n(c) [1]
  31   proof n(x+u+n(x+u+n(x+x)+n(c)))
  32       = n((x+u)+n(x+u+n(x+x)+n(c))) by ASS,COM;
  33      .= n(n(n((x+u)+x+x)+n((x+u)+n(x+x)))+n(x+u+n(x+x)+n(c))) by ROB;
  34      .= n(n(n(x+u+x+x)+n(x+u+n(x+x)))+n(x+u+n(x+x)+n(c))) by ASS;
  35      .= n(n(n(x+x+x+u)+n(x+u+n(x+x)))+n(x+u+n(x+x)+n(c))) by ASS,COM; // slow
  36      .= n(n(n(c)+n(x+u+n(x+x)))+n(n(c)+x+u+n(x+x))) by ASS,COM,C;
  37      .= n(c) by ROB,ASS,COM;
  38   qed by -;
  39
  40   n(u+n(c)) = x [2]
  41   proof n(u+n(c))
  42       = n(u+n(x+x+u+x)) by C,ASS,COM;
  43      .= n(u+n(x+x+u+n(u+n(x+x)))) by 0;
  44      .= n(n(n(u+x+x)+n(u+n(x+x)))+n(x+x+u+n(u+n(x+x)))) by ROB;
  45      .= n(n(x+x+u+n(u+n(x+x)))+n(n(u+x+x)+n(u+n(x+x)))) by COM;
  46      .= n(n((x+x+u)+n(u+n(x+x)))+n(n(u+x+x)+n(u+n(x+x)))) by ASS;
  47      .= n(n(n(u+n(x+x))+u+x+x)+n(n(u+n(x+x))+n(u+x+x))) by ASS,COM;
  48      .= n(u+n(x+x)) by ROB;
  49      .= x by 0;
  50   qed by -;
  51
  52   n(j+u) = x [3]
  53   proof n(j+u)
  54       = n(n(x+c+u)+u) by J,D,COM,ASS;
  55      .= n(n(x+c+u)+n(n(u+c)+n(u+n(c)))) by ROB;
  56      .= n(n(x+c+u)+n(x+n(c+u))) by 2,COM;
  57      .= x by ROB;
  58   qed by -;
  59
  60   n(x+n(x+n(x+x)+u+n(c))) = n(x+x) [4]
  61   proof n(x+n(x+n(x+x)+u+n(c)))
  62       = n(n(n(x+n(u+n(c)))+n(x+u+n(c)))+n(x+n(x+x)+u+n(c)))
  63             by ROB,ASS,COM;
  64      .= n(n(n(x+x)+n(x+u+n(c)))+n(n(x+x)+x+u+n(c))) by 2,ASS,COM;
  65      .= n(n(n(x+x)+x+u+n(c))+n(n(x+x)+n(x+u+n(c)))) by ASS,COM;
  66      .= n(x+x) by ROB,COM;
  67   qed by -;
  68
  69   n(x+n(c)) = u [5]
  70   proof n(x+n(c))
  71       = n(x+n(x+u+n(x+u+n(x+x)+n(c)))) by 1;
  72      .= n(n(u+n(x+x))+n(x+u+n(x+u+n(x+x)+n(c)))) by 0;
  73      .= n(n(u+n(x+x))+n(u+x+n(x+e))) by E,COM,ASS;
  74      .= n(n(u+n(x+n(x+n(x+x)+u+n(c))))+n(u+x+n(x+e))) by 4;
  75      .= n(n(u+n(x+n(x+(u+n(c))+n(x+x))))+n(u+x+n(x+e))) by COM;
  76      .= n(n(u+n(x+n(x+u+n(c)+n(x+x))))+n(u+x+n(x+e))) by ASS;
  77      .= n(n(u+n(x+n(x+u+n(x+x)+n(c))))+n(u+x+n(x+e))) by COM;
  78      .= n(n(u+n(x+n(x+e)))+n(u+x+n(x+e))) by E;
  79      .= u by ROB,COM;
  80   qed by -;
  81
  82   n(j+x) = u [6]
  83   proof n(j+x)
  84       = n(j+n(n(x+c)+n(x+n(c)))) by ROB;
  85      .= n(j+n(n(x+c)+u)) by 5;
  86      .= n(n(u+x+c)+n(u+n(x+c))) by J,D,COM,ASS;
  87      .= u by ROB;
  88   qed by -;
  89
  90   n(c+d) = n(c)
  91   proof n(c+d)
  92       = j by J;
  93      .= n(n(j+n(x+n(c)))+n(j+x+n(c))) by ROB,COM;
  94      .= n(n(j+u)+n(j+x+n(c))) by 5;
  95      .= n(x+n(j+x+n(c))) by 3;
  96      .= n(n(n(c)+u)+n(n(c)+j+x)) by 2,COM,ASS;
  97      .= n(n(n(c)+n(j+x))+n(n(c)+j+x)) by 6;
  98      .= n(c) by ROB,COM;
  99   qed by -;
 100
 101   thus ?c d. n(c+d) = n(c) by -`;;
 102
 103 timeout := 1;;
 104
 105 (* ======== REWRITE version ================================================ *)
 106
 107 let old_default_prover = !default_prover;;
 108 default_prover := "REWRITE_TAC",REWRITE_TAC;;
 109
 110 let ROBBINS = thm `;
 111
 112   let (+) be A->A->A;
 113   let n be A->A;
 114
 115   assume !x y. x+y = y+x [COM];
 116   assume !x y z. x+(y+z) = (x+y)+z [ASS];
 117   assume !a b. n(n(a+b)+n(a+n(b))) = a [ROB];
 118
 119   !x y z. x+y = y+x /\ (x+y)+z = x+(y+z) /\ x+(y+z) = y+(x+z) [AC]
 120     by MESON_TAC,COM,ASS;
 121
 122   consider x such that x:A = x;
 123
 124   set u = n(x+n(x)) [U];
 125   set d = x+u [D];
 126   set c = x+x+x+u [C];
 127   set j = n(c+d) [J];
 128   set e = u+n(x+x)+n(c) [E];
 129
 130   n(u+n(x+x)) = x [0]
 131   proof n(u+n(x+x))
 132       = n(n(x+x)+n(x+n(x))) by U,AC;
 133      .= x by ROB;
 134   qed by -;
 135
 136   n(x+u+n(x+u+n(x+x)+n(c))) = n(c) [1]
 137   proof n(x+u+n(x+u+n(x+x)+n(c)))
 138       = n((x+u)+n(x+u+n(x+x)+n(c))) by AC;
 139      .= n(n(n((x+u)+x+x)+n((x+u)+n(x+x)))+n(x+u+n(x+x)+n(c))) by ROB;
 140      .= n(n(n(c)+x+u+n(x+x))+n(n(c)+n(x+u+n(x+x)))) by C,AC;
 141      .= n(c) by ROB;
 142   qed by -;
 143
 144   n(u+n(c)) = x [2]
 145   proof n(u+n(c))
 146       = n(u+n(x+x+u+n(u+n(x+x)))) by 0,C,AC;
 147      .= n(n(n(u+x+x)+n(u+n(x+x)))+n(x+x+u+n(u+n(x+x)))) by ROB;
 148      .= n(n(n(u+n(x+x))+u+x+x)+n(n(u+n(x+x))+n(u+x+x))) by AC;
 149      .= n(u+n(x+x)) by ROB;
 150      .= x by 0;
 151   qed by -;
 152
 153   n(j+u) = x [3]
 154   proof n(j+u)
 155       = n(n(x+c+u)+u) by J,D,AC;
 156      .= n(n(x+c+u)+n(n(u+c)+n(u+n(c)))) by ROB;
 157      .= n(n(x+c+u)+n(x+n(c+u))) by 2,AC;
 158      .= x by ROB;
 159   qed by -;
 160
 161   n(x+n(x+n(x+x)+u+n(c))) = n(x+x) [4]
 162   proof n(x+n(x+n(x+x)+u+n(c)))
 163       = n(n(n(x+u+n(c))+n(x+n(u+n(c))))+n(x+n(x+x)+u+n(c))) by ROB;
 164      .= n(n(n(x+x)+x+u+n(c))+n(n(x+x)+n(x+u+n(c)))) by 2,AC;
 165      .= n(x+x) by ROB;
 166   qed by -;
 167
 168   n(x+n(c)) = u [5]
 169   proof n(x+n(c))
 170       = n(n(u+n(x+x))+n(x+u+n(x+u+n(x+x)+n(c)))) by 0,1;
 171      .= n(n(u+n(x+n(x+n(x+x)+u+n(c))))+n(u+x+n(x+e))) by 4,E,AC;
 172      .= n(n(u+x+n(x+e))+n(u+n(x+n(x+e)))) by E,AC;
 173      .= u by ROB;
 174   qed by -;
 175
 176   n(j+x) = u [6]
 177   proof n(j+x)
 178       = n(j+n(n(x+c)+n(x+n(c)))) by ROB;
 179      .= n(n(u+x+c)+n(u+n(x+c))) by 5,J,D,AC;
 180      .= u by ROB;
 181   qed by -;
 182
 183   n(c+d) = n(c)
 184   proof n(c+d)
 185       = j by J;
 186      .= n(n(j+x+n(c))+n(j+n(x+n(c)))) by ROB;
 187      .= n(n(u+n(c))+n(j+x+n(c))) by 2,3,5,AC;
 188      .= n(n(n(c)+j+x)+n(n(c)+n(j+x))) by 6,AC;
 189      .= n(c) by ROB;
 190   qed by -;
 191
 192   thus ?c d. n(c+d) = n(c) by MESON_TAC,-`;;
 193
 194 unhide_constant "+";;
 195 default_prover := old_default_prover;;
 196