Fixed various bugs related to case and inductives

case would fail when used on an inductive family. Fixed this, added more
test cases, and cleaned up examples.

example.rkt

@@ -47,27 +47,27 @@
 
 ;; -------------------
 ;; Write functions on inductive data
-;; TODO: This is not plus! Plus require recursion and I don't have
+(define (add1 (n : nat)) (s n))
-;; recursion!
-;(define (plus (n1 : nat) (n2 : nat))
-;  (case n1
-;    [z n2]
-;    ;; TODO: Add macro to enable writing this line as:
-;    ;; [(s x) (s (s x))]
-;    [s (λ (x : nat) (s (s x)))]))
-;
-;(define four (plus (s (s z)) (s (s z))))
-;(check-equal? four (s (s (s z))))
 
-(define (add1 (n1 : nat))
+(check-equal? (add1 (s z)) (s (s z)))
-  (case n1
+
-    [z (s z)]
+(define (sub1 (n : nat))
+  (case n
+    [z z]
     ;; TODO: Add macro to enable writing this line as:
     ;; [(s x) (s (s x))]
-    [s (λ (x : nat) (s (s x)))]))
+    [s (lambda (x : nat) x)]))
+(check-equal? (sub1 (s z)) z)
 
-(define two (add1 (s z)))
+#|
-(check-equal? two (s (s z)))
+;; TODO: Plus require recursion and I don't have recursion!
+(define (plus (n1 : nat) (n2 : nat))
+  (case n1
+    [z n2]
+    [s (λ (x : nat) (plus x (s n2)))]))
+
+(check-equal? (plus (s (s z)) (s (s z))) (s (s (s z))))
+|#
 
 ;; -------------------
 ;; It's annoying to have to write things explicitly curried
@@ -94,9 +94,6 @@
 ;; -------------------
 ;; Prove interesting theorems!
 
-#|
-;; TODO: Well, case can't seem to type-check non-Type inductives. So I
-;; guess we'll do a church encoding
 (define (thm:and-is-symmetric
           (x : (forall* (P : Type) (Q : Type)
                  ;; TODO: Can't use -> for the final clause because generated
@@ -107,31 +104,16 @@
 
 (define proof:and-is-symmetric
   (lambda* (P : Type) (Q : Type) (ab : (and P Q))
+    (case ab
+      (conj (lambda* (P : Type) (Q : Type) (x : P) (y : Q) (conj Q P y x))))))
+
+(define proof:and-is-symmetric^
+  (lambda* (S : Type) (R : Type) (ab : (and S R))
     (case ab
       (conj (lambda* (S : Type) (R : Type) (s : S) (r : R) (conj R S r s))))))
 
 (check-equal? (thm:and-is-symmetric proof:and-is-symmetric) T)
-|#
+(check-equal? (thm:and-is-symmetric proof:and-is-symmetric^) T)
-(define and^ (forall* (A : Type) (B : Type)
-                      (forall* (C :  Type) (f : (forall* (a : A) (b : B) C))
-                               C)))
-(define fst (lambda* (A : Type) (B : Type) (ab : (and^ A B)) (ab A (lambda* (a : A) (b : B) a))))
-(define snd (lambda* (A : Type) (B : Type) (ab : (and^ A B)) (ab B (lambda* (a : A) (b : B) b))))
-(define conj^ (lambda* (A : Type) (B : Type)
-                       (a : A) (b : B)
-                       (lambda* (C : Type) (f : (-> A (-> B C)))
-                                (f a b))))
-(define (thm:and^-is-symmetric
-          (x : (forall* (P : Type) (Q : Type)
-                 (ab : (and^ P Q))
-                 (and^ P Q))))
-  T)
-
-(define proof:and^-is-symmetric
-  (lambda* (P : Type) (Q : Type) (ab : (and^ P Q))
-    (conj^ Q P (snd P Q ab) (fst P Q ab))))
-
-(check-equal? T (thm:and^-is-symmetric proof:and^-is-symmetric))
 
 ;; -------------------
 ;; Gee, I wish there was a special syntax for theorems and proofs so I could think of
@@ -143,10 +125,24 @@
 (define-syntax-rule (qed thm pf)
   (check-equal? T (thm pf)))
 
-(define-theorem thm:and^-is-symmetric^
+(define-theorem thm:and-is-symmetric^^
-  (forall* (P : Type) (Q : Type) (ab : (and^ P Q)) (and^ P Q)))
+  (forall* (P : Type) (Q : Type) (ab : (and P Q)) (and Q P)))
 
-(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)))))
+(qed thm:proj1 proof:proj1)
+
+(define-theorem thm:proj2
+  (forall* (A : Type) (B : Type) (c : (and A B)) B))
+(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)))))
+(qed thm:proj2 proof:proj2)
 
 ;; -------------------
 ;; Gee, I wish I had special syntax for defining types like I do for
