From 8ba4ed17d95a4dcda8559789075f418e9bb9c08b Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 25 Sep 2015 16:52:49 -0400 Subject: [PATCH] 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 | 72 +++++++++++++++++++++++++++++++----------------- stdlib/maybe.rkt | 4 +-- stdlib/nat.rkt | 25 +++++++---------- stdlib/prop.rkt | 6 ++-- stdlib/sugar.rkt | 4 +-- 5 files changed, 64 insertions(+), 47 deletions(-) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index 0fb8dd7..53ac7df 100644 --- a/redex-curnel.rkt +++ b/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: - ; x_D is the inductive being eliminated - ; U is the sort of the motive - ; e_P is the motive - ; m_{0..n} are the methods - ; 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 + #| + | + | 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: + | x_D is the inductive being eliminated + | U is the sort of the motive + | e_P is the motive + | m_{0..n} are the methods + | 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))) - ,zero?) - (λ (x : nat) (λ (x_ih : (Π (x : nat) bool)) - ,ih-equal?))) - z) (s z)) + ,nat-equal? (Π (x : nat) (Π (y : nat) bool)))) (check-equal? - (term (reduce ,Σ (((((((elim nat) Type) (λ (x : nat) (Π (x : nat) bool))) - ,zero?) - (λ (x : nat) (λ (x_ih : (Π (x : nat) bool)) - ,ih-equal?))) - z) (s z)))) - false))) + (term (reduce ,Σ ((,nat-equal? zero) (s zero)))) + (term false)) + (check-equal? + (term (reduce ,Σ ((,nat-equal? (s zero)) zero))) + (term false)))) ;; This module just provide module language sugar over the redex model. diff --git a/stdlib/maybe.rkt b/stdlib/maybe.rkt index c8c3352..564017c 100644 --- a/stdlib/maybe.rkt +++ b/stdlib/maybe.rkt @@ -9,8 +9,8 @@ (module+ test (require rackunit "bool.rkt") #;(check-equal? - (case* maybe (some bool btrue) - (lambda (x : (maybe bool)) bool) + (case* maybe Type (some bool btrue) (bool) + (lambda* (A : Type) (x : (maybe A)) A) [(none (A : Type)) IH: () bfalse] [(some (A : Type) (x : A)) IH: () diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt index 2ae07b1..5853d5d 100644 --- a/stdlib/nat.rkt +++ b/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) - btrue - (lambda* (x : nat) (ih-n2 : bool) bfalse) - b2)) + (elim nat Type (lambda (x : nat) bool) + btrue + (lambda* (x : nat) (ih-n2 : bool) bfalse)) (lambda* (x : nat) (ih : (-> nat bool)) - (lambda (a2 : nat) - (elim nat Type (lambda (x : nat) bool) - bfalse - (lambda* (x : nat) (ih-bla : bool) - (ih x)) - a2))) - n1)) + (elim nat Type (lambda (x : nat) bool) + bfalse + (lambda* (x : nat) (ih-bla : bool) + (ih x)))))) (module+ test (check-equal? (nat-equal? z z) btrue) (check-equal? (nat-equal? z (s z)) bfalse) diff --git a/stdlib/prop.rkt b/stdlib/prop.rkt index 8a7b36a..83db7c7 100644 --- a/stdlib/prop.rkt +++ b/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)))) diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt index cb2a544..5f19edf 100644 --- a/stdlib/sugar.rkt +++ 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* ...) - #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) e)])) + [(_ D U e (p ...) P clause* ...) + #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)])) (define-syntax-rule (define-theorem name prop) (define name prop))