Fixed prop; removed define-theorem and qed macros
These macros were not really serving a good purpose. They were defined early on to demonstrate that metaprogramming can give us Coq-like notation, but really, we have much more interesting demos.
This commit is contained in:
William J. Bowman
parent
4cae9688fb
commit
822c114f62
31
oll.rkt
31
oll.rkt
|
|
@ -4,7 +4,7 @@
|
|||
(require
|
||||
"stdlib/sugar.rkt"
|
||||
"stdlib/nat.rkt"
|
||||
(only-in "curnel/redex-lang.rkt" [#%app real-app] [elim real-elim]))
|
||||
(only-in "cur.rkt" [#%app real-app] [elim real-elim]))
|
||||
|
||||
(provide
|
||||
define-relation
|
||||
|
|
@ -12,8 +12,7 @@
|
|||
Var
|
||||
avar
|
||||
var-equal?
|
||||
generate-coq
|
||||
#;(rename-out [oll-define-theorem define-theorem]))
|
||||
generate-coq)
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax-class dash
|
||||
|
|
@ -275,31 +274,14 @@
|
|||
(string-replace str (symbol->string (first p))
|
||||
(symbol->string (second p))))))
|
||||
(define (output-coq syn)
|
||||
(syntax-parse (cur-expand syn #'define #'define-theorem #'qed
|
||||
#'begin)
|
||||
(syntax-parse (cur-expand syn #'define #'begin)
|
||||
;; TODO: Need to add these to a literal set and export it
|
||||
;; Or, maybe overwrite syntax-parse
|
||||
#:literals (lambda forall data real-app real-elim define-theorem
|
||||
define qed begin Type)
|
||||
#:literals (lambda forall data real-app real-elim define begin Type)
|
||||
[(begin e ...)
|
||||
(for/fold ([str ""])
|
||||
([e (syntax->list #'(e ...))])
|
||||
(format "~a~n" (output-coq e)))]
|
||||
[(define-theorem name prop)
|
||||
(begin
|
||||
(fprintf (current-error-port) "Warning: If theorem ~a is not followed by a proof using (qed ...), the resulting Coq code may be malformed.~n" (output-coq #'name))
|
||||
(coq-lift-top-level
|
||||
(format "Theorem ~a : ~a.~n"
|
||||
(output-coq #'name)
|
||||
(output-coq #'prop)))
|
||||
"")]
|
||||
[(qed thm proof)
|
||||
;; TODO: Have some sort of coq-lift-to-theorem, to auto match
|
||||
;; proofs and theorems.
|
||||
(begin
|
||||
(coq-lift-top-level
|
||||
(format "Proof. exact ~a. Qed.~n" (output-coq #'proof)))
|
||||
"")]
|
||||
[(define name:id body)
|
||||
(begin
|
||||
(coq-lift-top-level
|
||||
|
|
@ -392,10 +374,9 @@
|
|||
"\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
|
||||
t))
|
||||
(check-regexp-match
|
||||
"Theorem thm_plus_commutes : \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
|
||||
"Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
|
||||
(parameterize ([coq-defns ""])
|
||||
(output-coq #'(define-theorem thm:plus-commutes
|
||||
(forall* (n : nat) (m : nat)
|
||||
(output-coq #'(define thm:plus-commutes (forall* (n : nat) (m : nat)
|
||||
(== nat (plus n m) (plus m n)))))
|
||||
(coq-defns)))
|
||||
(check-regexp-match
|
||||
|
|
|
|||
|
|
@ -167,6 +167,15 @@ corresponding @racket[expr], raising a syntax error if no type can be inferred.
|
|||
(y x))]
|
||||
}
|
||||
|
||||
@defform[(:: e type)]{
|
||||
Check that expression @racket[e] has type @racket[type], causing a type-error if not, and producing
|
||||
@racket[(void)] if so.
|
||||
|
||||
@examples[#:eval curnel-eval
|
||||
(:: z Nat)
|
||||
(:: true Nat)]
|
||||
}
|
||||
|
||||
@defform[(run syn)]{
|
||||
Like @racket[normalize/syn], but is a syntactic form which allows a Cur term to be written by
|
||||
computing part of the term from another Cur term.
|
||||
|
|
|
|||
|
|
@ -5,20 +5,26 @@
|
|||
(provide
|
||||
True T
|
||||
thm:anything-implies-true
|
||||
pf:anything-implies-true
|
||||
False
|
||||
Not
|
||||
And
|
||||
conj conj/i
|
||||
thm:and-is-symmetric proof:and-is-symmetric
|
||||
thm:proj1 proof:proj1
|
||||
thm:proj2 proof:proj2
|
||||
thm:and-is-symmetric pf:and-is-symmetric
|
||||
thm:proj1 pf:proj1
|
||||
thm:proj2 pf:proj2
|
||||
== refl)
|
||||
|
||||
(module+ test
|
||||
(require rackunit))
|
||||
|
||||
(data True : Type (T : True))
|
||||
|
||||
(define-theorem thm:anything-implies-true (forall (P : Type) True))
|
||||
(define thm:anything-implies-true (forall (P : Type) True))
|
||||
(define pf:anything-implies-true (lambda (P : Type) T))
|
||||
|
||||
(qed thm:anything-implies-true (lambda (P : Type) T))
|
||||
(module+ test
|
||||
(:: pf:anything-implies-true thm:anything-implies-true))
|
||||
|
||||
(data False : Type)
|
||||
|
||||
|
|
@ -35,39 +41,42 @@
|
|||
[b-type (type-infer/syn #'b)])
|
||||
#`(conj #,a-type #,b-type a b))]))
|
||||
|
||||
(define-theorem thm:and-is-symmetric
|
||||
(define thm:and-is-symmetric
|
||||
(forall* (P : Type) (Q : Type) (ab : (And P Q)) (And Q P)))
|
||||
|
||||
(define proof:and-is-symmetric
|
||||
(define pf:and-is-symmetric
|
||||
(lambda* (P : Type) (Q : Type) (ab : (And P Q))
|
||||
(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/i y x)))))
|
||||
|
||||
(qed thm:and-is-symmetric proof:and-is-symmetric)
|
||||
(module+ test
|
||||
(:: pf:and-is-symmetric thm:and-is-symmetric))
|
||||
|
||||
(define-theorem thm:proj1
|
||||
(define thm:proj1
|
||||
(forall* (A : Type) (B : Type) (c : (And A B)) A))
|
||||
|
||||
(define proof:proj1
|
||||
(define pf:proj1
|
||||
(lambda* (A : Type) (B : Type) (c : (And A B))
|
||||
(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))))
|
||||
|
||||
(qed thm:proj1 proof:proj1)
|
||||
(module+ test
|
||||
(:: pf:proj1 thm:proj1))
|
||||
|
||||
(define-theorem thm:proj2
|
||||
(define thm:proj2
|
||||
(forall* (A : Type) (B : Type) (c : (And A B)) B))
|
||||
|
||||
(define proof:proj2
|
||||
(define pf:proj2
|
||||
(lambda* (A : Type) (B : Type) (c : (And A B))
|
||||
(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))))
|
||||
|
||||
(qed thm:proj2 proof:proj2)
|
||||
(module+ test
|
||||
(:: pf:proj2 thm:proj2))
|
||||
|
||||
#| TODO: Disabled until #22 fixed
|
||||
(data Or : (forall* (A : Type) (B : Type) Type)
|
||||
|
|
@ -93,7 +102,7 @@
|
|||
(refl : (forall* (A : Type) (x : A) (== A x x))))
|
||||
|
||||
(module+ test
|
||||
(require rackunit "bool.rkt" "nat.rkt")
|
||||
(require "bool.rkt" "nat.rkt")
|
||||
(check-equal?
|
||||
(elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
|
||||
(λ* (A : Type) (x : A) z)
|
||||
|
|
|
|||
|
|
@ -17,15 +17,14 @@
|
|||
case*
|
||||
let
|
||||
|
||||
;; type-check
|
||||
::
|
||||
|
||||
;; reflection in syntax
|
||||
run
|
||||
step
|
||||
step-n
|
||||
query-type
|
||||
|
||||
;; don't use these
|
||||
define-theorem
|
||||
qed
|
||||
)
|
||||
|
||||
(require
|
||||
|
|
@ -132,17 +131,19 @@
|
|||
[(let (c:let-clause ...) body)
|
||||
#'((lambda* (c.id : c.type) ... body) c.e ...)]))
|
||||
|
||||
(define-syntax-rule (define-theorem name prop)
|
||||
(define name prop))
|
||||
|
||||
(define-syntax (qed stx)
|
||||
(syntax-case stx ()
|
||||
[(_ t pf)
|
||||
;; Normally type checking will only happen if a term is actually used. This forces a term to be
|
||||
;; checked against a particular type.
|
||||
(define-syntax (:: syn)
|
||||
(syntax-case syn ()
|
||||
[(_ pf t)
|
||||
(begin
|
||||
(unless (type-check/syn? #'pf #'t)
|
||||
(raise-syntax-error 'qed "Invalid proof"
|
||||
#'pf #'t))
|
||||
#'pf)]))
|
||||
(raise-syntax-error
|
||||
'::
|
||||
(format "Term ~a does not have expected type ~a. Inferred type was ~a"
|
||||
(cur->datum #'pf) (cur->datum #'t) (cur->datum (type-infer/syn #'pf)))
|
||||
syn))
|
||||
#'(void))]))
|
||||
|
||||
(define-syntax (run syn)
|
||||
(syntax-case syn ()
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user