src/Tests/Cube.hs

   1 module Tests.Cube
   2 where
   3
   4 import Prelude hiding (LT)
   5
   6 import Cardinal
   7 import Comparisons
   8 import Cube hiding (i, j, k)
   9 import FunctionValues
  10 import Misc (all_equal)
  11 import Tests.FunctionValues ()
  12 import Tetrahedron (b0, b1, b2, b3, c, fv,
  13                     v0, v1, v2, v3, volume)
  14
  15
  16
  17 -- Quickcheck tests.
  18
  19 -- | Since the grid size is necessarily positive, all tetrahedra
  20 --   (which comprise cubes of positive volume) must have positive volume
  21 --   as well.
  22 prop_all_volumes_positive :: Cube -> Bool
  23 prop_all_volumes_positive cube =
  24     null nonpositive_volumes
  25     where
  26       ts = tetrahedra cube
  27       volumes = map volume ts
  28       nonpositive_volumes = filter (<= 0) volumes
  29
  30 -- | In fact, since all of the tetrahedra are identical, we should
  31 --   already know their volumes. There's 24 tetrahedra to a cube, so
  32 --   we'd expect the volume of each one to be (1/24)*h^3.
  33 prop_all_volumes_exact :: Cube -> Bool
  34 prop_all_volumes_exact cube =
  35     and [volume t ~~= (1/24)*(delta^(3::Int)) | t <- tetrahedra cube]
  36     where
  37       delta = h cube
  38
  39 -- | All tetrahedron should have their v0 located at the center of the cube.
  40 prop_v0_all_equal :: Cube -> Bool
  41 prop_v0_all_equal cube = (v0 t0) == (v0 t1)
  42     where
  43       t0 = head (tetrahedra cube) -- Doesn't matter which two we choose.
  44       t1 = head $ tail (tetrahedra cube)
  45
  46
  47 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Note that the
  48 --   third and fourth indices of c-t1 have been switched. This is
  49 --   because we store the triangles oriented such that their volume is
  50 --   positive. If T and T-tilde share \<v0,v1,v2\> and v3,v3-tilde point
  51 --   in opposite directions, one of them has to have negative volume!
  52 prop_c0120_identity1 :: Cube -> Bool
  53 prop_c0120_identity1 cube =
  54    c t0 0 1 2 0 ~= (c t0 0 0 2 1 + c t3 0 0 1 2) / 2
  55      where
  56        t0 = tetrahedron0 cube
  57        t3 = tetrahedron3 cube
  58
  59
  60 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
  61 --   'prop_c0120_identity1' with tetrahedrons 1 and 2.
  62 prop_c0120_identity2 :: Cube -> Bool
  63 prop_c0120_identity2 cube =
  64    c t1 0 1 2 0 ~= (c t1 0 0 2 1 + c t0 0 0 1 2) / 2
  65      where
  66        t0 = tetrahedron0 cube
  67        t1 = tetrahedron1 cube
  68
  69 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
  70 --   'prop_c0120_identity1' with tetrahedrons 1 and 2.
  71 prop_c0120_identity3 :: Cube -> Bool
  72 prop_c0120_identity3 cube =
  73    c t2 0 1 2 0 ~= (c t2 0 0 2 1 + c t1 0 0 1 2) / 2
  74      where
  75        t1 = tetrahedron1 cube
  76        t2 = tetrahedron2 cube
  77
  78 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
  79 --   'prop_c0120_identity1' with tetrahedrons 2 and 3.
  80 prop_c0120_identity4 :: Cube -> Bool
  81 prop_c0120_identity4 cube =
  82    c t3 0 1 2 0 ~= (c t3 0 0 2 1 + c t2 0 0 1 2) / 2
  83      where
  84        t2 = tetrahedron2 cube
  85        t3 = tetrahedron3 cube
  86
  87
  88 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
  89 --   'prop_c0120_identity1' with tetrahedrons 4 and 5.
  90 prop_c0120_identity5 :: Cube -> Bool
  91 prop_c0120_identity5 cube =
  92     c t5 0 1 2 0 ~= (c t5 0 0 2 1 + c t4 0 0 1 2) / 2
  93     where
  94       t4 = tetrahedron4 cube
  95       t5 = tetrahedron5 cube
  96
  97 -- -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
  98 -- --   'prop_c0120_identity1' with tetrahedrons 5 and 6.
  99 prop_c0120_identity6 :: Cube -> Bool
 100 prop_c0120_identity6 cube =
 101    c t6 0 1 2 0 ~= (c t6 0 0 2 1 + c t5 0 0 1 2) / 2
 102      where
 103        t5 = tetrahedron5 cube
 104        t6 = tetrahedron6 cube
 105
 106
 107 -- -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
 108 -- --   'prop_c0120_identity1' with tetrahedrons 6 and 7.
 109 prop_c0120_identity7 :: Cube -> Bool
 110 prop_c0120_identity7 cube =
 111    c t7 0 1 2 0 ~= (c t7 0 0 2 1 + c t6 0 0 1 2) / 2
 112      where
 113        t6 = tetrahedron6 cube
 114        t7 = tetrahedron7 cube
 115
 116
 117 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). See
 118 --   'prop_c0120_identity1'.
 119 prop_c0210_identity1 :: Cube -> Bool
 120 prop_c0210_identity1 cube =
 121     c t0 0 2 1 0 ~= (c t0 0 1 1 1 + c t3 0 1 1 1) / 2
 122       where
 123         t0 = tetrahedron0 cube
 124         t3 = tetrahedron3 cube
 125
 126
 127 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). See
 128 --   'prop_c0120_identity1'.
 129 prop_c0300_identity1 :: Cube -> Bool
 130 prop_c0300_identity1 cube =
 131     c t0 0 3 0 0 ~= (c t0 0 2 0 1 + c t3 0 2 1 0) / 2
 132       where
 133         t0 = tetrahedron0 cube
 134         t3 = tetrahedron3 cube
 135
 136
 137 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). See
 138 --   'prop_c0120_identity1'.
 139 prop_c1110_identity :: Cube -> Bool
 140 prop_c1110_identity cube =
 141     c t0 1 1 1 0 ~= (c t0 1 0 1 1 + c t3 1 0 1 1) / 2
 142       where
 143         t0 = tetrahedron0 cube
 144         t3 = tetrahedron3 cube
 145
 146
 147 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). See
 148 --   'prop_c0120_identity1'.
 149 prop_c1200_identity1 :: Cube -> Bool
 150 prop_c1200_identity1 cube =
 151     c t0 1 2 0 0 ~= (c t0 1 1 0 1 + c t3 1 1 1 0) / 2
 152       where
 153         t0 = tetrahedron0 cube
 154         t3 = tetrahedron3 cube
 155
 156
 157 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). See
 158 --   'prop_c0120_identity1'.
 159 prop_c2100_identity1 :: Cube -> Bool
 160 prop_c2100_identity1 cube =
 161     c t0 2 1 0 0 ~= (c t0 2 0 0 1 + c t3 2 0 1 0) / 2
 162       where
 163         t0 = tetrahedron0 cube
 164         t3 = tetrahedron3 cube
 165
 166
 167
 168 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). Note that the
 169 --   third and fourth indices of c-t3 have been switched. This is
 170 --   because we store the triangles oriented such that their volume is
 171 --   positive. If T and T-tilde share \<v0,v1,v2\> and v3,v3-tilde
 172 --   point in opposite directions, one of them has to have negative
 173 --   volume!
 174 prop_c0102_identity1 :: Cube -> Bool
 175 prop_c0102_identity1 cube =
 176     c t0 0 1 0 2 ~= (c t0 0 0 1 2 + c t1 0 0 2 1) / 2
 177       where
 178         t0 = tetrahedron0 cube
 179         t1 = tetrahedron1 cube
 180
 181
 182 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). See
 183 --   'prop_c0102_identity1'.
 184 prop_c0201_identity1 :: Cube -> Bool
 185 prop_c0201_identity1 cube =
 186     c t0 0 2 0 1 ~= (c t0 0 1 1 1 + c t1 0 1 1 1) / 2
 187       where
 188         t0 = tetrahedron0 cube
 189         t1 = tetrahedron1 cube
 190
 191
 192 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). See
 193 --   'prop_c0102_identity1'.
 194 prop_c0300_identity2 :: Cube -> Bool
 195 prop_c0300_identity2 cube =
 196     c t0 0 3 0 0 ~= (c t0 0 2 1 0 + c t1 0 2 0 1) / 2
 197       where
 198         t0 = tetrahedron0 cube
 199         t1 = tetrahedron1 cube
 200
 201
 202 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). See
 203 --   'prop_c0102_identity1'.
 204 prop_c1101_identity :: Cube -> Bool
 205 prop_c1101_identity cube =
 206     c t0 1 1 0 1 ~= (c t0 1 0 1 1 + c t1 1 0 1 1) / 2
 207       where
 208         t0 = tetrahedron0 cube
 209         t1 = tetrahedron1 cube
 210
 211
 212 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). See
 213 --   'prop_c0102_identity1'.
 214 prop_c1200_identity2 :: Cube -> Bool
 215 prop_c1200_identity2 cube =
 216     c t0 1 2 0 0 ~= (c t0 1 1 1 0 + c t1 1 1 0 1) / 2
 217       where
 218         t0 = tetrahedron0 cube
 219         t1 = tetrahedron1 cube
 220
 221
 222 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). See
 223 --   'prop_c0102_identity1'.
 224 prop_c2100_identity2 :: Cube -> Bool
 225 prop_c2100_identity2 cube =
 226     c t0 2 1 0 0 ~= (c t0 2 0 1 0 + c t1 2 0 0 1) / 2
 227       where
 228         t0 = tetrahedron0 cube
 229         t1 = tetrahedron1 cube
 230
 231
 232 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). The third and
 233 --   fourth indices of c-t6 have been switched. This is because we
 234 --   store the triangles oriented such that their volume is
 235 --   positive. If T and T-tilde share \<v0,v1,v2\> and v3,v3-tilde
 236 --   point in opposite directions, one of them has to have negative
 237 --   volume!
 238 prop_c3000_identity :: Cube -> Bool
 239 prop_c3000_identity cube =
 240     c t0 3 0 0 0 ~= c t0 2 1 0 0 + c t6 2 1 0 0
 241                     - ((c t0 2 0 1 0 + c t0 2 0 0 1)/ 2)
 242       where
 243         t0 = tetrahedron0 cube
 244         t6 = tetrahedron6 cube
 245
 246
 247 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). See
 248 --   'prop_c3000_identity'.
 249 prop_c2010_identity :: Cube -> Bool
 250 prop_c2010_identity cube =
 251     c t0 2 0 1 0 ~= c t0 1 1 1 0 + c t6 1 1 0 1
 252                     - ((c t0 1 0 2 0 + c t0 1 0 1 1)/ 2)
 253       where
 254         t0 = tetrahedron0 cube
 255         t6 = tetrahedron6 cube
 256
 257
 258 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). See
 259 --   'prop_c3000_identity'.
 260 prop_c2001_identity :: Cube -> Bool
 261 prop_c2001_identity cube =
 262     c t0 2 0 0 1 ~= c t0 1 1 0 1 + c t6 1 1 1 0
 263                     - ((c t0 1 0 0 2 + c t0 1 0 1 1)/ 2)
 264       where
 265         t0 = tetrahedron0 cube
 266         t6 = tetrahedron6 cube
 267
 268
 269 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). See
 270 --   'prop_c3000_identity'.
 271 prop_c1020_identity :: Cube -> Bool
 272 prop_c1020_identity cube =
 273     c t0 1 0 2 0 ~= c t0 0 1 2 0 + c t6 0 1 0 2
 274                     - ((c t0 0 0 3 0 + c t0 0 0 2 1)/ 2)
 275       where
 276         t0 = tetrahedron0 cube
 277         t6 = tetrahedron6 cube
 278
 279
 280 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). See
 281 --   'prop_c3000_identity'.
 282 prop_c1002_identity :: Cube -> Bool
 283 prop_c1002_identity cube =
 284     c t0 1 0 0 2 ~= c t0 0 1 0 2 + c t6 0 1 2 0
 285                     - ((c t0 0 0 0 3 + c t0 0 0 1 2)/ 2)
 286       where
 287         t0 = tetrahedron0 cube
 288         t6 = tetrahedron6 cube
 289
 290
 291 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). See
 292 --   'prop_c3000_identity'.
 293 prop_c1011_identity :: Cube -> Bool
 294 prop_c1011_identity cube =
 295     c t0 1 0 1 1 ~= c t0 0 1 1 1 + c t6 0 1 1 1 -
 296                     ((c t0 0 0 1 2 + c t0 0 0 2 1)/ 2)
 297       where
 298         t0 = tetrahedron0 cube
 299         t6 = tetrahedron6 cube
 300
 301
 302
 303 -- | Given in Sorokina and Zeilfelder, p. 78.
 304 prop_cijk1_identity :: Cube -> Bool
 305 prop_cijk1_identity cube =
 306      and [ c t0 i j k 1 ~=
 307                  (c t1 (i+1) j k 0) * ((b0 t0) (v3 t1)) +
 308                  (c t1 i (j+1) k 0) * ((b1 t0) (v3 t1)) +
 309                  (c t1 i j (k+1) 0) * ((b2 t0) (v3 t1)) +
 310                  (c t1 i j k 1) * ((b3 t0) (v3 t1)) | i <- [0..2],
 311                                                       j <- [0..2],
 312                                                       k <- [0..2],
 313                                                       i + j + k == 2]
 314       where
 315         t0 = tetrahedron0 cube
 316         t1 = tetrahedron1 cube
 317
 318
 319 -- | The function values at the interior should be the same for all tetrahedra.
 320 prop_interior_values_all_identical :: Cube -> Bool
 321 prop_interior_values_all_identical cube =
 322     all_equal [i0, i1, i2, i3, i4, i5, i6, i7, i8,
 323                i9, i10, i11, i12, i13, i14, i15, i16,
 324                i17, i18, i19, i20, i21, i22, i23]
 325     where
 326       i0 = eval (Tetrahedron.fv (tetrahedron0 cube)) I
 327       i1 = eval (Tetrahedron.fv (tetrahedron1 cube)) I
 328       i2 = eval (Tetrahedron.fv (tetrahedron2 cube)) I
 329       i3 = eval (Tetrahedron.fv (tetrahedron3 cube)) I
 330       i4 = eval (Tetrahedron.fv (tetrahedron4 cube)) I
 331       i5 = eval (Tetrahedron.fv (tetrahedron5 cube)) I
 332       i6 = eval (Tetrahedron.fv (tetrahedron6 cube)) I
 333       i7 = eval (Tetrahedron.fv (tetrahedron7 cube)) I
 334       i8 = eval (Tetrahedron.fv (tetrahedron8 cube)) I
 335       i9 = eval (Tetrahedron.fv (tetrahedron9 cube)) I
 336       i10 = eval (Tetrahedron.fv (tetrahedron10 cube)) I
 337       i11 = eval (Tetrahedron.fv (tetrahedron11 cube)) I
 338       i12 = eval (Tetrahedron.fv (tetrahedron12 cube)) I
 339       i13 = eval (Tetrahedron.fv (tetrahedron13 cube)) I
 340       i14 = eval (Tetrahedron.fv (tetrahedron14 cube)) I
 341       i15 = eval (Tetrahedron.fv (tetrahedron15 cube)) I
 342       i16 = eval (Tetrahedron.fv (tetrahedron16 cube)) I
 343       i17 = eval (Tetrahedron.fv (tetrahedron17 cube)) I
 344       i18 = eval (Tetrahedron.fv (tetrahedron18 cube)) I
 345       i19 = eval (Tetrahedron.fv (tetrahedron19 cube)) I
 346       i20 = eval (Tetrahedron.fv (tetrahedron20 cube)) I
 347       i21 = eval (Tetrahedron.fv (tetrahedron21 cube)) I
 348       i22 = eval (Tetrahedron.fv (tetrahedron22 cube)) I
 349       i23 = eval (Tetrahedron.fv (tetrahedron23 cube)) I
 350
 351
 352 -- | We know what (c t6 2 1 0 0) should be from Sorokina and Zeilfelder, p. 87.
 353 --   This test checks the rotation works as expected.
 354 prop_c_tilde_2100_rotation_correct :: Cube -> Bool
 355 prop_c_tilde_2100_rotation_correct cube =
 356     expr1 == expr2
 357     where
 358       t0 = tetrahedron0 cube
 359       t6 = tetrahedron6 cube
 360
 361       -- What gets computed for c2100 of t6.
 362       expr1 = eval (Tetrahedron.fv t6) $
 363           (3/8)*I +
 364           (1/12)*(T + R + L + D) +
 365           (1/64)*(FT + FR + FL + FD) +
 366           (7/48)*F +
 367           (1/48)*B +
 368           (1/96)*(RT + LD + LT + RD) +
 369           (1/192)*(BT + BR + BL + BD)
 370
 371       -- What should be computed for c2100 of t6.
 372       expr2 = eval (Tetrahedron.fv t0) $
 373               (3/8)*I +
 374               (1/12)*(F + R + L + B) +
 375               (1/64)*(FT + RT + LT + BT) +
 376               (7/48)*T +
 377               (1/48)*D +
 378               (1/96)*(FR + FL + BR + BL) +
 379               (1/192)*(FD + RD + LD + BD)
 380
 381
 382 -- | We know what (c t6 2 1 0 0) should be from Sorokina and Zeilfelder, p. 87.
 383 --   This test checks the actual value based on the FunctionValues of the cube.
 384 prop_c_tilde_2100_correct :: Cube -> Bool
 385 prop_c_tilde_2100_correct cube =
 386     c t6 2 1 0 0 == (3/8)*int
 387                     + (1/12)*(f + r + l + b)
 388                     + (1/64)*(ft + rt + lt + bt)
 389                     + (7/48)*t + (1/48)*d + (1/96)*(fr + fl + br + bl)
 390                     + (1/192)*(fd + rd + ld + bd)
 391     where
 392       t0 = tetrahedron0 cube
 393       t6 = tetrahedron6 cube
 394       fvs = Tetrahedron.fv t0
 395       int = interior fvs
 396       f = front fvs
 397       r = right fvs
 398       l = left fvs
 399       b = back fvs
 400       ft = front_top fvs
 401       rt = right_top fvs
 402       lt = left_top fvs
 403       bt = back_top fvs
 404       t = top fvs
 405       d = down fvs
 406       fr = front_right fvs
 407       fl = front_left fvs
 408       br = back_right fvs
 409       bl = back_left fvs
 410       fd = front_down fvs
 411       rd = right_down fvs
 412       ld = left_down fvs
 413       bd = back_down fvs
 414
 415 -- Tests to check that the correct edges are incidental.
 416 prop_t0_shares_edge_with_t1 :: Cube -> Bool
 417 prop_t0_shares_edge_with_t1 cube =
 418     (v1 t0) == (v1 t1) && (v3 t0) == (v2 t1)
 419       where
 420         t0 = tetrahedron0 cube
 421         t1 = tetrahedron1 cube
 422
 423 prop_t0_shares_edge_with_t3 :: Cube -> Bool
 424 prop_t0_shares_edge_with_t3 cube =
 425     (v1 t0) == (v1 t3) && (v2 t0) == (v3 t3)
 426       where
 427         t0 = tetrahedron0 cube
 428         t3 = tetrahedron3 cube
 429
 430 prop_t0_shares_edge_with_t6 :: Cube -> Bool
 431 prop_t0_shares_edge_with_t6 cube =
 432     (v2 t0) == (v3 t6) && (v3 t0) == (v2 t6)
 433       where
 434         t0 = tetrahedron0 cube
 435         t6 = tetrahedron6 cube
 436
 437 prop_t1_shares_edge_with_t2 :: Cube -> Bool
 438 prop_t1_shares_edge_with_t2 cube =
 439     (v1 t1) == (v1 t2) && (v3 t1) == (v2 t2)
 440       where
 441         t1 = tetrahedron1 cube
 442         t2 = tetrahedron2 cube
 443
 444 prop_t1_shares_edge_with_t19 :: Cube -> Bool
 445 prop_t1_shares_edge_with_t19 cube =
 446     (v2 t1) == (v3 t19) && (v3 t1) == (v2 t19)
 447       where
 448         t1 = tetrahedron1 cube
 449         t19 = tetrahedron19 cube
 450
 451 prop_t2_shares_edge_with_t3 :: Cube -> Bool
 452 prop_t2_shares_edge_with_t3 cube =
 453     (v1 t1) == (v1 t2) && (v3 t1) == (v2 t2)
 454       where
 455         t1 = tetrahedron1 cube
 456         t2 = tetrahedron2 cube
 457
 458 prop_t2_shares_edge_with_t12 :: Cube -> Bool
 459 prop_t2_shares_edge_with_t12 cube =
 460     (v2 t2) == (v3 t12) && (v3 t2) == (v2 t12)
 461       where
 462         t2 = tetrahedron2 cube
 463         t12 = tetrahedron12 cube
 464
 465 prop_t3_shares_edge_with_t21 :: Cube -> Bool
 466 prop_t3_shares_edge_with_t21 cube =
 467     (v2 t3) == (v3 t21) && (v3 t3) == (v2 t21)
 468       where
 469         t3 = tetrahedron3 cube
 470         t21 = tetrahedron21 cube
 471
 472 prop_t4_shares_edge_with_t5 :: Cube -> Bool
 473 prop_t4_shares_edge_with_t5 cube =
 474     (v1 t4) == (v1 t5) && (v3 t4) == (v2 t5)
 475       where
 476         t4 = tetrahedron4 cube
 477         t5 = tetrahedron5 cube
 478
 479 prop_t4_shares_edge_with_t7 :: Cube -> Bool
 480 prop_t4_shares_edge_with_t7 cube =
 481     (v1 t4) == (v1 t7) && (v2 t4) == (v3 t7)
 482       where
 483         t4 = tetrahedron4 cube
 484         t7 = tetrahedron7 cube
 485
 486 prop_t4_shares_edge_with_t10 :: Cube -> Bool
 487 prop_t4_shares_edge_with_t10 cube =
 488     (v2 t4) == (v3 t10) && (v3 t4) == (v2 t10)
 489       where
 490         t4 = tetrahedron4 cube
 491         t10 = tetrahedron10 cube
 492
 493 prop_t5_shares_edge_with_t6 :: Cube -> Bool
 494 prop_t5_shares_edge_with_t6 cube =
 495     (v1 t5) == (v1 t6) && (v3 t5) == (v2 t6)
 496       where
 497         t5 = tetrahedron5 cube
 498         t6 = tetrahedron6 cube
 499
 500 prop_t5_shares_edge_with_t16 :: Cube -> Bool
 501 prop_t5_shares_edge_with_t16 cube =
 502     (v2 t5) == (v3 t16) && (v3 t5) == (v2 t16)
 503       where
 504         t5 = tetrahedron5 cube
 505         t16 = tetrahedron16 cube
 506
 507 prop_t6_shares_edge_with_t7 :: Cube -> Bool
 508 prop_t6_shares_edge_with_t7 cube =
 509     (v1 t6) == (v1 t7) && (v3 t6) == (v2 t7)
 510       where
 511         t6 = tetrahedron6 cube
 512         t7 = tetrahedron7 cube
 513
 514 prop_t7_shares_edge_with_t20 :: Cube -> Bool
 515 prop_t7_shares_edge_with_t20 cube =
 516     (v2 t7) == (v3 t20) && (v2 t7) == (v3 t20)
 517       where
 518         t7 = tetrahedron7 cube
 519         t20 = tetrahedron20 cube