git.iko.soy/Idris-dev
on master help sign in
Move total annotation in proof description
f5aea00Edwin Brady
docs/proofs/patterns.rst+12−17
compare with master
unifiedsplit
@@ -33,22 +33,14 @@ declaration:
33
33
34.. code-block:: idris
34.. code-block:: idris
35
35
36− total
37 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
36 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
38
37
39−The ``total`` annotation means that we aim to write a function which
40−passes the totality checker; i.e. it will terminate on all possible
41−well-typed inputs. This is important for proofs, since it provides a
42−guarantee that the proof is valid in *all* cases, not just those for
43−which it happens to be well-defined.
44−
45−To create a template definition for the proof, press ``\d`` the
38+To create a template definition for the proof, press ``\d`` (or the
46equivalent in your editor of choice) on the line with the type
39equivalent in your editor of choice) on the line with the type
47declaration. You should see:
40declaration. You should see:
48
41
49.. code-block:: idris
42.. code-block:: idris
50
43
51− total
52 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
44 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
53 plus_commutes n m = ?plus_commutes_rhs
45 plus_commutes n m = ?plus_commutes_rhs
54
46
@@ -59,7 +51,6 @@ should see:
59
51
60.. code-block:: idris
52.. code-block:: idris
61
53
62− total
63 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
54 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
64 plus_commutes Z m = ?plus_commutes_rhs_1
55 plus_commutes Z m = ?plus_commutes_rhs_1
65 plus_commutes (S k) m = ?plus_commutes_rhs_2
56 plus_commutes (S k) m = ?plus_commutes_rhs_2
@@ -91,7 +82,6 @@ It is a good idea to give these slightly more meaningful names:
91
82
92.. code-block:: idris
83.. code-block:: idris
93
84
94− total
95 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
85 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
96 plus_commutes Z m = ?plus_commutes_Z
86 plus_commutes Z m = ?plus_commutes_Z
97 plus_commutes (S k) m = ?plus_commutes_S
87 plus_commutes (S k) m = ?plus_commutes_S
@@ -107,7 +97,6 @@ yields:
107
97
108 plus_commutes_Z : m = plus m 0
98 plus_commutes_Z : m = plus m 0
109
99
110− total
111 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
100 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
112 plus_commutes Z m = plus_commutes_Z
101 plus_commutes Z m = plus_commutes_Z
113 plus_commutes (S k) m = ?plus_commutes_S
102 plus_commutes (S k) m = ?plus_commutes_S
@@ -280,7 +269,6 @@ state:
280
269
281.. code-block:: idris
270.. code-block:: idris
282
271
283− total
284 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
272 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
285 plus_commutes Z m = plus_commutes_Z
273 plus_commutes Z m = plus_commutes_Z
286 plus_commutes (S k) m = ?plus_commutes_S
274 plus_commutes (S k) m = ?plus_commutes_S
@@ -301,7 +289,6 @@ follows:
301
289
302.. code-block:: idris
290.. code-block:: idris
303
291
304− total
305 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
292 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
306 plus_commutes Z m = plus_commutes_Z
293 plus_commutes Z m = plus_commutes_Z
307 plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S
294 plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S
@@ -340,13 +327,21 @@ defined by matching on its first argument. The complete definition is:
340
327
341.. code-block:: idris
328.. code-block:: idris
342
329
330+ total
343 plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
331 plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
344 plus_commutes_S k Z = Refl
332 plus_commutes_S k Z = Refl
345 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
333 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
346
334
347−All metavariables have now been solved, and ``plus_commutes`` has a
335+All metavariables have now been solved,
336+
337+The ``total`` annotation means that we require the final function to
338+pass the totality checker; i.e. it will terminate on all possible
339+well-typed inputs. This is important for proofs, since it provides a
340+guarantee that the proof is valid in *all* cases, not just those for
341+which it happens to be well-defined.
342+
348−``total`` annotation, so we have completed the proof of commutativity of
343+Now that ``plus_commutes`` has a ``total`` annotation, we have completed the
349−addition on natural numbers.
344+proof of commutativity of addition on natural numbers.
350
345
351.. [1]
346.. [1]
352 Note that the left and right hand sides of the equality have been
347 Note that the left and right hand sides of the equality have been