# 🍃 Compare.v

Proofs

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 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 xdomain (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 xx) 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].
[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
| NoneTrue
| Some xdomain 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)).