🎲 Sampler.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Sampler.
Module Make.
Import FallbackArray.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Sampler.
Module Make.
Import FallbackArray.
Validity predicate for [Make.array_encoding_is_valid].
Module Valid.
Record t {A : Set} (x : FallbackArray.t A) : Prop := {
fallback_make : Forall (fun y ⇒ y = x.(t.default)) x.(t.items);
perv_int : Pervasives.Int31.Valid.non_negative
(Z.of_nat (Datatypes.length x.(t.items))); }.
End Valid.
Record t {A : Set} (x : FallbackArray.t A) : Prop := {
fallback_make : Forall (fun y ⇒ y = x.(t.default)) x.(t.items);
perv_int : Pervasives.Int31.Valid.non_negative
(Z.of_nat (Datatypes.length x.(t.items))); }.
End Valid.
Auxiliary lemma, we use it in [fallbackArray_make_default]
Lemma mk_items_default {a : Set} : ∀ (default : a) items,
Pervasives.Int.Valid.non_negative (Z.of_nat (Datatypes.length items)) →
Forall (fun y : a ⇒ y = default) items →
mk_items (Z.to_nat (List.length items)) default = items.
Proof.
intros default items H H_Length.
induction items; intros; [sfirstorder|].
assert (H' : Forall (fun y : a ⇒ y = default) (a0 :: items)) by scongruence.
specialize (Forall_inv_tail H') as H''; apply Forall_inv in H'.
rewrite List.length_eq, Pervasives.normalize_identity, Nat2Z.id; trivial;
simpl in ×.
assert (Y : Pervasives.Int.Valid.non_negative
(Z.of_nat (Datatypes.length items))) by lia.
apply IHitems in Y; [|trivial].
rewrite List.length_eq, Pervasives.normalize_identity,
Nat2Z.id in Y; [|lia]. rewrite H'. f_equal. scongruence.
Qed.
Pervasives.Int.Valid.non_negative (Z.of_nat (Datatypes.length items)) →
Forall (fun y : a ⇒ y = default) items →
mk_items (Z.to_nat (List.length items)) default = items.
Proof.
intros default items H H_Length.
induction items; intros; [sfirstorder|].
assert (H' : Forall (fun y : a ⇒ y = default) (a0 :: items)) by scongruence.
specialize (Forall_inv_tail H') as H''; apply Forall_inv in H'.
rewrite List.length_eq, Pervasives.normalize_identity, Nat2Z.id; trivial;
simpl in ×.
assert (Y : Pervasives.Int.Valid.non_negative
(Z.of_nat (Datatypes.length items))) by lia.
apply IHitems in Y; [|trivial].
rewrite List.length_eq, Pervasives.normalize_identity,
Nat2Z.id in Y; [|lia]. rewrite H'. f_equal. scongruence.
Qed.
Auxiliary lemma, we use it in [array_encoding_is_valid]
Lemma fallbackArray_make_default {a : Set} : ∀ (default : a) items,
Pervasives.Int.Valid.non_negative (Z.of_nat (Datatypes.length items)) →
Forall (fun y : a ⇒ y =
{| t.items := items; t.default := default |}.(t.default))
{| t.items := items; t.default := default |}.(t.items) →
make (length {| t.items := items; t.default := default |}) default =
{| t.items := items; t.default := default |}.
Proof.
intros default items H.
unfold make. pose proof mk_items_default default items H.
assert
(Y : {| t.items := items; t.default := default |}.(t.items) = items)
by scongruence.
assert
(Y' : {| t.items := items; t.default := default |}.(t.default) = default)
by scongruence.
rewrite Y, Y'.
hauto lq: on rew: off.
Qed.
Pervasives.Int.Valid.non_negative (Z.of_nat (Datatypes.length items)) →
Forall (fun y : a ⇒ y =
{| t.items := items; t.default := default |}.(t.default))
{| t.items := items; t.default := default |}.(t.items) →
make (length {| t.items := items; t.default := default |}) default =
{| t.items := items; t.default := default |}.
Proof.
intros default items H.
unfold make. pose proof mk_items_default default items H.
assert
(Y : {| t.items := items; t.default := default |}.(t.items) = items)
by scongruence.
assert
(Y' : {| t.items := items; t.default := default |}.(t.default) = default)
by scongruence.
rewrite Y, Y'.
hauto lq: on rew: off.
Qed.
Encoding [array_encoding] is valid.
Lemma array_encoding_is_valid `{Sampler.Make.FArgs} {A : Set} :
∀ (venc : Data_encoding.t A), Data_encoding.Valid.t (fun _ ⇒ True) venc →
Data_encoding.Valid.t Valid.t (Sampler.Make.array_encoding venc).
Proof.
intros; Data_encoding.Valid.data_encoding_auto.
intros ? H1; repeat split; [destruct H1; unfold length;
rewrite List.length_eq; lia..| |].
{ sauto lq: on use: fallbackArray_make_default. }
{ apply fallbackArray_make_default; destruct H1; lia; apply H1. }
Qed.
#[global] Hint Resolve array_encoding_is_valid : Data_encoding_db.
Module MassArray.
Module Valid.
∀ (venc : Data_encoding.t A), Data_encoding.Valid.t (fun _ ⇒ True) venc →
Data_encoding.Valid.t Valid.t (Sampler.Make.array_encoding venc).
Proof.
intros; Data_encoding.Valid.data_encoding_auto.
intros ? H1; repeat split; [destruct H1; unfold length;
rewrite List.length_eq; lia..| |].
{ sauto lq: on use: fallbackArray_make_default. }
{ apply fallbackArray_make_default; destruct H1; lia; apply H1. }
Qed.
#[global] Hint Resolve array_encoding_is_valid : Data_encoding_db.
Module MassArray.
Module Valid.
Validity predicate for [mass_array_encoding_is_valid].
Record t `{Sampler.Make.FArgs} {A : Set}
(x : t Sampler.Make.Mass.(Sampler.SMass.t)) := {
non_negative : Pervasives.Int31.Valid.non_negative
(Z.of_nat (Datatypes.length x.(t.items)));
forall_default : Forall (fun y ⇒ y = x.(t.default)) x.(t.items); }.
End Valid.
(x : t Sampler.Make.Mass.(Sampler.SMass.t)) := {
non_negative : Pervasives.Int31.Valid.non_negative
(Z.of_nat (Datatypes.length x.(t.items)));
forall_default : Forall (fun y ⇒ y = x.(t.default)) x.(t.items); }.
End Valid.
Encoding [mass_array_encoding] is valid.
Lemma mass_array_encoding_is_valid `{Sampler.Make.FArgs} {A : Set} :
Data_encoding.Valid.t (fun _ ⇒ True)
Sampler.Make.Mass.(Sampler.SMass.encoding) →
Data_encoding.Valid.t (Valid.t (A:=A)) Sampler.Make.mass_array_encoding.
Proof.
intros; Data_encoding.Valid.data_encoding_auto. intros ? H1.
repeat split; [destruct H1; unfold length;
rewrite List.length_eq; lia..|hauto l: on|].
apply fallbackArray_make_default; destruct H1; lia; apply H1.
Qed.
#[global] Hint Resolve mass_array_encoding_is_valid : Data_encoding_db.
End MassArray.
Module Int_Array_Encoding.
Module Valid.
Data_encoding.Valid.t (fun _ ⇒ True)
Sampler.Make.Mass.(Sampler.SMass.encoding) →
Data_encoding.Valid.t (Valid.t (A:=A)) Sampler.Make.mass_array_encoding.
Proof.
intros; Data_encoding.Valid.data_encoding_auto. intros ? H1.
repeat split; [destruct H1; unfold length;
rewrite List.length_eq; lia..|hauto l: on|].
apply fallbackArray_make_default; destruct H1; lia; apply H1.
Qed.
#[global] Hint Resolve mass_array_encoding_is_valid : Data_encoding_db.
End MassArray.
Module Int_Array_Encoding.
Module Valid.
Validity predicate for [int_array_encoding_is_valid].
Record t `{Sampler.Make.FArgs} {A : Set} (x : t int) := {
non_negative : Pervasives.Int31.Valid.non_negative
(Z.of_nat (Datatypes.length x.(t.items)));
default : Pervasives.Int31.Valid.t x.(t.default);
forall_default : Forall (fun y ⇒ y = x.(t.default)) x.(t.items); }.
End Valid.
non_negative : Pervasives.Int31.Valid.non_negative
(Z.of_nat (Datatypes.length x.(t.items)));
default : Pervasives.Int31.Valid.t x.(t.default);
forall_default : Forall (fun y ⇒ y = x.(t.default)) x.(t.items); }.
End Valid.
Auxiliary function, which is used in [int_array_encoding_is_valid]
and other encoding-related proofs in this file.
Lemma fold_left_eq : ∀ xs, (Lists.List.fold_left (fun (acc_value : list int)
(elt_value : int) ⇒ elt_value :: acc_value) xs nil = rev xs).
Proof.
intros. rewrite <- fold_left_rev_right. unfold rev, rev'.
rewrite <- rev_alt. remember (Lists.List.rev xs) as ys.
clear Heqys. induction ys; sfirstorder.
Qed.
(elt_value : int) ⇒ elt_value :: acc_value) xs nil = rev xs).
Proof.
intros. rewrite <- fold_left_rev_right. unfold rev, rev'.
rewrite <- rev_alt. remember (Lists.List.rev xs) as ys.
clear Heqys. induction ys; sfirstorder.
Qed.
Encoding [int_array_encoding] is valid.
Lemma int_array_encoding_is_valid `{Sampler.Make.FArgs} {A : Set} :
Data_encoding.Valid.t (Valid.t (A:=A)) Sampler.Make.int_array_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros x H1; destruct H1; unfold length; rewrite List.length_eq;
destruct x; simpl in ×.
repeat split; [lia..| | ].
{ unfold fold; rewrite fold_left_eq; unfold rev, rev';
repeat (rewrite <- rev_alt); rewrite rev_involutive; simpl;
apply Forall_impl with (P:=(fun y : int ⇒ y = default0)); lia. }
{ rewrite <- List.length_eq. apply fallbackArray_make_default; lia. }
Qed.
#[global] Hint Resolve int_array_encoding_is_valid : Data_encoding_db.
End Int_Array_Encoding.
Module Encoding_is_valid.
Module Valid.
Data_encoding.Valid.t (Valid.t (A:=A)) Sampler.Make.int_array_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros x H1; destruct H1; unfold length; rewrite List.length_eq;
destruct x; simpl in ×.
repeat split; [lia..| | ].
{ unfold fold; rewrite fold_left_eq; unfold rev, rev';
repeat (rewrite <- rev_alt); rewrite rev_involutive; simpl;
apply Forall_impl with (P:=(fun y : int ⇒ y = default0)); lia. }
{ rewrite <- List.length_eq. apply fallbackArray_make_default; lia. }
Qed.
#[global] Hint Resolve int_array_encoding_is_valid : Data_encoding_db.
End Int_Array_Encoding.
Module Encoding_is_valid.
Module Valid.
Validity predicate for [encoding_is_valid].
Record t `{Sampler.Make.FArgs} {A : Set} (x : Sampler.Make.t A) := {
non_neg_support : Pervasives.Int31.Valid.non_negative (Z.of_nat
(Datatypes.length x.(Sampler.Make.t.support).(t.items)));
forall_deflt_sup : Forall (fun y ⇒ y =
x.(Sampler.Make.t.support).(t.default))
x.(Sampler.Make.t.support).(t.items);
non_neg_p : Pervasives.Int31.Valid.non_negative (Z.of_nat
(Datatypes.length x.(Sampler.Make.t.p).(t.items)));
forall_deflt_p : Forall (fun y ⇒ y = x.(Sampler.Make.t.p).(t.default))
x.(Sampler.Make.t.p).(t.items);
non_neg_al : Pervasives.Int31.Valid.non_negative (Z.of_nat
(Datatypes.length x.(Sampler.Make.t.alias).(t.items)));
default_alias : Pervasives.Int31.Valid.t x.(Sampler.Make.t.alias).(t.default);
forall_df_al : Forall (fun y ⇒ y = x.(Sampler.Make.t.alias).(t.default))
x.(Sampler.Make.t.alias).(t.items) }.
End Valid.
non_neg_support : Pervasives.Int31.Valid.non_negative (Z.of_nat
(Datatypes.length x.(Sampler.Make.t.support).(t.items)));
forall_deflt_sup : Forall (fun y ⇒ y =
x.(Sampler.Make.t.support).(t.default))
x.(Sampler.Make.t.support).(t.items);
non_neg_p : Pervasives.Int31.Valid.non_negative (Z.of_nat
(Datatypes.length x.(Sampler.Make.t.p).(t.items)));
forall_deflt_p : Forall (fun y ⇒ y = x.(Sampler.Make.t.p).(t.default))
x.(Sampler.Make.t.p).(t.items);
non_neg_al : Pervasives.Int31.Valid.non_negative (Z.of_nat
(Datatypes.length x.(Sampler.Make.t.alias).(t.items)));
default_alias : Pervasives.Int31.Valid.t x.(Sampler.Make.t.alias).(t.default);
forall_df_al : Forall (fun y ⇒ y = x.(Sampler.Make.t.alias).(t.default))
x.(Sampler.Make.t.alias).(t.items) }.
End Valid.
Validity of encoding [encoding].
Lemma encoding_is_valid `{Sampler.Make.FArgs} {A : Set} :
∀ (enc : Data_encoding.t A), Data_encoding.Valid.t (fun _ ⇒ True) enc →
Data_encoding.Valid.t (fun _ ⇒ True)
Sampler.Make.Mass.(Sampler.SMass.encoding) →
Data_encoding.Valid.t Valid.t (Sampler.Make.encoding enc).
Proof.
intros enc H0 H1.
Data_encoding.Valid.data_encoding_auto. intros x H2; destruct H2;
unfold length; destruct x; simpl in *; rewrite List.length_eq in ×.
repeat split; try lia; try hauto l: on.
rewrite <- List.length_eq; apply fallbackArray_make_default; lia.
all : try (rewrite List.length_eq); try lia.
rewrite <- List.length_eq; apply fallbackArray_make_default; lia.
unfold fold. rewrite Int_Array_Encoding.fold_left_eq.
unfold rev, rev'. repeat (rewrite <- rev_alt); rewrite rev_involutive.
apply Forall_impl with (P:=(fun y : int ⇒ y = alias.(t.default))); lia.
rewrite <- List.length_eq; apply fallbackArray_make_default; lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Encoding_is_valid.
End Make.
Module Mass.
∀ (enc : Data_encoding.t A), Data_encoding.Valid.t (fun _ ⇒ True) enc →
Data_encoding.Valid.t (fun _ ⇒ True)
Sampler.Make.Mass.(Sampler.SMass.encoding) →
Data_encoding.Valid.t Valid.t (Sampler.Make.encoding enc).
Proof.
intros enc H0 H1.
Data_encoding.Valid.data_encoding_auto. intros x H2; destruct H2;
unfold length; destruct x; simpl in *; rewrite List.length_eq in ×.
repeat split; try lia; try hauto l: on.
rewrite <- List.length_eq; apply fallbackArray_make_default; lia.
all : try (rewrite List.length_eq); try lia.
rewrite <- List.length_eq; apply fallbackArray_make_default; lia.
unfold fold. rewrite Int_Array_Encoding.fold_left_eq.
unfold rev, rev'. repeat (rewrite <- rev_alt); rewrite rev_involutive.
apply Forall_impl with (P:=(fun y : int ⇒ y = alias.(t.default))); lia.
rewrite <- List.length_eq; apply fallbackArray_make_default; lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Encoding_is_valid.
End Make.
Module Mass.
Validity predicate for [Mass.t].
The encoding [Mass.encoding] is valid.
Lemma encoding_is_valid :
Data_encoding.Valid.t Valid.t
Sampler.Mass.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Mass.
Data_encoding.Valid.t Valid.t
Sampler.Mass.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Mass.
[Sampler.sample] has no internal errors
Lemma sample_is_valid {A}
(s : Sampler.Make.t A)
(f :
int →
Sampler.Mass.(Sampler.SMass.t) →
int × Sampler.Mass.(Sampler.SMass.t))
: letP? _ := Sampler.sample s f in True.
Proof. Admitted.
(s : Sampler.Make.t A)
(f :
int →
Sampler.Mass.(Sampler.SMass.t) →
int × Sampler.Mass.(Sampler.SMass.t))
: letP? _ := Sampler.sample s f in True.
Proof. Admitted.