From 61bdf8f5d4ca09c4935ea7072555d7af20c59d48 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Tue, 14 Apr 2015 19:16:47 -0400
Subject: [PATCH] Proper names and inductive families
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

These fixes are merged because properly testing the latter requires
having the former, while properly implementing the former is made
simpler by having the latter.

Fixed handling of names/substitution
===
* Added capture-avoiding substitution. Closes #7
* Added equivalence during typing checking, including α-equivalence and
  limited β-equivalence. Closes #8
* Exposed better typing-check reflection features to allow typing
  checking modulo equivalence.
* Tweaked QED macro to use new type-checking reflection feature.

Fixed inductive families
===
The implementation of inductive families is now based on the theoretical
models of inductive families, rather than an ad-hoc non-dependent
pattern matcher.

* Removed case and fix from Cur and Curnel. They are replaced by elim,
  the generic eliminator for inductive families. Closes #5. Since fix is
  no more, also closes #2.
* Elimination of false works! Closes #4.
* Changed uses of case to elim in Curnel
* Changed uses of case* in Cur to use eliminators. Breaks case* API.
* Fixed Coq generator to use eliminators
* Fixed Latex generator
---
 oll.rkt             |   68 +--
 proofs-for-free.rkt |    1 +
 redex-curnel.rkt    | 1190 +++++++++++++++++++++++++++++--------------
 stdlib/bool.rkt     |    7 +-
 stdlib/maybe.rkt    |   15 +-
 stdlib/nat.rkt      |   48 +-
 stdlib/prop.rkt     |   19 +-
 stdlib/sugar.rkt    |   26 +-
 stlc.rkt            |    7 +-
 9 files changed, 902 insertions(+), 479 deletions(-)

