🍃 S.v | Coq Tezos of OCaml 💫

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_arg.

Module MINIMAL_HASH.
  Definition to_Compare_S {t} (H : S.MINIMAL_HASH (t := t))
    : Compare.S (t := t) := {|
      Compare.S.op_eq := H.(S.MINIMAL_HASH.op_eq);
      Compare.S.op_ltgt := H.(S.MINIMAL_HASH.op_ltgt);
      Compare.S.op_lt := H.(S.MINIMAL_HASH.op_lt);
      Compare.S.op_lteq := H.(S.MINIMAL_HASH.op_lteq);
      Compare.S.op_gteq := H.(S.MINIMAL_HASH.op_gteq);
      Compare.S.op_gt := H.(S.MINIMAL_HASH.op_gt);
      Compare.S.compare := H.(S.MINIMAL_HASH.compare);
      Compare.S.equal := H.(S.MINIMAL_HASH.equal);
      Compare.S.max := H.(S.MINIMAL_HASH.max);
      Compare.S.min := H.(S.MINIMAL_HASH.min);
    |}.

    Module Valid.

      Record t {t} {H : S.MINIMAL_HASH (t := t)} : Prop := {
        Compare_S : Compare.S.Valid.t (to_Compare_S H);
      }.
      Arguments t {_}.
    End Valid.

  Lemma to_Compare_equal_eq {t} (H : S.MINIMAL_HASH (t := t)) :
    (to_Compare_S H).(Compare.S.equal) = H.(S.MINIMAL_HASH.equal).
  Proof.
    unfold to_Compare_S. reflexivity.
  Qed.

  Lemma valid_implies_equal_valid {t} {H : S.MINIMAL_HASH (t := t)}:
    Valid.t H → Compare.Equal.Valid.t (fun _ ⇒ True) H.(S.MINIMAL_HASH.equal).
  Proof.
    unfold Compare.Equal.Valid.t.
    intros Hval.
    destruct Hval as [Hval].
    rewrite <- to_Compare_equal_eq.
    remember (to_Compare_S H) as CH.
    apply (@Compare.S.valid_implies_equal_valid t CH) in Hval.
    unfold Compare.Equal.Valid.t in Hval.
    apply Hval ; constructor.
  Qed.
End MINIMAL_HASH.

Module RAW_DATA.
  Module Valid.
    Record t {t} {R : S.RAW_DATA (t := t)} : Prop := {
      of_bytes_opt_to_bytes v :
        R.(S.RAW_DATA.of_bytes_opt) (R.(S.RAW_DATA.to_bytes) v) =
        Some v;
      to_bytes_of_bytes_opt bytes :
        match R.(S.RAW_DATA.of_bytes_opt) bytes with
        | Some v ⇒ R.(S.RAW_DATA.to_bytes) v = bytes
        | None ⇒ True
        end;
    }.
    Arguments t {_}.
  End Valid.
End RAW_DATA.

Module B58_DATA.
  Module Valid.
    Record t {t} (B : S.B58_DATA (t := t)) : Prop := {
      of_to_b58_check value :
        B.(S.B58_DATA.of_b58check_opt) (B.(S.B58_DATA.to_b58check) value) =
        Some value;
      to_of_b58_check string :
        match B.(S.B58_DATA.of_b58check_opt) string with
        | Some value ⇒ B.(S.B58_DATA.to_b58check) value = string
        | None ⇒ True
        end;
    }.
  End Valid.
End B58_DATA.

Module ENCODER.
  Module Valid.
    Record t {t : Set} {domain} {E : S.ENCODER (t := t)} : Prop := {
      encoding : Data_encoding.Valid.t (fun _ ⇒ True) E.(S.ENCODER.encoding);
      rpc_arg : RPC_arg.Valid.t domain E.(S.ENCODER.rpc_arg);
    }.
    Arguments t {_}.
  End Valid.
End ENCODER.

