Library OptionHelpers
This file is part of
A Formal Definition of JML in Coq
and its Application to Runtime Assertion Checking
Ph.D. Thesis by Hermann Lehner
Online available at jmlcoq.info
Authors:
- Hermann Lehner
- David Pichardie (Bicolano)
- Andreas Kaegi (Syntax Rewritings, Implementation of ADTs)
Helper functions to work with option types:
- isSome : option A -> bool.
- optionMap : (A->B) -> option A -> option B.
- option2list : option A -> list A.
- optionList2list : list (option A) -> list A.
true iff exists a, oa = Some a
false iff oa = None.
a iff oa = Some a,
nil iff oa = None
Definition option2list (ox:option A) : list A :=
match ox with
| None => nil
| Some x => x :: nil
end.
match ox with
| None => nil
| Some x => x :: nil
end.
Map function f over a value of type option A.
Definition optionMap (f:A->B) (ox:option A) : option B :=
match ox with
| None => None
| Some x => Some (f x)
end.
match ox with
| None => None
| Some x => Some (f x)
end.
Extract all Some-values from the given list of option A-values
and return them as a list of A-values.
Fixpoint optionList2list (l:list (option A)) : list A :=
match l with
| nil => nil
| (Some x)::xs => x::(optionList2list xs)
| None::xs => optionList2list xs
end.
End OptionHelpers.
Implicit Arguments option2list [A].
Implicit Arguments optionMap [A B].
Implicit Arguments optionList2list [A].
Section Proofs.
Variable A : Type.
match l with
| nil => nil
| (Some x)::xs => x::(optionList2list xs)
| None::xs => optionList2list xs
end.
End OptionHelpers.
Implicit Arguments option2list [A].
Implicit Arguments optionMap [A B].
Implicit Arguments optionList2list [A].
Section Proofs.
Variable A : Type.
optionList2list retains all non-None elements of the given list l.
Lemma optionList2list_In : forall (x:A) (l:list (option A)),
In x (optionList2list l) <-> In (Some x) l.
Proof.
intros x l.
induction l.
simpl.
intuition.
case a.
intro a0.
simpl.
intuition.
left.
rewrite H2.
reflexivity.
left.
injection H2.
intro; assumption.
simpl.
intuition.
discriminate H2.
Qed.
End Proofs.
In x (optionList2list l) <-> In (Some x) l.
Proof.
intros x l.
induction l.
simpl.
intuition.
case a.
intro a0.
simpl.
intuition.
left.
rewrite H2.
reflexivity.
left.
injection H2.
intro; assumption.
simpl.
intuition.
discriminate H2.
Qed.
End Proofs.