.. _sect-theorems: ***************Theorem Proving*************** Equality======== Idris allows propositional equalities to be declared, allowing theorems aboutprograms to be stated and proved. An equality type is defined as follows in thePrelude: .. code-block:: idris     data Equal : a -> b -> Type where         Refl : Equal x x As a notational convenience, ``Equal x y`` can be written as ``x = y``.Equalities can be proposed between any values of any types, but the onlyway to construct a proof of equality is if values actually are equal.For example: .. code-block:: idris     fiveIsFive : 5 = 5    fiveIsFive = Refl     twoPlusTwo : 2 + 2 = 4    twoPlusTwo = Refl If we try... .. code-block:: idris     twoPlusTwoBad : 2 + 2 = 5    twoPlusTwoBad = Refl ...then we'll get an error: ::     Proofs.idr:8:17--10:1:While processing right hand side of Main.twoPlusTwoBad at Proofs.idr:8:1--10:1:    When unifying 4 = 4 and (fromInteger 2 + fromInteger 2) = (fromInteger 5)    Mismatch between:            4    and            5 .. _sect-empty: The Empty Type============== There is an empty type, ``Void``, which has no constructors. It is thereforeimpossible to construct a canonical element of the empty type. We can thereforeuse the empty type to prove that something is impossible, for example zero isnever equal to a successor: .. code-block:: idris     disjoint : (n : Nat) -> Z = S n -> Void    disjoint n prf = replace {p = disjointTy} prf ()      where        disjointTy : Nat -> Type        disjointTy Z = ()        disjointTy (S k) = Void Don't worry if you don't get all the details of how this works just yet -essentially, it applies the library function ``replace``, which uses anequality proof to transform a predicate. Here we use it to transform avalue of a type which can exist, the empty tuple, to a value of a typewhich can’t, by using a proof of something which can’t exist. Once we have an element of the empty type, we can prove anything.``void`` is defined in the library, to assist with proofs bycontradiction. .. code-block:: idris     void : Void -> a Proving Theorems================ When type checking dependent types, the type itself gets *normalised*.So imagine we want to prove the following theorem about the reductionbehaviour of ``plus``: .. code-block:: idris     plusReduces : (n:Nat) -> plus Z n = n We’ve written down the statement of the theorem as a type, in just thesame way as we would write the type of a program. In fact there is noreal distinction between proofs and programs. A proof, as far as we areconcerned here, is merely a program with a precise enough type toguarantee a particular property of interest. We won’t go into details here, but the Curry-Howard correspondence [#Timothy]_explains this relationship. The proof itself is immediate, because``plus Z n`` normalises to ``n`` by the definition of ``plus``: .. code-block:: idris     plusReduces n = Refl It is slightly harder if we try the arguments the other way, becauseplus is defined by recursion on its first argument. The proof also worksby recursion on the first argument to ``plus``, namely ``n``. .. code-block:: idris     plusReducesZ : (n:Nat) -> n = plus n Z    plusReducesZ Z = Refl    plusReducesZ (S k) = cong S (plusReducesZ k) ``cong`` is a function defined in the library which states that equalityrespects function application: .. code-block:: idris     cong : (f : t -> u) -> a = b -> f a = f b To see more detail on what's going on, we can replace the recursive call to``plusReducesZ`` with a hole: .. code-block:: idris        plusReducesZ (S k) = cong S ?help Then inspecting the type of the hole at the REPL shows us: ::     Main> :t help       k : Nat    -------------------------------------    help : k = (plus k Z) We can do the same for the reduction behaviour of plus on successors: .. code-block:: idris     plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)    plusReducesS Z m = Refl    plusReducesS (S k) m = cong S (plusReducesS k m) Even for small theorems like these, the proofs are a little tricky toconstruct in one go. When things get even slightly more complicated, itbecomes too much to think about to construct proofs in this “batchmode”. Idris provides interactive editing capabilities, which can help withbuilding proofs. For more details on building proofs interactively inan editor, see :ref:`proofs-index`. .. _sect-parity: Theorems in Practice==================== The need to prove theorems can arise naturally in practice. For example,previously (:ref:`sec-views`) we implemented ``natToBin`` using a function``parity``: .. code-block:: idris     parity : (n:Nat) -> Parity n We provided a definition for ``parity``, but without explanation.  We mighthave hoped that it would look something like the following: .. code-block:: idris     parity : (n:Nat) -> Parity n    parity Z     = Even {n=Z}    parity (S Z) = Odd {n=Z}    parity (S (S k)) with (parity k)      parity (S (S (j + j)))     | Even = Even {n=S j}      parity (S (S (S (j + j)))) | Odd  = Odd {n=S j} Unfortunately, this fails with a type error: ::     With.idr:26:17--27:3:While processing right hand side of Main.with block in 2419 at With.idr:24:3--27:3:    Can't solve constraint between:            plus j (S j)    and            S (plus j j) The problem is that normalising ``S j + S j``, in the type of ``Even``doesn't result in what we need for the type of the right hand side of``Parity``. We know that ``S (S (plus j j))`` is going to be equal to``S j + S j``, but we need to explain it to Idris with a proof. We canbegin by adding some *holes* (see :ref:`sect-holes`) to the definition: .. code-block:: idris     parity : (n:Nat) -> Parity n    parity Z     = Even {n=Z}    parity (S Z) = Odd {n=Z}    parity (S (S k)) with (parity k)      parity (S (S (j + j)))     | Even = let result = Even {n=S j} in                                              ?helpEven      parity (S (S (S (j + j)))) | Odd  = let result = Odd {n=S j} in                                              ?helpOdd Checking the type of ``helpEven`` shows us what we need to prove for the``Even`` case: ::       j : Nat      result : Parity (S (plus j (S j)))    --------------------------------------    helpEven : Parity (S (S (plus j j))) We can therefore write a helper function to *rewrite* the type to the formwe need: .. code-block:: idris     helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))    helpEven j p = rewrite plusSuccRightSucc j j in p The ``rewrite ... in`` syntax allows you to change the required type of anexpression by rewriting it according to an equality proof. Here, we haveused ``plusSuccRightSucc``, which has the following type: .. code-block:: idris     plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right We can see the effect of ``rewrite`` by replacing the right hand side of``helpEven`` with a hole, and working step by step. Beginning with the following: .. code-block:: idris     helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))    helpEven j p = ?helpEven_rhs We can look at the type of ``helpEven_rhs``: .. code-block:: idris       j : Nat      p : Parity (S (plus j (S j)))    --------------------------------------    helpEven_rhs : Parity (S (S (plus j j))) Then we can ``rewrite`` by applying ``plusSuccRightSucc j j``, which givesan equation ``S (j + j) = j + S j``, thus replacing ``S (j + j)`` (or,in this case, ``S (plus j j)`` since ``S (j + j)`` reduces to that) in thetype with ``j + S j``: .. code-block:: idris     helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))    helpEven j p = rewrite plusSuccRightSucc j j in ?helpEven_rhs Checking the type of ``helpEven_rhs`` now shows what has happened, includingthe type of the equation we just used (as the type of ``_rewrite_rule``): .. code-block:: idris     Main> :t helpEven_rhs       j : Nat       p : Parity (S (plus j (S j)))    -------------------------------------    helpEven_rhs : Parity (S (plus j (S j))) Using ``rewrite`` and another helper for the ``Odd`` case, we can complete``parity`` as follows: .. code-block:: idris     helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))    helpEven j p = rewrite plusSuccRightSucc j j in p     helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))    helpOdd j p = rewrite plusSuccRightSucc j j in p     parity : (n:Nat) -> Parity n    parity Z     = Even {n=Z}    parity (S Z) = Odd {n=Z}    parity (S (S k)) with (parity k)      parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})      parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j}) Full details of ``rewrite`` are beyond the scope of this introductory tutorial,but it is covered in the theorem proving tutorial (see :ref:`proofs-index`). .. _sect-totality: Totality Checking================= If we really want to trust our proofs, it is important that they aredefined by *total* functions — that is, a function which is defined forall possible inputs and is guaranteed to terminate. Otherwise we couldconstruct an element of the empty type, from which we could proveanything: .. code-block:: idris     -- making use of 'hd' being partially defined    empty1 : Void    empty1 = hd [] where        hd : List a -> a        hd (x :: xs) = x     -- not terminating    empty2 : Void    empty2 = empty2 Internally, Idris checks every definition for totality, and we can check atthe prompt with the ``:total`` command. We see that neither of the abovedefinitions is total: ::     Void> :total empty1    Void.empty1 is not covering due to call to function empty1:hd    Void> :total empty2    Void.empty2 is possibly not terminating due to recursive path Void.empty2 Note the use of the word “possibly” — a totality check can never be certain dueto the undecidability of the halting problem. The check is, therefore,conservative. It is also possible (and indeed advisable, in the case of proofs)to mark functions as total so that it will be a compile time error for thetotality check to fail: .. code-block:: idris     total empty2 : Void    empty2 = empty2 Reassuringly, our proof in Section :ref:`sect-empty` that the zero andsuccessor constructors are disjoint is total: .. code-block:: idris     Main> :total disjoint    Main.disjoint is Total The totality check is, necessarily, conservative. To be recorded astotal, a function ``f`` must: -  Cover all possible inputs -  Be *well-founded* — i.e. by the time a sequence of (possibly   mutually) recursive calls reaches ``f`` again, it must be possible to   show that one of its arguments has decreased. -  Not use any data types which are not *strictly positive* -  Not call any non-total functions Directives and Compiler Flags for Totality------------------------------------------ [NOTE: Not all of this is implemented yet for Idris 2] By default, Idris allows all well-typed definitions, whether total or not.However, it is desirable for functions to be total as far as possible, as thisprovides a guarantee that they provide a result for all possible inputs, infinite time. It is possible to make total functions a requirement, either: -  By using the ``--total`` compiler flag. -  By adding a ``%default total`` directive to a source file. All   definitions after this will be required to be total, unless   explicitly flagged as ``partial``. All functions *after* a ``%default total`` declaration are required tobe total. Correspondingly, after a ``%default partial`` declaration, therequirement is relaxed. Finally, the compiler flag ``--warnpartial`` causes to print a warningfor any undeclared partial function. Totality checking issues------------------------ Please note that the totality checker is not perfect! Firstly, it isnecessarily conservative due to the undecidability of the haltingproblem, so many programs which *are* total will not be detected assuch. Secondly, the current implementation has had limited effort putinto it so far, so there may still be cases where it believes a functionis total which is not. Do not rely on it for your proofs yet! Hints for totality------------------ In cases where you believe a program is total, but Idris does not agree, it ispossible to give hints to the checker to give more detail for a terminationargument. The checker works by ensuring that all chains of recursive callseventually lead to one of the arguments decreasing towards a base case, butsometimes this is hard to spot. For example, the following definition cannot bechecked as ``total`` because the checker cannot decide that ``filter (< x) xs``will always be smaller than ``(x :: xs)``: .. code-block:: idris     qsort : Ord a => List a -> List a    qsort [] = []    qsort (x :: xs)       = qsort (filter (< x) xs) ++          (x :: qsort (filter (>= x) xs)) The function ``assert_smaller``, defined in the prelude, is intended toaddress this problem: .. code-block:: idris     assert_smaller : a -> a -> a    assert_smaller x y = y It simply evaluates to its second argument, but also asserts to thetotality checker that ``y`` is structurally smaller than ``x``. This canbe used to explain the reasoning for totality if the checker cannot workit out itself. The above example can now be written as: .. code-block:: idris     total    qsort : Ord a => List a -> List a    qsort [] = []    qsort (x :: xs)       = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++          (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))) The expression ``assert_smaller (x :: xs) (filter (<= x) xs)`` assertsthat the result of the filter will always be smaller than the pattern``(x :: xs)``. In more extreme cases, the function ``assert_total`` marks asubexpression as always being total: .. code-block:: idris     assert_total : a -> a    assert_total x = x In general, this function should be avoided, but it can be very usefulwhen reasoning about primitives or externally defined functions (forexample from a C library) where totality can be shown by an externalargument.  .. [#Timothy] Timothy G. Griffin. 1989. A formulae-as-type notion of       control. In Proceedings of the 17th ACM SIGPLAN-SIGACT       symposium on Principles of programming languages (POPL       '90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714       http://doi.acm.org/10.1145/96709.96714