Tactics complete! after many hacks

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)

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-goal
        (update-current-proof
         (push-env ps (syntax-e name) #'P)
-       (lambda (x) #`(λ (x : P) #,x)))]
+        (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)
+(begin-for-syntax
-;  (match current-goal
+  (define (assumption ps type)
-;    [(∀ (x : P) body)
+    (for/first ([(k v) (in-dict (proof-state-env ps))]
-;     ;; TODO: These patterns seem to indicate env, goals, current-goal
+                #:when (cur-equal? v type))
-;     ;; TODO: should just be parameters, manipulated in a stateful manner.
+      k)))
-;     ;; TODO: No; don't be silly. Should instead define wrappers that allow
+(define-tactic (by-assumption ps)
-;     ;; TODO: you to focus on just what you care about.
+  (cond
-;     (match-let ([(list env goals current-goal body)
+    [(assumption ps (cur-expand (proof-state-current-goal ps)))
-;                  (obvious (push-env env name P) goals body)])
+     => (curry update-current-proof ps)]
-;       (list env goals current-goal `(λ (,x : ,P) ,body)))]
+    [else (error 'by-assumption "Cannot find an assumption that matches the goal")]))
-;    [(? assumption?) (by-assumption env goals current-goal)]
+
-;    [(? inductive?) (by-constructor env goals current-goal)]
+;; TODO: requires more support from curnel
-;    [_ (error 'obvious "This isn't all that obvious to me.")]))
+#;(begin-for-syntax
-;
+  (define (inductive? ps type)
-;(define-tactic (by-assumption env goals current-goal)
+    ))
-;  (match current-goal
+(define-tactic (obvious ps)
-;    [(? assumption P)
+  (syntax-parse (cur-expand (proof-state-current-goal ps))
-;     ;; TODO: How should "completing" a goal work? should the tactic
+    [(forall (x : P) t)
-;     ;; TODO: handle this, or the systen? Probably the system... detect when an
+     (obvious (intro #'x ps))]
-;     ;; TODO: expr with 0 holes has been returned, and type-check against
+    [t:expr
-;     ;; TODO: current goal.
+     (cond
-;     (list env goals current-goal (env-search-by-prop env P))]
+       [(assumption ps #'t) (by-assumption ps)]
-;    ;; TODO: Check uses of error vs errorf, or whatever
+       ;[(inductive? ps #'t) (by-constructor ps)]
-;    [_ (error 'by-assumption "You have not assumed this.")]))
+       [else (error 'obvious "This is not all that obvious to me.")])]))
 
 ;; Tactic DSL grammar:
 ;;   tactic-script ::= (qed (tactic-name args ...))
@@ -155,7 +161,8 @@
                   (syntax-local-eval #`(let* ([ps (new-proof-state #'#,t)]
                                               [ps (f #'args* ... ps)] ...)
                                              ps)))])
-          (displayln (current-theorem))
+          (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))
+  )