Skip to main content

🍃 Compare.v

Environment

See proofs, Gitlab , OCaml

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

Require Proto_alpha.Environment.Char.
Require Proto_alpha.Environment.Int32.
Require Proto_alpha.Environment.Int64.
Require Proto_alpha.Environment.Pervasives.
Require Proto_alpha.Environment.String.
Require Proto_alpha.Environment.Z.
Import Pervasives.Notations.

Module COMPARABLE.
  Record signature {t : Set} : Set := {
    t := t;
    compare : t t int;
  }.
End COMPARABLE.
Definition COMPARABLE := @COMPARABLE.signature.
Arguments COMPARABLE {_}.

Module S.
  Record signature {t : Set} : Set := {
    t := t;
    op_eq : t t bool;
    op_ltgt : t t bool;
    op_lt : t t bool;
    op_lteq : t t bool;
    op_gteq : t t bool;
    op_gt : t t bool;
    compare : t t int;
    equal : t t bool;
    max : t t t;
    min : t t t;
  }.
End S.
Definition S := @S.signature.
Arguments S {_}.

Definition Make {P_t : Set} (P : COMPARABLE (t := P_t))
  : S (t := P.(COMPARABLE.t)) :=
  {|
    S.op_eq x y := Z.eqb (P.(COMPARABLE.compare) x y) 0;
    S.op_ltgt x y := negb (Z.eqb (P.(COMPARABLE.compare) x y) 0);
    S.op_lt x y := Z.ltb (P.(COMPARABLE.compare) x y) 0;
    S.op_lteq x y := Z.leb (P.(COMPARABLE.compare) x y) 0;
    S.op_gteq x y := Z.geb (P.(COMPARABLE.compare) x y) 0;
    S.op_gt x y := Z.gtb (P.(COMPARABLE.compare) x y) 0;
    S.compare x y := P.(COMPARABLE.compare) x y;
    S.equal x y := Z.eqb (P.(COMPARABLE.compare) x y) 0;
    S.max x y :=
      if Z.leb (P.(COMPARABLE.compare) x y) 0 then
        y
      else
        x;
    S.min x y :=
      if Z.leb (P.(COMPARABLE.compare) x y) 0 then
        x
      else
        y;
  |}.

A utility function built on top of [Make] to make it simpler to use.
Definition Make_with_compare {A : Set} (compare : A A int) : S (t := A) :=
  Make {| COMPARABLE.compare := compare |}.

Definition Char : S (t := ascii) :=
  Make_with_compare Char.compare.

Definition int_of_bool (b : bool) : int :=
  if b then 1 else 0.

Definition Unit : S (t := unit) :=
  Make_with_compare (fun '_ '_ ⇒ 0).

Definition Bool : S (t := bool) :=
  Make_with_compare (fun x y
    match x, y with
    | false, false ⇒ 0
    | false, true ⇒ -1
    | true, false ⇒ 1
    | true, true ⇒ 0
    end
  ).

Definition Z : S (t := Z.t) :=
  {|
    S.op_eq := Z.eqb;
    S.op_ltgt x y := negb (x =? y);
    S.op_lt x y := x <? y;
    S.op_lteq x y := x <=? y;
    S.op_gteq x y := x >=? y;
    S.op_gt x y := x >? y;
    S.compare := Z.compare;
    S.equal := Z.eqb;
    S.max := Z.max;
    S.min := Z.min;
  |}.

Definition Int : S (t := int) := Z.

Module Int.
  Definition t : Set := int.

  Definition op_eq : int int bool := Int.(S.op_eq).

  Definition op_ltgt : int int bool := Int.(S.op_ltgt).

  Definition op_lt : int int bool := Int.(S.op_lt).

  Definition op_gt : int int bool := Int.(S.op_gt).

  Definition op_lteq : int int bool := Int.(S.op_lteq).

  Definition op_gteq : int int bool := Int.(S.op_gteq).

  Definition compare : int int int := Int.(S.compare).

  Definition max : int int int := Int.(S.max).

  Definition min : int int int := Int.(S.min).

  Definition equal : int int bool := Int.(S.equal).
End Int.

Definition Int32 : S (t := int32) := Z.

Definition Uint32 : S (t := int32) := Z.

Definition Int64 : S (t := int64) := Z.

Definition Uint64 : S (t := int64) := Z.

Definition String : S (t := string) :=
  Make_with_compare String.compare.

Definition Bytes : S (t := bytes) :=
  Make_with_compare String.compare.

Module List.
  Parameter compare : {a : Set},
    (a a int) list a list a int.
End List.

Definition List {P_t : Set} (P : COMPARABLE (t := P_t))
  : S (t := list P.(COMPARABLE.t)) :=
  Make_with_compare (List.compare P.(COMPARABLE.compare)).

Module Option.
  Definition compare {a : Set} (compare : a a int) (x y : option a)
    : int :=
    match x, y with
    | None, None ⇒ 0
    | None, Some _ ⇒ -1
    | Some _, None ⇒ 1
    | Some x, Some ycompare x y
    end.
End Option.

Definition Option {P_t : Set} (P : COMPARABLE (t := P_t))
  : S (t := option P.(COMPARABLE.t)) :=
  Make_with_compare (Option.compare P.(COMPARABLE.compare)).

Parameter Result :
   {Ok_t Error_t : Set},
   (Ok : COMPARABLE (t := Ok_t)),
   (Error : COMPARABLE (t := Error_t)),
  S (t := Pervasives.result Ok.(COMPARABLE.t) Error.(COMPARABLE.t)).

