🍃 Option.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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 v ⇒ P v
| None ⇒ True
end.
match x with
| Some v ⇒ P v
| None ⇒ True
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 v ⇒ P v
| None ⇒ True
end.
Definition terminates {A : Set} (x : M× A) : Prop :=
match x with
| None ⇒ False
| 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 v ⇒ e2 (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.
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 v ⇒ P v
| None ⇒ True
end.
Definition terminates {A : Set} (x : M× A) : Prop :=
match x with
| None ⇒ False
| 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 v ⇒ e2 (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).
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.
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.
(∀ 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.
(∀ 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.
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.
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.
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].