Proofs

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 x2eq x1 x2
| Pervasives.Error error1, Pervasives.Error error2error1 = error2
| _, _False
end.
End Eq.

Definition post_when_success {a : Set} (x : M? a) (P : a Prop) : Prop :=
match x with
| Pervasives.Ok vP 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 =
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.