From 3d441907f5f143374c113d038c3df7abcae15a4e Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Thu, 20 Aug 2015 18:10:57 -0400 Subject: [PATCH 1/3] Started on design of tactic system for Cur --- stdlib/tactics.rkt | 92 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 92 insertions(+) create mode 100644 stdlib/tactics.rkt diff --git a/stdlib/tactics.rkt b/stdlib/tactics.rkt new file mode 100644 index 0000000..638efd7 --- /dev/null +++ b/stdlib/tactics.rkt @@ -0,0 +1,92 @@ +#lang s-exp "../redex-curnel.rkt" + +;; 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. + +(begin-for-syntax + ;; current-goal is a Goal, a Cur proposition to be shown + (define-parameter current-goal none) + + ;; goals is a map of Naturals to Goals + (define-parameter goals (make-hash)) + + ;; current-expr is an Expr, a Cur expression that may include Holes. + (define-parameter current-expr hole) + + ;; 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)) + + ;; A tactic is a function that manipulates the current goal state. + ;; Tactic : Context -> Goals -> Goal -> (list Environment Goals Goal Expr) + + ;; tactics: map of tactic names to interpretation functions. + ;; i.e. tactics is a map Symbols => Tactics + (define-parameter tactics (make-hash)) + ) + +;; (define-tactic command-name function) +;; (define-tactic (command-name ctx goal-list current-goal args ...) 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 function) + (register-tactic! (syntax->datum #'name) + (syntax->datum #'function))])) + +;; NB: Assumes Cur terms are represented as lists +(define-tactic (intro env goals current-goal name) + ;; 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)")])) + +(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.")])) + +;; Tactic DSL grammar: +;; tactic-script ::= (qed (tactic-name args ...)) +;; tactic-name ::= dom(tactics) +;; args ::= dom(env) + +;; Open interactive REPL for tactic DSL; exit with QED command, which +;; returns a QED script +(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) From 32c824ca30479975d7893b881d391efb37721393 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Thu, 27 Aug 2015 18:29:58 -0400 Subject: [PATCH 2/3] More work on tactics, TODOs added to curnel --- redex-curnel.rkt | 6 +- stdlib/tactics.rkt | 193 +++++++++++++++++++++++++++++++-------------- 2 files changed, 137 insertions(+), 62 deletions(-) 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))) From 92654314756b916a8bb7f9f2b1157e5aea243fa4 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Wed, 9 Sep 2015 18:50:11 -0400 Subject: [PATCH 3/3] Tactics complete! after many hacks --- redex-curnel.rkt | 7 +++- stdlib/tactics.rkt | 86 ++++++++++++++++++++++++++-------------------- 2 files changed, 54 insertions(+), 39 deletions(-) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index c3bc128..7cbe3eb 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -985,7 +985,8 @@ cur-expand type-infer/syn type-check/syn? - normalize/syn) + normalize/syn + cur-equal?) run) (begin-for-syntax @@ -1139,6 +1140,10 @@ (define (run-cur->datum syn) (cur->datum (normalize/syn syn))) + ;; Are these two terms equivalent in type-systems internal equational reasoning? + (define (cur-equal? e1 e2) + (and (judgment-holds (equivalent ,(sigma) ,(run-cur->datum e1) ,(run-cur->datum e2)) #t))) + ;; TODO: OOps, type-infer doesn't return a cur term but a redex term ;; wrapped in syntax bla. This is bad. (define (type-infer/syn syn) diff --git a/stdlib/tactics.rkt b/stdlib/tactics.rkt index a3891c4..3e03c11 100644 --- a/stdlib/tactics.rkt +++ b/stdlib/tactics.rkt @@ -34,9 +34,8 @@ ;; 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 + (define hole 'hole) (define-struct proof-state (env goals current-goal current-proof)) (define current-proof-state (make-parameter #f)) @@ -48,7 +47,7 @@ (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)) + (proof-state (make-immutable-hash) (make-immutable-hash) prop values)) ;; push-env adds a mapping from name to P in (proof-state-env ps). ;; Proof-State -> Symbol -> Goal -> Proof-State @@ -68,7 +67,11 @@ (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)]))) + [current-proof (plug-ctxt (proof-state-current-proof ps) pf)])) + + (define (update-current-goal ps goal) + (struct-copy proof-state ps + [current-goal goal]))) ;; A tactic is a Racket function that manipulates the current proof state. ;; Tactic : Args ... Proof-State -> Proof-State @@ -79,6 +82,7 @@ (define-syntax (define-tactic syn) (syntax-case syn () [(_ (name args ... ps) body ...) + ;; TODO: quasisyntax/loc #'(begin-for-syntax (define (name args ... ps) body ...))] @@ -89,39 +93,41 @@ ;; (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: Maybe cur-expand current-goal by default ;; TODO: Goals should probably be Curnel terms (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)))] + (update-current-goal + (update-current-proof + (push-env ps (syntax-e name) #'P) + (lambda (x) #`(λ (x : P) #,x))) + #'body)] [_ (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. -; ;; 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.")])) +(begin-for-syntax + (define (assumption ps type) + (for/first ([(k v) (in-dict (proof-state-env ps))] + #:when (cur-equal? v type)) + k))) +(define-tactic (by-assumption ps) + (cond + [(assumption ps (cur-expand (proof-state-current-goal ps))) + => (curry update-current-proof ps)] + [else (error 'by-assumption "Cannot find an assumption that matches the goal")])) + +;; TODO: requires more support from curnel +#;(begin-for-syntax + (define (inductive? ps type) + )) +(define-tactic (obvious ps) + (syntax-parse (cur-expand (proof-state-current-goal ps)) + [(forall (x : P) t) + (obvious (intro #'x ps))] + [t:expr + (cond + [(assumption ps #'t) (by-assumption ps)] + ;[(inductive? ps #'t) (by-constructor ps)] + [else (error 'obvious "This is not all that obvious to me.")])])) ;; Tactic DSL grammar: ;; tactic-script ::= (qed (tactic-name args ...)) @@ -151,11 +157,12 @@ (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)) + [pf (proof-state-current-proof + (syntax-local-eval #`(let* ([ps (new-proof-state #'#,t)] + [ps (f #'args* ... ps)] ...) + ps)))]) + (when (procedure? pf) + (raise-syntax-error 'qed "Proof contains holes" (pf hole))) (unless (type-check/syn? pf t) (raise-syntax-error 'qed "Invalid proof" pf t)) pf)])) @@ -164,4 +171,7 @@ (define-theorem meow (forall (x : bool) bool)) (qed (intro x) - #;(by-assumption))) + (by-assumption)) + (define-theorem meow1 (forall (x : bool) bool)) + (qed (obvious)) + )