vouivre/rules.scm

   1 ;;;; Copyright (C) 2024 Vouivre Digital Corporation
   2 ;;;;
   3 ;;;; This file is part of Vouivre.
   4 ;;;;
   5 ;;;; Vouivre is free software: you can redistribute it and/or
   6 ;;;; modify it under the terms of the GNU General Public
   7 ;;;; License as published by the Free Software Foundation, either
   8 ;;;; version 3 of the License, or (at your option) any later version.
   9 ;;;;
  10 ;;;; Vouivre is distributed in the hope that it will be useful,
  11 ;;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
  12 ;;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
  13 ;;;; General Public License for more details.
  14 ;;;;
  15 ;;;; You should have received a copy of the GNU General Public
  16 ;;;; License along with Vouivre. If not, see <https://www.gnu.org/licenses/>.
  17
  18 (define-module (vouivre type rules)
  19   #:use-module (vouivre type system))
  20
  21 ;;;; Structural Rules
  22
  23 (define-rule formation-1
  24   (Γ ⊢ (type A))
  25   (Γ (: x A) ⊢ (type (B x))))
  26
  27 (define-rule formation-2
  28   (Γ ⊢ (type A))
  29   (Γ ⊢ (≐ A B)))
  30
  31 (define-rule formation-3
  32   (Γ ⊢ (type B))
  33   (Γ ⊢ (≐ A B)))
  34
  35 (define-rule formation-4
  36   (Γ ⊢ (type A))
  37   (Γ ⊢ (: a A)))
  38
  39 (define-rule formation-5
  40   (Γ ⊢ (: a A))
  41   (Γ ⊢ (≐ a b A)))
  42
  43 (define-rule formation-6
  44   (Γ ⊢ (: b A))
  45   (Γ ⊢ (≐ a b A)))
  46
  47 (define-rule type-reflexive
  48   (Γ ⊢ (≐ A A))
  49   (Γ ⊢ (type A)))
  50
  51 (define-rule type-symmetric
  52   (Γ ⊢ (≐ B A))
  53   (Γ ⊢ (≐ A B)))
  54
  55 (define-rule type-transitive
  56   (Γ ⊢ (≐ A C))
  57   (Γ ⊢ (≐ A B))
  58   (Γ ⊢ (≐ B C)))
  59
  60 (define-rule element-reflexive
  61   (Γ ⊢ (≐ a a A))
  62   (Γ ⊢ (: a A)))
  63
  64 (define-rule element-symmetric
  65   (Γ ⊢ (≐ b a A))
  66   (Γ ⊢ (≐ a b A)))
  67
  68 (define-rule element-transitive
  69   (Γ ⊢ (≐ a c A))
  70   (Γ ⊢ (≐ a b A))
  71   (Γ ⊢ (≐ b c A)))
  72
  73 (define-rule variable-conversion
  74   (Γ (: x A') Δ ⊢ J)
  75   (Γ ⊢ (≐ A A'))
  76   (Γ (: x A) Δ ⊢ J))
  77
  78 (define-rule substitution
  79   (Γ (/ Δ a x) ⊢ (/ J a x))
  80   (Γ ⊢ (: a A))
  81   (Γ (: x A) Δ ⊢ J))
  82
  83 (define-rule substitution-type-congruence
  84   (Γ (/ Δ a x) ⊢ (≐ (/ B a x) (/ B a' x)))
  85   (Γ ⊢ (≐ a a' A))
  86   (Γ (: x A) Δ ⊢ (type B)))
  87
  88 (define-rule substitution-element-congruence
  89   (Γ (/ Δ a x) ⊢ (≐ (/ b a x) (/ b a' x) (/ B a x)))
  90   (Γ ⊢ (≐ a a' A))
  91   (Γ (: x A) Δ ⊢ (: b B)))
  92
  93 (define-rule weakening
  94   (Γ (: x A) Δ ⊢ J)
  95   (Γ ⊢ (type A))
  96   (Γ Δ ⊢ J))
  97
  98 (define-rule generic-element
  99   (Γ (: x A) ⊢ (: x A))
 100   (Γ ⊢ (type A)))
 101
 102 ;;;; Structural Derivations
 103
 104 (define-derivation change-of-variables ((Γ (: x' A) Δ ⊢ J)
 105                                         (Γ ⊢ (type A))
 106                                         (Γ (: x A) Δ ⊢ J))
 107   (substitution #:start 1 a x' x x A A)
 108   (generic-element)
 109   (exact)
 110   (weakening #:end 1)
 111   (exact)
 112   (exact))
 113
 114 (define-derivation interchange ((Γ (: y B) (: x A) Δ ⊢ J)
 115                                 (Γ ⊢ (type B))
 116                                 (Γ ⊢ (type A))
 117                                 (Γ (: x A) (: y B) Δ ⊢ J))
 118   (substitution #:start 2 a y x y' A B)
 119   (weakening #:start 1)
 120   (weakening)
 121   (exact)
 122   (exact)
 123   (generic-element)
 124   (exact)
 125   (weakening #:end 1)
 126   (exact)
 127   (substitution #:start 2 a y' x y A B)
 128   (weakening #:end 1)
 129   (exact)
 130   (generic-element)
 131   (exact)
 132   (weakening #:start 1 #:end 2)
 133   (weakening)
 134   (exact)
 135   (exact)
 136   (exact))
 137
 138 (define-derivation element-conversion ((Γ ⊢ (: a A'))
 139                                        (Γ ⊢ (: a A))
 140                                        (Γ ⊢ (≐ A A')))
 141   (substitution a a x a' A A)
 142   (exact)
 143   (variable-conversion A A')
 144   (type-symmetric)
 145   (exact)
 146   (generic-element)
 147   (formation-3 A A)
 148   (exact))
 149
 150 (define-derivation congruence ((Γ ⊢ (≐ a b A'))
 151                                (Γ ⊢ (≐ a b A))
 152                                (Γ ⊢ (≐ A A')))
 153   (substitution-element-congruence a a a' b x x A A)
 154   (exact)
 155   (variable-conversion A A')
 156   (type-symmetric)
 157   (exact)
 158   (generic-element)
 159   (formation-3 A A)
 160   (exact))
 161
 162 ;;;; Dependent Function Type
 163
 164 (define-rule Π
 165   (Γ ⊢ (type (Π (: x A) (B x))))
 166   (Γ (: x A) ⊢ (type (B x))))
 167
 168 (define-rule Π-eq
 169   (Γ ⊢ (≐ (Π (: x A) (B x))
 170           (Π (: x A') (B' x))))
 171   (Γ ⊢ (≐ A A'))
 172   (Γ (: x A) ⊢ (≐ (B x) (B' x))))
 173
 174 (define-rule λ
 175   (Γ ⊢ (: (λ x (b x))
 176           (Π (: x A) (B x))))
 177   (Γ (: x A) ⊢ (: (b x) (B x))))
 178
 179 (define-rule λ-eq
 180   (Γ ⊢ (≐ (λ x (b x))
 181           (λ x (b' x))
 182           (Π (: x A) (B x))))
 183   (Γ (: x A) ⊢ (≐ (b x)
 184                   (b' x)
 185                   (B x))))
 186
 187 (define-rule evaluation
 188   (Γ (: x A) ⊢ (: (f x) (B x)))
 189   (Γ ⊢ (: f (Π (: x A) (B x)))))
 190
 191 (define-rule evaluation-eq
 192   (Γ (: x A) ⊢ (≐ (f x) (f' x) (B x)))
 193   (Γ ⊢ (≐ f f' (Π (: x A) (B x)))))
 194
 195 (define-rule β
 196   (Γ (: x A) ⊢ (≐ ((λ y (b y)) x)
 197                   (b x)
 198                   (B x)))
 199   (Γ (: x A) ⊢ (: (b x) (B x))))
 200
 201 (define-rule η
 202   (Γ ⊢ (≐ (λ x (f x))
 203           f
 204           (Π (: x A) (B x))))
 205   (Γ ⊢ (: f (Π (: x A) (B x)))))
 206
 207 ;;;; Ordinary Function Type
 208
 209 (define-derivation → ((Γ ⊢ (:= (→ A B) (type (Π (: x A) B))))
 210                       (Γ ⊢ (type A))
 211                       (Γ ⊢ (type B)))
 212   (Π)
 213   (weakening)
 214   (exact)
 215   (exact))
 216
 217 (define-derivation →-eq ((Γ ⊢ (≐ (→ A B) (→ A' B')))
 218                          (Γ ⊢ (≐ A A'))
 219                          (Γ ⊢ (≐ B B')))
 220   (type-transitive B (Π (: x A) B))
 221   (definition)
 222   (formation-2 B A')
 223   (exact)
 224   (formation-2 B B')
 225   (exact)
 226   (type-transitive B (Π (: x A') B'))
 227   (Π-eq)
 228   (exact)
 229   (weakening)
 230   (formation-2 B A')
 231   (exact)
 232   (exact)
 233   (type-symmetric)
 234   (definition)
 235   (formation-3 A A)
 236   (exact)
 237   (formation-3 A B)
 238   (exact))
 239
 240 (define-derivation →-λ ((Γ ⊢ (: (λ x (b x)) (→ A B)))
 241                         (Γ (: x A) ⊢ (: (b x) B))
 242                         (Γ ⊢ (type A))
 243                         (Γ ⊢ (type B)))
 244   (element-conversion A (Π (: x A) B))
 245   (λ)
 246   (exact)
 247   (type-symmetric)
 248   (definition)
 249   (exact)
 250   (exact))
 251
 252 (define-derivation →-λ-eq ((Γ ⊢ (≐ (λ x (b x))
 253                                    (λ x (b' x))
 254                                    (→ A B)))
 255                            (Γ (: x A) ⊢ (≐ (b x) (b' x) B))
 256                            (Γ ⊢ (type A))
 257                            (Γ ⊢ (type B)))
 258   (congruence A (Π (: x A) B))
 259   (λ-eq)
 260   (exact)
 261   (type-symmetric)
 262   (definition)
 263   (exact)
 264   (exact))
 265
 266 (define-derivation →-evaluation ((Γ (: x A) ⊢ (: (f x) B))
 267                                  (Γ ⊢ (: f (→ A B)))
 268                                  (Γ ⊢ (type A))
 269                                  (Γ ⊢ (type B)))
 270   (evaluation f f)
 271   (element-conversion A (→ A B))
 272   (exact)
 273   (definition)
 274   (exact)
 275   (exact))
 276
 277 (define-derivation →-evaluation-eq ((Γ (: x A) ⊢ (≐ (f x) (f' x) B))
 278                                     (Γ ⊢ (≐ f f' (→ A B)))
 279                                     (Γ ⊢ (type A))
 280                                     (Γ ⊢ (type B)))
 281   (evaluation-eq f f f' f')
 282   (congruence A (→ A B))
 283   (exact)
 284   (definition)
 285   (exact)
 286   (exact))
 287
 288 (define-derivation →-β ((Γ (: x A) ⊢ (≐ ((λ x (b x)) x)
 289                                         (b x)
 290                                         B))
 291                         (Γ (: x A) ⊢ (: (b x) B)))
 292   (β)
 293   (exact))
 294
 295 (define-derivation →-η ((Γ ⊢ (≐ (λ x (f x)) f (→ A B)))
 296                         (Γ ⊢ (: f (→ A B)))
 297                         (Γ ⊢ (type A))
 298                         (Γ ⊢ (type B)))
 299   (congruence A (Π (: x A) B))
 300   (η)
 301   (element-conversion A (→ A B))
 302   (exact)
 303   (definition)
 304   (exact)
 305   (exact)
 306   (type-symmetric)
 307   (definition)
 308   (exact)
 309   (exact))
 310
 311 ;;;; Identity Type
 312
 313 (define-rule =-formation
 314   (Γ (: x A) ⊢ (type (= a x)))
 315   (Γ ⊢ (: a A)))
 316
 317 (define-rule =-introduction
 318   (Γ ⊢ (: refl (= a a)))
 319   (Γ ⊢ (: a A)))
 320
 321 (define-rule =-elimination
 322   (Γ ⊢ (: ind-eq
 323             (→ (P a refl)
 324                (Π (: x A)
 325                   (Π (: p (= a x))
 326                      (P x p))))))
 327   (Γ ⊢ (: a A))
 328   (Γ (: x A) (: p (= a x)) ⊢ (type (P x p))))
 329
 330 (define-rule =-computation
 331   (Γ (: u (P a refl)) ⊢ (≐ (((ind-eq u) a) refl)
 332                              u
 333                              (P a refl)))
 334   (Γ ⊢ (: a A))
 335   (Γ (: x A) (: p (= a x)) ⊢ (type (P x p))))
 336
 337 ;;;; Dependent Pair Type
 338
 339 (define-rule Σ-formation
 340   (Γ ⊢ (type (Σ (: x A) (B x))))
 341   (Γ (: x A) ⊢ (type (B x))))
 342
 343 (define-rule Σ-eq
 344   (Γ ⊢ (≐ (Σ (: x A) (B x))
 345           (Σ (: x A') (B' x))))
 346   (Γ ⊢ (≐ A A'))
 347   (Γ (: x A) ⊢ (≐ (B x) (B' x))))
 348
 349 (define-rule Σ-introduction
 350   (Γ ⊢ (: pair (Π (: x A)
 351                   (→ (B x)
 352                      (Σ (: y A)
 353                         (B y))))))
 354   (Γ (: x A) ⊢ (type (B x))))
 355
 356 (define-rule Σ-elimination
 357   (Γ ⊢ (: ind-Σ (→ (Π (: x A)
 358                       (Π (: y (B x))
 359                          (P ((pair x) y))))
 360                    (Π (: z (Σ (: x A)
 361                               (B x)))
 362                       (P z)))))
 363   (Γ (: x A) ⊢ (type (B x)))
 364   (Γ (: z (Σ (: x A) (B x))) ⊢ (type (P z))))
 365
 366 (define-rule Σ-computation
 367   (Γ (: x A) (: y (B x)) (: g (Π (: x A)
 368                                  (Π (: y (B x))
 369                                     (P ((pair x) y)))))
 370      ⊢ (≐ ((ind-Σ g) ((pair x) y))
 371           ((g x) y)
 372           (P ((pair x) y))))
 373   (Γ (: z (Σ (: x A) (B x))) ⊢ (type (P z))))
 374
 375 ;;;; Natural Numbers
 376
 377 (define-rule ℕ-formation
 378   (⊢ (type ℕ)))
 379
 380 (define-rule ℕ-introduction-1
 381   (⊢ (: 0 ℕ)))
 382
 383 (define-rule ℕ-introduction-2
 384   (⊢ (: succ (→ ℕ ℕ))))
 385
 386 (define-rule ℕ-elimination
 387   (Γ ⊢ (: (ind-ℕ p0 ps)
 388           (Π (: n ℕ)
 389              (P n))))
 390   (Γ (: n ℕ) ⊢ (type (P n)))
 391   (Γ ⊢ (: p0 (P 0)))
 392   (Γ ⊢ (: ps (Π (: n ℕ)
 393                 (→ (P n)
 394                    (P (succ n)))))))
 395
 396 (define-rule ℕ-computation-1
 397   (Γ ⊢ (≐ ((ind-ℕ p0 ps) 0)
 398           p0
 399           (P 0)))
 400   (Γ (: n ℕ) ⊢ (type (P n)))
 401   (Γ ⊢ (: p0 (P 0)))
 402   (Γ ⊢ (: ps (Π (: n ℕ)
 403                 (→ (P n)
 404                    (P (succ n)))))))
 405
 406 (define-rule ℕ-computation-2
 407   (Γ (: n ℕ) ⊢ (≐ ((ind-ℕ p0 ps) (succ n))
 408                   (ps n ((ind-ℕ p0 ps) n))
 409                   (P (succ n))))
 410   (Γ (: n ℕ) ⊢ (type (P n)))
 411   (Γ ⊢ (: p0 (P 0)))
 412   (Γ ⊢ (: ps (Π (: n ℕ)
 413                 (→ (P n)
 414                    (P (succ n)))))))
 415
 416 ;;;; Boolean Type
 417
 418 (define-rule bool-formation
 419   (⊢ (type Bool)))
 420
 421 (define-rule bool-introduction-1
 422   (⊢ (: false Bool)))
 423
 424 (define-rule bool-introduction-2
 425   (⊢ (: true Bool)))
 426
 427 (define-rule bool-elimination
 428   (Γ ⊢ (: (ind-Bool p0 p1)
 429           (Π (: x Bool)
 430              (P x))))
 431   (Γ (: x Bool) ⊢ (type (P x)))
 432   (Γ ⊢ (: p0 (P false)))
 433   (Γ ⊢ (: p1 (P true))))
 434
 435 (define-rule bool-computation-1
 436   (Γ ⊢ (≐ ((ind-Bool p0 p1) false)
 437           p0
 438           (P false)))
 439   (Γ (: x Bool) ⊢ (type (P x)))
 440   (Γ ⊢ (: p0 (P false)))
 441   (Γ ⊢ (: p1 (P true))))
 442
 443 (define-rule bool-computation-2
 444   (Γ ⊢ (≐ ((ind-Bool p0 p1) true)
 445           p1
 446           (P true)))
 447   (Γ (: x Bool) ⊢ (type (P x)))
 448   (Γ ⊢ (: p0 (P false)))
 449   (Γ ⊢ (: p1 (P true))))
 450
 451 ;;;; List Type
 452
 453 (define-rule list-formation
 454   (Γ ⊢ (type (List A)))
 455   (Γ ⊢ (type A)))
 456
 457 (define-rule list-introduction-1
 458   (Γ ⊢ (: nil (List A)))
 459   (Γ ⊢ (type A)))
 460
 461 (define-rule list-introduction-2
 462   (Γ ⊢ (: cons (→ A (→ (List A)
 463                      (List A)))))
 464   (Γ ⊢ (type A)))
 465
 466 (define-rule list-elimination
 467   (Γ ⊢ (: (ind-List p0 ps)
 468           (Π (: xs (List A))
 469              (P xs))))
 470   (Γ ⊢ (type A))
 471   (Γ (: xs (List A)) ⊢ (type (P xs)))
 472   (Γ ⊢ (: p0 (P nil)))
 473   (Γ ⊢ (: ps (Π (: x A)
 474                 (Π (: xs (List A))
 475                    (→ (P xs)
 476                       (P ((cons x) xs))))))))
 477
 478 (define-rule list-computation-1
 479   (Γ ⊢ (≐ ((ind-List p0 ps) nil)
 480           p0
 481           (P nil)))
 482   (Γ ⊢ (type A))
 483   (Γ (: xs (List A)) ⊢ (type (P xs)))
 484   (Γ ⊢ (: p0 (P nil)))
 485   (Γ ⊢ (: ps (Π (: x A)
 486                 (Π (: xs (List A))
 487                    (→ (P xs)
 488                       (P ((cons x) xs))))))))
 489
 490 (define-rule list-computation-2
 491   (Γ (: x A) (: xs (List A)) ⊢ (≐ ((ind-List p0 ps) ((cons x) xs))
 492                                   (((ps x) xs) ((ind-List p0 ps) xs))
 493                                   (P ((cons x) xs))))
 494   (Γ ⊢ (type A))
 495   (Γ (: xs (List A)) ⊢ (type (P xs)))
 496   (Γ ⊢ (: p0 (P nil)))
 497   (Γ ⊢ (: ps (Π (: x A)
 498                 (Π (: xs (List A))
 499                    (→ (P xs)
 500                       (P ((cons x) xs))))))))
 501
 502 ;;;; Vector Type
 503
 504 (define-rule vector-formation
 505   (Γ ⊢ (type (Vector A n)))
 506   (Γ ⊢ (type A))
 507   (Γ ⊢ (: n ℕ)))
 508
 509 (define-rule vector-introduction-1
 510   (Γ ⊢ (: #() (Vector A 0)))
 511   (Γ ⊢ (type A)))
 512
 513 (define-rule vector-introduction-2
 514   (Γ ⊢ (: :: (Π (: n ℕ)
 515                 (→ A (→ (Vector A n)
 516                         (Vector A (succ n)))))))
 517   (Γ ⊢ (type A)))
 518
 519 (define-rule vector-elimination
 520   (Γ ⊢ (: (ind-Vector p0 ps)
 521           (Π (: n ℕ)
 522              (Π (: xs (Vector A n))
 523                 (P xs)))))
 524   (Γ ⊢ (type A))
 525   (Γ (: n ℕ) (: xs (Vector A n)) ⊢ (type (P xs)))
 526   (Γ ⊢ (: p0 (P #())))
 527   (Γ ⊢ (: ps (Π (: n ℕ)
 528                 (Π (: x A)
 529                    (Π (: xs (Vector A n))
 530                       (→ (P xs)
 531                          (P (((:: n) x) xs)))))))))
 532
 533 (define-rule vector-computation-1
 534   (Γ ⊢ (≐ ((ind-Vector p0 ps) #())
 535           p0
 536           (P #())))
 537   (Γ ⊢ (type A))
 538   (Γ (: n ℕ) (: xs (Vector A n)) ⊢ (type (P xs)))
 539   (Γ ⊢ (: p0 (P #())))
 540   (Γ ⊢ (: ps (Π (: n ℕ)
 541                 (Π (: x A)
 542                    (Π (: xs (Vector A n))
 543                       (→ (P xs)
 544                          (P (((:: n) x) xs)))))))))
 545
 546 (define-rule vector-computation-2
 547   (Γ (: x A) (: n ℕ) (: xs (Vector A n)) ⊢ (≐ (((ind-Vector p0 ps) n) (((:: n) x) xs))
 548                                               ((((ps n) x) xs)
 549                                                (((ind-Vector p0 ps) n) xs))
 550                                               (P (((:: n) x) xs))))
 551   (Γ ⊢ (type A))
 552   (Γ (: n ℕ) (: xs (Vector A n)) ⊢ (type (P xs)))
 553   (Γ ⊢ (: p0 (P #())))
 554   (Γ ⊢ (: ps (Π (: n ℕ)
 555                 (Π (: x A)
 556                    (Π (: xs (Vector A n))
 557                       (→ (P xs)
 558                          (P (((:: n) x) xs)))))))))
 559
 560 ;;;; More Derivations
 561
 562 (define-derivation identity ((Γ ⊢ (: (λ x x) (→ A A)))
 563                              (Γ ⊢ (type A)))
 564   (→-λ)
 565   (generic-element)
 566   (exact)
 567   (exact)
 568   (exact))
 569
 570 (define-derivation if ((Γ ⊢ (: (λ z (λ x (λ y ((ind-Bool y x) z))))
 571                                (Π (: z Bool)
 572                                   (→ (P true)
 573                                      (→ (P false)
 574                                         (P z))))))
 575                        (Γ (: z Bool) ⊢ (type (P z))))
 576   (λ)
 577   (→-λ #:start 1)
 578   (→-λ #:start 2)
 579   (interchange #:end 2)
 580   (bool-formation)
 581   (substitution A Bool a true x z)
 582   (bool-introduction-2)
 583   (exact)
 584   (interchange #:start 1)
 585   (weakening)
 586   (substitution A Bool a true x z)
 587   (bool-introduction-2)
 588   (exact)
 589   (bool-formation)
 590   (weakening)
 591   (substitution A Bool a true x z)
 592   (bool-introduction-2)
 593   (exact)
 594   (substitution A Bool a false x z)
 595   (bool-introduction-1)
 596   (exact)
 597   (evaluation #:start 2 f (ind-Bool y x))
 598   (bool-elimination #:start 2 (P false) (P false) (P true) (P true))
 599   (weakening #:end 1)
 600   (substitution A Bool a true x z)
 601   (bool-introduction-2)
 602   (exact)
 603   (weakening #:end 1)
 604   (substitution A Bool a false x z)
 605   (bool-introduction-1)
 606   (exact)
 607   (exact)
 608   (weakening #:end 1)
 609   (substitution A Bool a true x z)
 610   (bool-introduction-2)
 611   (exact)
 612   (generic-element)
 613   (substitution A Bool a false x z)
 614   (bool-introduction-1)
 615   (exact)
 616   (weakening #:start 1)
 617   (weakening)
 618   (substitution A Bool a true x z)
 619   (bool-introduction-2)
 620   (exact)
 621   (substitution A Bool a false x z)
 622   (bool-introduction-1)
 623   (exact)
 624   (generic-element)
 625   (substitution A Bool a true x z)
 626   (bool-introduction-2)
 627   (exact)
 628   (weakening #:end 1)
 629   (bool-formation)
 630   (weakening)
 631   (substitution A Bool a true x z)
 632   (bool-introduction-2)
 633   (exact)
 634   (substitution A Bool a false x z)
 635   (bool-introduction-1)
 636   (exact)
 637   (weakening #:start 1)
 638   (weakening)
 639   (bool-formation)
 640   (substitution #:start 1 A Bool a true x z)
 641   (bool-introduction-2 #:start 1)
 642   (exact)
 643   (exact)
 644   (weakening)
 645   (bool-formation)
 646   (substitution A Bool a true x z)
 647   (bool-introduction-2)
 648   (exact)
 649   (→ #:start 1)
 650   (weakening)
 651   (bool-formation)
 652   (substitution A Bool a false x z)
 653   (bool-introduction-1)
 654   (exact)
 655   (exact))
 656
 657 (define-derivation not ((Γ ⊢ (: (ind-Bool true false)
 658                                 (→ Bool Bool))))
 659   (element-conversion A (Π (: x Bool) Bool))
 660   (bool-elimination (P false) Bool (P true) Bool)
 661   (weakening)
 662   (bool-formation)
 663   (bool-formation)
 664   (bool-introduction-2)
 665   (bool-introduction-1)
 666   (type-symmetric)
 667   (definition)
 668   (bool-formation)
 669   (bool-formation))
 670
 671 (define-derivation constant ((Γ (: y B) ⊢ (: (λ x y) (→ A B)))
 672                              (Γ ⊢ (type A))
 673                              (Γ ⊢ (type B)))
 674   (→-λ #:start 1)
 675   (weakening #:start 1)
 676   (weakening)
 677   (exact)
 678   (exact)
 679   (generic-element)
 680   (exact)
 681   (weakening)
 682   (exact)
 683   (exact)
 684   (weakening)
 685   (exact)
 686   (exact))
 687
 688 (define-derivation =-inverse ((Γ ⊢ (: (λ x (ind-eq refl))
 689                                       (Π (: x A)
 690                                          (Π (: y A)
 691                                             (→ (= x y)
 692                                                (= y x))))))
 693                               (Γ ⊢ (type A))
 694                               (Γ ⊢ (: x A)))
 695   (λ)
 696   (substitution #:start 1 a refl x u A (= x x))
 697   (=-introduction #:start 1 A A)
 698   (generic-element)
 699   (exact)
 700   (→-evaluation #:start 1 f ind-eq)
 701   (element-conversion #:start 1 A (→ (= x x) (Π (: y A) (Π (: p (= x y)) (= y x)))))
 702   (=-elimination #:start 1)
 703   (generic-element)
 704   (exact)
 705   (weakening #:start 2)
 706   (=-formation #:start 1)
 707   (generic-element)
 708   (exact)
 709   (interchange)
 710   (exact)
 711   (exact)
 712   (=-formation #:start 1)
 713   (generic-element)
 714   (exact)
 715   (→-eq #:start 1)
 716   (type-reflexive #:start 1)
 717   (=-formation)
 718   (exact)
 719   (Π-eq #:start 1)
 720   (weakening)
 721   (exact)
 722   (type-reflexive)
 723   (exact)
 724   (type-symmetric #:start 2)
 725   (definition #:start 2)
 726   (=-formation #:start 1)
 727   (generic-element)
 728   (exact)
 729   (interchange)
 730   (exact)
 731   (exact)
 732   (=-formation #:start 1)
 733   (generic-element)
 734   (exact)
 735   (=-formation)
 736   (exact)
 737   (Π #:start 1)
 738   (→ #:start 2)
 739   (=-formation #:start 1)
 740   (generic-element)
 741   (exact)
 742   (interchange)
 743   (exact)
 744   (exact)
 745   (=-formation #:start 1)
 746   (generic-element)
 747   (exact))
 748
 749 (define-derivation add (((: m ℕ) ⊢ (: (ind-ℕ m ((λ n succ) m)) (→ ℕ ℕ))))
 750   (element-conversion #:start 1 A (Π (: x ℕ) ℕ))
 751   (ℕ-elimination #:start 1 (P 0) ℕ (P n) ℕ (P (succ n)) ℕ)
 752   (weakening #:start 1)
 753   (weakening)
 754   (ℕ-formation)
 755   (ℕ-formation)
 756   (weakening)
 757   (ℕ-formation)
 758   (ℕ-formation)
 759   (generic-element)
 760   (ℕ-formation)
 761   (element-conversion #:start 1 A (→ ℕ ℕ))
 762   (→-evaluation f (λ n succ))
 763   (→-λ)
 764   (weakening)
 765   (ℕ-formation)
 766   (ℕ-introduction-2)
 767   (ℕ-formation)
 768   (→)
 769   (ℕ-formation)
 770   (ℕ-formation)
 771   (ℕ-formation)
 772   (→)
 773   (ℕ-formation)
 774   (ℕ-formation)
 775   (definition #:start 1)
 776   (weakening)
 777   (ℕ-formation)
 778   (ℕ-formation)
 779   (weakening)
 780   (ℕ-formation)
 781   (ℕ-formation)
 782   (weakening)
 783   (ℕ-formation)
 784   (type-symmetric)
 785   (definition)
 786   (ℕ-formation)
 787   (ℕ-formation))
 788
 789 (define-derivation add-2-length ((Γ ⊢ (:= add-2-length
 790                                           (: (λ x (λ xs succ))
 791                                              (Π (: x A)
 792                                                 (Π (: xs (List A))
 793                                                    (→ ℕ ℕ))))))
 794                                  (Γ ⊢ (type A)))
 795   (λ)
 796   (λ #:start 1)
 797   (weakening #:start 1)
 798   (weakening)
 799   (exact)
 800   (list-formation)
 801   (exact)
 802   (weakening)
 803   (exact)
 804   (ℕ-introduction-2))
 805
 806 (define-derivation length ((Γ ⊢ (: (λ xs ((ind-List 0 add-2-length) xs))
 807                                    (→ (List A) ℕ)))
 808                            (Γ ⊢ (type A)))
 809   (→-λ)
 810   (evaluation f (ind-List 0 add-2-length))
 811   (list-elimination (P nil) ℕ x x (P ((cons x) xs)) ℕ)
 812   (exact)
 813   (weakening)
 814   (list-formation)
 815   (exact)
 816   (ℕ-formation)
 817   (ℕ-introduction-1)
 818   (add-2-length)
 819   (exact)
 820   (list-formation)
 821   (exact)
 822   (ℕ-formation))