Fixed bug in reduction of elim

elim was not checking that the arguments to be used for the parameters
of the inductive matched the actual parameters expected, resulting in
incorrect and non-deterministic unification, and thus incorrect
reduction when the parameters were unified incorrectly.

redex-curnel.rkt

@@ -308,20 +308,27 @@
            -->β)
       (--> (Σ (in-hole E (in-hole Θ (((elim x_D) U) e_P))))
            (Σ (in-hole E (in-hole Θ_r (in-hole Θ_i e_mi))))
-           ;; The elim form must appear applied like so:
+           #|
-           ;; (elim x_D U e_P m_0 ... m_i m_j ... m_n p ... (c_i p ... a ...))
+            |
-           ;; Where:
+            | The elim form must appear applied like so:
-           ;    x_D       is the inductive being eliminated
+            | (elim x_D U e_P m_0 ... m_i m_j ... m_n p ... (c_i p ... a ...))
-           ;    U         is the sort of the motive
+            | -->
-           ;    e_P       is the motive
+            |
-           ;    m_{0..n}  are the methods
+            | Where:
-           ;    p ...     are the parameters of x_D
+            |   x_D       is the inductive being eliminated
-           ;    c_i       is a constructor of x_d
+            |   U         is the sort of the motive
-           ;    a ...     are the non-parameter arguments to c_i
+            |   e_P       is the motive
-           ;; Unfortunately, Θ contexts turn all this inside out:
+            |   m_{0..n}  are the methods
-           ;; TODO: Write better abstractions for this notation
+            |   p ...     are the parameters of x_D
+            |   c_i       is a constructor of x_d
+            |   a ...     are the non-parameter arguments to c_i
+            | Unfortunately, Θ contexts turn all this inside out:
+            | TODO: Write better abstractions for this notation
+            |#
            (where (in-hole (Θ_p (in-hole Θ_i x_ci)) Θ_m)
                   Θ)
+           (where Ξ (parameters-of Σ x_D))
+           (judgment-holds (telescope-types Σ ∅ Θ_p Ξ))
            (where (in-hole Θ_a Θ_p)
                   Θ_i)
            (where ((x_c* : t_c*) ...)
@@ -605,6 +612,15 @@
       (term (constructor-of ,Σ s))
       (term nat)))
 
+  ;; TODO: inlined at least in type-infer
+  ;; TODO: Define generic traversals of Σ and Γ ?
+  (define-metafunction cic-redL
+    parameters-of : Σ x -> Ξ
+    [(parameters-of (Σ (x_D : (in-hole Ξ U) ((x : t) ...))) x_D)
+     Ξ]
+    [(parameters-of (Σ (x_1 : t_1 ((x : t) ...))) x_D)
+     (parameters-of Σ x_D)])
+
   ;; Returns the constructors for the inductively defined type x_D in
   ;; the signature Σ
   (define-metafunction cic-redL
@@ -1011,10 +1027,10 @@
     (check-holds
       (type-check ,Σ ∅ ,zero? (Π (x : nat) bool)))
     (check-equal?
-      (term (reduce ,Σ (,zero? z)))
+      (term (reduce ,Σ (,zero? zero)))
       (term true))
     (check-equal?
-      (term (reduce ,Σ (,zero? (s z))))
+      (term (reduce ,Σ (,zero? (s zero))))
       (term false))
     (define ih-equal?
       (term (((((elim nat) Type) (λ (x : nat) bool))
@@ -1024,21 +1040,27 @@
       (type-check ,Σ (∅ x_ih : (Π (x : nat) bool))
                   ,ih-equal?
                   (Π (x : nat) bool)))
+    (check-holds
+      (type-infer ,Σ ∅ nat (Unv 0)))
+    (check-holds
+      (type-infer ,Σ ∅ bool (Unv 0)))
+    (check-holds
+      (type-infer ,Σ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0))))
+    (define nat-equal?
+      (term (((((elim nat) Type) (λ (x : nat) (Π (x : nat) bool)))
+         ,zero?)
+        (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
+                            ,ih-equal?)))))
     (check-holds
       (type-check ,Σ ∅
-                  (((((((elim nat) Type) (λ (x : nat) (Π (x : nat) bool)))
+                  ,nat-equal?
-                      ,zero?)
-                     (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
-                                         ,ih-equal?)))
-                    z) (s z))
                   (Π (x : nat) (Π (y : nat) bool))))
     (check-equal?
-      (term (reduce ,Σ (((((((elim nat) Type) (λ (x : nat) (Π (x : nat) bool)))
+      (term (reduce ,Σ ((,nat-equal? zero) (s zero))))
-                 ,zero?)
+      (term false))
-                (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
+    (check-equal?
-                                    ,ih-equal?)))
+      (term (reduce ,Σ ((,nat-equal? (s zero)) zero)))
-               z) (s z))))
+      (term false))))
-      false)))
 
 ;; This module just provide module language sugar over the redex model.
 

