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)


Require Import List.

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.
Section OptionHelpers.
  Variable A : Type.
  Variable B : Type.

true iff exists a, oa = Some a false iff oa = None.
  Definition isSome (oa:option A) : bool :=
    match oa with
    | Some _ => true
    | None => false
    end.

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.

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.

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.

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.