@@ -13,29 +13,29 @@ Propositions and Judgments
14Propositions 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'.
14Propositions 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'.
15For instance, if the ``proposition`` is,
15For instance, if the ``proposition`` is,
16− <table border="1">
16+
18− <td>1+1=2</td>
18+| 1+1=2 |
21When we prove it, the ``judgment`` is,
21When we prove it, the ``judgment`` is,
22− <table border="1">
22+
23− <tr>
23++------------+
24− <td>1+1=2 true</td>
24+| 1+1=2 true |
25− </tr>
25++------------+
27Or if the ``proposition`` is,
27Or if the ``proposition`` is,
28− <table border="1">
28+
30− <td>1+1=3</td>
30+| 1+1=3 |
33Obviously 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,
33Obviously 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">
34+
35− <tr>
35++-------------+
36− <td>1+1=3 false</td>
36+| 1+1=3 false |
37− </tr>
37++-------------+
39This 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.
39This 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.
41So 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.
41So 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,
61is 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:
61is 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:
64− <tr>
64+.. code-block:: idris
65− <td><pre>Idris> 1+1=3
66+ Idris> 1+1=3
66−<span class="style1">2 = <span class="style1">3 : Type</pre></td>
67+ 2 = 3 : Type
70Both 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.
69Both 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.
71A 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
70A 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
73−<table border="1">
72+.. code-block:: idris
75− <td><pre>onePlusOne : 1+1=2
74+ onePlusOne : 1+1=2
76−onePlusOne = Refl</pre></td>
75+ onePlusOne = Refl
80So 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:
77So 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:
82.. code-block:: idris
79.. code-block:: idris
84 Idris> Refl
81 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
87So it must pattern match on its return type:
84So it must pattern match on its return type:
@@ -170,10 +167,11 @@ Especially when working with equalities containing variable terms (inside functi
171plusReducesR gives the following error:
168plusReducesR gives the following error:
173−<table border="1">
170+
174− <tr>
171+.. code-block:: idris
175− <td><pre>- + Errors (1)
173+ - + Errors (1)
176− `-- proof.idr line 6 col 17:
174+ `-- proof.idr line 6 col 17:
177 When checking right hand side of plusReducesR with expected type
175 When checking right hand side of plusReducesR with expected type
178 plus n 0 = n
176 plus n 0 = n
@@ -186,9 +184,7 @@ plusReducesR gives the following error:
186 Type mismatch between
184 Type mismatch between
189− plus n 0</pre></td>
187+ plus n 0
193So why is 'Refl' able to prove some equality types but not others?
189So why is 'Refl' able to prove some equality types but not others?
@@ -200,7 +196,7 @@ So when we type 1+1 in Idris it is immediately converted to 2 because definition
201.. code-block:: idris
197.. code-block:: idris
203− Idris> 1+1
199+ Idris> 1+1
204 2 : Integer
200 2 : Integer
206In the following pages we discuss how to resolve propositionaly equalies.
202In 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
219These are axioms, that is a propositions/types that are asserted to be true without proof. In Idris we can use the 'postulate' keyword
215These are axioms, that is a propositions/types that are asserted to be true without proof. In Idris we can use the 'postulate' keyword
221− <table border="1">
217+
222− <tr>
218+.. code-block:: idris
223− <td><pre>comutePlus ``postulate``: x -> y -> plus x y = plus y x
220+ commutePlus ``postulate``: x -> y -> plus x y = plus y x
227Alternatively 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.
222Alternatively 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.
229As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.
224As 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:
233- Should we try to implement both approaches?
228- Should we try to implement both approaches?
234- Should we define our types by constructing up from primitive types?
229- Should we define our types by constructing up from primitive types?
231+Proof theory affects these design decisions.