@@ -1,3 +1,7 @@
1In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,
5In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,
3- Propositions and judgments
7- Propositions and judgments
@@ -95,11 +99,11 @@ So now that we can represent propositions as types other aspects of propositiona
95+----------+-------------------+--------------------------+
99+----------+-------------------+--------------------------+
96| B | y=z | |
100| B | y=z | |
97+----------+-------------------+--------------------------+
101+----------+-------------------+--------------------------+
98−| and | A /\ B | Pair(x=y,y=z) |
102+| and | A /\\ B | ``Pair(x=y,y=z)`` |
99+----------+-------------------+--------------------------+
103+----------+-------------------+--------------------------+
100−| or | A \/ B | Either(x=y,y=z) |
104+| or | A \\/ B | ``Either(x=y,y=z)`` |
101+----------+-------------------+--------------------------+
105+----------+-------------------+--------------------------+
102−| implies | A -> B | (x=y) -> (y=x) |
106+| implies | A -> B | ``(x=y) -> (y=x)`` |
103+----------+-------------------+--------------------------+
107+----------+-------------------+--------------------------+
104| for all | y=z | |
108| for all | y=z | |
105+----------+-------------------+--------------------------+
109+----------+-------------------+--------------------------+
@@ -126,8 +130,8 @@ We can have a type which corresponds to disjunction:
126.. code-block:: idris
130.. code-block:: idris
128 data Or : Type -> Type -> Type where
132 data Or : Type -> Type -> Type where
129− OrIntroLeft : a -> A a b
133+ OrIntroLeft : a -> A a b
130− OrIntroRight : b -> A a b
134+ OrIntroRight : b -> A a b
132There is a built in type called 'Either'.
136There is a built in type called 'Either'.
@@ -202,7 +206,7 @@ In the following pages we discuss how to resolve propositionaly equalies.
202Axiomatic and Constructive Approaches
206Axiomatic and Constructive Approaches
203=====================================
207=====================================
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:
207- for all x,y : ``x+y=y+x``
211- for all x,y : ``x+y=y+x``
208- for all x: ``x + 0 = x = 0 + x``
212- 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
216.. code-block:: idris
220.. code-block:: idris
218− commutePlus ``postulate``: x -> y -> plus x y = plus y x
222+ postulate commutePlus: (x:Nat) -> (y:Nat) -> plus x y = plus y x
220Alternatively 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.
224Alternatively 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.
222As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.
226As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.
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:
226- Should we try to implement both approaches?
230- Should we try to implement both approaches?
227- Should we define our types by constructing up from primitive types?
231- Should we define our types by constructing up from primitive types?