Rename from "proof.c" to "theorem.c" because it defines theorems.
Chris Pressey
1 year, 16 days ago

0 | 0 | #!/bin/sh -ex |

1 | 1 | |

2 | 2 | CC="gcc -ansi -pedantic" |

3 | for MODULE in assert formula assumptions proof; do | |

3 | for MODULE in assert formula assumptions theorem; do | |

4 | 4 | (cd src && ${CC} ${CFLAGS} -I../include -c $MODULE.c -o $MODULE.o) |

5 | 5 | done |

0 | /* proof.h */ | |

0 | #include "theorem.h" | |

1 | 1 | |

2 | #ifndef PROOF_H | |

3 | #define PROOF_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 PROOF_H */ |

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 | #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 | } |

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 | } |