From 89c5c1ba68829931044c986aedeba4a53572e284 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 16 Jan 2015 22:54:35 -0500 Subject: [PATCH] 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 | 113 ++++++++++++++++++++++++------------------------- redex-core.rkt | 97 ++++++++++++++++++++---------------------- 2 files changed, 102 insertions(+), 108 deletions(-) diff --git a/example.rkt b/example.rkt index 38a9dad..a1472f8 100644 --- a/example.rkt +++ b/example.rkt @@ -47,27 +47,27 @@ ;; ------------------- ;; Write functions on inductive data -;; TODO: This is not plus! Plus require recursion and I don't have -;; 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 (n : nat)) (s n)) -(define (add1 (n1 : nat)) - (case n1 - [z (s z)] +(check-equal? (add1 (s z)) (s (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) -|# -(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)) +(check-equal? (thm:and-is-symmetric proof:and-is-symmetric^) T) ;; ------------------- ;; 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^ - (forall* (P : Type) (Q : Type) (ab : (and^ P Q)) (and^ P Q))) +(define-theorem thm:and-is-symmetric^^ + (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... -should result in a term of any type, I think. -(define-theorem thm:absurdidty - (forall (P : Type) (A : Type) (-> (and^ A (not A)) P))) +;;TODO: Can't pattern match on a inductive with 0 constructors yet. +(define-theorem thm:absurd + (forall* (P : Type) (A : Type) (a : A) (~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))) - ((snd A (not A) a*nota) (fst A (not A) a*nota)))) +(define-theorem thm:absurdidty + (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?!?! diff --git a/redex-core.rkt b/redex-core.rkt index ef50cf5..9d0450f 100644 --- a/redex-core.rkt +++ b/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 Σ t (x ...)) + constructors-for : Σ x (x ...) -> #t or #f + [(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] - ;; 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)))]) + [(positive any_1 any_2) #t]) (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