Module List_length_with.
  Fixpoint op_eq {a : Set} (l : list a) (n : int) : bool :=
    match l with
    | []n =? 0
    | _ :: lop_eq l (n -i 1)
    end.

  Parameter op_ltgt : {a : Set}, list a int bool.

  Parameter op_lt : {a : Set}, list a int bool.

  Parameter op_lteq : {a : Set}, list a int bool.

  Parameter op_gteq : {a : Set}, list a int bool.

  Parameter op_gt : {a : Set}, list a int bool.

  Parameter compare : {a : Set}, list a int int.

  Parameter equal : {a : Set}, list a int bool.
End List_length_with.

Module List_lengths.
  Parameter op_eq : {a b : Set}, list a list b bool.

  Parameter op_ltgt : {a b : Set}, list a list b bool.

  Parameter op_lt : {a b : Set}, list a list b bool.

  Parameter op_lteq : {a b : Set}, list a list b bool.

  Parameter op_gteq : {a b : Set}, list a list b bool.

  Parameter op_gt : {a b : Set}, list a list b bool.

  Parameter compare : {a b : Set}, list a list b int.

  Parameter equal : {a b : Set}, list a list b bool.
End List_lengths.

Parameter or_else : int (unit int) int.

Definition lexicographic {a b : Set} (compare_a : a a int)
  (compare_b : b b int) (x y : a × b) : int :=
  let (x_a, x_b) := x in
  let (y_a, y_b) := y in
  let a_res := compare_a x_a y_a in
  match a_res with
  | 0 ⇒ compare_b x_b y_b
  | _a_res
  end.

Definition Pair {P1_t P2_t : Set}
  (P1 : COMPARABLE (t := P1_t)) (P2 : COMPARABLE (t := P2_t))
  : S (t := P1.(COMPARABLE.t) × P2.(COMPARABLE.t)) :=
  Make_with_compare
    (lexicographic P1.(COMPARABLE.compare) P2.(COMPARABLE.compare)).

Module Notations.
  Infix "=i" := Int.op_eq
    (at level 70, no associativity).
  Infix "<>i" := Int.op_ltgt
    (at level 70, no associativity).
  Infix "<=i" := Int.op_lteq
    (at level 70, no associativity).
  Infix "<i" := Int.op_lt
    (at level 70, no associativity).
  Infix ">=i" := Int.op_gteq
    (at level 70, no associativity).
  Infix ">i" := Int.op_gt
    (at level 70, no associativity).

  Infix "=i32" := Int32.(S.op_eq)
    (at level 70, no associativity).
  Infix "<>i32" := Int32.(S.op_ltgt)
    (at level 70, no associativity).
  Infix "<=i32" := Int32.(S.op_lteq)
    (at level 70, no associativity).
  Infix "<i32" := Int32.(S.op_lt)
    (at level 70, no associativity).
  Infix ">=i32" := Int32.(S.op_gteq)
    (at level 70, no associativity).
  Infix ">i32" := Int32.(S.op_gt)
    (at level 70, no associativity).

  Infix "=i64" := Int64.(S.op_eq)
    (at level 70, no associativity).
  Infix "<>i64" := Int64.(S.op_ltgt)
    (at level 70, no associativity).
  Infix "<=i64" := Int64.(S.op_lteq)
    (at level 70, no associativity).
  Infix "<i64" := Int64.(S.op_lt)
    (at level 70, no associativity).
  Infix ">=i64" := Int64.(S.op_gteq)
    (at level 70, no associativity).
  Infix ">i64" := Int64.(S.op_gt)
    (at level 70, no associativity).

  Infix "=Z" := Z.(S.op_eq)
    (at level 70, no associativity).
  Infix "<>Z" := Z.(S.op_ltgt)
    (at level 70, no associativity).
  Infix "<=Z" := Z.(S.op_lteq)
    (at level 70, no associativity).
  Infix "<Z" := Z.(S.op_lt)
    (at level 70, no associativity).
  Infix ">=Z" := Z.(S.op_gteq)
    (at level 70, no associativity).
  Infix ">Z" := Z.(S.op_gt)
    (at level 70, no associativity).

  Infix "=s" := String.(S.op_eq)
    (at level 70, no associativity).
  Infix "<>s" := String.(S.op_ltgt)
    (at level 70, no associativity).
  Infix "<=s" := String.(S.op_lteq)
    (at level 70, no associativity).
  Infix "<s" := String.(S.op_lt)
    (at level 70, no associativity).
  Infix ">=s" := String.(S.op_gteq)
    (at level 70, no associativity).
  Infix ">s" := String.(S.op_gt)
    (at level 70, no associativity).
End Notations.

#[global] Hint Unfold
  Int.op_eq
  Int.op_ltgt
  Int.op_lt
  Int.op_gt
  Int.op_lteq
  Int.op_gteq
  Int.compare
  Int.max
  Int.min
  Int.equal
  : tezos_z.

Polymorphic comparison operators

These operators cannot be implemented in Coq but are sometimes useful to translate the tests. They are not used in the protocol itself. See the corresponding Proofs file for the specification of these operators.
Polymorphic equality, like in OCaml.
Parameter polymorphic_eq : {a : Set}, a a bool.

Polymorphic comparison, like in OCaml.
Parameter polymorphic_compare : {a : Set}, a a int.