diff --git a/oll.rkt b/oll.rkt
index 89366bd..711bee9 100644
--- a/oll.rkt
+++ b/oll.rkt
@@ -53,14 +53,14 @@
         (when (attribute latex-file)
           (with-output-to-file (syntax->datum #'latex-file)
             (thunk
-              (format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\end{mathpar}$$"
-                      (syntax->datum #'(n types* ...))
-                      (string-trim
-                        (for/fold ([str ""])
-                                  ([rule (attribute rules.latex)])
-                          (format "~a~a\\and~n" str rule))
-                        "\\and"
-                        #:left? #f)))
+              (printf (format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\\end{mathpar}$$"
+                       (syntax->datum #'(n types* ...))
+                       (string-trim
+                         (for/fold ([str ""])
+                                   ([rule (attribute rules.latex)])
+                                   (format "~a~a\\and~n" str rule))
+                         "\\and"
+                         #:left? #f))))
             #:exists 'append))
         #`(begin
             #,@(if (attribute coq-file)
@@ -187,7 +187,7 @@
                      #:left? #f))]))))
   (define (generate-latex-bnf file-name vars clauses)
     (with-output-to-file file-name
-      (thunk (output-latex-bnf vars clauses))
+      (thunk (printf (output-latex-bnf vars clauses)))
       #:exists 'append)))
 (module+ test
   (require "stdlib/sugar.rkt")
@@ -231,11 +231,19 @@
 (data var : Type (avar : (-> nat var)))
 
 (define (var-equal? (v1 : var) (v2 : var))
-  (case* v1
-    [(avar (n1 : nat))
-     (case* v2
-       [(avar (n2 : nat))
+  (case* var v1 (lambda* (v : var) bool)
+    [(avar (n1 : nat)) IH: ()
+     (case* var v2 (lambda* (v : var) bool)
+       [(avar (n2 : nat)) IH: ()
         (nat-equal? n1 n2)])]))
+(module+ test
+  (require rackunit)
+  (check-equal?
+    (var-equal? (avar z) (avar z))
+    btrue)
+  (check-equal?
+    (var-equal? (avar z) (avar (s z)))
+    bfalse))
 
 ;; See stlc.rkt for examples
 
@@ -263,7 +271,7 @@
                               #'begin)
        ;; TODO: Need to add these to a literal set and export it
        ;; Or, maybe overwrite syntax-parse
-       #:literals (lambda forall data real-app case define-theorem
+       #:literals (lambda forall data real-app elim define-theorem
                           define qed begin Type)
        [(begin e ...)
         (for/fold ([str ""])
@@ -303,7 +311,7 @@
                     (output-coq #'body)))
           "")]
        [(lambda ~! (x:id (~datum :) t) body:expr)
-        (format "(fun ~a : ~a => ~a)" (syntax-e #'x) (output-coq #'t)
+        (format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
                 (output-coq #'body))]
        [(forall ~! (x:id (~datum :) t) body:expr)
         (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
@@ -322,21 +330,14 @@
                           (output-coq #'t))]))))
           "")]
        [(Type i) "Type"]
-       [(case e (ec eb) ...)
-        (format "(match ~a with~n~aend)"
-                (output-coq #'e)
-                (for/fold ([strs ""])
-                          ([con   (syntax->list #'(ec ...))]
-                           [body  (syntax->list #'(eb ...))])
-                  (let* ([ids (generate-temporaries (constructor-args con))]
-                         [names (map (compose ~a syntax->datum) ids)])
-                    (format "~a| (~a) => ~a~n" strs
-                      (for/fold ([str (output-coq con)])
-                                ([n names])
-                        (format "~a ~a" str n))
-                      (for/fold ([body (output-coq body)])
-                                ([n names])
-                        (format "(~a ~a)" body n))))))]
+       [(elim var e P m ...)
+        (format "(~a_rect ~a~a ~a)"
+          (output-coq #'var)
+          (output-coq #'P)
+          (for/fold ([x ""])
+                    ([m (syntax->list #'(m ...))])
+            (format "~a ~a" x (output-coq m)))
+          (output-coq #'e))]
        [(real-app e1 e2)
         (format "(~a ~a)" (output-coq #'e1) (output-coq #'e2))]
        [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
@@ -377,14 +378,15 @@
                                 (meow g e t)]))
                (coq-defns))])
       (check-regexp-match
-        "Inductive meow : \\(forall temp. : gamma, \\(forall temp. : term, \\(forall temp. : type, Type\\)\\)\\) :="
+        "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
         (first (string-split t "\n")))
       (check-regexp-match
         "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
         (second (string-split t "\n"))))
-    (let ([t (output-coq #'(case z (z z) (s (lambda (n : nat) (s n)))))])
+    (let ([t (output-coq #'(elim nat e (lambda (x : nat) nat) z
+                             (lambda* (x : nat) (ih-x : nat) ih-x)))])
       (check-regexp-match
-        "\\(match z with\n\\| \\(z\\) => z\n\\| \\(s .+\\) => \\(\\(fun n : nat => \\(s n\\)\\) .+\\)\nend\\)"
+        "\\(nat_rect \\(fun x : nat => nat\\) z \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\) e\\)"
         t))
     (check-regexp-match
       "Theorem thm_plus_commutes : \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
diff --git a/proofs-for-free.rkt b/proofs-for-free.rkt
index ac591d1..e3b6b6d 100644
--- a/proofs-for-free.rkt
+++ b/proofs-for-free.rkt
@@ -77,6 +77,7 @@
 (define (CPSf-relation (f1 : CPSf) (f2 : CPSf))
   ;; TODO: Fix run so I can simply use (run CPSf) to perform
   ;; substitution
+  (translate (run CPSf))
   (translate (forall* (ans : Type) (k : (-> X ans)) ans)))
 #;(module+ test
   (require rackunit)
diff --git a/redex-curnel.rkt b/redex-curnel.rkt
index 7d5aaf1..fbc42d7 100644
--- a/redex-curnel.rkt
+++ b/redex-curnel.rkt
@@ -1,6 +1,5 @@
 #lang racket
 
-;; This module contains a model of CIC, ish.
 ;; TODO: Strip to racket/base as much as possible
 (module core racket
   (require
@@ -11,19 +10,33 @@
 
   (set-cache-size! 10000)
 
+  (module+ test
+    (require rackunit)
+    (define-syntax-rule (check-holds (e ...))
+      (check-true
+        (judgment-holds (e ...))))
+    (define-syntax-rule (check-not-holds (e ...))
+      (check-false
+        (judgment-holds (e ...)))))
+
   ;; References:
   ;; http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf
   ;; https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf
   ;; http://www.emn.fr/z-info/ntabareau/papers/universe_polymorphism.pdf
+  ;; http://people.cs.kuleuven.be/~jesper.cockx/Without-K/Pattern-matching-without-K.pdf
+  ;; http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.74
+  ;; http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf
 
-  ;; Core language. Surface langauge should provide short-hand, such as
-  ;; -> for non-dependent function types, and type inference.
+  ;; cicL is the core language of Cur. Very similar to TT (Idirs core)
+  ;; and Luo's UTT. Used to be similar to CIC, hence the name.
+  ;; Surface langauge should provide short-hand, such as -> for
+  ;; non-dependent function types, and type inference.
   (define-language cicL
     (i ::= natural)
     (U ::= (Unv i))
     (x ::= variable-not-otherwise-mentioned)
-    (v ::= (Π (x : t) t) (μ (x : t) t) (λ (x : t) t) x U)
-    (t e ::= (case e (x e) ...) v (t t)))
+    (v ::= (Π (x : t) t) (λ (x : t) t) elim x U)
+    (t e ::= v (t t)))
 
   (define x? (redex-match? cicL x))
   (define t? (redex-match? cicL t))
@@ -32,9 +45,9 @@
   (define U? (redex-match? cicL U))
 
   (module+ test
-    (require rackunit)
     (define-term Type (Unv 0))
     (check-true (x? (term T)))
+    (check-true (x? (term A)))
     (check-true (x? (term truth)))
     (check-true (x? (term zero)))
     (check-true (x? (term s)))
@@ -42,6 +55,8 @@
     (check-true (t? (term s)))
     (check-true (x? (term nat)))
     (check-true (t? (term nat)))
+    (check-true (t? (term A)))
+    (check-true (t? (term S)))
     (check-true (U? (term (Unv 0))))
     (check-true (U? (term Type)))
     (check-true (e? (term (λ (x_0 : (Unv 0)) x_0))))
@@ -78,13 +93,45 @@
      ----------------
      (unv-kind (Unv i_1) (Unv i_2) (Unv i_3))])
 
+  (define-judgment-form cicL
+    #:mode (α-equivalent I I)
+    #:contract (α-equivalent t t)
+
+    [----------------- "α-x"
+     (α-equivalent x x)]
+
+    [----------------- "α-U"
+     (α-equivalent U U)]
+
+    [(α-equivalent t_1 (subst t_3 x_1 x_0))
+     (α-equivalent t_0 t_2)
+     ----------------- "α-binder"
+     (α-equivalent (any (x_0 : t_0) t_1)
+                   (any (x_1 : t_2) t_3))]
+
+    [(α-equivalent e_0 e_2)
+     (α-equivalent e_1 e_3)
+     ----------------- "α-app"
+     (α-equivalent (e_0 e_1) (e_2 e_3))])
+  (module+ test
+    (check-holds (α-equivalent x x))
+    (check-not-holds (α-equivalent x y))
+    (check-holds (α-equivalent (λ (x : A) x)
+                               (λ (y : A) y))))
+
+
+
+
   ;; NB: Substitution is hard
+  ;; NB: Copy and pasted from Redex examples
   (define-metafunction cicL
     subst-vars : (x any) ... any -> any
     [(subst-vars (x_1 any_1) x_1) any_1]
-    [(subst-vars (x_1 any_1) (any_2 ...)) ((subst-vars (x_1 any_1) any_2) ...)]
+    [(subst-vars (x_1 any_1) (any_2 ...))
+     ((subst-vars (x_1 any_1) any_2) ...)]
     [(subst-vars (x_1 any_1) any_2) any_2]
-    [(subst-vars (x_1 any_1) (x_2 any_2) ... any_3) (subst-vars (x_1 any_1) (subst-vars (x_2 any_2) ... any_3))]
+    [(subst-vars (x_1 any_1) (x_2 any_2) ... any_3)
+     (subst-vars (x_1 any_1) (subst-vars (x_2 any_2) ... any_3))]
     [(subst-vars any) any])
 
   (define-metafunction cicL
@@ -92,19 +139,23 @@
     [(subst U x t) U]
     [(subst x x t) t]
     [(subst x_0 x t) x_0]
-    [(subst (any (x : t_0) t_1) x t) (any (x : (subst t_0 x t)) t_1)]
-    ;; TODO: Broken: needs capture avoiding, but currently require
-    ;; binders to be the same in term/type, so this is not a local
-    ;; change.
-    [(subst (any (x_0 : t_0) t_1) x t) (any (x_0 : (subst t_0 x t)) (subst t_1 x t)) ]
+    [(subst (any (x : t_0) t_1) x t)
+     (any (x : (subst t_0 x t)) t_1)]
+    [(subst (any (x_0 : t_0) t_1) x t)
+     (any (x_new : (subst (subst-vars (x_0 x_new) t_0) x t))
+       (subst (subst-vars (x_0 x_new) t_1) x t))
+     (where x_new
+            ,(variable-not-in
+               (term (x_0 t_0 x t t_1))
+               (term x_0)))]
     [(subst (e_0 e_1) x t) ((subst e_0 x t) (subst e_1 x t))]
-    [(subst (case e (x_0 e_0) ...) x t)
-     (case (subst e x t)
-       (x_0 (subst e_0 x t)) ...)])
+    [(subst elim x t) elim])
   (module+ test
-    (check-equal?
-      (term (Π (a : S) (Π (b : B) ((and S) B))))
-      (term (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
+    (check-true (t? (term (Π (a : A) (Π (b : B) ((and A) B))))))
+    (check-holds
+      (α-equivalent
+        (Π (a : S) (Π (b : B) ((and S) B)))
+        (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
   ;; NB:
   ;; TODO: Why do I not have tests for substitutions?!?!?!?!?!?!?!!?!?!?!?!?!?!!??!?!
 
@@ -115,95 +166,213 @@
      (subst-all (subst t x_0 e_0) (x ...) (e ...))])
 
   (define-extended-language cic-redL cicL
-    (E hole (E t) (case E (x e) ...)))
+    (E   ::= hole (v E) (E e)) ;; call-by-value
+    ;; Σ (signature). (inductive-name : type ((constructor : type) ...))
+    (Σ   ::= ∅ (Σ (x : t ((x : t) ...))))
+    (Ξ Φ ::= hole (Π (x : t) Ξ)) ;;(Telescope)
+    ;; NB: Does an apply context correspond to a substitution (γ)?
+    (Θ   ::= hole (Θ e)))        ;;(Apply context)
+  (define Σ? (redex-match? cic-redL Σ))
+  (define Ξ? (redex-match? cic-redL Ξ))
+  (define Φ? (redex-match? cic-redL Φ))
+  (define Θ? (redex-match? cic-redL Θ))
+  (define E? (redex-match? cic-redL E))
 
-  (define-metafunction cicL
-    inductive-name : t -> x or #f
-    [(inductive-name x) x]
-    [(inductive-name (t_1 t_2)) (inductive-name t_1)]
-    [(inductive-name t) #f])
-  (module+ test
-    (check-equal?
-      (term and)
-      (term (inductive-name ((and A) B)))))
-
-  (define-metafunction cicL
-    inductive-apply : t t -> t
-    [(inductive-apply e x) e]
-    [(inductive-apply e (e_1 e_2))
-     ((inductive-apply e e_1) e_2)])
-
-  ;; TODO: Congruence-closure instead of β
-  (define ==β
-    (reduction-relation cic-redL
-      (==> ((Π (x : t_0) t_1) t_2)
-           (subst t_1 x t_2))
-      (==> ((λ (x : t) e_0) e_1)
-           (subst e_0 x e_1))
-      (==> ((μ (x : t) e_0) e_1)
-           ((subst e_0 x (μ (x : t) e_0)) e_1))
-      (==> (case e_9
-             (x_0 e_0) ... (x e) (x_r e_r) ...)
-           (inductive-apply e e_9)
-           (where x (inductive-name e_9)))
-      with
-      [(--> (in-hole E t_0) (in-hole E t_1))
-       (==> t_0 t_1)]))
-
-  (define-metafunction cic-redL
-    reduce : e -> e
-    [(reduce e) ,(car (apply-reduction-relation* ==β (term e)))])
-  (module+ test
-    (check-equal? (term (reduce (Unv 0))) (term (Unv 0)))
-    (check-equal? (term (reduce ((λ (x : t) x) (Unv 0)))) (term (Unv 0)))
-    (check-equal? (term (reduce ((Π (x : t) x) (Unv 0)))) (term (Unv 0)))
-    ;; NB: Currently not reducing under binders. I forget why.
-    (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0)))))
-                  (term (Π (x : t) (Unv 0))))
-    (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) x))))
-                  (term (Π (x : t) x)))
-    (check-equal? (term (reduce (case (s z) (z (s z)) (s (λ (x : nat)
-                                                            (s (s x)))))))
-                  (term (s (s z))))
-    (check-equal? (term (reduce (case (s (s (s z))) (z (s z)) (s (λ (x : nat)
-                                                            (s (s x)))))))
-                  (term (s (s (s (s z)))))))
-
-  ;; TODO: Bi-directional and inference?
-  ;; http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
-
-  (define-extended-language cic-typingL cicL
-    (Σ Γ ::= ∅ (Γ x : t)))
-
-  (define Σ? (redex-match? cic-typingL Σ))
-  (define Γ? (redex-match? cic-typingL Γ))
   (module+ test
     ;; TODO: Rename these signatures, and use them in all future tests.
-    (define Σ (term (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))))
-
+    (define Σ (term (∅ (nat : (Unv 0) ((zero : nat) (s : (Π (x : nat) nat)))))))
     (define Σ0 (term ∅))
-    (define Σ2 (term (((∅ nat : (Unv 0)) z : nat) s : (Π (x : nat) nat))))
-    (define Σ3 (term (∅ and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))))))
-    (define Σ4 (term (,Σ3 conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B))))))))
-
+    (define Σ3 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ()))))
+    (define Σ4 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                               ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))))))
     (check-true (Σ? Σ0))
-    (check-true (Σ? Σ2))
+    (check-true (Σ? Σ))
     (check-true (Σ? Σ4))
     (check-true (Σ? Σ3))
-    (check-true (Σ? Σ4)))
+    (check-true (Σ? Σ4))
+    (define sigma (term ((((((∅ (true : (Unv 0) ((T : true))))
+                                (false : (Unv 0) ()))
+                                (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                                   ()))
+                                (nat : (Unv 0) ()))
+                                (heap : (Unv 0) ()))
+                                (pre : (Π (temp808 : heap) (Unv 0)) ()))))
+    (check-true (Σ? (term (∅ (true : (Unv 0) ((T : true)))))))
+    (check-true (Σ? (term (∅ (false : (Unv 0) ())))))
+    (check-true (Σ? (term (∅ (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                                  ())))))
+    (check-true (Σ? (term (∅ (nat : (Unv 0) ())))))
+    (check-true (Σ? (term (∅ (pre : (Π (temp808 : heap) (Unv 0)) ())))))
+
+    (check-true (Σ? (term ((∅ (true : (Unv 0) ((T : true)))) (false : (Unv 0) ())))))
+    (check-true (Σ? (term (((∅ (true : (Unv 0) ((T : true)))) (false : (Unv 0) ()))
+                               (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                                  ())))))
+    (check-true (Σ? sigma)))
+
+  (define-metafunction cic-redL
+    append-Σ : Σ Σ -> Σ
+    [(append-Σ Σ ∅) Σ]
+    [(append-Σ Σ_2 (Σ_1 (x : t ((x_c : t_c) ...))))
+     ((append-Σ Σ_2 Σ_1) (x : t ((x_c : t_c) ...)))])
+
+  ;; TODO: Test
+  (define-metafunction cic-redL
+    apply-telescope : t Ξ -> t
+    [(apply-telescope t hole) t]
+    [(apply-telescope t_0 (Π (x : t) Ξ)) (apply-telescope (t_0 x) Ξ)])
+
+  (define-metafunction cic-redL
+    apply-telescopes : t (Ξ ...) -> t
+    [(apply-telescopes t ()) t]
+    [(apply-telescopes t (Ξ_0 Ξ_rest ...))
+     (apply-telescopes (apply-telescope t Ξ_0) (Ξ_rest ...))])
+
+  ;; NB: Depends on clause order
+  (define-metafunction cic-redL
+    select-arg : x (x ...) (Θ e) -> e
+    [(select-arg x (x x_r ...) (in-hole Θ (hole e))) e]
+    [(select-arg x (x_1 x_r ...) (in-hole Θ (hole e)))
+     (select-arg x (x_r ...) Θ)])
+
+  (define-metafunction cic-redL
+    method-lookup : Σ x x (Θ e) -> e
+    [(method-lookup Σ x_D x_ci Θ)
+     (select-arg x_ci (x_0 ...) Θ)
+     (where ((x_0 : t_0) ...) (constructors-for Σ x_D))])
+  (module+ test
+    (check-equal?
+      (term (method-lookup ,Σ nat s
+            ((hole (s zero))
+             (λ (x : nat) (λ (ih-x : nat) (s (s zero)))))))
+      (term (λ (x : nat) (λ (ih-x : nat) (s (s zero)))))))
+
+  ;; Create the recursive applications of elim to the recursive
+  ;; arguments of an inductive constructor.
+  ;; TODO: Poorly documented, and poorly tested.
+  (define-metafunction cic-redL
+    elim-recur : x e Θ Θ Θ (x ...) -> Θ
+    [(elim-recur x_D e_P Θ
+       (in-hole Θ_m (hole e_mi))
+       (in-hole Θ_i (hole (in-hole Θ_r x_ci)))
+       (x_c0 ... x_ci x_c1 ...))
+     ((elim-recur x_D e_P Θ Θ_m Θ_i (x_c0 ... x_ci x_c1 ...))
+      (in-hole Θ (((elim x_D) (in-hole Θ_r x_ci)) e_P)))]
+    [(elim-recur x_D e_P Θ Θ_i Θ_nr (x ...)) hole])
+  (module+ test
+    (check-true
+      (redex-match? cic-redL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero))))
+    (check-equal?
+      (term (elim-recur nat (λ (x : nat) nat)
+              ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              (hole zero)
+              (zero s)))
+      (term (hole (((((elim nat) zero) (λ (x : nat) nat)) (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))))))
+    (check-equal?
+      (term (elim-recur nat (λ (x : nat) nat)
+              ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              (hole (s zero))
+              (zero s)))
+      (term (hole (((((elim nat) (s zero)) (λ (x : nat) nat)) (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))))))
+
+  (define-judgment-form cic-redL
+    #:mode (length-match I I)
+    #:contract (length-match Θ (x ...))
+    [----------------------
+     (length-match hole ())]
+
+    [(length-match Θ (x_r ...))
+     ----------------------
+     (length-match (Θ e) (x x_r ...))])
+
+  (define cic-->
+    (reduction-relation cic-redL
+      (--> (Σ (in-hole E ((any (x : t_0) t_1) t_2)))
+           (Σ (in-hole E (subst t_1 x t_2)))
+           -->β)
+      (--> (Σ (in-hole E (in-hole Θ_m (((elim x_D) (in-hole Θ_i x_ci)) e_P))))
+           (Σ (in-hole E (in-hole Θ_r (in-hole Θ_i e_mi))))
+           (where ((x_c : t_c) ... (x_ci : t_ci) (x_cr : t_cr) ...) (constructors-for Σ x_D))
+           ;; There should be a number of methods equal to the number of
+           ;; constructors; to ensure E doesn't capture methods
+           (judgment-holds (length-match Θ_m (x_c ... x_ci x_cr ...)))
+           (where e_mi (method-lookup Σ x_D x_ci Θ_m))
+           (where Θ_r (elim-recur x_D e_P Θ_m Θ_m Θ_i (x_c ... x_ci x_cr ...)))
+           -->elim)))
+
+  (define-metafunction cic-redL
+    reduce : Σ e -> e
+    [(reduce Σ e) e_r
+     (where (_ e_r) ,(car (apply-reduction-relation* cic--> (term (Σ e)))))])
+  (module+ test
+    (check-equal? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
+    (check-equal? (term (reduce ∅ ((λ (x : t) x) (Unv 0)))) (term (Unv 0)))
+    (check-equal? (term (reduce ∅ ((Π (x : t) x) (Unv 0)))) (term (Unv 0)))
+    ;; NB: Currently not reducing under binders. I forget why.
+    (check-equal? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0)))))
+                  (term (Π (x : t) (Unv 0))))
+    (check-equal? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x))))
+                  (term (Π (x : t) ((Π (x_0 : t) (x_0 x)) x))))
+    (check-equal? (term (reduce ,Σ (((((elim nat) zero) (λ (x : nat) nat))
+                                    (s zero))
+                                    (λ (x : nat) (λ (ih-x : nat)
+                                        (s (s x)))))))
+                  (term (s zero)))
+    (check-equal? (term (reduce ,Σ (((((elim nat) (s zero)) (λ (x : nat) nat))
+                                    (s zero))
+                                    (λ (x : nat) (λ (ih-x : nat)
+                                        (s (s x)))))))
+                  (term (s (s zero))))
+    (check-equal? (term (reduce ,Σ (((((elim nat) (s (s (s zero)))) (λ (x : nat) nat))
+                                     (s zero))
+                                     (λ (x : nat) (λ (ih-x : nat) (s (s x)))))))
+                  (term (s (s (s (s zero))))))
+
+    (check-equal?
+      (term (reduce ,Σ
+        (((((elim nat) (s (s zero))) (λ (x : nat) nat))
+          (s (s zero)))
+         (λ (x : nat) (λ (ih-x : nat) (s ih-x))))))
+      (term (s (s (s (s zero)))))))
+
+  (define-judgment-form cic-redL
+    #:mode (equivalent I I I)
+    #:contract (equivalent Σ t t)
+
+    [(where t_2 (reduce Σ t_0))
+     (where t_3 (reduce Σ t_1))
+     (α-equivalent t_2 t_3)
+     ----------------- "≡-αβ"
+     (equivalent Σ t_0 t_1)])
+
+  (define-extended-language cic-typingL cic-redL
+    ;; NB: There may be a bijection between Γ and Ξ. That's
+    ;; NB: interesting.
+    (Γ   ::= ∅ (Γ x : t)))
+  (define Γ? (redex-match? cic-typingL Γ))
 
   (define-metafunction cic-typingL
-    append-env : Γ Γ -> Γ
-    [(append-env Γ ∅) Γ]
-    [(append-env Γ_2 (Γ_1 x : t))
-     ((append-env Γ_2 Γ_1) x : t)])
+    append-Γ : Γ Γ -> Γ
+    [(append-Γ Γ ∅) Γ]
+    [(append-Γ Γ_2 (Γ_1 x : t))
+     ((append-Γ Γ_2 Γ_1) x : t)])
 
   ;; NB: Depends on clause order
   (define-metafunction cic-typingL
-    lookup : Γ x -> t or #f
-    [(lookup ∅ x) #f]
-    [(lookup (Γ x : t) x) t]
-    [(lookup (Γ x_0 : t_0) x_1) (lookup Γ x_1)])
+    lookup-Γ : Γ x -> t or #f
+    [(lookup-Γ ∅ x) #f]
+    [(lookup-Γ (Γ x : t) x) t]
+    [(lookup-Γ (Γ x_0 : t_0) x_1) (lookup-Γ Γ x_1)])
+
+  ;; NB: Depends on clause order
+  (define-metafunction cic-redL
+    lookup-Σ : Σ x -> t or #f
+    [(lookup-Σ ∅ x) #f]
+    [(lookup-Σ (Σ (x : t ((x_1 : t_1) ...))) x) t]
+    [(lookup-Σ (Σ (x_0 : t_0 ((x_1 : t_1) ... (x : t) (x_2 : t_2) ...))) x) t]
+    [(lookup-Σ (Σ (x_0 : t_0 ((x_1 : t_1) ...))) x) (lookup-Σ Σ x)])
 
   ;; NB: Depends on clause order
   (define-metafunction cic-typingL
@@ -212,88 +381,10 @@
     [(remove (Γ x : t) x) Γ]
     [(remove (Γ x_0 : t_0) x_1) (remove Γ x_1)])
 
-  (define-metafunction cic-typingL
-    result-type : Σ t -> t or #f
-    [(result-type Σ (Π (x : t) e)) (result-type Σ e)]
-    [(result-type Σ (e_1 e_2)) (result-type Σ e_1)]
-    [(result-type Σ x) ,(and (term (lookup Σ x)) (term x))]
-    [(result-type Σ t) #f])
-  (module+ test
-    (check-equal? (term nat) (term (result-type ,Σ (Π (x : nat) nat))))
-    (check-equal? (term nat) (term (result-type ,Σ nat))))
-
-  (define-judgment-form cic-typingL
-    #:mode (constructor-for I I O)
-    #:contract (constructor-for Σ t x)
-
-    [(where t_0 (result-type Σ t))
-     -------------
-     (constructor-for (Σ x : t) t_0 x)]
-
-    [(constructor-for Σ t_1 x)
-     -------------
-     (constructor-for (Σ x_0 : t_0) t_1 x)])
-  (module+ test
-    (check-true
-      (judgment-holds (constructor-for ((∅ truth : (Unv 0)) T : truth) truth T)))
-    (check-true
-      (judgment-holds
-        (constructor-for ((∅ nat : (Unv 0)) zero : nat)
-                         nat zero)))
-    (check set=?
-      (judgment-holds
-        (constructor-for (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))
-                         nat x) x)
-      (list (term zero) (term s))))
-  (define-metafunction cic-typingL
-    constructors-for : Σ x (x ...) -> #t or #f
-    [(constructors-for Σ x_0 (x ...))
-     ,((lambda (x y) (and (set=? x y) (= (length x) (length y))))
-       (term (x ...))
-       (judgment-holds (constructor-for Σ x_0 x_00) x_00))])
-  (module+ test
-    (check-true
-      (term (constructors-for (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))
-                         nat (zero s))))
-    (check-false
-      (term (constructors-for (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))
-                         nat (zero))))
-    (check-true
-      (term (constructors-for ,Σ4 and (conj)))))
-
-  (define-metafunction cicL
-    branch-type : t t t -> t
-    [(branch-type t_ind (Π (x_0 : t) e_0) (Π (x_1 : t) e_1))
-     (branch-type t_ind e_0 e_1)]
-    ;[(branch-type t_ind t_ind t) t])
-    [(branch-type t_ind t_other t) t])
-  (module+ test
-    (check-equal? (term (Unv 0)) (term (branch-type nat (lookup ,Σ zero) (Unv 0))))
-    (check-equal? (term nat) (term (branch-type nat nat nat)))
-    (check-equal? (term (Unv 0)) (term (branch-type nat (lookup ,Σ s) (Π (x : nat) (Unv 0)))))
-    (check-equal?
-      (term (Unv 0))
-      (term (branch-type and (lookup ,Σ4 conj)
-              (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) (Unv 0)))))))))
-
-  (define-metafunction cic-typingL
-    branch-types-match : Σ (x ...) (t ...) t t -> #t or #f
-    [(branch-types-match Σ (x ...) (t_11 ...) t t_1)
-     ,(andmap (curry equal? (term t)) (term ((branch-type t_1 (lookup Σ x) t_11) ...)))])
-  (module+ test
-    (check-true
-      (term (branch-types-match ((∅ truth : (Unv 0)) T : truth) () () (Unv 0) nat)))
-    (check-true
-      (term (branch-types-match ,Σ (zero s) ((Unv 0) (Π (x : nat) (Unv 0))) (Unv 0) nat)))
-    (check-true
-      (term (branch-types-match ,Σ (zero s) (nat (Π (x : nat) nat)) nat nat))))
-
   ;; TODO: Add positivity checking.
   (define-metafunction cicL
     positive : t any -> #t or #f
-    ;; (Unv 0); not a inductive constructor
     [(positive any_1 any_2) #t])
-
   (module+ test
     (check-true (term (positive nat nat)))
     (check-true (term (positive (Π (x : (Unv 0)) (Π (y : (Unv 0)) (Unv 0))) #f)))
@@ -310,248 +401,526 @@
 
     (check-true (term (positive (Unv 0) #f))))
 
+  ;; Holds when the signature Σ and typing context Γ are well-formed.
   (define-judgment-form cic-typingL
     #:mode (wf I I)
     #:contract (wf Σ Γ)
 
-    [-----------------
+    [----------------- "WF-Empty"
      (wf ∅ ∅)]
 
-    [(types Σ Γ t t_0)
+    [(type-infer Σ Γ t t_0)
      (wf Σ Γ)
-     -----------------
+     ----------------- "WF-Var"
      (wf Σ (Γ x : t))]
 
-    [(types Σ ∅ t t_0)
-     (wf Σ ∅)
-     (side-condition (positive t (result-type Σ t)))
-     -----------------
-     (wf (Σ x : t) ∅)])
+    [(wf Σ ∅)
+     (type-infer Σ ∅ t_D U_D)
+     (type-infer Σ (∅ x_D : t_D) t_c U_c) ...
+     ;; NB: Ugh this should be possible with pattern matching alone ....
+     (side-condition ,(map (curry equal? (term Ξ_D)) (term (Ξ_D* ...))))
+     (side-condition ,(map (curry equal? (term x_D)) (term (x_D* ...))))
+     (side-condition (positive t_D (t_c ...)))
+     ----------------- "WF-Inductive"
+     (wf (Σ (x_D : (name t_D (in-hole Ξ_D t))
+            ;; Checks that a constructor for x actually produces an x, i.e., that
+            ;; the constructor is well-formed.
+            ((x_c : (name t_c (in-hole Ξ_D* (in-hole Φ (in-hole Θ x_D*))))) ...))) ∅)])
   (module+ test
-    (check-true (judgment-holds (wf ∅ ∅)))
-    (check-true (judgment-holds (wf (∅ truth : (Unv 0)) ∅)))
-    (check-true (judgment-holds (wf ∅ (∅ x : (Unv 0)))))
-    (check-true (judgment-holds (wf (∅ nat : (Unv 0)) (∅ x : nat))))
-    (check-true (judgment-holds (wf (∅ nat : (Unv 0)) (∅ x : (Π (x : nat) nat))))))
+    (check-true (judgment-holds (wf ,Σ0 ∅)))
+    (check-true (redex-match? cic-redL (in-hole Ξ (Unv 0)) (term (Unv 0))))
+    (check-true (redex-match? cic-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
+                             (term (Π (x : nat) nat))))
+    (define (bindings-equal? l1 l2)
+      (map set=? l1 l2))
+    (check-pred
+      (curry bindings-equal?
+             (list (list
+                     (make-bind 'Ξ (term (Π (x : nat) hole)))
+                     (make-bind 'Φ (term hole))
+                     (make-bind 'Θ (term hole)))
+                   (list
+                     (make-bind 'Ξ (term hole))
+                     (make-bind 'Φ (term (Π (x : nat) hole)))
+                     (make-bind 'Θ (term hole)))))
+      (map match-bindings (redex-match cic-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
+                    (term (Π (x : nat) nat)))))
+    (check-pred
+      (curry bindings-equal?
+             (list
+                   (list
+                     (make-bind 'Φ (term (Π (x : nat) hole)))
+                     (make-bind 'Θ (term hole)))))
+      (map match-bindings (redex-match cic-redL (in-hole hole (in-hole Φ (in-hole Θ nat)))
+                    (term (Π (x : nat) nat)))))
 
-  ;; TODO: Add termination checking
-  (define-metafunction cicL
-    terminates? : t -> #t or #f
-    [(terminates? t) #t])
+    (check-true
+      (redex-match? cic-redL
+        (in-hole hole (in-hole hole (in-hole hole nat)))
+        (term nat)))
+    (check-true
+      (redex-match? cic-redL
+        (in-hole hole (in-hole (Π (x : nat) hole) (in-hole hole nat)))
+        (term (Π (x : nat) nat))))
+    (check-holds (wf (∅ (nat : (Unv 0) ())) ∅))
+
+    (check-holds (wf ,Σ0 ∅))
+    (check-holds (type-infer ∅ ∅ (Unv 0) U))
+    (check-holds (type-infer ∅ (∅ nat : (Unv 0)) nat U))
+    (check-holds (type-infer ∅ (∅ nat : (Unv 0)) (Π (x : nat) nat) U))
+    (check-true (term (positive nat (nat (Π (x : nat) nat)))))
+    (check-holds
+      (wf (∅ (nat : (Unv 0) ((zero : nat)))) ∅))
+    (check-holds
+      (wf (∅ (nat : (Unv 0) ((s : (Π (x : nat) nat))))) ∅))
+    (check-holds (wf ,Σ ∅))
+
+    (check-holds (wf ,Σ3 ∅))
+    (check-holds (wf ,Σ4 ∅))
+    (check-holds (wf (∅ (truth : (Unv 0) ())) ∅))
+    (check-holds (wf ∅ (∅ x : (Unv 0))))
+    (check-holds (wf (∅ (nat : (Unv 0) ())) (∅ x : nat)))
+    (check-holds (wf (∅ (nat : (Unv 0) ())) (∅ x : (Π (x : nat) nat)))))
+
+  ;; Returns the inductive hypotheses required for eliminating the
+  ;; inductively defined type x_D with motive t_P, where the telescope
+  ;; Φ are the inductive arguments to a constructor for x_D
+  (define-metafunction cic-redL
+    hypotheses-for : x t Φ -> Φ
+    [(hypotheses-for x_D t_P hole) hole]
+    [(hypotheses-for x_D t_P (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
+     ;; TODO: Thread through Σ for reduce
+     (Π (x_h : (in-hole Φ (reduce ∅ ((in-hole Θ t_P) (apply-telescope x Φ)))))
+        (hypotheses-for x_D t_P Φ_1))
+     ;; NB: Lol hygiene
+     (where x_h ,(string->symbol (format "~a-~a" 'ih (term x))))])
+
+  ;; Returns the inductive arguments to a constructor for the
+  ;; inducitvely defined type x_D, where the telescope Φ are the
+  ;; non-parameter arguments to the constructor.
+  (define-metafunction cic-redL
+    inductive-args : x Φ -> Φ
+    [(inductive-args x_D hole) hole]
+    [(inductive-args x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
+     (Π (x : (in-hole Φ (in-hole Θ x_D))) (inductive-args x_D Φ_1))]
+    ;; NB: Depends on clause order
+    [(inductive-args x_D (Π (x : t) Φ_1))
+     (inductive-args x_D Φ_1)])
+
+  ;; Returns the methods required for eliminating the inductively
+  ;; defined type x_D, whose parameters/indices are Ξ_pi and whose
+  ;; constructors are ((x_ci : t_ci) ...), with motive t_P.
+  (define-metafunction cic-redL
+    methods-for : x Ξ t ((x : t) ...) -> Ξ
+    [(methods-for x_D Ξ_pi t_P ()) hole]
+    [(methods-for x_D Ξ_pi t_P ((x_ci : (in-hole Ξ_pi (in-hole Φ (in-hole Θ x_D))))
+                                (x_c : t) ...))
+     (Π (x_mi : (in-hole Ξ_pi (in-hole Φ (in-hole Φ_h
+                  ;; NB: Manually reducing types because no conversion
+                  ;; NB: rule
+                  ;; TODO: Thread through Σ for reduce
+                  ;; TODO: Might be able to remove this now that I have
+                  ;; TODO: equivalence in type-check
+                  (reduce ∅ ((in-hole Θ t_P) (apply-telescopes x_ci (Ξ_pi Φ))))))))
+        (methods-for x_D Ξ_pi t_P ((x_c : t) ...)))
+     (where Φ_h (hypotheses-for x_D t_P (inductive-args x_D Φ)))
+     ;; NB: Lol hygiene
+     (where x_mi ,(string->symbol (format "~a-~a" 'm (term x_ci))))])
   (module+ test
-    (check-false (term (terminates? (μ (x : (Unv 0)) x))))
-    (check-false (term (terminates? (μ (x : (Unv 0)) (λ (y : (Unv 0)) (x y))))))
-    (check-true (term (terminates? (μ (x : (Unv 0)) (λ (y : (Unv 0)) y))))))
+    (check-equal?
+      (term (methods-for nat hole P ((zero : nat) (s : (Π (x : nat) nat)))))
+      (term (Π (m-zero : (P zero))
+          (Π (m-s : (Π (x : nat) (Π (ih-x : (P x)) (P (s x)))))
+             hole))))
+    (check-equal?
+      (term (methods-for nat hole (λ (x : nat) nat) ((zero : nat) (s : (Π (x : nat) nat)))))
+      (term (Π (m-zero : nat) (Π (m-s : (Π (x : nat) (Π (ih-x : nat) nat)))
+                                     hole))))
+    (check-equal?
+      (term (methods-for and (Π (A : Type) (Π (B : Type) hole))
+              (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
+              ((conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B)
+                                                                    ((and A) B)))))))))
+      (term (Π (m-conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) true)))))
+               hole)))
+    (check-true (x? (term false)))
+    (check-true (Ξ? (term hole)))
+    (check-true (t? (term (λ (y : false) (Π (x : Type) x)))))
+    (check-true (redex-match? cicL ((x : t) ...) (term ())))
+    (check-equal?
+      (term (methods-for false hole (λ (y : false) (Π (x : Type) x))
+              ()))
+      (term hole)))
 
+  ;; Returns the inductively defined type that x constructs
+  ;; NB: Depends on clause order
+  (define-metafunction cic-redL
+    constructor-of : Σ x -> x
+    [(constructor-of (Σ (x : t ((x_0 : t_0) ... (x_c : t_c) (x_1 : t_1) ...)))
+                     x_c) x]
+    [(constructor-of (Σ (x_1 : t_1 ((x_c : t) ...))) x)
+     (constructor-of Σ x)])
+  (module+ test
+    (check-equal?
+      (term (constructor-of ,Σ zero))
+      (term nat))
+    (check-equal?
+      (term (constructor-of ,Σ s))
+      (term nat)))
+
+  ;; Returns the constructors for the inductively defined type x_D in
+  ;; the signature Σ
+  (define-metafunction cic-redL
+    constructors-for : Σ x -> ((x : t) ...) or #f
+    ;; NB: Depends on clause order
+    [(constructors-for ∅ x_D) #f]
+    [(constructors-for (Σ (x_D : t_D ((x : t) ...))) x_D)
+     ((x : t) ...)]
+    [(constructors-for (Σ (x_1 : t_1 ((x : t) ...))) x_D)
+     (constructors-for Σ x_D)])
+  (module+ test
+    (check-equal?
+      (term (constructors-for ,Σ nat))
+      (term ((zero : nat) (s : (Π (x : nat) nat)))))
+    (check-equal?
+      (term (constructors-for ,sigma false))
+      (term ())))
+
+  ;; Holds when an apply context Θ provides arguments that match the
+  ;; telescope Ξ
   (define-judgment-form cic-typingL
-    #:mode (types I I I O)
-    #:contract (types Σ Γ e t)
+    #:mode (telescope-types I I I I)
+    #:contract (telescope-types Σ Γ Θ Ξ)
+
+    [----------------- "TT-Hole"
+     (telescope-types Σ Γ hole hole)]
+
+    [(type-check Σ Γ e t)
+     (telescope-types Σ Γ Θ Ξ)
+     ----------------- "TT-Match"
+     (telescope-types Σ Γ (in-hole Θ (hole e)) (Π (x : t) Ξ))])
+  (module+ test
+    (check-holds
+      (telescope-types ,Σ ∅ (hole zero) (Π (x : nat) hole)))
+    (check-true
+      (redex-match? cic-redL (in-hole Θ (hole e))
+                    (term ((hole zero) (λ (x : nat) x)))))
+    (check-holds
+      (telescope-types ,Σ ∅ (hole zero)
+                       (methods-for nat hole
+                                    (λ (x : nat) nat)
+                                    ((zero : nat)))))
+    (check-holds
+      (type-check ,Σ ∅ (λ (x : nat) (λ (ih-x : nat) x))
+             (Π (x : nat) (Π (ih-x : nat) nat))))
+    (check-holds
+      (telescope-types ,Σ ∅
+                       ((hole zero)
+                        (λ (x : nat) (λ (ih-x : nat) x)))
+                       (methods-for nat hole
+                                    (λ (x : nat) nat)
+                                    (constructors-for ,Σ nat))))
+    (check-holds
+      (telescope-types (,Σ4 (true : (Unv 0) ((tt : true))))
+                       ∅ (hole (λ (A : (Unv 0)) (λ (B : (Unv 0))
+                                                      (λ (a : A) (λ (b : B) tt)))))
+                       (methods-for and (Π (A : Type) (Π (B : Type) hole))
+                                    (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
+                                    (constructors-for ,Σ4 and))))
+    (check-holds
+      (telescope-types ,sigma (∅ x : false)
+                       hole
+                       (methods-for false hole (λ (y : false) (Π (x : Type) x))
+                                    ()))))
+
+  ;; TODO: Bi-directional and inference?
+  ;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
+
+  ;; Holds when e has type t under signature Σ and typing context Γ
+  (define-judgment-form cic-typingL
+    #:mode (type-infer I I I O)
+    #:contract (type-infer Σ Γ e t)
 
     [(unv-ok U_0 U_1)
      (wf Σ Γ)
      ----------------- "DTR-Axiom"
-     (types Σ Γ U_0 U_1)]
+     (type-infer Σ Γ U_0 U_1)]
 
-    [(where t (lookup Σ x))
+    [(where t (lookup-Σ Σ x))
      ----------------- "DTR-Inductive"
-     (types Σ Γ x t)]
+     (type-infer Σ Γ x t)]
 
-    ;; TODO: Require alpha-equiv here, at least.
-    [(where t (lookup Γ x))
+    [(where t (lookup-Γ Γ x))
      ----------------- "DTR-Start"
-     (types Σ Γ x t)]
+     (type-infer Σ Γ x t)]
 
-    [(types Σ Γ t_0 U_1)
-     (types Σ (Γ x : t_0) t U_2)
+    [(type-infer Σ Γ t_0 U_1)
+     (type-infer Σ (Γ x : t_0) t U_2)
      (unv-kind U_1 U_2 U)
      ----------------- "DTR-Product"
-     (types Σ Γ (Π (x : t_0) t) U)]
+     (type-infer Σ Γ (Π (x : t_0) t) U)]
 
-    [(types Σ Γ e_0 (Π (x_0 : t_0) t_1))
-     (types Σ Γ e_1 t_0)
+    [(type-infer Σ Γ e_0 (Π (x_0 : t_0) t_1))
+     (type-infer Σ Γ e_1 t_2)
+     (equivalent Σ t_0 t_2)
      ----------------- "DTR-Application"
-     (types Σ Γ (e_0 e_1) (subst t_1 x_0 e_1))]
+     (type-infer Σ Γ (e_0 e_1) (subst t_1 x_0 e_1))]
 
-    ;; TODO: This restriction that the names be the same is a little annoying
-    [(types Σ (Γ x : t_0) e t_1)
-     (types Σ Γ (Π (x : t_0) t_1) U)
+    [(type-infer Σ (Γ x : t_0) e t_1)
+     (type-infer Σ Γ (Π (x : t_0) t_1) U)
      ----------------- "DTR-Abstraction"
-     (types Σ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
+     (type-infer Σ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
 
-    [(side-condition (terminates? (μ (x : t_0) e)))
-     (types Σ (Γ x : t_0) e t_0)
-     (types Σ Γ t_0 U)
-     ----------------- "DTR-Fix"
-     (types Σ Γ (μ (x : t_0) e) t_0)]
+    [(type-infer Σ Γ x_D (in-hole Ξ U_D))
+     (type-infer Σ Γ e_D (in-hole Θ_ai x_D))
+     (type-infer Σ Γ e_P (in-hole Ξ_1 (Π (x : (in-hole Θ_Ξ x_D)) U_P)))
+     (equivalent Σ (in-hole Ξ (Unv 0)) (in-hole Ξ_1 (Unv 0)))
+     ;; methods
+     (telescope-types Σ Γ Θ_m (methods-for x_D Ξ e_P (constructors-for Σ x_D)))
+     ----------------- "DTR-Elim_D"
+     (type-infer Σ Γ (in-hole Θ_m (((elim x_D) e_D) e_P)) (reduce Σ ((in-hole Θ_ai e_P) e_D)))])
 
-    [(types Σ Γ e t_9)
-     (where t_1 (inductive-name t_9))
-     (side-condition (constructors-for Σ t_1 (x_0 x_1 ...)))
-     (types Σ Γ e_0 t_00)
-     (types Σ Γ e_1 t_11) ...
-     ;; TODO Some of these meta-functions aren't very consistent in terms
-     ;; of interface
-     (where t (branch-type t_1 (lookup Σ x_0) t_00))
-     (side-condition (branch-types-match Σ (x_1 ...) (t_11 ...) t t_1))
-     ----------------- "DTR-Case"
-     (types Σ Γ (case e (x_0 e_0) (x_1 e_1) ...) t)]
+  (define-judgment-form cic-typingL
+    #:mode (type-check I I I I)
+    #:contract (type-check Σ Γ e t)
 
-    ;; TODO: This shouldn't be a special case, but I failed to forall
-    ;; quantify properly over the branches in the above case, and I'm lazy.
-    ;; TODO: Seem to need bidirectional checking to pull this off
-    ;; http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
-    #;[(types Σ Γ e t_9)
-     (where t_1 (inductive-name t_9))
-     (side-condition (constructors-for Σ t_1 ()))
-     ----------------- "DTR-Case-Empty"
-     (types Σ Γ (case e) t)]
-
-    ;; TODO: beta-equiv
-    ;; This rule is no good for algorithmic checking; Redex infinitly
-    ;; searches it.
-    ;; Perhaps something closer to Zombies = type would be better.
-    ;; For now, reduce types
-    #;[(types Σ Γ e (in-hole E t))
-     (where t_0 (in-hole E t))
-     (where t_1 ,(car (apply-reduction-relation* ==β (term t_0))))
-     (types Σ Γ t_1 U)
-     ----------------- "DTR-Conversion"
-     (types Σ Γ e t_1)])
+    [(type-infer Σ Γ e t_0)
+     (equivalent Σ t t_0)
+     ----------------- "DTR-Check"
+     (type-check Σ Γ e t)])
   (module+ test
-    (check-true (judgment-holds (types ∅ ∅ (Unv 0) (Unv 1))))
-    (check-true (judgment-holds (types ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1))))
-    (check-true (judgment-holds (types ∅ (∅ x : (Unv 0)) x (Unv 0))))
-    (check-true (judgment-holds (types ∅ ((∅ x_0 : (Unv 0)) x_1 : (Unv 0))
-                                       (Π (x_3 : x_0) x_1) (Unv 0))))
+    (check-holds (type-infer ∅ ∅ (Unv 0) (Unv 1)))
+    (check-holds (type-infer ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1)))
+    (check-holds (type-infer ∅ (∅ x : (Unv 0)) x (Unv 0)))
+    (check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_1 : (Unv 0))
+                             (Π (x_3 : x_0) x_1) (Unv 0)))
+    (check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) x_0 U_1))
+    (check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_2 : x_0) (Unv 0) U_2))
+    (check-holds (unv-kind (Unv 0) (Unv 0) (Unv 0)))
+    (check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) (Π (x_2 : x_0) (Unv 0)) t))
 
-    (check-true (judgment-holds (types ∅ (∅ x_0 : (Unv 0)) x_0 U_1)))
-    (check-true (judgment-holds (types ∅ ((∅ x_0 : (Unv 0)) x_2 : x_0) (Unv 0) U_2)))
-    (check-true (judgment-holds (unv-kind (Unv 0) (Unv 0) (Unv 0))))
-    (check-true (judgment-holds (types ∅ (∅ x_0 : (Unv 0)) (Π (x_2 : x_0) (Unv 0)) t)))
-
-    (check-true (judgment-holds (types ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0)))))
-    (check-true (judgment-holds (types ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x))
-                                       (Π (y : (Unv 0)) (Π (x : y) y)))))
+    (check-holds (type-infer ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0))))
+    (check-holds (type-infer ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x))
+                             (Π (y : (Unv 0)) (Π (x : y) y))))
 
     (check-equal? (list (term (Unv 1)))
       (judgment-holds
-        (types ∅ ((∅ x1 : (Unv 0)) x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0)))
+        (type-infer ∅ ((∅ x1 : (Unv 0)) x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0)))
                U)
         U))
+    ;; ---- Elim
+    ;; TODO: Clean up/Reorganize these tests
     (check-true
-      (judgment-holds
-        (types ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0))
-               U)))
-    (check-true
-      (judgment-holds
-        (types ∅ (∅ x1 : (Unv 0)) (λ (x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0))))
-               t)))
-    (check-true
-      (judgment-holds (types ((∅ truth : (Unv 0)) T : truth)
-                             ∅
-                             T
-                             truth)))
-    (check-true
-      (judgment-holds (types ((∅ truth : (Unv 0)) T : truth)
-                             ∅
-                             (Unv 0)
-                             (Unv 1))))
-    (check-true
-      (judgment-holds (types ((∅ truth : (Unv 0)) T : truth)
-                             ∅
-                             (case T (T (Unv 0)))
-                             (Unv 1))))
+      (redex-match? cic-typingL
+                    (in-hole Θ_m (((elim x_D) e_D) e_P))
+                    (term ((((elim truth) T) (Π (x : truth) (Unv 1))) (Unv 0)))))
+    (define Σtruth (term (∅ (truth : (Unv 0) ((T : truth))))))
+    (check-holds (type-infer ,Σtruth ∅ truth (in-hole Ξ U)))
+    (check-holds (type-infer ,Σtruth ∅ T (in-hole Θ_ai truth)))
+    (check-holds (type-infer ,Σtruth ∅ (λ (x : truth) (Unv 1))
+                        (in-hole Ξ (Π (x : (in-hole Θ truth)) U))))
+    (check-equal?
+      (term (methods-for truth hole (λ (x : truth) (Unv 1)) ((T : truth))))
+      (term (Π (m-T : (Unv 1)) hole)))
+    (check-holds (telescope-types ,Σtruth ∅ (hole (Unv 0))
+                                  (methods-for truth hole
+                                               (λ (x : truth) (Unv 1))
+                                               ((T : truth)))))
+    (check-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
+                        ∅
+                        ((((elim truth) T) (λ (x : truth) (Unv 1))) (Unv 0))
+                        (Unv 1)))
 
-    (check-false
-      (judgment-holds (types ((∅ truth : (Unv 0)) T : truth)
-                             ∅
-                             (case T (T (Unv 0)) (T (Unv 0)))
-                             (Unv 1))))
+    (check-not-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
+                            ∅
+                            (((((elim truth) T) (Unv 1)) Type) Type)
+                            (Unv 1)))
+    (check-holds
+      (type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))
+    (check-holds
+      (type-infer ∅ (∅ x1 : (Unv 0)) (λ (x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0))))
+                  t))
     (define-syntax-rule (nat-test syn ...)
-      (check-true (judgment-holds
-                    (types (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))
-                           syn ...))))
+      (check-holds (type-infer ,Σ syn ...)))
     (nat-test ∅ (Π (x : nat) nat) (Unv 0))
     (nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
-    (nat-test ∅ (case zero (zero zero) (s (λ (x : nat) x)))
+
+    (check-holds
+      (type-infer ,Σ ∅ nat (in-hole Ξ U)))
+    (check-holds
+      (type-infer ,Σ ∅ zero (in-hole Θ_ai nat)))
+    (check-holds
+      (type-infer ,Σ ∅ (λ (x : nat) nat)
+             (in-hole Ξ (Π (x : (in-hole Θ nat)) U))))
+    (nat-test ∅ (((((elim nat) zero) (λ (x : nat) nat)) zero)
+                 (λ (x : nat) (λ (ih-x : nat) x)))
               nat)
     (nat-test ∅ nat (Unv 0))
     (nat-test ∅ zero nat)
     (nat-test ∅ s (Π (x : nat) nat))
     (nat-test ∅ (s zero) nat)
-    (nat-test ∅ (case zero (zero (s zero)) (s (λ (x : nat) (s (s x)))))
+    (nat-test ∅ (((((elim nat) zero) (λ (x : nat) nat))
+                  (s zero))
+                  (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
               nat)
-    (nat-test ∅ (case zero (zero (s zero)) (s (λ (x : nat) (s (s x)))))
-              nat)
-    (check-false (judgment-holds
-                    (types (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))
-                           ∅
-                           (case zero (zero (s zero)))
-                           nat)))
+    (nat-test (∅ n : nat)
+      (((((elim nat) n) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x)))
+      nat)
+    (check-holds
+      (type-check (,Σ (bool : (Unv 0) ((btrue : bool) (bfalse : bool))))
+             (∅ n2 : nat)
+             (((((elim nat) n2) (λ (x : nat) bool)) btrue) (λ (x : nat) (λ (ih-x : bool) bfalse)))
+             bool))
+    (check-not-holds
+      (type-check ,Σ ∅
+             ((((elim nat) zero) nat) (s zero))
+             nat))
     (define lam (term (λ (nat : (Unv 0)) nat)))
     (check-equal?
       (list (term (Π (nat : (Unv 0)) (Unv 0))))
-      (judgment-holds (types ,Σ0 ∅ ,lam t) t))
+      (judgment-holds (type-infer ,Σ0 ∅ ,lam t) t))
     (check-equal?
       (list (term (Π (nat : (Unv 0)) (Unv 0))))
-      (judgment-holds (types ,Σ2 ∅ ,lam t) t))
+      (judgment-holds (type-infer ,Σ ∅ ,lam t) t))
     (check-equal?
       (list (term (Π (x : (Π (y : (Unv 0)) y)) nat)))
-      (judgment-holds (types (∅ nat : (Unv 0)) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat))
+      (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat))
                             t) t))
     (check-equal?
       (list (term (Π (y : (Unv 0)) (Unv 0))))
-      (judgment-holds (types (∅ nat : (Unv 0)) ∅ (λ (y : (Unv 0)) y) t) t))
+      (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (y : (Unv 0)) y) t) t))
     (check-equal?
       (list (term (Unv 0)))
-      (judgment-holds (types (∅ nat : (Unv 0)) ∅
+      (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅
                             ((λ (x : (Π (y : (Unv 0)) (Unv 0))) (x nat))
                              (λ (y : (Unv 0)) y))
                             t) t))
     (check-equal?
       (list (term (Unv 0)) (term (Unv 1)))
       (judgment-holds
-        (types ,Σ4 ∅ (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))
+        (type-infer ,Σ4 ∅ (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))
                U) U))
