Proper names and inductive families

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

@@ -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}$$"
+              (printf (format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\\end{mathpar}$$"
-                      (syntax->datum #'(n types* ...))
+                       (syntax->datum #'(n types* ...))
-                      (string-trim
+                       (string-trim
-                        (for/fold ([str ""])
+                         (for/fold ([str ""])
-                                  ([rule (attribute rules.latex)])
+                                   ([rule (attribute rules.latex)])
-                          (format "~a~a\\and~n" str rule))
+                                   (format "~a~a\\and~n" str rule))
-                        "\\and"
+                         "\\and"
-                        #:left? #f)))
+                         #: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
+  (case* var v1 (lambda* (v : var) bool)
-    [(avar (n1 : nat))
+    [(avar (n1 : nat)) IH: ()
-     (case* v2
+     (case* var v2 (lambda* (v : var) bool)
-       [(avar (n2 : nat))
+       [(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) ...)
+       [(elim var e P m ...)
-        (format "(match ~a with~n~aend)"
+        (format "(~a_rect ~a~a ~a)"
-                (output-coq #'e)
+          (output-coq #'var)
-                (for/fold ([strs ""])
+          (output-coq #'P)
-                          ([con   (syntax->list #'(ec ...))]
+          (for/fold ([x ""])
-                           [body  (syntax->list #'(eb ...))])
+                    ([m (syntax->list #'(m ...))])
-                  (let* ([ids (generate-temporaries (constructor-args con))]
+            (format "~a ~a" x (output-coq m)))
-                         [names (map (compose ~a syntax->datum) ids)])
+          (output-coq #'e))]
-                    (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))))))]
        [(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"

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)

stdlib/bool.rkt

@@ -8,9 +8,10 @@
 (define-syntax (if syn)
   (syntax-case syn ()
     [(_ t s f)
-     #'(case t
+     ;; Compute the motive
-         [btrue s]
+     (let ([M #`(lambda (x : #,(type-infer/syn #'t))
-         [bfalse f])]))
+                  #,(type-infer/syn #'s))])
+       (quasisyntax/loc syn (elim bool t #,M s f)))]))
 
 (define (bnot (x : bool)) (if x bfalse btrue))
 (module+ test

stdlib/maybe.rkt

@@ -8,9 +8,12 @@
 
 (module+ test
   (require rackunit "bool.rkt")
-  ;; TODO: Dependent pattern matching doesn't work yet
+  #;(check-equal?
-  #;(check-equal? (case* (some bool btrue)
+    (case* maybe (some bool btrue)
-                  [(none (A : Type)) bfalse]
+      (lambda (x : (maybe bool)) bool)
-                  [(some (A : Type) (x : bool))
+      [(none (A : Type)) IH: ()
-                   (if x btrue bfalse)])
+       bfalse]
-                btrue))
+      [(some (A : Type) (x : A)) IH: ()
+       ;; TODO: Don't know how to use dependency yet
+       (if x btrue bfalse)])
+    btrue))

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
+(define (plus (n1 : nat) (n2 : nat))
-  (fix (plus : (forall* (n1 : nat) (n2 : nat) nat))
+  (case* nat n1 (lambda (x : nat) nat)
-    (lambda (n1 : nat)
+    [z n2]
-      (lambda (n2 : nat)
+    [(s (x : nat)) IH: ((ih-n1 : nat))
-        (case n1
+     (s ih-n1)]))
-          [z n2]
-          [s (λ (x : nat) (plus x (s n2)))])))))
 (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)
+;; Credit to this function goes to Max
-  (case* n1
+(define (nat-equal? (n1 : nat))
-    [z (case* n2
+  (elim nat n1 (lambda (x : nat) (-> nat bool))
-         [z btrue]
+    (lambda (n2 : nat)
-         [(s (n3 : nat)) bfalse])]
+      (elim nat n2 (lambda (x : nat) bool)
-    [(s (n3 : nat))
+        btrue
-       (case* n2
+        (lambda* (x : nat) (ih-n2 : bool) bfalse)))
-         [z btrue]
+    (lambda* (x : nat) (ih : (-> nat bool))
-         [(s (n4 : nat)) (nat-equal? n3 n4)])]))
+      (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? (nat-equal? z z) btrue)
-  (check-equal? bfalse (nat-equal? z (s z)))
+  (check-equal? (nat-equal? z (s z)) bfalse)
-  (check-equal? btrue (nat-equal? (s z) (s z))))
+  (check-equal? (nat-equal? (s z) (s z)) btrue))
+
+

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
+    (case* and ab
-      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) (conj Q P y x)))))
+      (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)
 

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 (:)
+    (syntax-case clause (: IH:)
-      [((con (a : A) ...) body) #'(con (lambda* (a : A) ... body))]
+      [((con (a : A) ...) IH: ((x : t) ...) body)
-      [(e body) #'(e 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* ...)
+    [(_ D e P clause* ...)
-     #`(case e #,@(map rewrite-clause (syntax->list #'(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
+(define-syntax (qed stx)
-;; because reasons. So manually insert a run in the type annotation
+  (syntax-case stx ()
-(define-syntax-rule (qed thm pf)
+    [(_ t pf)
-  ((lambda (x : (run thm)) Type) pf))
+     (begin
+       (unless (type-check/syn? #'pf #'t)
+         (raise-syntax-error 'qed "Invalid proof"
+           #'pf #'t))
+       #'pf)]))
 

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))
+(define (lookup-gamma (g : gamma) (x : var))
-  (case* g
+  (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"