@@ -0,0 +1,231 @@
1+In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,
2+
3+- Propositions and judgments
4+- Boolean and constructive logic
5+- Curry-Howard correspondence
6+- Definitional and propositional equalities
7+- Axiomatic and constructive approaches
8+
9+Propositions and Judgments
10+==========================
11+
12+Propositions 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'.
13+For instance, if the ``proposition`` is,
14+
15++-------+
16+| 1+1=2 |
17++-------+
18+
19+When we prove it, the ``judgment`` is,
20+
21++------------+
22+| 1+1=2 true |
23++------------+
24+
25+Or if the ``proposition`` is,
26+
27++-------+
28+| 1+1=3 |
29++-------+
30+
31+Obviously 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,
32+
33++-------------+
34+| 1+1=3 false |
35++-------------+
36+
37+This 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.
38+
39+So 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.
40+
41+A false proposition is taken to be a contradiction and if we have a contradiction then we can prove anything, so we need to avoid this. Some languages, used in proof assistants, prevent contradictions but such languages cannot be Turing complete, so Idris does not prevent contradictions.
42+
43+The logic we are using is called constructive (or sometimes intuitional) because we are constructing a 'database' of judgments.
44+
45+There are also many other types of logic, another important type of logic for Idris programmers is '``linear logic``' but that's not discussed on this page.
46+
47+Curry-Howard correspondence
48+===========================
49+
50+So how to we relate these proofs to Idris programs? It turns out that there is a correspondence between constructive logic and type theory. They are the same structure and we can switch backward and forward between the two notations because they are the same thing.
51+
52+The way that this works is that a proposition is a type so this,
53+
54+.. code-block:: idris
55+
56+ Idris> 1+1=2
57+ 2 = 2 : Type
58+
59+is 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:
60+
61+
62+.. code-block:: idris
63+
64+ Idris> 1+1=3
65+ 2 = 3 : Type
66+
67+Both 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.
68+A 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
69+
70+.. code-block:: idris
71+
72+ onePlusOne : 1+1=2
73+ onePlusOne = Refl
74+
75+So 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:
76+
77+.. code-block:: idris
78+
79+ Idris> Refl
80+ (input):Can't infer argument A to Refl, Can't infer argument x to Refl
81+
82+So it must pattern match on its return type:
83+
84+.. code-block:: idris
85+
86+ Idris> the (1=1) Refl
87+ Refl : 1 = 1
88+
89+So now that we can represent propositions as types other aspects of propositional logic can also be translated to types as follows:
90+
91++----------+-------------------+--------------------------+
92+| | propositions | example of possible type |
93++----------+-------------------+--------------------------+
94+| A | x=y | |
95++----------+-------------------+--------------------------+
96+| B | y=z | |
97++----------+-------------------+--------------------------+
98+| and | A /\ B | Pair(x=y,y=z) |
99++----------+-------------------+--------------------------+
100+| or | A \/ B | Either(x=y,y=z) |
101++----------+-------------------+--------------------------+
102+| implies | A -> B | (x=y) -> (y=x) |
103++----------+-------------------+--------------------------+
104+| for all | y=z | |
105++----------+-------------------+--------------------------+
106+| exists | y=z | |
107++----------+-------------------+--------------------------+
108+
109+
110+And (conjunction)
111+-----------------
112+
113+We can have a type which corresponds to conjunction:
114+
115+.. code-block:: idris
116+
117+ AndIntro : a -> b -> A a b
118+
119+There is a built in type called 'Pair'.
120+
121+Or (disjunction)
122+----------------
123+
124+We can have a type which corresponds to disjunction:
125+
126+.. code-block:: idris
127+
128+ data Or : Type -> Type -> Type where
129+ OrIntroLeft : a -> A a b
130+ OrIntroRight : b -> A a b
131+
132+There is a built in type called 'Either'.
133+
134+Definitional and Propositional Equalities
135+=========================================
136+
137+We have seen that we can 'prove' a type by finding a way to construct a term. In the case of equality types there is only one constructor which is 'Refl'.
138+We have also seen that each side of the equation does not have to be identical like '2=2'. It is enough that both sides are ``definitionaly equal`` like this:
139+
140+.. code-block:: idris
141+
142+ onePlusOne : 1+1=2
143+ onePlusOne = Refl
144+
145+So both sides of this equation nomalise to 2 and so Refl will type match and the proposition is proved.
146+
147+We don't have to stick to terms, can also use symbolic parameters so the following will compile:
148+
149+.. code-block:: idris
150+
151+ varIdentity : m = m
152+ varIdentity = Refl
153+
154+If a proposition/equality type is not definitionaly equal but is still true then it is ``propositionaly equal``. In this case we may still be able to prove it but some steps in the proof may require us to add something into the terms or at least to take some sideways steps to get to a proof.
155+
156+Especially when working with equalities containing variable terms (inside functions) it can be hard to know which equality types are definitially equal, in this example plusReducesL is '``definitially equal``' but plusReducesR is not (although it is '``propositionaly equal``'). The only difference between them is the order of the operands.
157+
158+.. code-block:: idris
159+
160+ plusReducesL : (n:Nat) -> plus Z n = n
161+ plusReducesL n = Refl
162+
163+ plusReducesR : (n:Nat) -> plus n Z = n
164+ plusReducesR n = Refl
165+
166+plusReducesR gives the following error:
167+
168+
169+.. code-block:: idris
170+
171+ - + Errors (1)
172+ `-- proof.idr line 6 col 17:
173+ When checking right hand side of plusReducesR with expected type
174+ plus n 0 = n
175+
176+ Type mismatch between
177+ n = n (Type of Refl)
178+ and
179+ plus n 0 = n (Expected type)
180+
181+ Specifically:
182+ Type mismatch between
183+ n
184+ and
185+ plus n 0
186+
187+So why is 'Refl' able to prove some equality types but not others?
188+
189+The first answer is that 'plus' is defined in such a way that it splits on its first argument so it is simple to prove when 0 is the first argument but not the second. So what is the general way to know if Refl will work?
190+
191+If an equality type can be proved/constructed by using Refl alone it is known as a ``definitional equality``. In order to be definitinally equal both sides of the equation must normalise to unique values. That is, each step in the proof must reduce the term so each step is effectively forced.
192+
193+So when we type 1+1 in Idris it is immediately converted to 2 because definitional equality is built in.
194+
195+.. code-block:: idris
196+
197+ Idris> 1+1
198+ 2 : Integer
199+
200+In the following pages we discuss how to resolve propositionaly equalies.
201+
202+Axiomatic and Constructive Approaches
203+=====================================
204+
205+How should we define types so that we can do proofs on them? In the natural numbers with plus example we could have started by treating it as a group based on the plus operator. So we have axioms:
206+
207+- for all x,y : ``x+y=y+x``
208+- for all x: ``x + 0 = x = 0 + x``
209+- for all x,y,z: ``(x + y) + z = x + (x + z)``
210+
211+Then we can implement '+' so that it respects these axioms (presumably implemented in hardware).
212+
213+These are axioms, that is a propositions/types that are asserted to be true without proof. In Idris we can use the 'postulate' keyword
214+
215+
216+.. code-block:: idris
217+
218+ commutePlus ``postulate``: x -> y -> plus x y = plus y x
219+
220+Alternatively 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.
221+
222+As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.
223+
224+So what can we learn from this to implement out own types:
225+
226+- Should we try to implement both approaches?
227+- Should we define our types by constructing up from primitive types?
228+
229+Proof theory affects these design decisions.
230+
231+