+    (check-holds
+      (type-check ,Σ4 (∅ S : (Unv 0)) conj (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))
+    (check-holds
+      (type-check ,Σ4 (∅ S : (Unv 0))
+        conj (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : P) (Π (y : Q) ((and P) Q)))))))
+    (check-holds
+      (type-check ,Σ4 (∅ S : (Unv 0)) S (Unv 0)))
+    (check-holds
+      (type-check ,Σ4 (∅ S : (Unv 0)) (conj S)
+             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
+    (check-holds
+      (type-check ,Σ4 (∅ S : (Unv 0)) (conj S)
+             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
+    (check-holds
+      (type-check ,Σ4 ∅ (λ (S : (Unv 0)) (conj S))
+             (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
+    (check-holds
+      (type-check (,Σ4 (true : (Unv 0) ((tt : true)))) ∅
+             ((((conj true) true) tt) tt)
+             ((and true) true)))
+    (check-holds
+      (type-infer ,Σ4 ∅ and (in-hole Ξ U_D)))
+    (check-holds
+      (type-infer (,Σ4 (true : (Unv 0) ((tt : true)))) ∅
+             ((((conj true) true) tt) tt)
+             (in-hole Θ and)))
+    (check-holds
+      (type-infer (,Σ4 (true : (Unv 0) ((tt : true)))) ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
+             (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
+    (check-holds
+      (type-check (,Σ4 (true : (Unv 0) ((tt : true)))) ∅
+             ((((elim and) ((((conj true) true) tt) tt))
+               (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                              true))))
+              (λ (A : (Unv 0))
+                 (λ (B : (Unv 0))
+                    (λ (a : A)
+                       (λ (b : B) tt)))))
+             true))
+    (check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
+    (check-holds
+      (type-infer ,Σ4 ∅ and (in-hole Ξ U)))
+    (check-holds
+      (type-infer ,Σ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
+                  ab (in-hole Θ and)))
     (check-true
-      (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) conj (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B))))))))
-    (check-true
-      (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) S (Unv 0))))
-    (check-true
-      (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) (conj S)
-                             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
-    (check-true
-      (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) (conj S)
-                             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
-    (check-true
-      (judgment-holds (types ,Σ4 ∅ (λ (S : (Unv 0)) (conj S))
-                             (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))))
-    (check-true
-      (judgment-holds (types ((,Σ4 true : (Unv 0)) tt : true) ∅
-                             ((((conj true) true) tt) tt)
-                             ((and true) true))))
-    (check-true
-      (judgment-holds (types ((,Σ4 true : (Unv 0)) tt : true) ∅
-                             (case ((((conj true) true) tt) tt)
-                               (conj (λ (A : (Unv 0))
-                                        (λ (B : (Unv 0))
-                                           (λ (a : A)
-                                              (λ (b : B) a))))))
-                             A)))
-    (define sigma (term (((((((∅ true : (Unv 0)) T : true) false : (Unv 0)) equal : (Π (A : (Unv 0))
-                                                              (Π (B : (Unv 0)) (Unv 0))))
-        nat : (Unv 0)) heap : (Unv 0)) pre : (Π (temp808 : heap) (Unv 0)))))
+      (redex-match? cic-redL
+        (in-hole Ξ (Π (x : (in-hole Θ and)) U))
+        (term (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0)))))))
+    (check-holds
+      (type-infer ,Σ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
+                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                 ((and B) A))))
+                  (in-hole Ξ (Π (x : (in-hole Θ and)) U))))
+    (check-holds
+      (equivalent ,Σ4
+        (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))
+        (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : ((and P) Q)) (Unv 0))))))
+    (check-holds
+      (type-infer ,Σ4 ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                            ((and B) A))))
+             (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
+    (check-holds
+      (type-check ,Σ4
+                  (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q))
+             ((((elim and) ab)
+               (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                              ((and B) A)))))
+              (λ (A : (Unv 0))
+                 (λ (B : (Unv 0))
+                    (λ (a : A)
+                       (λ (b : B) ((((conj B) A) b) a))))))
+             ((and Q) P)))
+    (check-holds
+      (type-check (,Σ4 (true : (Unv 0) ((tt : true)))) ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) ((and B) A))))
+             (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))))
+    (check-holds
+      (type-infer (,Σ4 (true : (Unv 0) ((tt : true))))
+             ((∅ A : Type) B : Type)
+             (conj B)
+             t))
+    (check-holds
+      (type-check (,Σ4 (true : (Unv 0) ((tt : true)))) ∅
+             ((((elim and) ((((conj true) true) tt) tt))
+               (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                              ((and B) A)))))
+              (λ (A : (Unv 0))
+                 (λ (B : (Unv 0))
+                    (λ (a : A)
+                       (λ (b : B) ((((conj B) A) b) a))))))
+             ((and true) true)))
     (define gamma (term (∅ temp863 : pre)))
