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 |
|