@@ -13,29 +13,29 @@ Propositions and Judgments
1313
1414Propositions are the subject of our proofs, before the proof then we can't formally say if they are true or not. If the proof is successful then the result is a 'judgment'.
1515For instance, if the ``proposition`` is,
16− <table border="1">
17− <tr>
18− <td>1+1=2</td>
19− </tr>
20− </table>
16+
17++-------+
18+| 1+1=2 |
19++-------+
20+
2121When we prove it, the ``judgment`` is,
22− <table border="1">
23− <tr>
24− <td>1+1=2 true</td>
25− </tr>
26− </table>
22+
23++------------+
24+| 1+1=2 true |
25++------------+
26+
2727Or if the ``proposition`` is,
28− <table border="1">
29− <tr>
30− <td>1+1=3</td>
31− </tr>
32− </table>
28+
29++-------+
30+| 1+1=3 |
31++-------+
32+
3333Obviously we can't prove it is true, but it is still a valid proposition and perhaps we can prove it is false so the ``judgment`` is,
34− <table border="1">
35− <tr>
36− <td>1+1=3 false</td>
37− </tr>
38− </table>
34+
35++-------------+
36+| 1+1=3 false |
37++-------------+
38+
3939This may seem a bit pedantic but it is important to be careful, in mathematics not every proposition is true or false for instance, a proposition may be unproven or even unprovable.
4040
4141So the logic here is different from the logic that comes from boolean algebra. In that case what is not true is false and what is not false is true. The logic we are using here does not have this 'law of excluded middle' so we have to be careful not to use it.
@@ -60,29 +60,26 @@ The way that this works is that a proposition is a type so this,
6060
6161is a proposition and it is also a type. This is built into Idris so when an '=' equals sign appears in a function type an equality type is generated. The following will also produce an equality type:
6262
63−<table border="1">
64− <tr>
65− <td><pre>Idris> 1+1=3
66−<span class="style1">2 = <span class="style1">3 : Type</pre></td>
67− </tr>
68−</table>
63+
64+.. code-block:: idris
65+
66+ Idris> 1+1=3
67+ 2 = 3 : Type
6968
7069Both of these are valid propositions so both are valid equality types. But how do we represent true judgment, that is, how do we denote 1+1=2 is true but not 1+1=3.
7170A type that is true is inhabited, that is, it can be constructed. An equality type has only on constructor 'Refl' so a proof of 1+1=2 is
7271
73−<table border="1">
74− <tr>
75− <td><pre>onePlusOne : 1+1=2
76−onePlusOne = Refl</pre></td>
77− </tr>
78−</table>
72+.. code-block:: idris
73+
74+ onePlusOne : 1+1=2
75+ onePlusOne = Refl
7976
8077So how can Refl, which is a constructor without any parameters, construct and equality type? If we type it on its own then it can't:
8178
8279.. code-block:: idris
8380
8481 Idris> Refl
85− (input):Can't infer argument A to <span class="style1">Refl, Can't infer argument x to <span class="style1">Refl
82+ (input):Can't infer argument A to Refl, Can't infer argument x to Refl
8683
8784So it must pattern match on its return type:
8885
@@ -170,10 +167,11 @@ Especially when working with equalities containing variable terms (inside functi
170167
171168plusReducesR gives the following error:
172169
173−<table border="1">
174− <tr>
175− <td><pre>- + Errors (1)
176− `-- proof.idr line 6 col 17:
170+
171+.. code-block:: idris
172+
173+ - + Errors (1)
174+ `-- proof.idr line 6 col 17:
177175 When checking right hand side of plusReducesR with expected type
178176 plus n 0 = n
179177
@@ -186,9 +184,7 @@ plusReducesR gives the following error:
186184 Type mismatch between
187185 n
188186 and
189− plus n 0</pre></td>
190− </tr>
191−</table>
187+ plus n 0
192188
193189So why is 'Refl' able to prove some equality types but not others?
194190
@@ -200,7 +196,7 @@ So when we type 1+1 in Idris it is immediately converted to 2 because definition
200196
201197.. code-block:: idris
202198
203− Idris> 1+1
199+ Idris> 1+1
204200 2 : Integer
205201
206202In the following pages we discuss how to resolve propositionaly equalies.
@@ -218,12 +214,11 @@ Then we can implement '+' so that it respects these axioms (presumably implement
218214
219215These are axioms, that is a propositions/types that are asserted to be true without proof. In Idris we can use the 'postulate' keyword
220216
221− <table border="1">
222− <tr>
223− <td><pre>comutePlus ``postulate``: x -> y -> plus x y = plus y x
224−</pre></td>
225− </tr>
226− </table>
217+
218+.. code-block:: idris
219+
220+ commutePlus ``postulate``: x -> y -> plus x y = plus y x
221+
227222Alternatively we could define the natural numbers based on Zero and Successor. The axioms above then become derived rules and we also gain the ability to do inductive proofs.
228223
229224As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.
@@ -232,3 +227,7 @@ So what can we learn from this to implement out own types:
232227
233228- Should we try to implement both approaches?
234229- Should we define our types by constructing up from primitive types?
230+
231+Proof theory affects these design decisions.
232+
233+