Skip to main content

🍃 Option.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.

Like [List.Forall] but for the option type.
Definition Forall {a : Set} (P : a Prop) (x : option a) : Prop :=
  match x with
  | Some vP v
  | NoneTrue
  end.

When the predicate is always [True] then [Forall] is true.
Lemma Forall_True {a : Set} (x : option a) :
  Forall (fun _True) x.
Proof.
  now destruct x.
Qed.

Definition post_when_success {a : Set} (x : option a) (P : a Prop) : Prop :=
  match x with
  | Some vP v
  | NoneTrue
  end.

Definition terminates {A : Set} (x : M× A) : Prop :=
  match x with
  | NoneFalse
  | Some _True
  end.

Lemma bind_return {A : Set} (e : M× A) :
  (let× x := e in return× x) =
  e.
  now destruct e.
Qed.

Lemma rewrite_bind_left {A A' B : Set}
  (e1 : M× A) (e1' : M× A') (f : A A') (e2 : A' M× B)
  (H_e1 : (let× v := e1 in return× f v) = e1') :
  Option.bind e1 (fun ve2 (f v)) =
  Option.bind e1' e2.
  destruct e1; simpl in *; now rewrite <- H_e1.
Qed.

Lemma rewrite_bind_right {A B : Set} (e1 : M× A) (e2 e2' : A M× B)
  (H : v, e2 v = e2' v) :
  Option.bind e1 e2 =
  Option.bind e1 e2'.
  destruct e1; now simpl.
Qed.

Axiom: if [catch None f] returns [Some]thing, then [f] didn't raise any error.
Axiom catch_error_some : {A : Set} {f : unit A} (v v0 : A),
  Option.catch None f = Some v f tt = v ( exn,
  f tt Pervasives.raise exn).

Axiom: if [catch None f] returns [None], then [f] raised some error.
Axiom catch_error_none: {A : Set} (f : unit A),
  Option.catch None f = None exn, f tt = Pervasives.raise exn.

Lemma (converse of Axiom [catch_error_some]): if [f] didn't raise any error, then [catch None f] returns [Some (f tt)]
Lemma catch_error_some_inversion {A : Set} (f : unit A) :
( exn,
f tt Pervasives.raise exn) Option.catch None f = Some (f tt).
Proof.
  intros H.
  destruct (Option.catch None f) as [v0 |] eqn:eq_v0.
  { apply catch_error_some in eq_v0 ; [| assumption ].
    destruct eq_v0 as [Hv0 ?]. rewrite Hv0. reflexivity. }
  { exfalso.
    apply catch_error_none in eq_v0. destruct eq_v0 as [exn Hexn].
    unfold "~" in H. apply (H exn). assumption.
  }
Qed.

Lemma (another converse of Axiom [catch_error_some]): if [f] didn't raise any error, then [catch None f] has returned [Some]thing. This lemma may be useful if one has [Option.catch None f = Some v], but the unification [f tt] and [v] is not trivial.
Lemma catch_error_some_inversion_ex {A : Set} (f : unit A) :
( exn,
f tt Pervasives.raise exn) v, Option.catch None f = Some v.
Proof.
  intros H.
  destruct (Option.catch None f) as [v0 |] eqn:eq_v0 ; [ v0 ; reflexivity |].
  apply catch_error_none in eq_v0. destruct eq_v0 as [exn Hexn].
  exfalso.
  specialize (H exn) as H0.
  apply H0.
  assumption.
Qed.

Lemma (converse of [catch_error_none]): if [f] has raised an error, then [catch None f] returns [None].
Lemma catch_error_none_inversion {A : Set} (f : unit A) exn :
  f tt = V0.Pervasives.raise exn Option.catch None f = None.
Proof.
  intros H.
  destruct (Option.catch None f) as [v0 |] eqn:H_v0 ; [| reflexivity].
  exfalso.
  apply catch_error_some in H_v0 ; [| exact v0].
  destruct H_v0 as [H1 H2].
  specialize (H2 exn) as H20.
  apply H20.
  assumption.
Qed.

Special case of axiom [catch_error_some]: [Option.catch] runs [f] and returns [None] if [f] raises an exception. Thus, [Option.catch = Some a} implies that [a = f ()].
Lemma catch_some_eq {A : Set} (f : unit A) (a : A) :
  Option.catch None f = Some a a = f tt.
Proof.
  intros.
  assert (Himp :
    (f tt = a) ( exn, f tt Pervasives.raise exn) a = f tt).
  { intros H0. destruct H0. symmetry. assumption. }
  apply Himp.
  apply catch_error_some ; assumption.
Qed.

Special case of [catch_error_none_inversion]. Catching exceptions from a [raise] instruction returns [None].
Lemma catch_raise {A : Set} (exn : extensible_type) :
  Option.catch (a := A) None (fun _Pervasives.raise exn) = None.
Proof.
  apply catch_error_none_inversion with (exn0 := exn).
  reflexivity.
Qed.

When there are no errors we can return the result. This axiom is to be applied carefully so that one makes sure that there are indeed no axioms exiting in the function [f].

Another possibility would be to specify that valid values of each verified

type cannot be equal to [raise exn] for any [exn]. Then, [catch_no_errors] could be discarded.
Axiom catch_no_errors : {A : Set} (f : unit A),
  Option.catch (a := A) None f = Some (f tt).