🗂️ Indexable.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Module Valid.
Definition t {a : Set} (x : Indexable.t a) : Prop :=
match x with
| Indexable.Value _ | Indexable.Hidden_value _ ⇒ True
| Indexable.Index index | Indexable.Hidden_index index ⇒
Int32.Valid.non_negative index
end.
End Valid.
Module Index.
Module Valid.
Definition t {a : Set} (x : Indexable.t a) : Prop :=
match x with
| Indexable.Index _ ⇒ Valid.t x
| _ ⇒ False
end.
End Valid.
End Index.
Module Value.
Module Valid.
Definition t {a : Set} (x : Indexable.t a) : Prop :=
match x with
| Indexable.Value _ ⇒ Valid.t x
| _ ⇒ False
end.
End Valid.
End Value.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Module Valid.
Definition t {a : Set} (x : Indexable.t a) : Prop :=
match x with
| Indexable.Value _ | Indexable.Hidden_value _ ⇒ True
| Indexable.Index index | Indexable.Hidden_index index ⇒
Int32.Valid.non_negative index
end.
End Valid.
Module Index.
Module Valid.
Definition t {a : Set} (x : Indexable.t a) : Prop :=
match x with
| Indexable.Index _ ⇒ Valid.t x
| _ ⇒ False
end.
End Valid.
End Index.
Module Value.
Module Valid.
Definition t {a : Set} (x : Indexable.t a) : Prop :=
match x with
| Indexable.Value _ ⇒ Valid.t x
| _ ⇒ False
end.
End Valid.
End Value.
Two elements are said equivalent if they are equal once we forget about
their hidden status.
[destruct] does not depend on the hidden status.
Lemma {a : Set} (i1 i2 : Indexable.t a) :
eq_forgetting_hidden i1 i2 →
Indexable.destruct i1 = Indexable.destruct i2.
Proof.
sauto q: on.
Qed.
eq_forgetting_hidden i1 i2 →
Indexable.destruct i1 = Indexable.destruct i2.
Proof.
sauto q: on.
Qed.
[forget] does not depend on the hidden status.
Lemma {a : Set} (i1 i2 : Indexable.t a) :
eq_forgetting_hidden i1 i2 →
Indexable.forget i1 = Indexable.forget i2.
Proof.
sauto q: on.
Qed.
Lemma encoding_is_valid {a : Set} (val_encoding : Data_encoding.t a) :
Data_encoding.Valid.t (fun _ ⇒ True) val_encoding →
Data_encoding.Valid.t Valid.t (Indexable.encoding val_encoding).
Admitted.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
eq_forgetting_hidden i1 i2 →
Indexable.forget i1 = Indexable.forget i2.
Proof.
sauto q: on.
Qed.
Lemma encoding_is_valid {a : Set} (val_encoding : Data_encoding.t a) :
Data_encoding.Valid.t (fun _ ⇒ True) val_encoding →
Data_encoding.Valid.t Valid.t (Indexable.encoding val_encoding).
Admitted.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
[in_memory_size] does not depend on the hidden status.
Lemma {a : Set} ims (i1 i2 : Indexable.t a) :
eq_forgetting_hidden i1 i2 →
Indexable.in_memory_size ims i1 = Indexable.in_memory_size ims i2.
Proof.
sauto q: on.
Qed.
eq_forgetting_hidden i1 i2 →
Indexable.in_memory_size ims i1 = Indexable.in_memory_size ims i2.
Proof.
sauto q: on.
Qed.
[size_value] does not depend on the hidden status.
Lemma {a : Set} ims (i1 i2 : Indexable.t a) :
eq_forgetting_hidden i1 i2 →
Indexable.size_value ims i1 = Indexable.size_value ims i2.
Proof.
sauto q: on.
Qed.
eq_forgetting_hidden i1 i2 →
Indexable.size_value ims i1 = Indexable.size_value ims i2.
Proof.
sauto q: on.
Qed.
The [compare] function is valid and forgets about the hidden status.
Lemma compare_is_valid {a : Set} (c_value : a → a → int) :
Compare.Valid.t (fun _ ⇒ True) id c_value →
Compare.Valid.t (fun _ ⇒ True) Indexable.forget (Indexable.compare c_value).
Proof.
intros H.
apply (Compare.equality (
let proj_value x :=
match x with
| Indexable.Hidden_value x | Indexable.Value x ⇒ Some x
| _ ⇒ None
end in
let proj_index x :=
match x with
| Indexable.Hidden_index x | Indexable.Index x ⇒ Some x
| _ ⇒ None
end in
let proj x :=
(proj_value x, proj_index x) in
Compare.projection proj (
Compare.lexicographic
(Compare.Option.compare c_value) (Compare.Option.compare Int32.compare)
)
)); [intros [] [] **; cbn; try (now destruct c_value); reflexivity |].
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
eapply Compare.lexicographic_is_valid; eapply Compare.option_is_valid; [
apply H |
apply Compare.int32_is_valid
].
}
all: hauto drew: off.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
Lemma compare_values_is_valid {a : Set} (c_value : a → a → int) :
Compare.Valid.t (fun _ ⇒ True) id c_value →
Compare.Valid.t Value.Valid.t id (Indexable.compare_values c_value).
Proof.
intros H.
apply (Compare.equality (
let proj x :=
match x with
| Indexable.Value x ⇒ Some x
| _ ⇒ None
end in
Compare.projection proj (Compare.Option.compare c_value)
)); [sauto lq: on rew: off|].
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
eapply Compare.option_is_valid.
apply H.
}
all: intros [] []; unfold id; sfirstorder.
Qed.
#[global] Hint Resolve compare_values_is_valid : Compare_db.
Lemma compare_indexes_is_valid {a : Set} :
Compare.Valid.t Index.Valid.t id (Indexable.compare_indexes (a := a)).
Proof.
apply (Compare.equality (
let proj x :=
match x with
| Indexable.Index x ⇒ Some x
| _ ⇒ None
end in
Compare.projection proj (Compare.Option.compare (Compare.Int32.(Compare.S.compare)))
)); [sauto lq: on rew: off|].
eapply Compare.implies.
{
eapply Compare.projection_is_valid.
eapply Compare.option_is_valid.
apply Compare.int32_is_valid.
}
all: intros [] []; unfold id; hauto l: on.
Qed.
#[global] Hint Resolve compare_indexes_is_valid : Compare_db.
Module VALUE.
Module Valid.
Import TezosOfOCaml.Proto_alpha.Indexable.VALUE.
Record t {t : Set} (V : Indexable.VALUE (t := t)) : Prop := {
encoding : Data_encoding.Valid.t (fun _ ⇒ True) V.(encoding);
compare : Compare.Valid.t (fun _ ⇒ True) id V.(compare);
}.
End Valid.
End VALUE.
Module INDEXABLE.
Module Valid.
Import TezosOfOCaml.Proto_alpha.Indexable.INDEXABLE.
Record t {v_t : Set} (I : Indexable.INDEXABLE (v_t := v_t)) : Prop := {
encoding : Data_encoding.Valid.t Valid.t I.(encoding);
index_encoding : Data_encoding.Valid.t Index.Valid.t I.(index_encoding);
value_encoding : Data_encoding.Valid.t Value.Valid.t I.(value_encoding);
compare : Compare.Valid.t (fun _ ⇒ True) Indexable.forget I.(compare);
compare_values : Compare.Valid.t Value.Valid.t id I.(compare_values);
}.
End Valid.
End INDEXABLE.
Lemma Make_is_valid {t : Set} (V : Indexable.VALUE (t := t)) :
VALUE.Valid.t V → INDEXABLE.Valid.t (Indexable.Make V).
Proof.
intro H.
constructor.
{ apply encoding_is_valid.
apply H.
}
{ Data_encoding.Valid.data_encoding_auto.
intros [] ?; simpl in *; try easy.
split; lia.
}
{ Data_encoding.Valid.data_encoding_auto; try apply H.
hauto l: on.
}
{ apply compare_is_valid.
apply H.
}
{
apply compare_values_is_valid.
apply H.
}
Qed.
Compare.Valid.t (fun _ ⇒ True) id c_value →
Compare.Valid.t (fun _ ⇒ True) Indexable.forget (Indexable.compare c_value).
Proof.
intros H.
apply (Compare.equality (
let proj_value x :=
match x with
| Indexable.Hidden_value x | Indexable.Value x ⇒ Some x
| _ ⇒ None
end in
let proj_index x :=
match x with
| Indexable.Hidden_index x | Indexable.Index x ⇒ Some x
| _ ⇒ None
end in
let proj x :=
(proj_value x, proj_index x) in
Compare.projection proj (
Compare.lexicographic
(Compare.Option.compare c_value) (Compare.Option.compare Int32.compare)
)
)); [intros [] [] **; cbn; try (now destruct c_value); reflexivity |].
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
eapply Compare.lexicographic_is_valid; eapply Compare.option_is_valid; [
apply H |
apply Compare.int32_is_valid
].
}
all: hauto drew: off.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
Lemma compare_values_is_valid {a : Set} (c_value : a → a → int) :
Compare.Valid.t (fun _ ⇒ True) id c_value →
Compare.Valid.t Value.Valid.t id (Indexable.compare_values c_value).
Proof.
intros H.
apply (Compare.equality (
let proj x :=
match x with
| Indexable.Value x ⇒ Some x
| _ ⇒ None
end in
Compare.projection proj (Compare.Option.compare c_value)
)); [sauto lq: on rew: off|].
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
eapply Compare.option_is_valid.
apply H.
}
all: intros [] []; unfold id; sfirstorder.
Qed.
#[global] Hint Resolve compare_values_is_valid : Compare_db.
Lemma compare_indexes_is_valid {a : Set} :
Compare.Valid.t Index.Valid.t id (Indexable.compare_indexes (a := a)).
Proof.
apply (Compare.equality (
let proj x :=
match x with
| Indexable.Index x ⇒ Some x
| _ ⇒ None
end in
Compare.projection proj (Compare.Option.compare (Compare.Int32.(Compare.S.compare)))
)); [sauto lq: on rew: off|].
eapply Compare.implies.
{
eapply Compare.projection_is_valid.
eapply Compare.option_is_valid.
apply Compare.int32_is_valid.
}
all: intros [] []; unfold id; hauto l: on.
Qed.
#[global] Hint Resolve compare_indexes_is_valid : Compare_db.
Module VALUE.
Module Valid.
Import TezosOfOCaml.Proto_alpha.Indexable.VALUE.
Record t {t : Set} (V : Indexable.VALUE (t := t)) : Prop := {
encoding : Data_encoding.Valid.t (fun _ ⇒ True) V.(encoding);
compare : Compare.Valid.t (fun _ ⇒ True) id V.(compare);
}.
End Valid.
End VALUE.
Module INDEXABLE.
Module Valid.
Import TezosOfOCaml.Proto_alpha.Indexable.INDEXABLE.
Record t {v_t : Set} (I : Indexable.INDEXABLE (v_t := v_t)) : Prop := {
encoding : Data_encoding.Valid.t Valid.t I.(encoding);
index_encoding : Data_encoding.Valid.t Index.Valid.t I.(index_encoding);
value_encoding : Data_encoding.Valid.t Value.Valid.t I.(value_encoding);
compare : Compare.Valid.t (fun _ ⇒ True) Indexable.forget I.(compare);
compare_values : Compare.Valid.t Value.Valid.t id I.(compare_values);
}.
End Valid.
End INDEXABLE.
Lemma Make_is_valid {t : Set} (V : Indexable.VALUE (t := t)) :
VALUE.Valid.t V → INDEXABLE.Valid.t (Indexable.Make V).
Proof.
intro H.
constructor.
{ apply encoding_is_valid.
apply H.
}
{ Data_encoding.Valid.data_encoding_auto.
intros [] ?; simpl in *; try easy.
split; lia.
}
{ Data_encoding.Valid.data_encoding_auto; try apply H.
hauto l: on.
}
{ apply compare_is_valid.
apply H.
}
{
apply compare_values_is_valid.
apply H.
}
Qed.