Skip to main content

💥 Error.v

Proofs

Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.

[intros] + [Tactics.destruct_pairs] @Q not sure it should be here @TODO move
Ltac i_des_pairs := intros ; Tactics.destruct_pairs.

[No_internal_errors.t term] ensures that [term] does *not* reduce to any of the errors in the error list [internal_errors] which is local to this module.
Module No_internal_errors.
  Definition t {a : Set} (x : M? a) : Prop :=
    match x with
    | Pervasives.Ok _True
    | Pervasives.Error eError.not_internal e
    end.
End No_internal_errors.

Splitting the verification of internal errors for the operator [let?].
Lemma no_internal_errors_let {a b}
  (x : M? a) (f : a M? b) :
  No_internal_errors.t x
  ( x, No_internal_errors.t (f x))
  No_internal_errors.t (let? v := x in f v).
Proof.
  intros Hx Hf.
  now destruct x; simpl.
Qed.

Ltac no_internal_errors_lets :=
  match goal with
  | [ |- _, _ ] ⇒ intro; no_internal_errors_lets
  | _
      Tactics.destruct_pairs; (try exact I);
      try (apply Error.no_internal_errors_let;
           no_internal_errors_lets)
  end.

Split the verification of a [letP?] into two parts.
Lemma split_letP {a b : Set}
  (x : M? a) (f : a M? b) (P : a Prop) (Q : b Prop) :
  (letP? x := x in P x)
  ( x, P x letP? y := f x in Q y)
  letP? y := (let? x := x in f x) in Q y.
Proof.
  sauto lq: on.
Qed.

Useful tactics. This module can be imported.
Module Tactics_letP.
[intros] + [Tactics.destruct_pairs] @TODO perhaps move
  Ltac i_des_pairs := intros ; Tactics.destruct_pairs.

  Ltac esplit_letP := eapply split_letP.

  Ltac iesplit_letP := i_des_pairs ; eapply split_letP.
End Tactics_letP.

Split the verification of a [letP?] into two parts for the case of a standard [let].
Lemma split_letP_let {a b : Set}
  (x : a) (f : a M? b) (P : a Prop) (Q : b Prop) :
  P x
  ( x, P x letP? y := f x in Q y)
  letP? y := (let x := x in f x) in Q y.
Proof.
  sauto lq: on.
Qed.

Split the verification of a [letP?] into two parts.
Lemma follow_letP {a : Set}
  (x : M? a) (P : a Prop) (Q : a Prop) :
  ( x, P x Q x)
  (letP? x := x in P x)
  letP? x := x in Q x.
Proof.
  intros.
  destruct x eqn:E; simpl in *; [apply H|]; trivial.
Qed.

A version of [split_letP] with a trivial precondition.
Lemma split_letP_triv {a b : Set}
  (x : M? a) (f : a M? b) (Q : b Prop) :
  (letP? x := x in True)
  ( x, letP? y := f x in Q y)
  letP? y := (let? x := x in f x) in Q y.
Proof.
  intros Hx Hf.
  apply (split_letP _ _ (fun _True)); [exact Hx|].
  intros; apply Hf.
Qed.

[split_error_with lemma] applies [Error.split_letP] and solve the first subgoal with [now apply lemma]
Ltac split_error_with lemma :=
  eapply Error.split_letP; [now apply lemma|intros].

A lemma to get around rewriting under a [let?]
Lemma let_ext {a b : Set} (x y : M? a)
  (f g : a M? b) :
  x = y
  ( x, f x = g x)
  (let? x := x in f x) =
  (let? y := y in g y).
Proof.
  intros Hxy Hfg.
  rewrite Hxy.
  destruct y.
  { simpl. apply Hfg. }
  { reflexivity. }
Qed.

Eliminate an error case by using an [_is_valid] lemma
Lemma is_valid_impl_not_internal {a : Set} (x : M? a) (Q : a Prop) e
  (H_is_valid : letP? y := x in Q y) :
  x = Pervasives.Error e
  Error.not_internal e.
Proof.
  unfold bind_prop. intros H_eq.
  rewrite H_eq in ×. easy.
Qed.