Module HASH.
  Definition to_MINIMAL_HASH {t Set_t Map_t}
    (H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
    : S.MINIMAL_HASH (t := t) := {|
      S.MINIMAL_HASH.name := H.(S.HASH.name);
      S.MINIMAL_HASH.title := H.(S.HASH.title);
      S.MINIMAL_HASH.pp := H.(S.HASH.pp);
      S.MINIMAL_HASH.pp_short := H.(S.HASH.pp_short);
      S.MINIMAL_HASH.op_eq := H.(S.HASH.op_eq);
      S.MINIMAL_HASH.op_ltgt := H.(S.HASH.op_ltgt);
      S.MINIMAL_HASH.op_lt := H.(S.HASH.op_lt);
      S.MINIMAL_HASH.op_lteq := H.(S.HASH.op_lteq);
      S.MINIMAL_HASH.op_gteq := H.(S.HASH.op_gteq);
      S.MINIMAL_HASH.op_gt := H.(S.HASH.op_gt);
      S.MINIMAL_HASH.compare := H.(S.HASH.compare);
      S.MINIMAL_HASH.equal := H.(S.HASH.equal);
      S.MINIMAL_HASH.max := H.(S.HASH.max);
      S.MINIMAL_HASH.min := H.(S.HASH.min);
      S.MINIMAL_HASH.hash_bytes := H.(S.HASH.hash_bytes);
      S.MINIMAL_HASH.hash_string := H.(S.HASH.hash_string);
      S.MINIMAL_HASH.zero := H.(S.HASH.zero);
    |}.

  Lemma to_MINIMAL_equal_eq {t Set_t Map_t}
    (H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
    (to_MINIMAL_HASH H).(MINIMAL_HASH.equal) = H.(S.HASH.equal).
  Proof.
    unfold to_MINIMAL_HASH. reflexivity.
  Qed.

  Definition to_RAW_DATA {t Set_t Map_t}
    (H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
    : S.RAW_DATA (t := t) := {|
      S.RAW_DATA.size_value := H.(S.HASH.size_value);
      S.RAW_DATA.to_bytes := H.(S.HASH.to_bytes);
      S.RAW_DATA.of_bytes_opt := H.(S.HASH.of_bytes_opt);
      S.RAW_DATA.of_bytes_exn := H.(S.HASH.of_bytes_exn);
    |}.

  Definition to_B58_DATA {t Set_t Map_t}
    (H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
    : S.B58_DATA (t := t) := {|
      S.B58_DATA.to_b58check := H.(HASH.to_b58check);
      S.B58_DATA.to_short_b58check := H.(HASH.to_short_b58check);
      S.B58_DATA.of_b58check_exn := H.(HASH.of_b58check_exn);
      S.B58_DATA.of_b58check_opt := H.(HASH.of_b58check_opt);
      S.B58_DATA.b58check_encoding := H.(HASH.b58check_encoding);
    |}.

  Definition to_ENCODER {t Set_t Map_t}
    (H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
    : S.ENCODER (t := t) := {|
      S.ENCODER.encoding := H.(S.HASH.encoding);
      S.ENCODER.rpc_arg := H.(S.HASH.rpc_arg);
    |}.

  Definition to_INDEXES {t Set_t Map_t}
    (H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
    : S.INDEXES (t := t) := {|
      S.INDEXES._Set := H.(S.HASH._Set);
      S.INDEXES.Map := H.(S.HASH.Map);
    |}.

  Module Valid.
    Record t {t Set_t Map_t} {domain}
      {H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)} : Prop := {
      MINIMAL_HASH : MINIMAL_HASH.Valid.t (to_MINIMAL_HASH H);
      RAW_DATA : RAW_DATA.Valid.t (to_RAW_DATA H);
      B58_DATA : B58_DATA.Valid.t (to_B58_DATA H);
      ENCODER : ENCODER.Valid.t domain (to_ENCODER H);
    }.
    Arguments t {_ _ _}.
  End Valid.