-    (check-true (judgment-holds (wf ,sigma ∅)))
-    (check-true (judgment-holds (wf ,sigma ,gamma)))
+    (check-holds (wf ,sigma ∅))
+    (check-holds (wf ,sigma ,gamma))
+    (check-holds
+      (type-infer ,sigma ,gamma (Unv 0) t))
+    (check-holds
+      (type-infer ,sigma ,gamma pre t))
+    (check-holds
+      (type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
+    (check-holds
+      (type-infer ,sigma ,gamma pre t))
+    (check-holds
+      (type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
+    (check-holds
+      (type-infer ,sigma (,gamma x : false) false (in-hole Ξ U_D)))
+    (check-holds
+      (type-infer ,sigma (,gamma x : false) x (in-hole Θ false)))
+    (check-holds
+      (type-infer ,sigma (,gamma x : false) (λ (y : false) (Π (x : Type) x))
+             (in-hole Ξ (Π (x : (in-hole Θ false)) U))))
     (check-true
-      (judgment-holds (types ,sigma ,gamma (Unv 0) t)))
-    (check-true
-      (judgment-holds (types ,sigma ,gamma pre t)))
-    (check-true
-      (judgment-holds (types ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1))))
-    (check-true
-      (judgment-holds (types ,sigma (,gamma x : false) (case x) t)))))
+      (redex-match? cic-typingL (in-hole Θ_m (((elim x_D) e_D) e_P))
+                    (term (((elim false) x) (λ (y : false) (Π (x : Type) x))))))
+    (check-holds
+      (type-check ,sigma (,gamma x : false)
+             (((elim false) x) (λ (y : false) (Π (x : Type) x)))
+             (Π (x : (Unv 0)) x)))))
 
 ;; This module just provide module language sugar over the redex model.
 
