proof-mechs
1 ; Using the Zbepi language and base Logji helpers, manually compute various 2 ; proofs. This shows the underlying mechanisms used, which hopefully will 3 ; suggest patterns that the high-level proof language should provide. 4 5 6 ; The first law of portation 7 ; (= (⇒ (∧ a b) c) 8 ; (⇒ a (⇒ b c))) 9 ; Assume the needed axioms, laws, and helpers are already defined 10 11 ($when (instance? '(= (⇒ (∧ a b) c) ; | First step true because 12 (∨ (¬ (∧ a b)) c)) ; | instance of a law 13 material-implication) ; | 14 ($let (('(= (⇒ (∧ a b) c) ; | 15 (∨ (¬ (∧ a b)) c)) ; | 16 #T)) ; | 17 18 ; 2nd step uses transparency 19 ($when (instance? '(= (¬ (∧ a b)) 20 (∨ (¬ a) (¬ b))) 21 duality) 22 ($let ((value-representative (string-copy "V.R."))) 23 ($let (('(¬ (∧ a b)) value-representative) 24 ('(∨ (¬ a) (¬ b)) value-representative)) 25 (when (term-equal? '(∨ (¬ (∧ a b)) c) 26 '(∨ (∨ (¬ a) (¬ b)) c)) 27 ; NO: term-equal? not strict enough 28 ($let (('(= (∨ (¬ (∧ a b)) c) 29 (∨ (∨ (¬ a) (¬ b)) c)) 30 #T)) 31 ))))))) 32 33 34 35 #; 36 ($define $make-law 37 ($vau (vars-types expr val) env 38 (eval (list $let (map ($lambda (x) 39 (list (list quote (list $type (car x))) 40 (cadr x))) 41 vars-types) 42 (list $let (list (list (list quote expr) val)) 43 (list quote expr))) 44 env))) 45 46 47 48 ; TODO: Should the below calculation methods be implemented in Scheme instead? 49 ; I think so, at least for now. 50 51 ($define transparency 52 ($let ((=-term ($let (('($type x) anything) 53 ('($type y) anything)) 54 '(= x y)))) 55 ($lambda (rule path) 56 ($lambda (expr env known unknown) 57 ($if (instance? (make-term expr env) =-term) 58 ($let ((e1 (cadr expr)) 59 (e2 (caddr expr))) 60 ($let ((s1 (tree-ref/path e1 path)) 61 (s2 (tree-ref/path e2 path))) 62 ($if (equal?/except-path e1 e2 path) 63 (rule 64 (list = s1 s2) env 65 ($lambda (val) 66 ($if (boolean? val) 67 (known val) 68 (error "rule didn't give boolean"))) 69 unknown) 70 (error "other sub-expressions not equal" e1 e2)))) 71 (error "not = term" expr)))))) 72 73 74 ($define law 75 ($lambda (b) 76 ($lambda (expr env known unknown) 77 ($if (instance? (make-term expr env) (binding-ident b)) 78 (known (binding-val b)) 79 (unknown))))) 80 81 82 ($define consistency 83 ($lambda (enclosing) 84 85 (define (binding x e) 86 (cond ((pair? x) (env-binding e (make-term x e))) 87 ((symbol? x) (env-binding e x)) 88 (else (make-binding #F x)))) 89 90 ($let* ((e-expr (term-expr enclosing)) 91 (e-env (term-env enclosing)) 92 (e-val (binding-val (env-binding e-env enclosing))) 93 (e-optr (car e-expr)) 94 (e-opnd (cdr e-expr))) 95 96 (define (possib-vals expr) 97 (let ((b (binding expr e-env))) 98 ($if b 99 (cons (list (binding-val b)) 100 #F) 101 (cons (eval (list type-values (list $type expr)) 102 e-env) 103 (make-term expr e-env))))) 104 105 (let* ((optr-pv/t (possib-vals e-optr)) 106 (optr-pv (car optr-pv/t)) 107 (optr-t (cdr optr-pv/t))) 108 109 ($if (for-all applicative? optr-pv) 110 111 ($let* ((opnd-pv/t (map possib-vals e-opnd)) 112 (opnd-pv (map car opnd-pv/t)) 113 (opnd-t (map cdr opnd-pv/t)) 114 (unbound-terms (cons optr-t opnd-t)) 115 (vals-possibs (permute (cons optr-pv opnd-pv))) 116 (e-val-possibs 117 ($let ((params (do ((n (length (car vals-possibs)) 118 (- n 1)) 119 (a '() (cons (string-symbol 120 (string-append "p" 121 (number->string n))) 122 a))) 123 ((= 0 n) a)))) 124 (map ($lambda (vp) 125 ($let* ((t (eval (cons (list $vau params #F 126 (list $quote params)) 127 vp) 128 empty-env)) 129 (b (env-binding e-env t))) 130 ($if b 131 (cons (binding-val b) vp) 132 (error "unknown value for possibility" vp)))) 133 vals-possibs))) 134 (same-val-possibs 135 (filter (lambda (x) (eqv? e-val (car x))) 136 e-val-possibs)) 137 (new-vals-env 138 (if (= 1 (length same-val-possibs)) 139 (fold-left (lambda (e t v) 140 (if t (bind e t v) e)) 141 empty-env 142 unbound-terms 143 (cdar same-val-possibs)) 144 empty-env))) 145 146 ($lambda (expr env known unknown) 147 ($let ((b (env-binding new-vals-env (make-term expr env)))) 148 ($if b 149 (known (binding-val b)) 150 (unknown))))) 151 152 (error "not applicative" e-optr)))))) 153 154 155 ($define $calculate 156 ($vau (expr : method . rest) env 157 (if (($symbol=? :) :) 158 ((eval method env) 159 expr env 160 ($lambda (val) 161 ($let ((t (make-term expr env))) 162 ($if (null? rest) 163 (make-binding t val) 164 (eval (list $let (list (list t val)) 165 (cons $calculate rest)) 166 env)))) 167 ($lambda () (error "unable to evaluate" expr))) 168 (error "invalid syntax" :)))) 169 170 171 172 173 ($calculate 174 175 (= (⇒ (∧ a b) c) 176 (∨ (¬ (∧ a b)) c)) : (law mat-impl) 177 178 (= (∨ (¬ (∧ a b)) c) 179 (∨ (∨ (¬ a) (¬ b)) c)) : (transparency (law duality) (path 1)) 180 181 (= (∨ (∨ (¬ a) (¬ b)) c) 182 (∨ (¬ a) (∨ (¬ b) c))) : (law disj-assoc) 183 184 (= (∨ (¬ a) (∨ (¬ b) c)) 185 (⇒ a (∨ (¬ b) c))) : (law mat-impl) 186 187 (= (⇒ a (∨ (¬ b) c)) 188 (⇒ a (⇒ b c))) : (transparency (law mat-impl) (path 2)) 189 190 191 (⇒ (∧ (= (∨ (¬ a) (∨ (¬ b) c)) 192 (⇒ a (∨ (¬ b) c))) 193 (= (⇒ a (∨ (¬ b) c)) 194 (⇒ a (⇒ b c)))) 195 (= (∨ (¬ a) (∨ (¬ b) c)) 196 (⇒ a (⇒ b c)))) : (law equality-transitivity) 197 198 (∧ (= (∨ (¬ a) (∨ (¬ b) c)) 199 (⇒ a (∨ (¬ b) c))) 200 (= (⇒ a (∨ (¬ b) c)) 201 (⇒ a (⇒ b c)))) : zbepi ; TODO: what's a better name? 202 203 (= (∨ (¬ a) (∨ (¬ b) c)) 204 (⇒ a (⇒ b c))) : (consistency '(⇒ (∧ (= (∨ (¬ a) (∨ (¬ b) c)) 205 (⇒ a (∨ (¬ b) c))) 206 (= (⇒ a (∨ (¬ b) c)) 207 (⇒ a (⇒ b c)))) 208 (= (∨ (¬ a) (∨ (¬ b) c)) 209 (⇒ a (⇒ b c))))) 210 211 212 ; ... finish all the transitivity 213 214 (= (⇒ (∧ a b) c) 215 (⇒ a (⇒ b c))) : (consistency ...) 216 ) 217 218 219 220 221 222 ($prove (= (⇒ (∧ a b) c) 223 (⇒ a (⇒ b c))) 224 ) 225