I write a EDSL which checks a proof (in intuitionistic propositional logic) and then generates a corresponding natural deduction. This is based on my SMathML.
(define (type-of var env)
(cond ((assoc var env) => cdr)
(else (error 'type-of "unknown variable ~s" var))))
(define (extend-env var type env)
(cons (cons var type) env))
(define (reify t)
(define (reify t)
(match t
((-> ,t1 ,t2) (&impl (@reify t1) (@reify t2)))
((conj ,t1 ,t2) (&conj (@reify t1) (@reify t2)))
((disj ,t1 ,t2) (&disj (@reify t1) (@reify t2)))
(bot $bottom)
(top $top)
(,else t)))
(define (@reify t)
(match t
((-> ,t1 ,t2) (@impl (@reify t1) (@reify t2)))
((conj ,t1 ,t2) (@conj (@reify t1) (@reify t2)))
((disj ,t1 ,t2) (@disj (@reify t1) (@reify t2)))
(bot $bottom)
(top $top)
(,else t)))
(reify t))
(struct result (t c) #:transparent)
(define (VAR u)
(lambda (env)
(define t (type-of u env))
(result t (assume u (&true (reify t))))))
(define (CONS a b)
(lambda (env)
(match-define (result ta ca) (a env))
(match-define (result tb cb) (b env))
(define type `(conj ,ta ,tb))
(result type
(&rull $conjI ca cb
(&true (reify type))))))
(define (CAR a)
(lambda (env)
(match-define (result ta ca) (a env))
(match ta
((conj ,t1 ,t2)
(result t1 (&rull $conjE1 ca
(&true (reify t1))))))))
(define (CDR a)
(lambda (env)
(match-define (result ta ca) (a env))
(match ta
((conj ,t1 ,t2)
(result t2 (&rull $conjE2 ca
(&true (reify t2))))))))
(define (LAM u t body)
(lambda (env)
(match-define (result tbody cbody)
(body (extend-env u t env)))
(define type `(-> ,t ,tbody))
(result type
(&rull (&implI u) cbody
(&true (reify type))))))
(define (APP a b)
(lambda (env)
(match-define (result ta ca) (a env))
(match-define (result tb cb) (b env))
(match ta
((-> ,t1 ,t2)
(unless (equal? t1 tb)
(error 'APP "type mismatch"))
(result t2 (&rull $implE ca cb
(&true (reify t2))))))))
(define (INL tb a)
(lambda (env)
(match-define (result ta ca) (a env))
(define type `(disj ,ta ,tb))
(result type (&rull $disjI1 ca
(&true (reify type))))))
(define (INR ta b)
(lambda (env)
(match-define (result tb cb) (b env))
(define type `(disj ,ta ,tb))
(result type (&rull $disjI2 cb
(&true (reify type))))))
(define (CASE a u1 b1 u2 b2)
(lambda (env)
(match-define (result ta ca) (a env))
(match ta
((disj ,t1 ,t2)
(match-define (result tb1 cb1)
(b1 (extend-env u1 t1 env)))
(match-define (result tb2 cb2)
(b2 (extend-env u2 t2 env)))
(unless (equal? tb1 tb2)
(error 'CASE "branch type mismatch"))
(result tb1 (&rull (&disjE u1 u2) ca cb1 cb2
(&true (reify tb1))))))))
(define (ND proof)
(result-c (proof '())))
Here are some examples.
(MB (ND (LAM $u `(-> (disj ,$A ,$B) ,$C)
(CONS (LAM $w $A
(APP (VAR $u)
(INL $B (VAR $w))))
(LAM $x $B
(APP (VAR $u)
(INR $A (VAR $x))))))))
(MB (ND (LAM $u `(conj (-> ,$A ,$C) (-> ,$B ,$C))
(LAM $w `(disj ,$A ,$B)
(CASE (VAR $w)
$x (APP (CAR (VAR $u)) (VAR $x))
$y (APP (CDR (VAR $u)) (VAR $y)))))))
(let ((Neg (lambda (A) `(-> ,A bot))))
(MB (ND (LAM $u (Neg `(disj ,$A ,(Neg $A)))
(APP (LAM $v (Neg $A)
(APP (VAR $u)
(INR $A (VAR $v))))
(LAM $w $A
(APP (VAR $u)
(INL (Neg $A) (VAR $w)))))))))
Have fun with it!