From 3fd22a905897402c3f70be547008426896114310 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 2 Aug 2017 14:58:27 -0400
Subject: [PATCH] add eq-elim and more equality proof examples

---
 turnstile/examples/dep2.rkt             | 35 +++++++++--------
 turnstile/examples/tests/dep2-tests.rkt | 50 ++++++++++++++++---------
 2 files changed, 51 insertions(+), 34 deletions(-)

diff --git a/turnstile/examples/dep2.rkt b/turnstile/examples/dep2.rkt
index 3298a19..06a1862 100644
--- a/turnstile/examples/dep2.rkt
+++ b/turnstile/examples/dep2.rkt
@@ -7,8 +7,7 @@
 
 (provide (rename-out [#%type *])
          Π → ∀
-       = eq-refl
-       ;;eq-elim
+       = eq-refl eq-elim
 ;;          Nat Z S nat-ind
          λ
          (rename-out [app #%app]) ann
@@ -54,7 +53,7 @@
 ;; TODO: add tests to check this
 (define-typed-syntax (Π ([X:id : τ_in] ...) τ_out) ≫
   ;; TODO: check that τ_in and τ_out have #%type?
-  [[X ≫ X- : τ_in] ... ⊢ [τ_out ≫ τ_out- ⇒ _] [τ_in ≫ τ_in- ⇒ _] ...]
+  [[X ≫ X- : τ_in] ... ⊢ [τ_out ≫ τ_out- ⇐ #%type] [τ_in ≫ τ_in- ⇐ #%type] ...]
   -------
   [⊢ (∀- (X- ...) (→- τ_in- ... τ_out-)) ⇒ #%type])
 
@@ -78,30 +77,34 @@
 ;; equality -------------------------------------------------------------------
 (define-internal-type-constructor =)
 (define-typed-syntax (= t1 t2) ≫
-  [⊢ t1 ≫ t1- ⇒ _] [⊢ t2 ≫ t2- ⇒ _]
+  [⊢ t1 ≫ t1- ⇒ ty]
+  [⊢ t2 ≫ t2- ⇐ ty]
   ;; #:do [(printf "t1: ~a\n" (stx->datum #'t1-))
   ;;       (printf "t2: ~a\n" (stx->datum #'t2-))]
 ;  [t1- τ= t2-]
   ---------------------
   [⊢ (=- t1- t2-) ⇒ #%type])
 
+;; Q: what is the operational meaning of eq-refl?
 (define-typed-syntax (eq-refl e) ≫
   [⊢ e ≫ e- ⇒ _]
   ----------
   [⊢ (#%app- void-) ⇒ (= e- e-)])
 
-;; (define-typed-syntax (eq-elim t P pt w peq) ≫
-;;   [⊢ t ≫ t- ⇒ ty]
-;; ; [⊢ P ≫ P- ⇒ _] 
-;; ; [⊢ pt ≫ pt- ⇒ _]
-;; ; [⊢ w ≫ w- ⇒ _]
-;; ; [⊢ peq ≫ peq- ⇒ _]
-;;   [⊢ P ≫ P- ⇐ (→ ty #%type)]
-;;   [⊢ pt ≫ pt- ⇐ (P- t-)]
-;;   [⊢ w ≫ w- ⇐ ty]
-;;   [⊢ peq ≫ peq- ⇐ (= t- w-)]
-;;   --------------
-;;   [⊢ (#%app- void-) ⇒ (P- w-)])
+;; eq-elim: t : T
+;;          P : (T -> Type)
+;;          pt : (P t)
+;;          w : T
+;;          peq : (= t w)
+;;       -> (P w)
+(define-typed-syntax (eq-elim t P pt w peq) ≫
+  [⊢ t ≫ t- ⇒ ty]
+  [⊢ P ≫ P- ⇐ (→ ty #%type)]
+  [⊢ pt ≫ pt- ⇐ (app P- t-)]
+  [⊢ w ≫ w- ⇐ ty]
+  [⊢ peq ≫ peq- ⇐ (= t- w-)]
+  --------------
+  [⊢ pt- ⇒ (app P- w-)])
 
 ;; lambda and #%app -----------------------------------------------------------
 
diff --git a/turnstile/examples/tests/dep2-tests.rkt b/turnstile/examples/tests/dep2-tests.rkt
index 7071d02..2560434 100644
--- a/turnstile/examples/tests/dep2-tests.rkt
+++ b/turnstile/examples/tests/dep2-tests.rkt
@@ -231,6 +231,7 @@
 (check-type (eq-refl one) : (= one one))
 (typecheck-fail (ann (eq-refl one) : (= two one))
  #:verb-msg "expected (= two one), given (= one one)")
+(check-type (ann (eq-refl one) : (= one one)) : (= one one))
 (check-type (eq-refl one) : (= (s z) one))
 (check-type (eq-refl two) : (= (s (s z)) two))
 (check-type (eq-refl two) : (= (s one) two))
@@ -240,26 +241,39 @@
 (check-type (eq-refl two) : (= (plus one one) two))
 (check-not-type (eq-refl two) : (= (plus one one) one))
 
-;; ;; symmetry of =
-;; (check-type 
-;;  (λ ([A : *][B : *])
-;;    (λ ([e : (= A B)])
-;;      (eq-elim A (λ ([W : *]) (= W A)) (eq-refl A) B e)))
-;;  : (∀ (A B) (→ (= A B) (= B A))))
-;; (check-not-type
-;;  (λ ([A : *][B : *])
-;;    (λ ([e : (= A B)])
-;;      (eq-elim A (λ ([W : *]) (= W A)) (eq-refl A) B e)))
-;;  : (∀ (A B) (→ (= A B) (= A B))))
+;; symmetry of =
+(check-type (∀ (A B) (→ (= A B) (= B A))) : *)
+(check-type
+ (λ ([A : *][B : *])
+   (λ ([e : (= A B)])
+     (eq-elim A (λ ([W : *]) (= W A)) (eq-refl A) B e)))
+ : (∀ (A B) (→ (= A B) (= B A))))
 
-;; ;; transitivity of =
-;; (check-type
-;;  (λ ([X : *][Y : *][Z : *])
-;;    (λ ([e1 : (= X Y)][e2 : (= Y Z)])
-;;      (eq-elim Y (λ ([W : *]) (= X W)) e1 Z e2)))
-;;  : (∀ (A B C) (→ (= A B) (= B C) (= A C))))
+(check-type
+  (λ (A B)
+    (λ (e)
+      (eq-elim A (λ (W) (= W A)) (eq-refl A) B e)))
+ : (∀ (A B) (→ (= A B) (= B A))))
 
-;; tests recursive app/eval
+(check-not-type
+ (λ ([A : *][B : *])
+   (λ ([e : (= A B)])
+     (eq-elim A (λ ([W : *]) (= W A)) (eq-refl A) B e)))
+ : (∀ (A B) (→ (= A B) (= A B))))
+
+;; transitivity of =
+(check-type
+ (λ ([X : *][Y : *][Z : *])
+   (λ ([e1 : (= X Y)][e2 : (= Y Z)])
+     (eq-elim Y (λ ([W : *]) (= X W)) e1 Z e2)))
+ : (∀ (A B C) (→ (= A B) (= B C) (= A C))))
+(check-type
+ (λ (X Y Z)
+   (λ (e1 e2)
+     (eq-elim Y (λ (W) (= X W)) e1 Z e2)))
+ : (∀ (A B C) (→ (= A B) (= B C) (= A C))))
+
+;; general tests that app/eval is properly applied recursively
 (check-type ((λ ([f : (→ * *)][x : *]) (f x))
              (λ ([x : *]) x)
              *)