@@ -157,16 +153,20 @@
 
 (define-type (not (A : Type)) (-> A false))
 
-(define-type (and^^ (A : Type) (B : Type))
-  (forall* (C :  Type) (f : (forall* (a : A) (b : B) C)) C))
 #|
-TODO: Can't seem to pattern match on a inductive with 0 constructors...
+;;TODO: Can't pattern match on a inductive with 0 constructors yet.
-should result in a term of any type, I think.
+(define-theorem thm:absurd
-(define-theorem thm:absurdidty
+  (forall* (P : Type) (A : Type) (a : A) (~a : (not A)) P))
-  (forall (P : Type) (A : Type) (-> (and^ A (not A)) P)))
+(qed thm:absurd (lambda* (P : Type) (A : Type) (a : A) (~a : (not A))
+       (case (~a a))))
 
-(define (proof:absurdidty (P : Type) (A : Type) (a*nota : (and^ A (not A)))
+(define-theorem thm:absurdidty
-  ((snd A (not A) a*nota) (fst A (not A) a*nota))))
+  (forall* (P : Type) (A : Type) (a*nota : (and A (not A))) P))
+
+;; TODO: Not sure why this doesn't type-check.. probably not handling
+;; inductive families correctly in (case ...)
+(define (proof:absurdidty (P : Type) (A : Type) (a*nota : (and A (not A))))
+  ((proof:proj2 A (not A) a*nota) (proof:proj1 A (not A) a*nota)))
 |#
 
 ;; -------------------
@@ -182,7 +182,7 @@ should result in a term of any type, I think.
     ;; TODO: We want all forall*s to be expanded by this point. Should
     ;; look into Racket macro magic to expand syn before matching on it.
     [(_ (forall (x : t0) t1))
-     ;; TODO: Should carry around assumptions to enable inhabhit-type to use
+     ;; TODO: Should carry around assumptions to enable inhabit-type to use
      ;; them
      #'(lambda (x : t0) (inhabit-type t1))]
     [(_ t)
@@ -197,7 +197,6 @@ should result in a term of any type, I think.
 
 #;(define is-this-inhabited? (inhabit-type false))
 
-
 ;; -------------------
 ;; Unit test your theorems before proving them!
 
@@ -212,7 +211,7 @@ should result in a term of any type, I think.
 (define type-thm:true?
   (forall* (A : Type) (B : Type) (P : Type)
     ;; If A implies P and (and A B) then P
-    (->* (-> A P) (and^ A B) P)))
+    (->* (-> A P) (and A B) P)))
 
 (define-theorem thm:true? type-thm:true?)
 
@@ -220,7 +219,5 @@ should result in a term of any type, I think.
      ;; TODO: inhabit-type ought to be able to reduce (type-thm:true? true true true)
      ;; but can't. Maybe instead there should be a reduce tactic/macro.
      (inhabit-type (forall (a : (-> true true))
-                   (forall (f : (and^ true true))
+                   (forall (f : (and true true))
                    true))))
-
-;; TODO: Interopt with Racket at runtime via contracts?!?!

redex-core.rkt

@@ -22,7 +22,7 @@
     (x ::= variable-not-otherwise-mentioned)
     ;; TODO: Having 2 binders is stupid.
     (v ::= (Π (x : t) t) (λ (x : t) t) x U)
