@@ -1,3 +1,7 @@
1+*******************
2+Background Material
3+*******************
4+
15In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,
26
37- Propositions and judgments
@@ -95,11 +99,11 @@ So now that we can represent propositions as types other aspects of propositiona
9599+----------+-------------------+--------------------------+
96100| B | y=z | |
97101+----------+-------------------+--------------------------+
98−| and | A /\ B | Pair(x=y,y=z) |
102+| and | A /\\ B | ``Pair(x=y,y=z)`` |
99103+----------+-------------------+--------------------------+
100−| or | A \/ B | Either(x=y,y=z) |
104+| or | A \\/ B | ``Either(x=y,y=z)`` |
101105+----------+-------------------+--------------------------+
102−| implies | A -> B | (x=y) -> (y=x) |
106+| implies | A -> B | ``(x=y) -> (y=x)`` |
103107+----------+-------------------+--------------------------+
104108| for all | y=z | |
105109+----------+-------------------+--------------------------+
@@ -126,8 +130,8 @@ We can have a type which corresponds to disjunction:
126130.. code-block:: idris
127131
128132 data Or : Type -> Type -> Type where
129− OrIntroLeft : a -> A a b
130− OrIntroRight : b -> A a b
133+ OrIntroLeft : a -> A a b
134+ OrIntroRight : b -> A a b
131135
132136There is a built in type called 'Either'.
133137
@@ -202,7 +206,7 @@ In the following pages we discuss how to resolve propositionaly equalies.
202206Axiomatic and Constructive Approaches
203207=====================================
204208
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:
209+How should we define types so that we can do proofs on them? In the natural numbers with the plus example we could have started by treating it as a group based on the plus operator. So we have axioms:
206210
207211- for all x,y : ``x+y=y+x``
208212- for all x: ``x + 0 = x = 0 + x``
@@ -215,13 +219,13 @@ These are axioms, that is a propositions/types that are asserted to be true with
215219
216220.. code-block:: idris
217221
218− commutePlus ``postulate``: x -> y -> plus x y = plus y x
222+ postulate commutePlus: (x:Nat) -> (y:Nat) -> plus x y = plus y x
219223
220224Alternatively 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.
221225
222226As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.
223227
224−So what can we learn from this to implement out own types:
228+So what can we learn from this to implement our own types:
225229
226230- Should we try to implement both approaches?
227231- Should we define our types by constructing up from primitive types?