git @ Cat's Eye Technologies Philomath / d88471c
Merge pull request #1 from catseye/develop-202209xx Develop 2022.09xx Chris Pressey authored 2 years ago GitHub committed 2 years ago
8 changed file(s) with 273 addition(s) and 270 deletion(s). Raw diff Collapse all Expand all
+2
-2
README.md less more
5757 the following things, it is possible it is no longer a valid proof:
5858
5959 * includes the file `proof.c` directly, rather than including `proof.h`
60 * casts a `struct proof` value to some other type
61 * casts a value of some other type to a `struct proof`
60 * casts a `struct theorem` value to some other type
61 * casts a value of some other type to a `struct theorem`
6262
6363 Fortunately, it is possible to statically analyze a C source file and confirm
6464 that it does none of these things, if such a level of assurance is desired.
+1
-1
build.sh less more
00 #!/bin/sh -ex
11
22 CC="gcc -ansi -pedantic"
3 for MODULE in assert formula assumptions proof; do
3 for MODULE in assert formula assumptions theorem; do
44 (cd src && ${CC} ${CFLAGS} -I../include -c $MODULE.c -o $MODULE.o)
55 done
+13
-13
eg/demo-proof4.c less more
1111 #include "proof.h"
1212
1313 int main(int argc, char **argv) {
14 struct proof *step1 = suppose(disj(neg(var("p")), var("q")), 1); /* Suppose ~p \/ q (1) */
15 struct proof *step2 = suppose(neg(var("p")), 2); /* Now, suppose ~p (2) */
16 struct proof *step3 = suppose(var("p"), 3); /* Further, suppose p (3) */
17 struct proof *step4 = neg_elim(step3, step2); /* So bottom, by neg_elim */
18 struct proof *step5 = absr_elim(step4, var("q")); /* Hence q, by absr_elim */
19 struct proof *step6 = impl_intro(3, step5); /* Hence, p -> q by (3) */
20 struct proof *step7 = suppose(var("q"), 4); /* Now, suppose q (4) */
21 struct proof *step8 = suppose(var("p"), 5); /* Further, suppose p (5) */
22 struct proof *step9 = conj_intro(step7, step8); /* So q /\ p, by conj_intro */
23 struct proof *stepA = conj_elim_lhs(step9); /* So q (under (5)), by conj_elim */
24 struct proof *stepB = impl_intro(5, stepA); /* Hence, p -> q by (5) */
25 struct proof *stepC = disj_elim(step1, step6, 2, stepB, 4); /* So, p -> q by disj_elim with (2), (4) */
26 struct proof *stepD = impl_intro(1, stepC); /* So, ~p \/ q -> (p -> q) by (1) */
14 struct theorem *step1 = suppose(disj(neg(var("p")), var("q")), 1); /* Suppose ~p \/ q (1) */
15 struct theorem *step2 = suppose(neg(var("p")), 2); /* Now, suppose ~p (2) */
16 struct theorem *step3 = suppose(var("p"), 3); /* Further, suppose p (3) */
17 struct theorem *step4 = neg_elim(step3, step2); /* So bottom, by neg_elim */
18 struct theorem *step5 = absr_elim(step4, var("q")); /* Hence q, by absr_elim */
19 struct theorem *step6 = impl_intro(3, step5); /* Hence, p -> q by (3) */
20 struct theorem *step7 = suppose(var("q"), 4); /* Now, suppose q (4) */
21 struct theorem *step8 = suppose(var("p"), 5); /* Further, suppose p (5) */
22 struct theorem *step9 = conj_intro(step7, step8); /* So q /\ p, by conj_intro */
23 struct theorem *stepA = conj_elim_lhs(step9); /* So q (under (5)), by conj_elim */
24 struct theorem *stepB = impl_intro(5, stepA); /* Hence, p -> q by (5) */
25 struct theorem *stepC = disj_elim(step1, step6, 2, stepB, 4); /* So, p -> q by disj_elim with (2), (4) */
26 struct theorem *stepD = impl_intro(1, stepC); /* So, ~p \/ q -> (p -> q) by (1) */
2727 return proves(
2828 stepD,
2929 impl(disj(neg(var("p")), var("q")), impl(var("p"), var("q")))
+6
-6
eg/demo-proof5.c less more
77 #include "proof.h"
88
99 int main(int argc, char **argv) {
10 struct proof *step1 = suppose(impl(neg(var("p")), absr()), 1); /* Suppose ~p -> _|_ (1) */
11 struct proof *step2 = suppose(neg(var("p")), 2); /* Now, suppose ~p (2) */
12 struct proof *step3 = impl_elim(step2, step1); /* Hence, _|_ */
13 struct proof *step4 = neg_intro(2, step3); /* And thus ~ our ~p, a.k.a. ~~p */
14 struct proof *step5 = double_neg_elim(step4); /* a.k.a. p, to a classicist */
15 struct proof *step6 = impl_intro(1, step5); /* So (~p -> _|_) -> p */
10 struct theorem *step1 = suppose(impl(neg(var("p")), absr()), 1); /* Suppose ~p -> _|_ (1) */
11 struct theorem *step2 = suppose(neg(var("p")), 2); /* Now, suppose ~p (2) */
12 struct theorem *step3 = impl_elim(step2, step1); /* Hence, _|_ */
13 struct theorem *step4 = neg_intro(2, step3); /* And thus ~ our ~p, a.k.a. ~~p */
14 struct theorem *step5 = double_neg_elim(step4); /* a.k.a. p, to a classicist */
15 struct theorem *step6 = impl_intro(1, step5); /* So (~p -> _|_) -> p */
1616 return proves(
1717 step6,
1818 impl(impl(neg(var("p")), absr()), var("p"))
+1
-33
include/proof.h less more
0 /* proof.h */
0 #include "theorem.h"
11
2 #ifndef PROOF_H
3 #define PROOF_H 1
4
5 #include "formula.h"
6
7 struct proof;
8
9 int proves(struct proof *, struct formula *);
10
11 struct proof *suppose(struct formula *, int);
12
13 struct proof *conj_intro(struct proof *, struct proof *);
14 struct proof *conj_elim_lhs(struct proof *);
15 struct proof *conj_elim_rhs(struct proof *);
16
17 struct proof *impl_intro(int, struct proof *);
18 struct proof *impl_elim(struct proof *, struct proof *);
19
20 struct proof *disj_intro_lhs(struct formula *, struct proof *);
21 struct proof *disj_intro_rhs(struct proof *, struct formula *);
22 struct proof *disj_elim(struct proof *, struct proof *, int, struct proof *, int);
23
24 struct proof *conj_elim_lhs(struct proof *);
25 struct proof *conj_elim_rhs(struct proof *);
26
27 struct proof *neg_intro(int, struct proof *);
28 struct proof *neg_elim(struct proof *, struct proof *);
29
30 struct proof *absr_elim(struct proof *, struct formula *);
31 struct proof *double_neg_elim(struct proof *);
32
33 #endif /* ndef PROOF_H */
+34
-0
include/theorem.h less more
0 /* theorem.h */
1
2 #ifndef THEOREM_H
3 #define THEOREM_H 1
4
5 #include "formula.h"
6
7 struct theorem;
8
9 int proves(struct theorem *, struct formula *);
10
11 struct theorem *suppose(struct formula *, int);
12
13 struct theorem *conj_intro(struct theorem *, struct theorem *);
14 struct theorem *conj_elim_lhs(struct theorem *);
15 struct theorem *conj_elim_rhs(struct theorem *);
16
17 struct theorem *impl_intro(int, struct theorem *);
18 struct theorem *impl_elim(struct theorem *, struct theorem *);
19
20 struct theorem *disj_intro_lhs(struct formula *, struct theorem *);
21 struct theorem *disj_intro_rhs(struct theorem *, struct formula *);
22 struct theorem *disj_elim(struct theorem *, struct theorem *, int, struct theorem *, int);
23
24 struct theorem *conj_elim_lhs(struct theorem *);
25 struct theorem *conj_elim_rhs(struct theorem *);
26
27 struct theorem *neg_intro(int, struct theorem *);
28 struct theorem *neg_elim(struct theorem *, struct theorem *);
29
30 struct theorem *absr_elim(struct theorem *, struct formula *);
31 struct theorem *double_neg_elim(struct theorem *);
32
33 #endif /* ndef THEOREM_H */
+0
-215
src/proof.c less more
0 #include <stdio.h>
1 #include <stdlib.h>
2
3 #include "assert.h"
4 #include "formula.h"
5 #include "assumptions.h"
6 #include "proof.h"
7
8 struct proof {
9 struct assumptions *assumptions;
10 struct formula *conclusion;
11 };
12
13 struct proof *
14 mk_proof(struct assumptions *assumptions, struct formula *conclusion) {
15 struct proof *p = (struct proof *)malloc(sizeof(struct proof));
16 assert(p != NULL, "mk_proof: could not allocate proof object");
17 #ifdef DEBUG
18 fprintf(stdout, "-----------------------------------------\n");
19 fprintf(stdout, "Created proof of ");
20 formula_fprint(stdout, conclusion);
21 fprintf(stdout, " under assumptions:\n");
22 assumptions_fprint(stdout, assumptions);
23 fprintf(stdout, "-----------------------------------------\n\n");
24 #endif
25 p->assumptions = assumptions;
26 p->conclusion = conclusion;
27 return p;
28 }
29
30 int proves(struct proof *p, struct formula *c) {
31 /* Asserts that the proof p proves the formula c. If it does,
32 a successful system exit code (i.e. 0) is returned, with
33 which the process may exit. */
34 assert(p->assumptions == NULL, "proves: proof contains undischarged assumptions");
35 #ifdef DEBUG
36 if (!formula_eq(p->conclusion, c)) {
37 fprintf(stdout, "Claim: ");
38 formula_fprint(stdout, c);
39 fprintf(stdout, "\n");
40 fprintf(stdout, "Conclusion of proof: ");
41 formula_fprint(stdout, p->conclusion);
42 fprintf(stdout, "\n");
43 }
44 #endif
45 assert(formula_eq(p->conclusion, c), "proves: proof does not prove what is claimed");
46 return 0;
47 }
48
49 struct proof *
50 suppose(struct formula *formula, int label) {
51 return mk_proof(
52 assume(label, formula, NULL),
53 formula
54 );
55 }
56
57 struct proof *
58 conj_intro(struct proof *x, struct proof *y) {
59 /* If x is proved, and y is proved, then x & y is proved. */
60 return mk_proof(
61 merge(x->assumptions, y->assumptions),
62 conj(x->conclusion, y->conclusion)
63 );
64 }
65
66 struct proof *
67 conj_elim_lhs(struct proof *x) {
68 /* If x (of the form y & z) is proved, then y is proved. */
69 assert(x->conclusion->type == CONJ, "conj_elim_lhs: not a conjunction");
70 return mk_proof(
71 x->assumptions,
72 x->conclusion->lhs
73 );
74 }
75
76 struct proof *
77 conj_elim_rhs(struct proof *x) {
78 /* If x (of the form y & z) is proved, then z is proved. */
79 assert(x->conclusion->type == CONJ, "conj_elim_rhs: not a conjunction");
80 return mk_proof(
81 x->assumptions,
82 x->conclusion->rhs
83 );
84 }
85
86 struct proof *
87 impl_intro(int label, struct proof *y) {
88 /* If y is proved under the assumption x, then x -> y is proved. */
89 struct formula *f = lookup(label, y->assumptions);
90 struct assumptions *a = discharge(label, y->assumptions);
91 #ifdef DEBUG
92 if (f == NULL) {
93 fprintf(stdout, "Label %d not found in:", label);
94 assumptions_fprint(stdout, a);
95 fprintf(stdout, "\n");
96 }
97 #endif
98 assert(f != NULL, "impl_intro: label not found in assumptions");
99 return mk_proof(
100 a,
101 impl(f, y->conclusion)
102 );
103 }
104
105 struct proof *
106 impl_elim(struct proof *x, struct proof *y) {
107 /* If x is proved, and y (of the form x -> z) is proved, then z is proved. */
108 assert(y->conclusion->type == IMPL, "impl_elim: not an implication");
109 assert(formula_eq(y->conclusion->lhs, x->conclusion), "impl_elim: formula mismatch");
110 return mk_proof(
111 merge(x->assumptions, y->assumptions),
112 y->conclusion->rhs
113 );
114 }
115
116 struct proof *
117 disj_intro_lhs(struct formula *fx, struct proof *y) {
118 /* If y is proved, then x v y is proved, for any x. */
119 return mk_proof(
120 y->assumptions,
121 disj(fx, y->conclusion)
122 );
123 }
124
125 struct proof *
126 disj_intro_rhs(struct proof *x, struct formula *fy) {
127 /* If x is proved, then x v y is proved, for any y. */
128 return mk_proof(
129 x->assumptions,
130 disj(x->conclusion, fy)
131 );
132 }
133
134 struct proof *
135 disj_elim(struct proof *z, struct proof *x, int label1, struct proof *y, int label2) {
136 /* If z is proved, and under the assumption labelled "1" x is proved, and under
137 the assumption labelled "2" y is proved, and x concludes the same as y,
138 and z is proved and z is in the form "1" v "2", then x is proved. */
139 struct formula *f1, *f2;
140 struct assumptions *a_x, *a_y;
141
142 assert(z->conclusion->type == DISJ, "disj_elim: not a disjunction");
143
144 f1 = lookup(label1, x->assumptions);
145 a_x = discharge(label1, x->assumptions);
146
147 f2 = lookup(label2, y->assumptions);
148 a_y = discharge(label2, y->assumptions);
149
150 assert(formula_eq(x->conclusion, y->conclusion), "disj_elim: mismatched conclusions");
151 assert(formula_eq(z->conclusion->lhs, f1), "disj_elim: mismatched assumption on lhs");
152 assert(formula_eq(z->conclusion->rhs, f2), "disj_elim: mismatched assumption on rhs");
153
154 return mk_proof(
155 merge(z->assumptions, merge(a_x, a_y)),
156 x->conclusion
157 );
158 }
159
160 struct proof *
161 neg_intro(int label, struct proof *x)
162 {
163 /* If x is absurdum and x is proved under the assumption y, then not-y is proved. */
164 struct formula *f = lookup(label, x->assumptions);
165 struct assumptions *a = discharge(label, x->assumptions);
166 assert(x->conclusion->type == ABSR, "neg_intro: not absurdum");
167 #ifdef DEBUG
168 if (f == NULL) {
169 fprintf(stdout, "Label %d not found in:", label);
170 assumptions_fprint(stdout, a);
171 fprintf(stdout, "\n");
172 }
173 #endif
174 assert(f != NULL, "neg_intro: label not found in assumptions");
175 return mk_proof(
176 a,
177 neg(f)
178 );
179 }
180
181 struct proof *
182 neg_elim(struct proof *x, struct proof *y)
183 {
184 /* If x has the form z and x is proved, and y has the form not-z and y is proved,
185 then absurdum is proved. */
186 assert(y->conclusion->type == NEG, "neg_elim: not a negation");
187 assert(formula_eq(x->conclusion, y->conclusion->rhs), "neg_elim: mismatched conclusions");
188 return mk_proof(
189 merge(x->assumptions, y->assumptions),
190 absr()
191 );
192 }
193
194 struct proof *
195 absr_elim(struct proof *x, struct formula *fy)
196 {
197 /* If x is absurdum and x is proved, then y is proved for any y. */
198 assert(x->conclusion->type == ABSR, "absr_elim: not absurdum");
199 return mk_proof(
200 x->assumptions,
201 fy
202 );
203 }
204
205 struct proof *
206 double_neg_elim(struct proof *x)
207 {
208 assert(x->conclusion->type == NEG, "double_neg_elim: not a negation");
209 assert(x->conclusion->rhs->type == NEG, "double_neg_elim: not a double negation");
210 return mk_proof(
211 x->assumptions,
212 x->conclusion->rhs->rhs
213 );
214 }
+216
-0
src/theorem.c less more
0 #include <stdio.h>
1 #include <stdlib.h>
2
3 #include "assert.h"
4 #include "formula.h"
5 #include "assumptions.h"
6 #include "proof.h"
7
8 struct theorem {
9 struct assumptions *assumptions;
10 struct formula *conclusion;
11 };
12
13 struct theorem *
14 mk_theorem(struct assumptions *assumptions, struct formula *conclusion) {
15 struct theorem *t = (struct theorem *)malloc(sizeof(struct theorem));
16 assert(t != NULL, "mk_theorem: could not allocate theorem object");
17 #ifdef DEBUG
18 fprintf(stdout, "-----------------------------------------\n");
19 fprintf(stdout, "Created theorem ");
20 formula_fprint(stdout, conclusion);
21 fprintf(stdout, " under assumptions:\n");
22 assumptions_fprint(stdout, assumptions);
23 fprintf(stdout, "-----------------------------------------\n\n");
24 #endif
25 t->assumptions = assumptions;
26 t->conclusion = conclusion;
27 return t;
28 }
29
30 int proves(struct theorem *t, struct formula *c) {
31 /* Asserts that the theorem t proves the formula c. If it does,
32 a successful system exit code (i.e. 0) is returned, with
33 which the process may exit. */
34 assert(t->assumptions == NULL, "proves: proof contains undischarged assumptions");
35 #ifdef DEBUG
36 if (!formula_eq(t->conclusion, c)) {
37 fprintf(stdout, "Claim: ");
38 formula_fprint(stdout, c);
39 fprintf(stdout, "\n");
40 fprintf(stdout, "Conclusion of proof: ");
41 formula_fprint(stdout, t->conclusion);
42 fprintf(stdout, "\n");
43 }
44 #endif
45 assert(formula_eq(t->conclusion, c), "proves: proof does not prove what is claimed");
46 return 0;
47 }
48
49 struct theorem *
50 suppose(struct formula *formula, int label) {
51 return mk_theorem(
52 assume(label, formula, NULL),
53 formula
54 );
55 }
56
57 struct theorem *
58 conj_intro(struct theorem *x, struct theorem *y) {
59 /* If x is a theorem, and y is a theorem, then x & y is a theorem. */
60 return mk_theorem(
61 merge(x->assumptions, y->assumptions),
62 conj(x->conclusion, y->conclusion)
63 );
64 }
65
66 struct theorem *
67 conj_elim_lhs(struct theorem *x) {
68 /* If x (of the form y & z) is a theorem, then y is a theorem. */
69 assert(x->conclusion->type == CONJ, "conj_elim_lhs: not a conjunction");
70 return mk_theorem(
71 x->assumptions,
72 x->conclusion->lhs
73 );
74 }
75
76 struct theorem *
77 conj_elim_rhs(struct theorem *x) {
78 /* If x (of the form y & z) is a theorem, then z is a theorem. */
79 assert(x->conclusion->type == CONJ, "conj_elim_rhs: not a conjunction");
80 return mk_theorem(
81 x->assumptions,
82 x->conclusion->rhs
83 );
84 }
85
86 struct theorem *
87 impl_intro(int label, struct theorem *y) {
88 /* If y is a theorem under the assumption x, then x -> y is a theorem. */
89 struct formula *f = lookup(label, y->assumptions);
90 struct assumptions *a = discharge(label, y->assumptions);
91 #ifdef DEBUG
92 if (f == NULL) {
93 fprintf(stdout, "Label %d not found in:", label);
94 assumptions_fprint(stdout, a);
95 fprintf(stdout, "\n");
96 }
97 #endif
98 assert(f != NULL, "impl_intro: label not found in assumptions");
99 return mk_theorem(
100 a,
101 impl(f, y->conclusion)
102 );
103 }
104
105 struct theorem *
106 impl_elim(struct theorem *x, struct theorem *y) {
107 /* If x is a theorem, and y (of the form x -> z) is a theorem, then z is a theorem. */
108 assert(y->conclusion->type == IMPL, "impl_elim: not an implication");
109 assert(formula_eq(y->conclusion->lhs, x->conclusion), "impl_elim: formula mismatch");
110 return mk_theorem(
111 merge(x->assumptions, y->assumptions),
112 y->conclusion->rhs
113 );
114 }
115
116 struct theorem *
117 disj_intro_lhs(struct formula *fx, struct theorem *y) {
118 /* If y is a theorem, then x v y is a theorem, for any x. */
119 return mk_theorem(
120 y->assumptions,
121 disj(fx, y->conclusion)
122 );
123 }
124
125 struct theorem *
126 disj_intro_rhs(struct theorem *x, struct formula *fy) {
127 /* If x is a theorem, then x v y is a theorem, for any y. */
128 return mk_theorem(
129 x->assumptions,
130 disj(x->conclusion, fy)
131 );
132 }
133
134 struct theorem *
135 disj_elim(struct theorem *z, struct theorem *x, int label1, struct theorem *y, int label2) {
136 /* If z is a theorem, and under the assumption labelled "1" x is a theorem, and under
137 the assumption labelled "2" y is a theorem, and x concludes the same as y,
138 and z (in the form "1" v "2") is a theorem, then x is a theorem. */
139 struct formula *f1, *f2;
140 struct assumptions *a_x, *a_y;
141
142 assert(z->conclusion->type == DISJ, "disj_elim: not a disjunction");
143
144 f1 = lookup(label1, x->assumptions);
145 a_x = discharge(label1, x->assumptions);
146
147 f2 = lookup(label2, y->assumptions);
148 a_y = discharge(label2, y->assumptions);
149
150 assert(formula_eq(x->conclusion, y->conclusion), "disj_elim: mismatched conclusions");
151 assert(formula_eq(z->conclusion->lhs, f1), "disj_elim: mismatched assumption on lhs");
152 assert(formula_eq(z->conclusion->rhs, f2), "disj_elim: mismatched assumption on rhs");
153
154 return mk_theorem(
155 merge(z->assumptions, merge(a_x, a_y)),
156 x->conclusion
157 );
158 }
159
160 struct theorem *
161 neg_intro(int label, struct theorem *x)
162 {
163 /* If x is absurdum and x is a theorem under the assumption y, then not-y is a theorem. */
164 struct formula *f = lookup(label, x->assumptions);
165 struct assumptions *a = discharge(label, x->assumptions);
166 assert(x->conclusion->type == ABSR, "neg_intro: not absurdum");
167 #ifdef DEBUG
168 if (f == NULL) {
169 fprintf(stdout, "Label %d not found in:", label);
170 assumptions_fprint(stdout, a);
171 fprintf(stdout, "\n");
172 }
173 #endif
174 assert(f != NULL, "neg_intro: label not found in assumptions");
175 return mk_theorem(
176 a,
177 neg(f)
178 );
179 }
180
181 struct theorem *
182 neg_elim(struct theorem *x, struct theorem *y)
183 {
184 /* If x has the form z and x is a theorem, and y has the form not-z and y is a theorem,
185 then absurdum is a theorem. */
186 assert(y->conclusion->type == NEG, "neg_elim: not a negation");
187 assert(formula_eq(x->conclusion, y->conclusion->rhs), "neg_elim: mismatched conclusions");
188 return mk_theorem(
189 merge(x->assumptions, y->assumptions),
190 absr()
191 );
192 }
193
194 struct theorem *
195 absr_elim(struct theorem *x, struct formula *fy)
196 {
197 /* If x is absurdum and x is a theorem, then y is a theorem for any y. */
198 assert(x->conclusion->type == ABSR, "absr_elim: not absurdum");
199 return mk_theorem(
200 x->assumptions,
201 fy
202 );
203 }
204
205 struct theorem *
206 double_neg_elim(struct theorem *x)
207 {
208 /* If x is a theorem and x is in the form not-not-y, then y is a theorem. */
209 assert(x->conclusion->type == NEG, "double_neg_elim: not a negation");
210 assert(x->conclusion->rhs->type == NEG, "double_neg_elim: not a double negation");
211 return mk_theorem(
212 x->assumptions,
213 x->conclusion->rhs->rhs
214 );
215 }