diff --git a/redex-curnel.rkt b/redex-curnel.rkt index fbc42d7..c3bc128 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -119,9 +119,6 @@ (check-holds (α-equivalent (λ (x : A) x) (λ (y : A) y)))) - - - ;; NB: Substitution is hard ;; NB: Copy and pasted from Redex examples (define-metafunction cicL @@ -165,6 +162,8 @@ [(subst-all t (x_0 x ...) (e_0 e ...)) (subst-all (subst t x_0 e_0) (x ...) (e ...))]) + ;; TODO: I think a lot of things can be simplified if I rethink how + ;; TODO: model contexts, telescopes, and such. (define-extended-language cic-redL cicL (E ::= hole (v E) (E e)) ;; call-by-value ;; Σ (signature). (inductive-name : type ((constructor : type) ...)) @@ -217,6 +216,7 @@ ((append-Σ Σ_2 Σ_1) (x : t ((x_c : t_c) ...)))]) ;; TODO: Test + ;; TODO: Isn't this just plug? (define-metafunction cic-redL apply-telescope : t Ξ -> t [(apply-telescope t hole) t] diff --git a/stdlib/tactics.rkt b/stdlib/tactics.rkt index 638efd7..a3891c4 100644 --- a/stdlib/tactics.rkt +++ b/stdlib/tactics.rkt @@ -1,92 +1,167 @@ #lang s-exp "../redex-curnel.rkt" +(require racket/stxparam + racket/trace + racket/syntax + (for-syntax racket/trace racket/syntax)) ;; NB: The design of Cur currently seems to prevent intermediate type-checking ;; NB: during a tactic-based proof, unless I were to either reimplement the ;; NB: type-checker or extend it with a notion of holes. +;; NB: Per below, note that Cur already has contexts. The issue with +;; NB: type-checking intermediate results has to do with the fact that Cur +;; NB: contexts are not exposed properly, nor is type-checking defined on +;; NB: them. + +;;; A Goal is a syntax object representing a Cur proposition (type). + +;;; A Expr is a syntax object representing Cur expression (term). + +;;; A Hole is a procedure of type + +;;; A Ctxt is a procedure (Either Ctxt Expr) -> (Either Ctxt Expr) +;;; representing a Cur expression with a hole. + +;;; A Environment is a map from Symbol to Goal. + +;; A Proof-State is a struct containing: +;; env: An Environment, the assumptions introduced during a tactic +;; script. +;; goals: A map from Natural to Goal, the goals necessary to finish +;; this proof +;; current-goal: A Natural, the index into goals of the current Goal +;; to be proved. +;; current-proof: A (Either Ctxt Expr), representing the proof so far. +;; current-proof is an Expr, the proof is complete. + +(define-syntax-parameter hole + (lambda (stx) (raise-syntax-error "HOLEEEEE!"))) (begin-for-syntax - ;; current-goal is a Goal, a Cur proposition to be shown - (define-parameter current-goal none) + (define-struct proof-state (env goals current-goal current-proof)) - ;; goals is a map of Naturals to Goals - (define-parameter goals (make-hash)) + (define current-proof-state (make-parameter #f)) - ;; current-expr is an Expr, a Cur expression that may include Holes. - (define-parameter current-expr hole) + ;; The current theorem; used internally to achieve a Coq-like notation + ;; for defining theorems and tactic-based proofs. + (define current-theorem (make-parameter #f)) - ;; env is an Environment, a map of Symbols to Cur propositions, - ;; i.e., a map of of names to assumptions introduced during the - ;; tactic script - (define-parameter env (make-hash)) + (define (new-proof-state prop) + (unless prop + (raise-syntax-error 'qed "You can't use qed without a first using define-theorem")) + (proof-state (make-hash) (make-hash) prop values)) - ;; A tactic is a function that manipulates the current goal state. - ;; Tactic : Context -> Goals -> Goal -> (list Environment Goals Goal Expr) + ;; push-env adds a mapping from name to P in (proof-state-env ps). + ;; Proof-State -> Symbol -> Goal -> Proof-State + (define (push-env ps name P) + (struct-copy proof-state ps + [env (hash-set (proof-state-env ps) name P)])) - ;; tactics: map of tactic names to interpretation functions. - ;; i.e. tactics is a map Symbols => Tactics - (define-parameter tactics (make-hash)) - ) + ;; TODO: Cur already has contexts; perhaps they should be exposed? + ;; Ctxt -> (Either Ctxt Expr) -> (Either Ctxt Expr) + ;; C1[C2] + (define (plug-ctxt C1 C2) (C1 C2)) + (define Ctxt? procedure?) + + (define (proof-complete? ps) (not (Ctxt? (proof-state-current-proof ps)))) + + (define (update-current-proof ps pf) + ;; TODO: Check for proof completion? + (struct-copy proof-state ps + [current-proof (plug-ctxt (proof-state-current-proof ps) pf)]))) + +;; A tactic is a Racket function that manipulates the current proof state. +;; Tactic : Args ... Proof-State -> Proof-State + +;;; Syntax for defining tactics. ;; (define-tactic command-name function) -;; (define-tactic (command-name ctx goal-list current-goal args ...) body) +;; (define-tactic (command-name args ... Proof-State) body) (define-syntax (define-tactic syn) (syntax-case syn () - [(_ (name ctx goal-list current-goal args ...) body ...) - (register-tactic! (syntax->datum #'name) - (syntax->datum #'(lambda (ctx goal-list current-goal args ...) body ...)))] + [(_ (name args ... ps) body ...) + #'(begin-for-syntax + (define (name args ... ps) + body ...))] [(_ name function) - (register-tactic! (syntax->datum #'name) - (syntax->datum #'function))])) + (raise-syntax-error "Syntax not yet defined")])) -;; NB: Assumes Cur terms are represented as lists -(define-tactic (intro env goals current-goal name) +;; (define-goal-tactic command-name function) +;; (define-goal-tactic (command-name args ... ctx goal-list current-goal) body) + +(define-tactic (intro name ps) ;; TODO: Probably need to cur-expand current-goal ;; TODO: Goals should probably be Curnel terms - (match current-goal - [(∀ (x : P) body) - (list (push-env env name P) goals body - `(λ (,name : ,P) ,hole))] - [_ (error 'intro "Can only intro when current goal is of the form (∀ - (x : P) body)")])) + (syntax-parse (cur-expand (proof-state-current-goal ps)) + [(forall (x:id : P:expr) body:expr) + (update-current-proof + (push-env ps (syntax-e name) #'P) + (lambda (x) #`(λ (x : P) #,x)))] + [_ (error 'intro "Can only intro when current goal is of the form (∀ (x : P) body)")])) -(define-tactic (obvious env goals current-goal) - (match current-goal - [(∀ (x : P) body) - ;; TODO: These patterns seem to indicate env, goals, current-goal - ;; TODO: should just be parameters, manipulated in a stateful manner. - (match-let ([(list env goals current-goal body) - (obvious (push-env env name P) goals body)]) - (list env goals current-goal `(λ (,x : ,P) ,body)))] - [(? assumption?) (by-assumption env goals current-goal)] - [(? inductive?) (by-constructor env goals current-goal)] - [_ (error 'obvious "This isn't all that obvious to me.")])) - -(define-tactic (by-assumption env goals current-goal) - (match current-goal - [(? assumption P) - ;; TODO: How should "completing" a goal work? should the tactic - ;; TODO: handle this, or the systen? Probably the system... detect when an - ;; TODO: expr with 0 holes has been returned, and type-check against - ;; TODO: current goal. - (list env goals current-goal (env-search-by-prop env P))] - ;; TODO: Check uses of error vs errorf, or whatever - [_ (error 'by-assumption "You have not assumed this.")])) +;(define-tactic (obvious env goals current-goal) +; (match current-goal +; [(∀ (x : P) body) +; ;; TODO: These patterns seem to indicate env, goals, current-goal +; ;; TODO: should just be parameters, manipulated in a stateful manner. +; ;; TODO: No; don't be silly. Should instead define wrappers that allow +; ;; TODO: you to focus on just what you care about. +; (match-let ([(list env goals current-goal body) +; (obvious (push-env env name P) goals body)]) +; (list env goals current-goal `(λ (,x : ,P) ,body)))] +; [(? assumption?) (by-assumption env goals current-goal)] +; [(? inductive?) (by-constructor env goals current-goal)] +; [_ (error 'obvious "This isn't all that obvious to me.")])) +; +;(define-tactic (by-assumption env goals current-goal) +; (match current-goal +; [(? assumption P) +; ;; TODO: How should "completing" a goal work? should the tactic +; ;; TODO: handle this, or the systen? Probably the system... detect when an +; ;; TODO: expr with 0 holes has been returned, and type-check against +; ;; TODO: current goal. +; (list env goals current-goal (env-search-by-prop env P))] +; ;; TODO: Check uses of error vs errorf, or whatever +; [_ (error 'by-assumption "You have not assumed this.")])) ;; Tactic DSL grammar: ;; tactic-script ::= (qed (tactic-name args ...)) ;; tactic-name ::= dom(tactics) ;; args ::= dom(env) +;; TODO: ;; Open interactive REPL for tactic DSL; exit with QED command, which ;; returns a QED script -(define-syntax interactive-qed) +;(define-syntax interactive-qed) ;; Drop into tactic DSL, ends either explicitly or implicitly with the ;; QED command. ;; Example: -;; (define-theorem name prop -;; (qed -;; (intro x) -;; (elim) -;; (apply f x))) -(define-syntax qed) +;; (define-theorem name prop) +;; (qed +;; (intro x) +;; (elim) +;; (apply f x))) +(define-syntax (define-theorem syn) + (syntax-case syn () + [(_ name prop) + (begin + (current-theorem (cur-expand #'prop)) + #'(define name prop))])) +(define-syntax (qed syn) + (syntax-case syn () + [(_ (f args* ...) ...) + (let* ([t (current-theorem)] + [pf (proof-state-current-proof + (syntax-local-eval #`(let* ([ps (new-proof-state #'#,t)] + [ps (f #'args* ... ps)] ...) + ps)))]) + (displayln (current-theorem)) + (unless (type-check/syn? pf t) + (raise-syntax-error 'qed "Invalid proof" pf t)) + pf)])) +(module+ test + (require "bool.rkt") + (define-theorem meow (forall (x : bool) bool)) + (qed + (intro x) + #;(by-assumption)))