@@ -591,13 +960,12 @@
       [dep-lambda λ]
       [dep-app #%app]
 
-      [dep-fix fix]
-
       [dep-forall forall]
       [dep-forall ∀]
 
       [dep-inductive data]
-      [dep-case case]
+
+      [dep-elim elim]
 
       [dep-var #%top]
 
@@ -655,15 +1023,32 @@
             (error 'core-error "We built a bad sigma ~s" x))
           x)))
 
-    (define (extend-env/term env x t)
+    (define (extend-Γ/term env x t)
       (term (,(env) ,x : ,t)))
 
-    (define (extend-env/term! env x t) (env (extend-env/term env x t)))
+    (define (extend-Γ/term! env x t) (env (extend-Γ/term env x t)))
 
-    (define (extend-env/syn env x t)
-      (term (,(env) ,(syntax->datum x) : ,(cur->datum t))))
+    (define (extend-Γ/syn env x t)
+      (extend-Γ/term env (syntax->datum x) (cur->datum t)))
 
-    (define (extend-env/syn! env x t) (env (extend-env/syn env x t)))
+    (define (extend-Γ/syn! env x t) (env (extend-Γ/syn env x t)))
+
+    (define (extend-Σ/term env x t c*)
+      (term (,(env) (,x : ,t (,@c*)))))
+
+    (define (extend-Σ/term! env x t c*)
+      (env (extend-Σ/term env x t c*)))
+
+    (define (extend-Σ/syn env x t c*)
+      (extend-Σ/term env (syntax->datum x) (cur->datum t)
+        (for/list ([c (syntax->list c*)])
+          (syntax-case c ()
+            [(c : ct)
+             (parameterize ([gamma (extend-Γ/syn gamma x t)])
+               (term (,(syntax->datum #'c) : ,(cur->datum #'ct))))]))))
+
+    (define (extend-Σ/syn! env x t c*)
+      (env (extend-Σ/syn env x t c*)))
 
     (define bind-subst (make-parameter (list null null)))
 
@@ -675,13 +1060,18 @@
     ;; TODO: Still absurdly slow. Probably doing n^2 checks of sigma and
     ;; gamma. And lookup on sigma, gamma are linear, so probably n^2 lookup time.
     (define (type-infer/term t)
-      (let ([t (judgment-holds (types ,(sigma) ,(gamma) ,t t_0) t_0)])
+      (let ([t (judgment-holds (type-infer ,(sigma) ,(gamma) ,t t_0) t_0)])
         (and (pair? t) (car t))))
 
+    (define (type-check/term? e t)
+      (and (judgment-holds (type-check ,(sigma) ,(gamma) ,e ,t)) #t))
+
     (define (syntax->curnel-syntax syn) (denote syn (cur->datum syn)))
 
     (define (denote syn t)
-      #`(term (reduce (subst-all #,(datum->syntax syn t) #,(first (bind-subst)) #,(second (bind-subst))))))
+      (quasisyntax/loc
+        syn
+        (term (reduce #,(sigma) (subst-all #,(datum->syntax syn t) #,(first (bind-subst)) #,(second (bind-subst)))))))
 
     ;; TODO: Blanket disarming is probably a bad idea.
     (define orig-insp (variable-reference->module-declaration-inspector
@@ -692,7 +1082,7 @@
     (define (core-expand syn)
       (disarm
         (local-expand syn 'expression
-          (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π μ case
+          (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π elim
                                Unv #%datum))))))
 
     ;; Only type-check at the top-level, to prevent exponential
@@ -709,10 +1099,10 @@
           (let cur->datum ([syn syn])
             (syntax-parse (core-expand syn)
               #:literals (term reduce #%app subst-all)
-              #:datum-literals (case Π λ μ : Unv)
+              #:datum-literals (elim Π λ : Unv)
               [x:id (syntax->datum #'x)]
               [(subst-all e _ _) (syntax->datum #'e)]
-              [(reduce e) (cur->datum #'e)]
+              [(reduce Σ e) (cur->datum #'e)]
               [(term e) (cur->datum #'e)]
               [(Unv i) (term (Unv ,(syntax->datum #'i)))]
               ;; TODO: should really check that b is one of the binders
@@ -721,14 +1111,17 @@
               [(b:id (x:id : t) e)
                (let* ([x (syntax->datum #'x)]
                       [t (cur->datum #'t)]
-                      [e (parameterize ([gamma (extend-env/term gamma x t)])
+                      [e (parameterize ([gamma (extend-Γ/term gamma x t)])
                            (cur->datum #'e))])
                  (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
-              [(case e (ec eb) ...)
-               (term (case ,(cur->datum #'e)
-                           ,@(map (lambda (c b) `(,c ,(cur->datum b)))
-                                  (syntax->datum #'(ec ...))
-                                  (syntax->list #'(eb ...)))))]
+              [(elim t e P m ...)
+               (let* ([t (cur->datum #'t)]
+                      [e (cur->datum #'e)]
+                      [P (cur->datum #'P)]
+                      [e (term (((elim ,t) ,e) ,P))])
+                 (for/fold ([e e])
+                           ([m (syntax->list #'(m ...))])
+                   (term (,e ,(cur->datum m)))))]
               [(#%app e1 e2)
                (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
       (unless (and inner-expand? (type-infer/term reified-term))
@@ -740,27 +1133,28 @@
       reified-term)
 
     ;; Reflection tools
+    (define (normalize/syn syn)
+      (denote syn (term (reduce ,(sigma) (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst)))))))
+
+    (define (run-cur->datum syn)
+      (cur->datum (normalize/syn syn)))
 
     ;; TODO: OOps, type-infer doesn't return a cur term but a redex term
     ;; wrapped in syntax bla. This is bad.
     (define (type-infer/syn syn)
-      (let ([t (type-infer/term (cur->datum syn))])
+      (let ([t (type-infer/term (run-cur->datum syn))])
         (and t (datum->syntax syn t))))
 
     (define (type-check/syn? syn type)
-      (let ([t (type-infer/term (cur->datum syn))])
-        (equal? t (cur->datum type))))
-
-    (define (normalize/syn syn)
-      (denote syn (term (reduce (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst)))))))
+      (type-check/term? (run-cur->datum syn) (run-cur->datum type)))
 
     ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is
     ;; expanded until expansion reaches a Curnel form, or one of the
     ;; identifiers in ls.
     (define (cur-expand syn . ls)
       (disarm (local-expand syn 'expression
-                (append (syntax-e #'(Type dep-inductive dep-case dep-lambda dep-app
-                                   dep-fix dep-forall dep-var))
+                (append (syntax-e #'(Type dep-inductive dep-lambda dep-app
+                                   dep-elim dep-forall dep-var))
                         ls)))))
 
     ;; TODO: OOps, run doesn't return a cur term but a redex term
@@ -780,8 +1174,8 @@
     (define (cur-identifier-bound? id)
       (let ([x (syntax->datum id)])
         (and (x? x)
-             (or (term (lookup ,(gamma) ,x))
-               (term (lookup ,(sigma) ,x))))))
+             (or (term (lookup-Γ ,(gamma) ,x))
+               (term (lookup-Σ ,(sigma) ,x))))))
 
     (define (filter-cur-exports syn modes)
       (partition (compose cur-identifier-bound? export-local-id)
@@ -793,8 +1187,9 @@
         (syntax-case syn ()
           [(_ e ...)
            (let-values ([(cur ~cur) (filter-cur-exports #'(e ...) modes)])
-             (set! envs (for/list ([e cur])
-                          (let* ([x (syntax->datum (export-local-id e))]
+             ;; TODO: Ignoring the built envs for now
+             #;(set! envs (for/list ([e cur])
+                       (let* ([x (syntax->datum (export-local-id e))]
                                  [t (type-infer/term x)]
                                  [env (if (term (lookup ,(gamma) ,x)) #'gamma #'sigma)])
                             #`(extend-env/term! #,env #,(export-out-sym e) #,t))))
@@ -845,7 +1240,7 @@
                              ;; TODO: Do not DIY gensym
                              (set! gn (add1 gn))
                              (set! out-gammas
-                               #`(#,@out-gammas (gamma (term (append-env
+                               #`(#,@out-gammas (gamma (term (append-Γ
                                                                ,(gamma)
                                                                ,#,new-id)))))
                              (cons (struct-copy import imp [local-id new-id])
@@ -858,7 +1253,7 @@
                              ;; TODO: Do not DIY gensym
                              (set! sn (add1 sn))
                              (set! out-sigmas
-                               #`(#,@out-sigmas (sigma (term (append-env
+                               #`(#,@out-sigmas (sigma (term (append-Σ
                                                                ,(sigma)
                                                                ,#,new-id)))))
                              (cons (struct-copy import imp [local-id new-id])
@@ -921,43 +1316,46 @@
   #;(define-syntax (dep-datum syn) (denote #'syn))
   (define-syntax (dep-lambda syn)
     (syntax-case syn (:)
-      [(_ (x : t) e) (syntax->curnel-syntax #`(λ (x : t) e))]))
+      [(_ (x : t) e)
+       (syntax->curnel-syntax
+         (quasisyntax/loc syn (λ (x : t) e)))]))
 
   (define-syntax (dep-app syn)
     (syntax-case syn ()
-      [(_ e1 e2) (syntax->curnel-syntax #`(#%app e1 e2))]))
-
-  (define-syntax (dep-case syn)
-    (syntax-case syn ()
-      [(_ e ...) (syntax->curnel-syntax #`(case e ...))]))
+      [(_ e1 e2)
+       (syntax->curnel-syntax
+         (quasisyntax/loc syn (#%app e1 e2)))]))
 
   (define-syntax (dep-forall syn)
     (syntax-case syn (:)
-      [(_ (x : t) e) (syntax->curnel-syntax #`(Π (x : t) e))]))
+      [(_ (x : t) e)
+       (syntax->curnel-syntax
+         (quasisyntax/loc syn (Π (x : t) e)))]))
 
   (define-syntax (Type syn)
     (syntax-case syn ()
-      [(_ i) (syntax->curnel-syntax #'(Unv i))]
-      [_ #'(Type 0)]))
-
-  (define-syntax (dep-fix syn)
-   (syntax-case syn (:)
-     [(_ (x : t) e) (syntax->curnel-syntax #`(μ (x : t) e))]))
+      [(_ i)
+       (syntax->curnel-syntax
+         (quasisyntax/loc syn (Unv i)))]
+      [_ (quasisyntax/loc syn (Type 0))]))
 
   (define-syntax (dep-inductive syn)
     (syntax-case syn (:)
       [(_ i : ti (x1 : t1) ...)
        (begin
-         (extend-env/syn! sigma #'i #'ti)
-         (for ([x (syntax->list #`(x1 ...))]
-               [t (syntax->list #`(t1 ...))])
-           (extend-env/syn! sigma x t))
+         (extend-Σ/syn! sigma #'i #'ti #'((x1 : t1) ...))
          #'(void))]))
 
+  (define-syntax (dep-elim syn)
+    (syntax-case syn (:)
+      [(_ D e P method ...)
+       (syntax->curnel-syntax
+         (quasisyntax/loc syn (elim D e P method ...)))]))
+
   ;; TODO: Not sure if this is the correct behavior for #%top
   (define-syntax (dep-var syn)
     (syntax-case syn ()
-      [(_ . id) #`(term (reduce id))]))
+      [(_ . id) #`(term (reduce #,(sigma) id))]))
 
   ;; TODO: Syntax-parse
   (define-syntax (dep-define syn)
@@ -970,7 +1368,7 @@
        ;; environment and have denote do a giant substitution
        (let ([e (cur->datum #'e)]
              [id (syntax->datum #'id)])
-         (extend-env/term! gamma id (type-infer/term e))
+         (extend-Γ/term! gamma id (type-infer/term e))
          (add-binding/term! id e)
          #'(void))])))
 
diff --git a/stdlib/bool.rkt b/stdlib/bool.rkt
index e900a43..dc05ed2 100644
--- a/stdlib/bool.rkt
+++ b/stdlib/bool.rkt
@@ -8,9 +8,10 @@
 (define-syntax (if syn)
   (syntax-case syn ()
     [(_ t s f)
-     #'(case t
-         [btrue s]
-         [bfalse f])]))
+     ;; Compute the motive
+     (let ([M #`(lambda (x : #,(type-infer/syn #'t))
+                  #,(type-infer/syn #'s))])
+       (quasisyntax/loc syn (elim bool t #,M s f)))]))
 
 (define (bnot (x : bool)) (if x bfalse btrue))
 (module+ test
diff --git a/stdlib/maybe.rkt b/stdlib/maybe.rkt
index 5ce02ad..c8c3352 100644
--- a/stdlib/maybe.rkt
+++ b/stdlib/maybe.rkt
@@ -8,9 +8,12 @@
 
 (module+ test
   (require rackunit "bool.rkt")
-  ;; TODO: Dependent pattern matching doesn't work yet
-  #;(check-equal? (case* (some bool btrue)
-                  [(none (A : Type)) bfalse]
-                  [(some (A : Type) (x : bool))
-                   (if x btrue bfalse)])
-                btrue))
+  #;(check-equal?
+    (case* maybe (some bool btrue)
+      (lambda (x : (maybe bool)) bool)
+      [(none (A : Type)) IH: ()
+       bfalse]
+      [(some (A : Type) (x : A)) IH: ()
+       ;; TODO: Don't know how to use dependency yet
+       (if x btrue bfalse)])
+    btrue))
diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt
index 1a80012..6b2047d 100644
--- a/stdlib/nat.rkt
+++ b/stdlib/nat.rkt
@@ -2,7 +2,7 @@
 (require "sugar.rkt" "bool.rkt")
 ;; TODO: override (all-defined-out) to enable exporting all these
 ;; properly.
-(provide nat z s add1 sub1 plus nat-equal?)
+(provide nat z s add1 sub1 plus )
 (module+ test
   (require rackunit))
 
@@ -15,33 +15,37 @@
   (check-equal? (add1 (s z)) (s (s z))))
 
 (define (sub1 (n : nat))
-  (case n
+  (case* nat n (lambda (x : nat) nat)
     [z z]
-    [s (lambda (x : nat) x)]))
+    [(s (x : nat)) IH: ((ih-n : nat)) x]))
 (module+ test
   (check-equal? (sub1 (s z)) z))
 
-(define plus
-  (fix (plus : (forall* (n1 : nat) (n2 : nat) nat))
-    (lambda (n1 : nat)
-      (lambda (n2 : nat)
-        (case n1
-          [z n2]
-          [s (λ (x : nat) (plus x (s n2)))])))))
+(define (plus (n1 : nat) (n2 : nat))
+  (case* nat n1 (lambda (x : nat) nat)
+    [z n2]
+    [(s (x : nat)) IH: ((ih-n1 : nat))
+     (s ih-n1)]))
 (module+ test
   (check-equal? (plus z z) z)
   (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
 
-(define-rec (nat-equal? (n1 : nat) (n2 : nat) : bool)
-  (case* n1
-    [z (case* n2
-         [z btrue]
-         [(s (n3 : nat)) bfalse])]
-    [(s (n3 : nat))
-       (case* n2
-         [z btrue]
-         [(s (n4 : nat)) (nat-equal? n3 n4)])]))
+;; Credit to this function goes to Max
+(define (nat-equal? (n1 : nat))
+  (elim nat n1 (lambda (x : nat) (-> nat bool))
+    (lambda (n2 : nat)
+      (elim nat n2 (lambda (x : nat) bool)
+        btrue
+        (lambda* (x : nat) (ih-n2 : bool) bfalse)))
+    (lambda* (x : nat) (ih : (-> nat bool))
+      (lambda (n2 : nat)
+        (elim nat n2 (lambda (x : nat) bool)
+          bfalse
+          (lambda* (x : nat) (ih-bla : bool)
+            (ih x)))))))
 (module+ test
-  (check-equal? btrue (nat-equal? z z))
-  (check-equal? bfalse (nat-equal? z (s z)))
-  (check-equal? btrue (nat-equal? (s z) (s z))))
+  (check-equal? (nat-equal? z z) btrue)
+  (check-equal? (nat-equal? z (s z)) bfalse)
+  (check-equal? (nat-equal? (s z) (s z)) btrue))
+
+
diff --git a/stdlib/prop.rkt b/stdlib/prop.rkt
index 0049924..8a7b36a 100644
--- a/stdlib/prop.rkt
+++ b/stdlib/prop.rkt
@@ -18,7 +18,7 @@
 
 (define-theorem thm:anything-implies-true (forall (P : Type) true))
 
-(qed (run thm:anything-implies-true) (lambda (P : Type) T))
+(qed thm:anything-implies-true (lambda (P : Type) T))
 
 (data false : Type)
 
@@ -31,20 +31,23 @@
 (define-theorem thm:and-is-symmetric
   (forall* (P : Type) (Q : Type) (ab : (and P Q)) (and Q P)))
 
-;; TODO: BAH! pattern matching on inductive families is still broken.
 (define proof:and-is-symmetric
   (lambda* (P : Type) (Q : Type) (ab : (and P Q))
-    (case* ab
-      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) (conj Q P y x)))))
+    (case* and ab
+      (lambda* (P : Type) (Q : Type) (ab : (and P Q))
+         (and Q P))
+      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj Q P y x)))))
 
-#;(qed thm:and-is-symmetric proof:and-is-symmetric)
+(qed thm:and-is-symmetric proof:and-is-symmetric)
 
 (define-theorem thm:proj1
   (forall* (A : Type) (B : Type) (c : (and A B)) A))
 
 (define proof:proj1
   (lambda* (A : Type) (B : Type) (c : (and A B))
-    (case c (conj (lambda* (A : Type) (B : Type) (a : A) (b : B) a)))))
+    (case* and c
+      (lambda* (A : Type) (B : Type) (c : (and A B)) A)
+      ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
 
 (qed thm:proj1 proof:proj1)
 
@@ -53,7 +56,9 @@
 
 (define proof:proj2
   (lambda* (A : Type) (B : Type) (c : (and A B))
-    (case c (conj (lambda* (A : Type) (B : Type) (a : A) (b : B) b)))))
+    (case* and c
+      (lambda* (A : Type) (B : Type) (c : (and A B)) B)
+      ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
 
 (qed thm:proj2 proof:proj2)
 
diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt
index a3ed30b..6959fcd 100644
--- a/stdlib/sugar.rkt
+++ b/stdlib/sugar.rkt
@@ -66,22 +66,30 @@
     [(_ (name (a : t) ... : t_res) body)
      #'(define name (fix (name : (forall* (a : t) ... t_res))
                       (lambda* (a : t) ... body)))]))
+
 (begin-for-syntax
   (define (rewrite-clause clause)
-    (syntax-case clause (:)
-      [((con (a : A) ...) body) #'(con (lambda* (a : A) ... body))]
-      [(e body) #'(e body)])))
+    (syntax-case clause (: IH:)
+      [((con (a : A) ...) IH: ((x : t) ...) body)
+       #'(lambda* (a : A) ... (x : t) ... body)]
+      [(e body) #'body])))
 
+;; TODO: Expects clauses in same order as constructors as specified when
+;; TODO: inductive D is defined.
 (define-syntax (case* syn)
   (syntax-case syn ()
-    [(_ e clause* ...)
-     #`(case e #,@(map rewrite-clause (syntax->list #'(clause* ...))))]))
+    [(_ D e P clause* ...)
+     #`(elim D e P #,@(map rewrite-clause (syntax->list #'(clause* ...))))]))
 
 (define-syntax-rule (define-theorem name prop)
   (define name prop))
 
-;; TODO: Current implementation doesn't do beta/eta while type-checking
-;; because reasons. So manually insert a run in the type annotation
-(define-syntax-rule (qed thm pf)
-  ((lambda (x : (run thm)) Type) pf))
+(define-syntax (qed stx)
+  (syntax-case stx ()
+    [(_ t pf)
+     (begin
+       (unless (type-check/syn? #'pf #'t)
+         (raise-syntax-error 'qed "Invalid proof"
+           #'pf #'t))
+       #'pf)]))
 
diff --git a/stlc.rkt b/stlc.rkt
index 9616a33..ae129c0 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -17,13 +17,14 @@
   (emp-gamma : gamma)
   (extend-gamma : (->* gamma var stlc-type gamma)))
 
-(define-rec (lookup-gamma (g : gamma) (x : var) : (maybe stlc-type))
-  (case* g
+(define (lookup-gamma (g : gamma) (x : var))
+  (case* gamma g (lambda* (g : gamma) (maybe stlc-type))
     [emp-gamma (none stlc-type)]
     [(extend-gamma (g1 : gamma) (v1 : var) (t1 : stlc-type))
+     IH: ((ih-g1 : (maybe stlc-type)))
      (if (var-equal? v1 x)
          (some stlc-type t1)
-         (lookup-gamma g1 x))]))
+         ih-g1)]))
 
 (define-relation (has-type gamma stlc-term stlc-type)
   #:output-coq "stlc.v"