stdlib/maybe.rkt

@@ -9,8 +9,8 @@
 (module+ test
   (require rackunit "bool.rkt")
   #;(check-equal?
-    (case* maybe (some bool btrue)
+    (case* maybe Type (some bool btrue) (bool)
-      (lambda (x : (maybe bool)) bool)
+      (lambda* (A : Type) (x : (maybe A)) A)
       [(none (A : Type)) IH: ()
        bfalse]
       [(some (A : Type) (x : A)) IH: ()

stdlib/nat.rkt

@@ -15,14 +15,14 @@
   (check-equal? (add1 (s z)) (s (s z))))
 
 (define (sub1 (n : nat))
-  (case* nat Type n (lambda (x : nat) nat)
+  (case* nat Type n () (lambda (x : nat) nat)
     [z z]
     [(s (x : nat)) IH: ((ih-n : nat)) x]))
 (module+ test
   (check-equal? (sub1 (s z)) z))
 
 (define (plus (n1 : nat) (n2 : nat))
-  (case* nat Type n1 (lambda (x : nat) nat)
+  (case* nat Type n1 () (lambda (x : nat) nat)
     [z n2]
     [(s (x : nat)) IH: ((ih-n1 : nat))
      (s ih-n1)]))
@@ -31,21 +31,16 @@
   (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
 
 ;; Credit to this function goes to Max
-(define (nat-equal? (n1 : nat))
+(define nat-equal?
   (elim nat Type (lambda (x : nat) (-> nat bool))
-    (lambda (b2 : nat)
+    (elim nat Type (lambda (x : nat) bool)
-      (elim nat Type (lambda (x : nat) bool)
+          btrue
-        btrue
+          (lambda* (x : nat) (ih-n2 : bool) bfalse))
-        (lambda* (x : nat) (ih-n2 : bool) bfalse)
-        b2))
     (lambda* (x : nat) (ih : (-> nat bool))
-      (lambda (a2 : nat)
+      (elim nat Type (lambda (x : nat) bool)
-        (elim nat Type (lambda (x : nat) bool)
+            bfalse
-          bfalse
+            (lambda* (x : nat) (ih-bla : bool)
-          (lambda* (x : nat) (ih-bla : bool)
+                     (ih x))))))
-            (ih x))
-          a2)))
-    n1))
 (module+ test
   (check-equal? (nat-equal? z z) btrue)
   (check-equal? (nat-equal? z (s z)) bfalse)

stdlib/prop.rkt

@@ -33,7 +33,7 @@
 
 (define proof:and-is-symmetric
   (lambda* (P : Type) (Q : Type) (ab : (and P Q))
-    (case* and ab
+    (case* and Type ab (P Q)
       (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)))))
@@ -45,7 +45,7 @@
 
 (define proof:proj1
   (lambda* (A : Type) (B : Type) (c : (and A B))
-    (case* and c
+    (case* and Type c (A B)
       (lambda* (A : Type) (B : Type) (c : (and A B)) A)
       ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
 
@@ -56,7 +56,7 @@
 
 (define proof:proj2
   (lambda* (A : Type) (B : Type) (c : (and A B))
-    (case* and c
+    (case* and Type c (A B)
       (lambda* (A : Type) (B : Type) (c : (and A B)) B)
       ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
 

stdlib/sugar.rkt

@@ -78,8 +78,8 @@
 ;; TODO: inductive D is defined.
 (define-syntax (case* syn)
   (syntax-case syn ()
-    [(_ D U e P clause* ...)
+    [(_ D U e (p ...) P clause* ...)
-     #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) e)]))
+     #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
 
 (define-syntax-rule (define-theorem name prop)
   (define name prop))