🍃 Error_monad.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Data_encoding.

The encoding [error_encoding] is valid.

Axiom error_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Error_monad.error_encoding.
#[global] Hint Resolve error_encoding_is_valid : Data_encoding_db.

A notion of equality given an equality on values.

Module Eq.
  Definition t {a b : Set} (eq : a → b → Prop) (x1 : M? a) (x2 : M? b) :
    Prop :=
    match x1, x2 with
    | Pervasives.Ok x1, Pervasives.Ok x2 ⇒ eq x1 x2
    | Pervasives.Error error1, Pervasives.Error error2 ⇒ error1 = error2
    | _, _ ⇒ False
    end.
End Eq.

Definition post_when_success {a : Set} (x : M? a) (P : a → Prop) : Prop :=
  match x with
  | Pervasives.Ok v ⇒ P v
  | Pervasives.Error _ ⇒ True
  end.

Lemma post_when_success_bind {a b : Set} (e1 : M? a) (e2 : a → M? b)
  (P1 : a → Prop) (H1 : post_when_success e1 P1) (P2 : b → Prop)
  : (∀ (v1 : a), P1 v1 → post_when_success (e2 v1) P2) →
    post_when_success (let? v1 := e1 in e2 v1) P2.
Proof.
  intro H.
  destruct e1; simpl; trivial.
  now apply H.
Qed.

Definition terminates {A : Set} (x : M? A) : Prop :=
  match x with
  | Pervasives.Error _ ⇒ False
  | Pervasives.Ok _ ⇒ True
  end.

Lemma bind_return_eq {A : Set} (e : M? A) :
  (let? x := e in return? x) =
  e.
Proof.
  now destruct e.
Qed.

Lemma rewrite_bind {A B : Set} (e1 : M? A) (e2 e2' : A → M? B)
  (H : ∀ v, e2 v = e2' v) :
  Error_monad.op_gtgtquestion e1 e2 =
  Error_monad.op_gtgtquestion e1 e2'.
Proof.
  destruct e1; now simpl.
Qed.

Lemma elim_record_trace_eval {A : Set} (mk_error : unit → _error)
  (x : M? A) (v : A)
  : x = return? v →
    record_trace_eval mk_error x = return? v.
Proof.
  intro H; now rewrite H.
Qed.

When adding an error which is not internal, then it can be altogether ignored when check internal errors do not occur.

Lemma letP_Build_extensible_elim {B} {s} {A} {a} {mb : M? B} {P : B → Prop} :
  (List.mem eqb s Error.internal_errors = false) →
  (letP? x := mb in P x ) →
  (letP? x := trace_value (Build_extensible s A a) mb in P x).
Proof.
  Opaque List.mem Error.internal_errors.
  intros H1 H2.
  destruct mb as [res | err] ; [assumption |].
  unfold bind_prop, Error.not_internal, Error.in_ in ×. simpl. rewrite H1.
  assumption.
  Transparent List.mem Error.internal_errors.
Qed.