🍃 Compare.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.

General presentation: 1 - [compare.ml] mainly defines two modules [COMPARABLE] and [S] and a functor [Make] from [COMPARABLE] to [S]. [COMPARABLE] depends on [t : Set], its signature is [compare : t -> t -> int]. Notice that the output of [compare] lives in [int] [S] also depends on [t : Set] signature of [S] is [op_eq, op_lt, equal : t -> t -> bool , compare : t -> t -> int]. Notice that [compare] still outputs an [int] whereas the other functions (including [equal]) mostly output a [bool] The functore [Make] defines all the field [op_eq, op_lt, equal] and so on from the comparison function [COMPARABLE.compare] 2 - Therefore, we start defining validity predicates for equalities of type [t -> t -> bool] and comparison functions (defining preorders) of type [t -> t -> int]. A boolean equality is valid when it captures propositional equality. A preorder is valid when it satisfies the usual axioms of preorders + a congruence axiom regarding the [int] output of [compare]. The canonical projection associated to a preorder is denoted [f] (i.e., [f] is s.t. [f x = f y] iff [x =< y /\ y =< x]. In this file, we mostly have [f = id]. In particular, orders, rather than general preorders, are considered. The validity predicates are parametrized with [domain]s, i.e. functions of type [t -> Prop] (although in this file, [domain] is trivial, i.e., [domain = fun _ => True].) 3 - We apply these validity predicates on equalities and preorders to the types [COMPARABLE] and [S]. In this case, [domain]s are trivial and we consider orders (rather than general preorders). The main validity predicate of this file, [S.Valid.t], specifies that an inhabitant of [S] is valid when:

it is in the image of the functor [Make]

it is built from a valid preorder within the type [COMPARABLE]

The main result of this file, [S.valid_implies_equal_valid], is that any valid [S] specifies a valid equality.

Module Equal.
  Module Valid.

An equality [equal] is valid when it decides the standard equality [=].

    Definition t {a : Set} (domain : a → Prop) (equal : a → a → bool)
      : Prop :=
      ∀ x y,
      domain x → domain y →
      (x = y) ↔ (equal x y = true).

An equality function stays valid when restricted to a smaller domain.

    Lemma implies {a : Set} (domain1 domain2 : a → Prop) equal :
      (∀ x, domain2 x → domain1 x) →
      t domain1 equal →
      t domain2 equal.
    Proof.
      unfold t; intros.
      hauto lq: on rew: off.
    Qed.
  End Valid.

Definition of an equality function by projection to another equality function.

  Definition projection {a b : Set} (proj : a → b) (equal : b → b → bool) :
    a → a → bool :=
    fun x1 x2 ⇒
    equal (proj x1) (proj x2).

The projection to another equality function is valid.

  Lemma projection_is_valid {a b : Set} (proj : a → b) domain equal :
    Valid.t domain equal →
    (∀ x y, proj x = proj y → x = y) →
    Valid.t (fun x ⇒ domain (proj x)) (projection proj equal).
  Proof.
    unfold Valid.t, projection; intros.
    sfirstorder.
  Qed.

Definition of a equality function on a product [a1 * a2] given equality functions on [a1] and [a2].

  Definition couple {a1 a2 : Set}
    (equal1 : a1 → a1 → bool) (equal2 : a2 → a2 → bool) :
    (a1 × a2) → (a1 × a2) → bool :=
    fun '(x1, x2) '(y1, y2) ⇒
    equal1 x1 y1 && equal2 x2 y2.

The product equality [couple equal1 equal2] is valid on the product domain when [equal1] and [equal2] are valid. @Question: shouldn't we define the product domain as well?

  Lemma couple_is_valid {a1 a2 : Set}
    domain1 (equal1 : a1 → a1 → bool)
    domain2 (equal2 : a2 → a2 → bool) :
    Valid.t domain1 equal1 →
    Valid.t domain2 equal2 →
    Valid.t (fun '(x1, x2) ⇒ domain1 x1 ∧ domain2 x2) (couple equal1 equal2).
  Proof.
    unfold Valid.t, couple; intros.
    destruct x, y.
    split; intro.
    { hauto lq: on use: andb_true_intro. }
    { hauto lq: on rew: off use: andb_prop. }
  Qed.

The equality function in [int] is valid.

  Lemma int_is_valid :
    Valid.t (fun _ ⇒ True) Compare.Int.equal.
  Proof.
    unfold Valid.t.
    lia.
  Qed.
End Equal.

Restricts the set of results to { -1 , 0 , +1 }

Definition wrap_compare {a : Set} (compare : a → a → int) (x y : a) : int :=
  let res := compare x y in
  match res with
  | 0 ⇒ 0
  | _ ⇒
    if res >i 0 then
      1
    else
      -1
  end.

[lexicographic_one] allows inverting (in mock-code) [(x_a,x_b) < (y_a,y_b)] into [x_a < y_a \/ (x_a equiv y_a /\ x_b < y_b)]

Lemma lexicographic_one {a b : Set}
  {compare_a : a → a → _} {compare_b : b → b → _}
  {x_a y_a : a} {x_b y_b : b}
  : Compare.lexicographic compare_a compare_b (x_a, x_b) (y_a, y_b) = 1 →
    compare_a x_a y_a = 1 ∨ (compare_a x_a y_a = 0 ∧ compare_b x_b y_b = 1).
Proof.
  simpl.
  destruct (compare_a _ _); tauto.
Qed.

Definition projection {a b : Set} (proj : a → b) (compare : b → b → int) :
  a → a → int :=
  fun x1 x2 ⇒
    compare (proj x1) (proj x2).

Definition of the comparison as a pre-order on an equivalence relation.

Module Valid.

We consider two elements to be equivalent if their images using [f] are the same.

  Record t {a a' : Set}
    {domain : a → Prop} {f : a → a'} {compare : a → a → int} : Prop := {
    congruence_left x1 x2 y :
      domain x1 → domain x2 → domain y →
      f x1 = f x2 → compare x1 y = compare x2 y;
    image x y :
      domain x → domain y →
      match compare x y with
      | -1 | 0 | 1 ⇒ True
      | _ ⇒ False
      end;
    zero x y :
      domain x → domain y →
      compare x y = 0 → f x = f y;
    sym x y :
      domain x → domain y →
      compare x y = - compare y x;
    trans x y z :
      domain x → domain y → domain z →
      compare x y = 1 →
      compare y z = 1 →
      compare x z = 1;
  }.
  Arguments t {_ _}.

  Lemma refl {a a' : Set} {domain} {f : a → a'} {compare : a → a → int}
    (H : t domain f compare) (x : a) :
    domain x → compare x x = 0.
  Proof.
    sauto lq: on solve: lia.
  Qed.

  Lemma f_eq {a a' : Set} {domain} {f : a → a'} {compare : a → a → int}
    (H : t domain f compare) (x y : a) :
    domain x → domain y →
    f x = f y →
    compare x y = 0.
  Proof.
    intros.
    assert (compare x y = compare y y). {
      erewrite H.(congruence_left); sfirstorder.
    }
    erewrite <- refl; hauto lq: on.
  Qed.

  Lemma congruence_right {a a' : Set} {domain} {f : a → a'}
    {compare : a → a → int} :
    t domain f compare →
    ∀ (x y1 y2 : a),
    domain x → domain y1 → domain y2 →
    f y1 = f y2 → compare x y1 = compare x y2.
  Proof.
    sauto l: on.
  Qed.

  Lemma image_either {a a' : Set} {domain} {f : a → a'}
    {compare : a → a → int} :
    t domain f compare →
    ∀ x y,
    domain x → domain y →
    compare x y = -1 ∨ compare x y = 0 ∨ compare x y = 1.
  Proof.
    intros H x y H_x H_y.
    pose proof (H.(image) x y H_x H_y).
    hauto q: on.
  Qed.

  Lemma trans_lt {a a' : Set} {domain} {f : a → a'}
    {compare : a → a → int} :
    t domain f compare →
    ∀ x y z, domain x → domain y → domain z →
    compare x y = -1 →
    compare y z = -1 →
    compare x z = -1.
  Proof.
    intros.
    rewrite (sym H) in *; auto.
    rewrite <- Pos2Z.opp_pos in ×.
    rewrite Z.opp_inj_wd in ×.
    apply (trans H _ y); auto.
  Qed.

  Lemma less_neg1 {a : Set} {compare : a → a → int} :
    t (fun _ ⇒ True) (fun x ⇒ x) compare →
    ∀ k k', compare k k' < 0 → compare k k' = -1.
  Proof.
    intros Hv k k' Hkk'.
    destruct (compare k k') eqn:Hc; [lia|lia|].
    pose (Compare.Valid.image Hv k k' I I) as Him.
    rewrite Hc in Him.
    destruct p; tauto.
  Qed.

From a (possible) order function [compare : a -> a -> int], outputs the possible associated equality. @TODO use perhaps [Compare.Make] later, e.g., with [S.equal].

  Definition equal_of_compare {a : Set} (compare : a → a → int) (x y : a)
    : bool
    := Z.eqb (compare x y) 0.

@TODO spec

  (* Lemma Compare_Valid_id_implies_Equal_valid {a : Set}  {domain compare} :
    (t domain id compare) ->
     Equal.Valid.t domain (equal_of_compare compare). *)
  Lemma compare_valid_id_implies_equal_valid {a domain compare} :
    (@t a a domain id compare) →
     @Equal.Valid.t a domain (equal_of_compare compare).
  Proof.
    intros Hcomp.
    unfold equal_of_compare.
    intros x y Hx Hy. constructor ; intro H.
    { subst y.
      assert (H : compare x x = 0) by sauto q: on.
      rewrite H. reflexivity.
    }
    { inversion Hcomp as [cong_left image zero sym trans].
      apply Z.eqb_eq in H.
      apply zero ; assumption.
    }
  Qed.
End Valid.

The field [equal] of the functor [Compare.Make] is just [equal_of_compare] of the underlying [compare] function of a [C : COMPARABLE].

Lemma equal_equal_of_compare_eq {A} {C : COMPARABLE (t := A)} :
 Valid.equal_of_compare C.(Compare.COMPARABLE.compare) =
   (Compare.Make C).(Compare.S.equal).
Proof.
  unfold Valid.equal_of_compare, Compare.Make. reflexivity.
Qed.

[option] is an endofunctor on comparable type, i.e., from a comparable type + domain, [option] canonically defines a new comparable type + domain.

Lemma option_is_valid {a a' : Set} {domain} {f : a → a'}
  {compare : a → a → int} :
  Valid.t domain f compare →
  Valid.t
    (fun x ⇒
      match x with
      | None ⇒ True
      | Some x ⇒ domain x
      end
    )
    (Option.map f)
    (Compare.Option.compare compare).
Proof.
  intros.
  constructor; intros; destruct_all (option a); simpl in *; try easy.
  sauto lq: on rew: off.
  all: sfirstorder.
Qed.

The lexicographic preorder defined from two valid preorder is valid.

Lemma lexicographic_is_valid {a b a' b' : Set}
  {domain_a domain_b}
  {f_a : a → a'} {f_b : b → b'}
  {compare_a : a → a → int} {compare_b : b → b → int} :
  Valid.t domain_a f_a compare_a →
  Valid.t domain_b f_b compare_b →
  let domain '(x_a, x_b) := domain_a x_a ∧ domain_b x_b in
  let f '(x_a, x_b) := (f_a x_a, f_b x_b) in
  Valid.t domain f (Compare.lexicographic compare_a compare_b).
Proof.
  intros H_a H_b.
  constructor; unfold lexicographic; intros; destruct_all (a × b).
  { erewrite H_a.(Valid.congruence_left);
      try erewrite H_b.(Valid.congruence_left);
      try tauto;
      try congruence.
  }
  { match goal with
    | |- context[compare_a ?x ?y] ⇒
      pose proof (H_a.(Valid.image) a1 a0);
      destruct compare_a eqn:?;
      sfirstorder
    end.
  }
  { sauto lq: on rew: off. }
  { rewrite H_a.(Valid.sym); try rewrite H_b.(Valid.sym); try tauto.
    now destruct compare_a.
  }
  { repeat match goal with
    | [H : match _ with _ ⇒ _ end = 1 |- _] ⇒
      let H_zero := fresh "H_zero" in
      let H_one := fresh "H_one" in
      destruct (lexicographic_one H) as [H_one|[H_zero H_one]];
      clear H
    end.
    { match goal with
      | x1 : a, x2 : a, x3 : a |- _ ⇒
        now rewrite (H_a.(Valid.trans) x1 x2 x3)
      end.
    }
    { replace (compare_a a2 a0) with 1; trivial.
      match goal with
      | x1 : a, x2 : a, x3 : a |- _ ⇒
        rewrite (H_a.(Valid.congruence_left) x1 x2 x3)
      end; sfirstorder.
    }
    { replace (compare_a a2 a0) with 1; trivial.
      match goal with
      | x1 : a, x2 : a, x3 : a |- _ ⇒
        rewrite (Valid.congruence_right H_a x1 x2 x3)
      end; sfirstorder.
    }
    { replace (compare_a a2 a0) with 0.
      { match goal with
        | x1 : b, x2 : b, x3 : b |- _ ⇒
          rewrite (H_b.(Valid.trans) x1 x2 x3)
        end; sfirstorder.
      }
      { symmetry.
        apply (Valid.f_eq (domain := domain_a) (f := f_a)); try tauto.
        now repeat match goal with
        | x1 : a, x2 : a |- _ ⇒
          rewrite (H_a.(Valid.zero) x1 x2) by tauto
        end.
      }
    }
  }
Qed.

If two comparison functions [compare1] and [compare2] are equal on the same [domain], one is valid iff the other one is.

Lemma equality {a a' : Set}
  {domain : a → Prop} (compare1 compare2 : a → a → int) {f : a → a'} :
  (∀ x y,
    domain x → domain y →
    compare1 x y = compare2 x y
  ) →
  Valid.t domain f compare1 →
  Valid.t domain f compare2.
Proof.
  intros H_eq H_compare1.
  constructor; intros;
    repeat (rewrite <- H_eq in *; trivial); try now apply H_compare1.
  now apply H_compare1 with (y := y).
Qed.

Any projection function [f1] can be replaced with an extensionally equal function [f2] without modifyint the associated validity predicate.

Lemma equality_f {a a' : Set}
  {domain} {f1 f2 : a → a'} {compare : a → a → int} :
  Valid.t domain f1 compare →
  (∀ x, f1 x = f2 x) →
  Valid.t domain f2 compare.
Proof.
  constructor; intros.
  sauto lq: on rew: off.
  all: sfirstorder.
Qed.

Lemma implies {a b1 b2 : Set}
  {domain1 domain2 : a → Prop} {f1 : a → b1} {f2 : a → b2}
  {compare : a → a → int} :
  Valid.t domain1 f1 compare →
  (∀ x, domain2 x → domain1 x) →
  (∀ x1 x2, domain1 x1 → domain2 x2 →
    f1 x1 = f1 x2 ↔ f2 x1 = f2 x2) →
  Valid.t domain2 f2 compare.
Proof.
  intros H; intros; constructor; intros;
    try apply H; sfirstorder.
Qed.

Lemma projection_is_valid {a b c : Set}
  {domain_b} {f_b : b → c} {compare_b : b → b → int} (proj : a → b) :
  Valid.t domain_b f_b compare_b →
  let domain_a x :=
    domain_b (proj x) in
  let f_a x :=
    f_b (proj x) in
  let compare_a := projection proj compare_b in
  Valid.t domain_a f_a compare_a.
Proof.
  intros; constructor; sfirstorder.
Qed.

This lemma allows to cut off the rightmost [None]s from the given tuple of options.

This is helpful for proving the comparison of tuples of options, like [(None, None, Some x, None)] vs [(None, None, Some y, None)]. If right part is cut off, then we can just use [simpl] to continue working with the tuple which equals to the original tuple.

Lemma lexicographic_option_right_neutral {a b : Set}
  (compare1 : a → a → int) (compare2 : b → b → int) x y :
  Compare.lexicographic compare1 (Option.compare compare2) (x, None) (y, None) =
  compare1 x y.
Proof.
  hauto lq: on.
Qed.

Now, we prove that various usual types, as they are defined in `Compare` (i.e. as records), are valid.

[Compare.Unit] is a valid order.

Lemma unit_is_valid :
  Valid.t (fun _ ⇒ True) id Compare.Unit.(Compare.S.compare).
Proof.
  constructor; intros; try easy.
  now destruct_all unit.
Qed.

[Compare.Bool] is a valid order.

Lemma bool_is_valid :
  Valid.t (fun _ ⇒ True) id Compare.Bool.(Compare.S.compare).
Proof.
  constructor; intros;
    now repeat match goal with
    | [b : bool |- _] ⇒ destruct b
    end.
Qed.

[Compare.Z] is a valid order.

Lemma z_is_valid : Valid.t (fun _ ⇒ True) id Compare.Z.(Compare.S.compare).
Proof.
  constructor; unfold id;
    repeat match goal with
    | [|- ∀ (_ : int), _] ⇒ intro
    end;
    simpl; unfold Z.compare;
    sauto.
Qed.

[Compare.Int] is a valid order.

Lemma int_is_valid :
  Valid.t (fun _ ⇒ True) id Compare.Int.(Compare.S.compare).
Proof.
  exact z_is_valid.
Qed.

[Compare.Int32] is a valid order.

Lemma int32_is_valid :
  Valid.t (fun _ ⇒ True) id Compare.Int32.(Compare.S.compare).
Proof.
  exact z_is_valid.
Qed.

[Compare.64] is a valid order.

Lemma int64_is_valid :
  Valid.t (fun _ ⇒ True) id Compare.Int64.(Compare.S.compare).
Proof.
  exact z_is_valid.
Qed.

[Compare.String] is a valid order. @TODO Prove

Axiom string_is_valid :
  Valid.t (fun _ ⇒ True) id Compare.String.(Compare.S.compare).

Lemma wrap_compare_eq {a : Set}
  {domain} {f : a → a} {compare : a → a → int} :
  Valid.t domain f compare →
  ∀ x y,
  domain x → domain y →
  (wrap_compare compare) x y = compare x y.
Proof.
  unfold id, wrap_compare.
  intros H x y.
  assert (H_image := H.(Valid.image) x y).
  destruct (compare x y);
    try match goal with
    | [p : positive |- _] ⇒ destruct p
    end;
    tauto.
Qed.

Lemma wrap_compare_is_valid {a : Set}
  {domain} {f : a → a} {compare : a → a → int} :
  Valid.t domain f compare →
  Valid.t domain f (wrap_compare compare).
Proof.
  intros.
  apply (equality compare); trivial.
  intros.
  now rewrite (wrap_compare_eq (domain := domain) (f := f)).
Qed.

#[global] Hint Resolve
              option_is_valid
              lexicographic_is_valid
              unit_is_valid
              bool_is_valid
              z_is_valid
              int_is_valid
              int32_is_valid
              int64_is_valid
              string_is_valid
  : Compare_db.

Ltac valid_auto :=
  (* We try to solve the goal using the hints first *)
  (try now eauto 1 with Compare_db);

  (* If this doesn't help we start by unfolding the definition of the encoding
     we verify *)
  match goal with
  | [|- Valid.t _ _ ?compare] ⇒ try unfold compare
  end;
  eapply implies;
  repeat (
      simpl ||
      match goal with
      | [|- Valid.t _ _ (projection _ _)] ⇒ eapply projection_is_valid
      | [|- Valid.t _ _ (_ _)] ⇒
          first [
              eapply option_is_valid |
              eapply lexicographic_is_valid |
              eapply unit_is_valid |
              eapply bool_is_valid |
              eapply z_is_valid |
              eapply int_is_valid |
              eapply int32_is_valid |
              eapply int64_is_valid |
              eapply string_is_valid
            ]
      | _ ⇒ solve [eauto 1 with Compare_db]
      end
    );
  trivial; try tauto; try dtauto;
  try (intros []; tauto); try (intros []; dtauto).

Module COMPARABLE.
  Module Valid.

@TODO spec Note that we use only the *identity* function. Thus, validity pertains to *orders* only (and not *preorders* in general).

    Definition t {t} (C : Compare.COMPARABLE (t := t)) : Prop :=
      Valid.t (fun _ ⇒ True) id C.(Compare.COMPARABLE.compare).
  End Valid.
End COMPARABLE.

Module S.
  Definition to_COMPARABLE {t} (C : Compare.S (t := t))
    : Compare.COMPARABLE (t := t)
    := {|
      Compare.COMPARABLE.compare := C.(Compare.S.compare);
    |}.

  Module Eq.

[Eq.t C1 C2] when [C1] and [C2] can be identified (i.e. have the same fields).

    Record t {t} {C1 C2 : Compare.S (t := t)} : Prop := {
      op_eq x y : C1.(Compare.S.op_eq) x y = C2.(Compare.S.op_eq) x y;
      op_ltgt x y : C1.(Compare.S.op_ltgt) x y = C2.(Compare.S.op_ltgt) x y;
      op_lt x y : C1.(Compare.S.op_lt) x y = C2.(Compare.S.op_lt) x y;
      op_lteq x y : C1.(Compare.S.op_lteq) x y = C2.(Compare.S.op_lteq) x y;
      op_gteq x y : C1.(Compare.S.op_gteq) x y = C2.(Compare.S.op_gteq) x y;
      op_gt x y : C1.(Compare.S.op_gt) x y = C2.(Compare.S.op_gt) x y;
      equal x y : C1.(Compare.S.equal) x y = C2.(Compare.S.equal) x y;
      max x y : C1.(Compare.S.max) x y = C2.(Compare.S.max) x y;
      min x y : C1.(Compare.S.min) x y = C2.(Compare.S.min) x y;
    }.
    Arguments t {_}.
  End Eq.

  Module Valid.

Validity predicate for the type [S]. The field compare specifies that the field [compare] of [C] is a valid order. The field [eq] specifies that any [C : Compare.S] should be obtained via the functor [Make], i.e. all the fields of [C] can be computed from its fields [compare]

    Record t {t} {C : Compare.S (t := t)} : Prop := {
      compare : COMPARABLE.Valid.t (to_COMPARABLE C);
      is_Make : Eq.t C (Compare.Make (to_COMPARABLE C));
    }.
    Arguments t {_}.
  End Valid.

By default, the domain is trivial.

  Lemma valid_implies_equal_valid {t} {C : Compare.S (t := t)} :
    Valid.t C → (Equal.Valid.t (fun _ ⇒ True) C.(Compare.S.equal)).
  Proof.
    intro H.
    destruct H as [Hcomp His_Make].
    destruct His_Make.
    intros x y _ _.
    rewrite equal.
    rewrite <- equal_equal_of_compare_eq.
    (* [to_COMPARABLE] is just reading a record field. *)
    unfold to_COMPARABLE in × ; simpl in ×.
    apply @Valid.compare_valid_id_implies_equal_valid with (fun _ ⇒ True) ; easy.
    (* [COMPARABLE.Valid.t] is just a wrapper of the current goal. *)
  Qed.
End S.

This proof is already in the [Proofs/List.v] module, but we put it there to avoid circular dependencies.

Lemma length_is_valid {a : Set} (l : list a) :
  Pervasives.Int.Valid.t (List.length l).
Proof.
  induction l; simpl; lia.
Qed.

Module List_length_with.

The [List_length_with.op_eq] operator is like comparing the length.

  Lemma op_eq_eq {a : Set} (l : list a) (n : int) :
    Pervasives.Int.Valid.t n →
    List_length_with.op_eq l n =
    (List.length l =? n).
  Proof.
    generalize n; clear n.
    induction l; simpl; intros; [reflexivity|].
    rewrite IHl by lia.
    pose proof (length_is_valid l).
    lia.
  Qed.
End List_length_with.

Polymorphic comparison operators

The polymorphic equality is valid.

Axiom polymorphic_eq_is_valid :
  ∀ {a : Set},
    Equal.Valid.t (fun _ ⇒ True) (Compare.polymorphic_eq (a := a)).

A useful lemma for tests using the polymorphic equality.

Lemma polymorphic_eq_true : ∀ {a : Set} (v1 v2 : a),
  v1 = v2 →
  polymorphic_eq v1 v2 = true.
Proof.
  intros.
  now apply (polymorphic_eq_is_valid (a := a)).
Qed.

The polymorphic comparison is valid.

Axiom polymorphic_compare_is_valid :
  ∀ {a : Set},
  Valid.t (fun _ ⇒ True) id (Compare.polymorphic_compare (a := a)).