💥 Error.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
[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 e ⇒ Error.not_internal e
end.
End No_internal_errors.
Definition t {a : Set} (x : M? a) : Prop :=
match x with
| Pervasives.Ok _ ⇒ True
| Pervasives.Error e ⇒ Error.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.
(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.
(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.
[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.
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.
(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.
(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.
(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]
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.
(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