🍃 Bounded.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V7.

Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V7.Proofs.Int32.

Module BOUNDS.
  Import Environment.V7.Bounded.BOUNDS.

The validity condition for [BOUNDS].

  Module Valid.
    Record t {ocaml_type : Set} (domain : ocaml_type → Prop)
      (B : Bounded.BOUNDS (ocaml_type := ocaml_type)) : Prop := {
      min_value : domain B.(min_value);
      max_value : domain B.(max_value);
    }.
  End Valid.
End BOUNDS.

Module S.
  Import Environment.V7.Bounded.S.

  Definition to_BOUNDS {t ocaml_type}
    (B : Bounded.S (t := t) (ocaml_type := ocaml_type))
    : Bounded.BOUNDS (ocaml_type := ocaml_type) := {|
    Bounded.BOUNDS.min_value := B.(min_value);
    Bounded.BOUNDS.max_value := B.(max_value);
  |}.

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

The validity condition for [S]

  Module Valid.
    Record t {t ocaml_type : Set}
      (domain : ocaml_type → Prop)
      (B : Bounded.S (t := t) (ocaml_type := ocaml_type))
      : Prop := {
      BOUNDS : BOUNDS.Valid.t domain (to_BOUNDS B);
      Compare_S : Compare.S.Valid.t (to_Compare_S B);
      encoding : Data_encoding.Valid.t
        (fun _ ⇒ True) B.(Bounded.S.encoding);
      to_value b : domain (B.(Bounded.S.to_value) b);
      to_of_value i b :
        B.(Bounded.S.of_value) i = Some b →
        B.(Bounded.S.to_value) b = i;
      of_to_value b :
        B.(Bounded.S.of_value)
          (B.(Bounded.S.to_value) b) = Some b;
    }.
  End Valid.
End S.

The functor [Int64] is valid.

Axiom Int64_is_Valid :
  ∀ (B : Bounded.BOUNDS (ocaml_type := int64)),
  BOUNDS.Valid.t Int64.Valid.t B →
  S.Valid.t Int64.Valid.t (Bounded.Int64 B).

The functor [Int32] is valid.

Axiom Int32_is_Valid :
  ∀ (B : Bounded.BOUNDS (ocaml_type := int32)),
  BOUNDS.Valid.t Int32.Valid.t B →
  S.Valid.t Int32.Valid.t (Bounded.Int32 B).

The module [Non_negative_int32] is valid.

Axiom Non_negative_int32_is_Valid :
  S.Valid.t Int32.Valid.non_negative Bounded.Non_negative_int32.

The functor [Int31] is valid.

Axiom Int31_is_Valid :
  ∀ (B : Bounded.BOUNDS (ocaml_type := int)),
  BOUNDS.Valid.t Pervasives.Int.Valid.t B →
  S.Valid.t Pervasives.Int.Valid.t (Bounded.Int31 B).

The functor [Int16] is valid.

Axiom Int16_is_Valid :
∀ (B : Bounded.BOUNDS (ocaml_type := int)),
BOUNDS.Valid.t Pervasives.Int16.Valid.t B →
S.Valid.t Pervasives.Int16.Valid.t (Bounded.Int16 B).

The functor [Uint16] is valid.

Axiom Uint16_is_Valid :
  ∀ (B : Bounded.BOUNDS (ocaml_type := int)),
  BOUNDS.Valid.t Pervasives.UInt16.Valid.t B →
  S.Valid.t Pervasives.UInt16.Valid.t (Bounded.Uint16 B).

The functor [Int8] is valid.

Axiom Int8_is_Valid :
∀ (B : Bounded.BOUNDS (ocaml_type := int)),
BOUNDS.Valid.t Pervasives.Int8.Valid.t B →
S.Valid.t Pervasives.Int8.Valid.t (Bounded.Int8 B).

The functor [Uint8] is valid.

Axiom Uint8_is_Valid :
  ∀ (B : Bounded.BOUNDS (ocaml_type := int)),
  BOUNDS.Valid.t Pervasives.UInt8.Valid.t B →
  S.Valid.t Pervasives.UInt8.Valid.t (Bounded.Uint8 B).