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