-    (t e ::= (case e (x e) (x e)...) v (t t)))
+    (t e ::= (case e (x e) ...) v (t t)))
 
   (module+ test
     (require rackunit)
@@ -31,6 +31,21 @@
     (define e? (redex-match? cicL e))
     (define v? (redex-match? cicL v))
     (define U? (redex-match? cicL U))
+
+    ;; TODO: Rename these signatures, and use them in all future tests.
+    (define Σ (term (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat))))
+
+    (define Σ0 (term ∅))
+    (define Σ2 (term (((∅ nat : Type) z : nat) s : (Π (x : nat) nat))))
+    (define Σ3 (term (∅ and : (Π (A : Type) (Π (B : Type) Type)))))
+    (define Σ4 (term (,Σ3 conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((and A) B))))))))
+    (define Σ? (redex-match? cic-typingL Σ))
+
+    (check-true (Σ? Σ0))
+    (check-true (Σ? Σ2))
+    (check-true (Σ? Σ4))
+    (check-true (Σ? Σ3))
+    (check-true (Σ? Σ4))
     (check-true (x? (term T)))
     (check-true (x? (term truth)))
     (check-true (x? (term zero)))
@@ -114,7 +129,7 @@
   ;; TODO: Why do I not have tests for substitutions?!?!?!?!?!?!?!!?!?!?!?!?!?!!??!?!
 
   (define-extended-language cic-redL cicL
-    (E hole (E t) (λ (x : t) E) (Π (x : t) E)))
+    (E hole (E t) (λ (x : t) E) (Π (x : t) E) (case E (x e) ...)))
 
   (define-metafunction cicL
     inductive-name : t -> x
@@ -141,8 +156,7 @@
       (==> (case e_9
              (x_0 e_0) ... (x e) (x_r e_r) ...)
            (inductive-apply e e_9)
-           (where x (inductive-name e_9))
+           (where x (inductive-name e_9)))
-           )
       with
       [(--> (in-hole E t_0) (in-hole E t_1))
        (==> t_0 t_1)]))
@@ -163,8 +177,7 @@
                   (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))))))
+                  (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
@@ -189,10 +202,10 @@
   (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
-    (define Σ (term (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat))))
     (check-equal? (term nat) (term (result-type ,Σ (Π (x : nat) nat))))
     (check-equal? (term nat) (term (result-type ,Σ nat))))
 
