_automation.mm1

do {
  (def (id x) x)
  (def (ignore . _))
  (def dbg @ match-fn* [(x) (print x) x]
    [(x y) (display @ string-append (->string x) ": " (->string y)) y])
  (def (foldl l z s) (if (null? l) z (foldl (tl l) (s z (hd l)) s)))
  (def (foldli i l z s) (if (null? l) z (foldli {i + 1} (tl l) (s i z (hd l)) s)))
  (def (foldr l z s) (if (null? l) z (s (hd l) (foldr (tl l) z s))))
  (def (foldri i l z s) (if (null? l) z (s i (hd l) (foldri {i + 1} (tl l) z s))))
  (def (range a b) (if {a = b} () (cons a (range {a + 1} b))))
  (def (for a b f) (if {a = b} #undef (begin (f a) (for {a + 1} b f))))
  (def last (match-fn [(a) a] [(_ . l) (last l)]))
  (def split-last @ match-fn
    [(and (_) l) l]
    [(a . l) @ match (split-last l) @ (r . l2) '(,r ,a . ,l2)]
    [() ()])
  (def (append . ls) @ foldr ls () @ fn (l l2) @ foldr l l2 cons)
  (def (rev l) @ foldl l () (fn (l a) (cons a l)))
  (def (len l) @ foldl l 0 (fn (n _) {n + 1}))
  (def (filter l p) @ foldl l () @ fn (l2 x) @ if (p x) (cons x l2) l2)
  (def (repeat a n) (if {n = 0} () (cons a (repeat a {n - 1}))))
  (def (iterate n f a) (if {n = 0} a (f (iterate {n - 1} f a))))
  (def (find l) @ match l
    [((k v) . l) (def f (find l)) @ fn (a) @ if {k == a} v (f a)]
    [() @ fn (a)])
  (def (verb e) (copy-span e (list ':verb e)))
  (def (exact e) (refine (verb e)))
  (def (result) (hd (get-goals)))
  (def (target) (goal-type (result)))
  (def (inspect-result f) (def g (result)) (refine (f)) (display @ pp g))
  (def (later) @ match (get-goals)
    [(g . gs) (apply set-goals @ append gs @ list g)])
  (def mvar-sort @ match-fn @ (mvar s _) s)
  (def (report a) (def g (result)) (refine a) (print g))
  (def (atom-map . xs) (get! @ apply atom-map! xs))
  (def (lookup-fn xs) (def m (apply atom-map xs)) (fn k (apply lookup m k)))
  (def (atom-app . xs) (string->atom (apply string-append (map ->string xs))))
  (def transpose @ match-fn*
    [(xs) (apply map list xs)]
    [(n xs) (if (null? xs) (repeat () n) (apply map list xs))])
  (def (join xs) (apply append xs))
  (def (rmap . args) (apply map (split-last args)))
  (def (scan . args) (apply rmap args) #undef)
  (def (undef? x) (not (def? x)))
  (def (error-at sp msg) (report-at 'error sp msg))
  (def (info-at sp msg) (report-at 'info sp msg))
  (def goal! @ match-fn*
    [(ty) (ref! (goal ty))]
    [(pos ty) (ref! (copy-span pos (goal ty)))])
  (def (swap) @ match (get-goals) [(x . y) (apply set-goals @ append y @ list x)])
  (def suffices @ match-fn*
    [(h) (have h _) (swap)]
    [xs (apply have xs) (swap)])
  (def (get-proof x) @ match (get-decl x)
    [('theorem _ _ _ _ _ pf) (hd @ tl @ pf)]
    [_ (error "not a theorem")])
  (def (pp-proof x) (display @ pp @ get-proof x))

  (def (get-def exp) @ match (get-decl exp)
    [('def _ _ _ _ _ val) val]
    [_ (error "not a definition")])

  --| This utility will take a verbatim proof and "unelaborate" it into a refine script
  --| using ! on every step. This is useful to get `refine` to re-typecheck a term when
  --| testing tactics which produce verbatim proofs.
  (def unelab @ letrec (
    [(args bs xs)
      @ if (null? bs) (map rec xs)
      @ cons (hd xs) @ args (tl bs) (tl xs)]
    [rec @ match-fn
      [(':conv tgt _ p) '{,(rec p) : ,tgt}]
      [(f . xs)
        (cons '! f @ args (nth 2 @ get-decl f) xs)]
      [e e]])
    rec)

  --| This is a special variable used by `mm0-rs doc` to shorten axiom list printouts.
  --| It is an atom map from a name for the axiom list to a list of axioms.
  (def axiom-sets (atom-map!))
  --| Declare a new axiom set, which is used by the docgen tool to shorten axiom lists.
  (def (add-axiom-set! x doc xs) (insert! axiom-sets x (cons doc xs)))

  --| `(named pf)` wraps a proof script `pf`, runs it, then gathers all
  --| unassigned metavariables and assigns them to dummies.
  --| `(named x1 ... xn pf)` is the same but names the first `n` variables `x1,...,xn`.
  --| This is commonly used for proofs where we don't care to name the
  --| dummy variables.
  (def named
    (def (assign-mvar m x) @ match x ['_] [_ (set! m (dummy! x (mvar-sort m)))])
    @ match-fn*
      [((? atom? d) es) (refine es) (scan (get-mvars) (list d) assign-mvar)]
      [(ds es) (refine es) (scan (get-mvars) ds assign-mvar)]
      [(es) (refine es)
        (def n (ref! 1))
        (scan (get-mvars) @ fn (v)
          (assign-mvar v (atom-app "a" n)) (set! n {n + 1}))
        (if {n = 1} (display "unnecessary (named)"))])

  --| `(name-all x1 ... xn)` instantiates all metavariables in the current
  --| proof state. It is the same as `named` but it can be used in the middle of a
  --| proof instead of as a wrapper around a complete proof.
  (def (name-all . ds)
    (def (assign-mvar m x) @ match x ['_] [_ (set! m (dummy! x (mvar-sort m)))])
    (scan (get-mvars) ds assign-mvar))

  (def ((tac-thm stmt f))
    @ match (get-goals) @ (g)
    (def res (f))
    (if (def? res) (refine res))
    (match (get-goals) [()] [_ (stat) (error "not all goals are solved")])
    '(() ,g))
  (def (add-tac-thm! x bis hyps ret vis f)
    (add-thm! x bis hyps ret vis (tac-thm ret f)))

  (def eq-for @ lookup-fn '([wff iff] [nat eq] [set eqs]))
  (def eq-sort @ lookup-fn '([iff wff] [eq nat] [eqs set]))
  (def nf-for @ lookup-fn '([wff nf] [nat nfn] [set nfs]))
  (def eqid-for @ lookup-fn '([wff biid] [nat eqid] [set eqsid]))
  (def eqidd-for @ lookup-fn '([wff biidd] [nat eqidd] [set eqsidd]))
  (def eqd-map (atom-map!)) (set-merge-strategy eqd-map merge-map)
  (def (eqd-for . e) (apply lookup eqd-map e))
  (def (register-eqd df) (fn (tgt) (insert! eqd-map df tgt)))
  (def (get-tgt-args args df . s) @ match args
    [() (apply atom-app df s)]
    [((? atom? t)) (apply atom-app t s)]
    [('quote (? atom? t)) t])

  (def (maybe-atom-map hs)
    @ if (apply and @ map (fn (x) (atom? (hd x))) hs)
      (let ([m (get! @ apply atom-map! hs)])
        @ fn (x) (lookup m x))
      (find hs))
  (def (eqtac-ctx ltr hyps)
    @ foldr hyps () @ fn (h ls)
      @ match (match (infer-type h) [('im _ R) R] [R R])
        [('eq L R) '([,(if ltr L R) ,h] . ,ls)]
        [_ ls])
  (def (eqtac-core ltr ctx t)
    @ match t @ (eq L R)
    @ letrec (
      [(f A) @ match (ctx A)
        [#undef @ match A
          [((? atom? t) . es)
            @ if (null? es) #undef @ begin
            @ match (eqd-for t) [#undef] @ eqd
            @ match (get-decl eqd) @ (_ _ bis hs ('im _ (eq (t . args) _)) ...)
            (def subterms @ apply atom-map! @ map list args es)
            (def isrefl (ref! #t))
            (def subproofs @ rmap hs @ match-fn @ (h ('im _ (eq arg _)))
              @ if (atom? arg)
                (or_refl isrefl @ lookup subterms arg)
                (eqidd-for (infer-sort A)))
            @ if isrefl #undef (cons eqd subproofs)]
          [e #undef]]
        [res res]]
      [(or_refl isrefl A) @ match (f A)
        [#undef (eqidd-for (infer-sort A))]
        [e (set! isrefl #f) e]])
    (or_refl (ref!) (if ltr L R)))
  (def ((eqtac-with ltr . hyps) refine t)
    @ refine t @ match t
    [('im G (and rhs (eq L R)))
      @ letrec ([add-locals @ match-fn*
        [(('an G D) f)
          (add-locals G @ fn (a p) (f a '(anwl ,G ,D ,a ,p)))
          (add-locals D @ fn (a p) (f a '(anwr ,G ,D ,a ,p)))]
        [((and a (h . _)) f) @ if (def? (eq-sort h)) (f a '(id ,a))]
        [_]])
      (def ctx (ref! (eqtac-ctx #t hyps)))
      (add-locals G @ match-fn* @ ((eq L R) p)
        (def v (if ltr L R))
        (def v @ match v [(mvar s _) (def d (dummy! s)) (set! v d) d] [_ v])
        (set! ctx '([,v ,(verb p)] . ,(get! ctx))))
      (eqtac-core ltr (maybe-atom-map ctx) rhs)]
    [(eq L R) '(trud ,(eqtac-core ltr (maybe-atom-map @ eqtac-ctx #t hyps) t))])

  --| A refine script that will prove formulas of the form `x = a -> (p <-> ?q)`
  --| by substituting all instances of `x` with `a` in `p`. This works whether `?q`
  --| is a metavariable or the substitution.
  (def eqtac (eqtac-with #t))

  --| Like `eqtac` but works in reverse:
  --| it will prove formulas of the form `x = a -> (?p <-> q)`
  --| by substituting all instances of `a` with `x` in `q`. If `x` is a metavariable, it
  --| also assigns it to a new dummy variable.
  (def ((eqtac-gen a) refine t) @ refine t
    @ match t @ ('im (eq x _) _)
      (def y (match x [(mvar s _) (dummy! s)] [_ x]))
      '{,(eqtac-with #f) : (im (eq ,y ,a) _)})

  --| This metaprogram proves a statement of the form
  --| $ G -> a1 = a2 $ > $ G -> b1 = b2 $ > $ G -> foo a1 b1 = foo a2 b2 $
  --| for any definition foo.
  (def (add-eqd-thm df . args)
    (def tgt (get-tgt-args args df "eqd"))
    @ match (get-decl df)
      [#undef (error (string-append "declaration '" (->string df) "' not found"))]
      [(_ _ () ...)]
      [(_ _ bis (ret _) . rest)
        (def G @ if (apply or (map (match-fn [('G ...) #t] [_ #f]) bis)) '_G '_G)
        @ if (def? (get-decl tgt)) (insert! eqd-map df tgt) @ begin
        (def ctx (atom-map!))
        @ match (map join @ transpose 4 @ rmap bis @ match-fn
          [(and (x s) e) (insert! ctx x (list s)) '((,e) () (,x) (,x))]
          [(v s vs) @ let ([v1 (atom-app '_ v 1)] [v2 (atom-app '_ v 2)] [hv (atom-app '_ v 'h)])
            (insert! ctx v (list v1 v2 s hv))
            '(() ((,v ,s ,v1 ,v2 ,hv))
              (,v1) (,v2))]) @ (xs vs es1 es2)
        (def xs1 (map hd xs))
        (def bis '((,G wff ()) . ,(append xs @ join @ rmap vs
          @ match-fn [(v s v1 v2 hv) '((,v1 ,s ,xs1) (,v2 ,s ,xs1))])))
        (def hs @ rmap vs @ match-fn [(v s v1 v2 hv) '(,hv (im ,G (,(eq-for s) ,v1 ,v2)))])
        (def rete '(im ,G (,(eq-for ret) (,df . ,es1) (,df . ,es2))))
        (match rest
          [() (add-thm! tgt bis hs rete)]
          [(_ ds v) @ add-thm! tgt bis hs rete () @ fn () @ list ds
            (def ds (rmap ds @ match-fn @ (x s) (insert! ctx x (list s)) x))
            @ letrec (
              [preproof (match-fn
                [(? atom? v) (lookup ctx v)]
                [((? atom? t) . es)
                  @ match (get-decl t) @ (_ _ bis (ret _) ...)
                  @ if (null? es) (list ret) @ begin
                  (def isrefl (ref! #t))
                  @ match (transpose 5 @ rmap bis es @ match-fn*
                    [((_ _) x) '((,x) () () ,x ,x)]
                    [((_ _ _) e)
                      @ match (preproof e)
                        [(s) '(() (,e ,e) ((,(eqidd-for s) ,G ,e)) ,e ,e)]
                        [(e1 e2 s p) (set! isrefl #f)
                          '(() (,e1 ,e2) (,p) ,e1 ,e2)]]) @ (xs ts ps es1 es2)
                  @ if isrefl (list ret) @ begin
                  @ match (eqd-for t)
                    [#undef (error @ string-append "equality theorem not found for " (->string t))]
                    [eqd '((,t . ,es1) (,t . ,es2) ,ret
                      (,eqd ,G . ,(append (join xs) (join ts) (join ps))))]])]
              [(mk-proof e) (match (preproof e)
                [(s) '(,e ,e (,(eqidd-for s) ,G ,e))]
                [(e1 e2 s p) (list e1 e2 p)])])
            @ match (mk-proof v) @ (t1 t2 p)
            '(:conv ,rete (im ,G (,(eq-for ret)
              (:unfold ,df ,es1 ,ds ,t1)
              (:unfold ,df ,es2 ,ds ,t2))) ,p)])
        (insert! eqd-map df tgt)])

  (def (ded-to-thm t)
    @ match (get-decl t) @ (_ _ ((G 'wff ()) . bis) hs ('im _ ret) ...)
    @ if (apply and @ rmap bis @ match-fn [(_ _ ()) #t] [_ #f]) @ begin
    (def rete @ foldr hs ret @ match-fn* [((_ ('im _ h)) r) '(im ,h ,r)])
    @ list bis rete @ fn () @ list ()
    @ letrec (
      [(exps l r) @ match r
        [('im e1 e2) (list 'exp l e1 e2 (exps (list 'an l e1) e2))]
        [_ (cons t l @ append (map hd bis) @
          map (match-fn [(_ h) h]) @ rev @ conjuncts l)]]
      [conjuncts @ match-fn
        [('an e1 e2)
          @ match (conjuncts e1)
            [(_) '((,e2 (anr ,e1 ,e2)) (,e1 (anl ,e1 ,e2)))]
            [hs (cons '(,e2 (anr ,e1 ,e2)) @
              rmap hs @ match-fn [(e h) '(,e (anwl ,e1 ,e2 ,e ,h))])]]
        [e '((,e (id ,e)))]])
    @ match rete [('im l r) (exps l r)])

  (def (make-eqNd-thms df)
    @ match (get-decl df) @ (_ _ bis (ret _) . rest)
    (def G '_G) (def h0 '_h)
    @ letrec (
      [mk-bis @ match-fn
        [() '(() () () () ())]
        [((and (x _) e) . bis)
          @ match (mk-bis bis) @ (pes vs es pp data)
          '((,x . ,pes) ,vs ,es ,pp
            ,(rmap data @ match-fn [(b t1 t2 h es ps)
              '(,b (,x . ,t1) (,x . ,t2) ,h ,es ,ps)]))]
        [((v s _) . bis)
          @ match (mk-bis bis) @ (pes vs es pp data)
          @ let ([v1 (atom-app '_ v 1)] [v2 (atom-app '_ v 2)])
          '((,v . ,pes)
            ((,v ,s) . ,vs)
            (,v ,v . ,es)
            ((,(eqidd-for s) ,G ,v) . ,pp)
            ((((,v1 ,s) (,v2 ,s) . ,vs)
              (,v1 . ,pes)
              (,v2 . ,pes)
              (im ,G (,(eq-for s) ,v1 ,v2))
              (,v1 ,v2 . ,es)
              (,h0 . ,pp)) .
             ,(rmap data @ match-fn @ (b t1 t2 h es ps)
              '(((,v ,s) . ,b) (,v . ,t1) (,v . ,t2) ,h (,v ,v . ,es) ((,(eqidd-for s) ,G ,v) . ,ps)))))]])
    (def xs @ join @ rmap bis @ match-fn [(and (_ _) e) (list e)] [_ ()])
    @ rmap (match (mk-bis bis) [(_ _ _ _ data) data]) @ match-fn @ (vs t1 t2 h es ps)
      (def xs1 (map hd xs))
      (def vs+ (rmap vs @ match-fn @ (v s) '(,v ,s ,xs1)))
      @ list
        '((,G wff ()) . ,(append xs vs+))
        '((,h0 ,h))
        '(im ,G (,(eq-for ret) (,df . ,t1) (,df . ,t2)))
        (match (eqd-for df)
          [#undef (error @ string-append "equality theorem not found for " (->string df))]
          [eqd '(,eqd ,G . ,(append xs1 es ps))]))

  (def eval-map (atom-map!
    '[im ,(fn (a b) {(not (eval a)) or (eval b)})]
    '[not ,(fn (a) (not (eval a)))]))
  (set-merge-strategy eval-map merge-map)
  (def (eval e) @ match e @ ((? atom? t) . es)
    (apply
      (lookup eval-map t @ fn () @ error
        @ string-append "unknown function encountered during evaluation: " (->string t))
      es))

  --| This is used as an annotation.
  --| * `@(add-eval f) def foo ..` will add `f` as an evaluator for `foo`,
  --|   which is used by the `eval` function (which can evaluate many
  --|   closed terms of sort `nat` or `wff` to values).
  --| * `@(add-eval)` will attempt to evaluate the body of the definition
  --|   and use that as the result.
  (def ((add-eval . f) a)
    (if (def? @ lookup eval-map a) (error "already defined evaluation rule"))
    @ insert! eval-map a @ match f
    [(f) (if (fn? f) f (fn () f))]
    [() (def x @ eval @ nth 6 @ get-decl a) (fn () x)])

  --| `@eval-check` is an annotation that can be placed on theorems or axioms which
  --| are closed terms, and will check that the theorem/axiom evaluates to `#t`.
  --| This is not formally rigorous as the evaluator is not verified, but it can be
  --| viewed as a cross-check of the axiom or the evaluator, depending on your
  --| point of view.
  (def (eval-check a) @ match (eval @ nth 4 @ get-decl a) [#t])

  --| `(named pf)` wraps a proof script `pf`, runs it, then gathers all
  --| unassigned metavariables and assigns them to dummies.
  --| `(named x1 ... xn pf)` is the same but names the first `n` variables `x1,...,xn`.
  --| This is commonly used for proofs where we don't care to name the
  --| dummy variables.
  (def named
    (def (assign-mvar m x) @ match x ['_] [_ (set! m (dummy! x (mvar-sort m)))])
    @ match-fn*
      [((? atom? d) es) (refine es) (scan (get-mvars) (list d) assign-mvar)]
      [(ds es) (refine es) (scan (get-mvars) ds assign-mvar)]
      [(es) (refine es)
        (def n (ref! 1))
        (scan (get-mvars) @ fn (v)
          (assign-mvar v (atom-app "a" n)) (set! n {n + 1}))
        (if {n = 1} (display "unnecessary (named)"))])
};

-- configuration
do {
  (set-timeout 500)
  (def (refine-extra-args refine tgt e . ps)
    @ refine tgt (foldl ps (verb e) @ fn (acc p2) @ copy-span e '(mp ,acc ,p2)))
};