From b4090ae2cf6bb8a6e4f984f74e22b9832de35543 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Fri, 27 Mar 2015 21:49:03 -0400
Subject: [PATCH] Ahhh fucking substitution

I'm dumb
---
 redex-curnel.rkt | 28 +++++++++++++++++++++++++++-
 stdlib/nat.rkt   |  9 +++++----
 stdlib/prop.rkt  |  5 +++--
 3 files changed, 35 insertions(+), 7 deletions(-)

diff --git a/redex-curnel.rkt b/redex-curnel.rkt
index 6179752..bee1c72 100644
--- a/redex-curnel.rkt
+++ b/redex-curnel.rkt
@@ -527,7 +527,6 @@
       (term (constructors-for ,sigma false))
       (term ())))
 
-
   ;; Holds when an apply context Θ provides arguments that match the
   ;; telescope Ξ
   (define-judgment-form cic-typingL
@@ -736,6 +735,12 @@
     (nat-test (∅ n : nat)
       (((((elim nat) n) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x)))
       nat)
+    (check-true
+      (judgment-holds
+        (types (,Σ (bool : (Unv 0) ((btrue : bool) (bfalse : bool))))
+          (∅ n2 : nat)
+          (((((elim nat) n2) (λ (x : nat) bool)) btrue) (λ (x : nat) (λ (ih-x : bool) bfalse)))
+          bool)))
     (check-false (judgment-holds
                     (types ,Σ
                            ∅
@@ -806,6 +811,27 @@
                                      (λ (a : A)
                                         (λ (b : B) tt)))))
                              true)))
+    (check-true
+      (judgment-holds
+        (types (,Σ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-true
+      (judgment-holds
+        (types (,Σ4 (true : (Unv 0) ((tt : true))))
+               ((∅ A : Type) B : Type)
+               (conj B)
+               t) t))
+    (check-true
+      (judgment-holds (types (,Σ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)))
diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt
index 2de63ce..8f80bc5 100644
--- a/stdlib/nat.rkt
+++ b/stdlib/nat.rkt
@@ -31,17 +31,18 @@
   (check-equal? (plus z z) z)
   (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
 
-(define (nat-equal? (n1 : nat) (n2 : nat) : bool)
+(define (nat-equal? (n1 : nat) (n2 : nat))
   (case* nat n1 (lambda (x : nat) bool)
     [z (case* nat n2 (lambda (x : nat) bool)
          [z btrue]
          [(s (x : nat)) IH: ((ih-x : bool)) bfalse])]
+    ;; TODO: Can't finish correct definition due to issues with names
     [(s (x : nat)) IH: ((ih-x : bool))
        (case* nat n2 (lambda (x : nat) bool)
          [z bfalse]
          [(s (x : nat)) IH: ((ih-x : 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..8f932f1 100644
--- a/stdlib/prop.rkt
+++ b/stdlib/prop.rkt
@@ -31,10 +31,11 @@
 (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
+      (lambda* (P : Type) (Q : Type) (ab : (and P Q))
+         (and Q P))
       ((conj (P : Type) (Q : Type) (x : P) (y : Q)) (conj Q P y x)))))
 
 #;(qed thm:and-is-symmetric proof:and-is-symmetric)