@@ -220,18 +233,20 @@
                          nat x) x)
       (list (term zero) (term s))))
   (define-metafunction cic-typingL
-    constructors-for : Σ t (x ...) -> #t or #f
+    constructors-for : Σ x (x ...) -> #t or #f
-    [(constructors-for Σ t (x ...))
+    [(constructors-for Σ x_0 (x ...))
      ,((lambda (x y) (and (set=? x y) (= (length x) (length y))))
        (term (x ...))
-       (judgment-holds (constructor-for Σ t x_00) x_00))])
+       (judgment-holds (constructor-for Σ x_0 x_00) x_00))])
   (module+ test
     (check-true
       (term (constructors-for (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat))
                          nat (zero s))))
     (check-false
       (term (constructors-for (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat))
-                         nat (zero)))))
+                         nat (zero))))
+    (check-true
+      (term (constructors-for ,Σ4 and (conj)))))
 
   (define-metafunction cicL
     branch-type : t t t -> t
@@ -243,12 +258,6 @@
     (check-equal? (term Type) (term (branch-type nat (lookup ,Σ zero) Type)))
     (check-equal? (term nat) (term (branch-type nat nat nat)))
     (check-equal? (term Type) (term (branch-type nat (lookup ,Σ s) (Π (x : nat) Type))))
-    (define Σ3 (term (∅ and : (Π (A : Type) (Π (B : Type) Type)))))
-    (define Σ4 (term (,Σ3 conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((and A) B))))))))
-    (define Σ? (redex-match? cic-typingL Σ))
-    (check-true (Σ? Σ3))
-    (check-true (Σ? Σ4))
-
     (check-equal?
       (term Type)
       (term (branch-type and (lookup ,Σ4 conj)
@@ -266,35 +275,11 @@
     (check-true
       (term (branch-types-match ,Σ (zero s) (nat (Π (x : nat) nat)) nat nat))))
 
-  ;; TODO: I'm pretty sure this is wrong
+  ;; TODO: Add positivity checking.
   (define-metafunction cicL
     positive : t any -> #t or #f
     ;; Type; not a inductive constructor
-    [(positive t any) #t]
+    [(positive any_1 any_2) #t])
-    ;; nat
-    [(positive x_0 x_0) #t]
-    ;; nat -> t_1 ... -> nat
-    [(positive (Π (x : x_1) t_1) x_0)
-     (positive t_1 x_0)]
-    ;; Type -> t_1 ... -> nat
-    [(positive (Π (x : U) t_1) any)
-     (positive t_1 any)]
-    ;; (t_0 -> t_2) -> t_1 ... -> nat
-    [(positive (Π (x : (Π (x_1 : t_0) t_2)) t_1) x_0)
-     ,(and (term (copositive (Π (x_1 : t_0) t_2) x_0)) (term (positive t_1 x_0)))])
-
-  (define-metafunction cicL
-    copositive : t any -> #t or #f
-    [(copositive U any) #t]
-    [(copositive x_0 x_0) #f]
-    [(copositive (Π (x : x_0) t_1) x_0) #f]
-    ;; x_1 -> t_1 ... -> nat
-    [(copositive (Π (x : x_1) t_1) x_0)
-     (positive t_1 x_0)]
-    [(copositive (Π (x : U) t_1) x_0)
-     (positive t_1 x_0)]
-    [(copositive (Π (x : (Π (x_1 : t_0) t_2)) t_1) x_0)
-     ,(and (term (positive (Π (x_1 : t_0) t_2) x_0)) (term (copositive t_1 x_0)))])
 
   (module+ test
     (check-true (term (positive nat nat)))
@@ -310,8 +295,7 @@
     ;; Not sure if this is actually supposed to pass
     (check-false (term (positive (Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat) nat)))
 
-    (check-true (term (positive Type #f)))
+    (check-true (term (positive Type #f))))
-    )
 
   (define-judgment-form cic-typingL
     #:mode (wf I I)
@@ -383,6 +367,15 @@
      ----------------- "DTR-Case"
      (types Σ Γ (case e (x_0 e_0) (x_1 e_1) ...) 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
+    #;[(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.
@@ -465,12 +458,10 @@
                            ∅
                            (case zero (zero (s zero)))
                            nat)))
-    (define Σ0 (term ∅))
     (define lam (term (λ (nat : Type) nat)))
     (check-equal?
       (list (term (Π (nat : Type) Type)))
       (judgment-holds (types ,Σ0 ∅ ,lam t) t))
-    (define Σ2 (term (((∅ nat : Type) z : nat) s : (Π (x : nat) nat))))
     (check-equal?
       (list (term (Π (nat : Type) Type)))
       (judgment-holds (types ,Σ2 ∅ ,lam t) t))
@@ -502,10 +493,13 @@
     (check-true
       (judgment-holds (types ,Σ4 (∅ S : Type) (conj S)
                              (Π (B : Type) (Π (a : S) (Π (b : B) ((and S) B)))))))
-    ;; Failing due to lack of unification of case branches
     (check-true
       (judgment-holds (types ,Σ4 ∅ (λ (S : Type) (conj S))
                              (Π (S : Type) (Π (B : Type) (Π (a : S) (Π (b : B) ((and S) B))))))))
+    (check-true
+      (judgment-holds (types ((,Σ4 true : Type) tt : true) ∅
+                             ((((conj true) true) tt) tt)
+                             ((and true) true))))
     (check-true
       (judgment-holds (types ((,Σ4 true : Type) tt : true) ∅
                              (case ((((conj true) true) tt) tt)
@@ -513,7 +507,7 @@
                                         (λ (B : Type)
                                            (λ (a : A)
                                               (λ (b : B) a))))))
-                             t) t))
+                             A)))
     (define sigma (term (((((((∅ true : Type) T : true) false : Type) equal : (Π (A : Type)
                                                               (Π (B : Type) Type)))
         nat : Type) heap : Type) pre : (Π (temp808 : heap) Type))))
@@ -525,7 +519,10 @@
     (check-true
       (judgment-holds (types ,sigma ,gamma pre t)))
     (check-true
-      (judgment-holds (types ,sigma (,gamma tmp863 : pre) Type (Unv 0)))))
+      (judgment-holds (types ,sigma (,gamma tmp863 : pre) Type (Unv 0))))
+    (check-true
+      (judgment-holds (types ,sigma (,gamma x : false) (case x) t)))
+    )
 
 
   (define-judgment-form cic-typingL