``` ```

# Module with helper notation for writing partial functions

(** version 1.0
``` ```
 Each function that might not terminate, takes as an extra argument a maximum recursion depth, and returns a "result" type (kind of "option")
``` Inductive res (A : Set) : Set :=   | Ok : A -> res A   | Timeout : res A . Implicit Arguments Ok [A]. Hint Constructors res. ```
 To return directly a value write "Ok v"
``` ```
 To extract the returned value from a subcomputation `e` write ``` var <- e ; rest ``` `var` is a variable bound in `rest` to the value of `e` If `e` terminates with a `Timeout` then the whole thing yields `Timeout`
``` Notation "var <- e ; rest" :=       (match e with        | Ok x => (fun var => rest) x        | Timeout => Timeout _ end)       (at level 60, right associativity) . ```
 Like the above but when the type is `Prop`. When the subcomputation yields `Timeout` this yields `True` (appropriate for partial correctness proofs)
``` Notation "var <-- e ; rest" :=       (match e with        | Ok x => (fun var => rest) x        | Timeout => True end)       (at level 80, right associativity) . ```
 Now a notation to do the top-level pattern matching on the `depth` argument Write ``` timeout depth in body ``` when you want to first timeout if depth is 0 or else evaluate body with a smaller depth. `depth` is bound in `body`.
``` Notation "'timeout' depth 'in' body" :=     (match depth with        O => Timeout _      | S depth => body     end)     (at level 80) . ```
 A tactic to clean up after functional induction on functions using Timeout
``` Ltac indhyp :=   repeat match goal with    | [ H : (Ok _ = Ok _) |- _ ] => inversion H; clear H; subst    | [ H : (Ok _ = Timeout _) |- _ ] => discriminate H    | [ H : (Timeout _ = Ok _) |- _ ] => discriminate H ```
 We get rid of all instances of recursive invocations. For each one it seems that the function induction adds a hypothesis "rec invoc" = Ok _
```    | [ H1 : (?E = Ok _) ,        H2 : context[?E] |- _ ] => rewrite H1 in H2    | [ H1 : (?E = Ok _) |- context[?E] ] => rewrite H1    | [ H1 : (?E = Timeout _) ,        H2 : context[?E] |- _ ] => rewrite H1 in H2    | [ H1 : (?E = Timeout _) |- context[?E] ] => rewrite H1   end.    ```

## EXAMPLE

``` Section Example. ```
 A function that computes div2 for even numbers and loops for odd numbers
```   Fixpoint pdiv2 (n: nat) (depth: nat) { struct depth } : res nat :=     timeout depth in     match n with      | O => Ok O      | S O => pdiv2 n depth      | S (S n) => d <- pdiv2 n depth ;                   Ok (1 + d)     end.     ```
 Pdiv2 correctness: if the function terminates then it computes div2
```    ```
 Hint for using functional induction: the statement should refer to pdiv2 only applied to two universal quantified variables
```      Theorem pdiv2_correct: forall (n depth: nat), d <-- pdiv2 n depth ;                                                 n = d + d.    ```
 Total correctness: the function terminates for all even numbers. There is is no free lunch here. We must define the domain of the function.
```   Inductive isEven : nat -> Prop :=     | eO : isEven O     | eSS : forall n : nat, isEven n -> isEven (S (S n))   .      Theorem pdiv2_correct2: forall (n : nat), isEven n ->                                             exists depth : nat ,                                             pdiv2 n depth <> Timeout nat.       ```
 Total correctness: the function does not terminate for all odd numbers
```   Theorem pdiv2_correct3: forall (n : nat), isEven (S n) ->                                               forall (depth : nat) ,                                               pdiv2 n depth = Timeout nat. End Example.    ```

## History

``` ```
 version 1.0 (Oct 21, 2006). First version.
``` ```
Index