Library lib.Nonterm


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
This page has been generated by coqdoc