🍃 Compare.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Pervasives.
Module Equal.
Module Valid.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Pervasives.
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).
: Prop :=
∀ x y,
domain x → domain y →
(x = y) ↔ (equal x y = true).
A equality function stays valid when there is an inclusion between the
domains.
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.
(∀ 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).
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.
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 couple given two equality
functions.
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.
(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 equlity from a couple of equality functions is valid.
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.
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.
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.
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).
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).
Valid.t (fun _ ⇒ True) Compare.Int.equal.
Proof.
unfold Valid.t.
lia.
Qed.
End Equal.
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.
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).
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.
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.
End Valid.
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.
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.
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.
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.
{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.
End Valid.
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.
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.
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.
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 cut right part, 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.
Lemma unit_is_valid :
Valid.t (fun _ ⇒ True) id Compare.Unit.(Compare.S.compare).
Proof.
constructor; intros; try easy.
now destruct_all unit.
Qed.
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.
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.
Lemma int_is_valid :
Valid.t (fun _ ⇒ True) id Compare.Int.(Compare.S.compare).
Proof.
exact z_is_valid.
Qed.
Lemma int32_is_valid :
Valid.t (fun _ ⇒ True) id Compare.Int32.(Compare.S.compare).
Proof.
exact z_is_valid.
Qed.
Lemma int64_is_valid :
Valid.t (fun _ ⇒ True) id Compare.Int64.(Compare.S.compare).
Proof.
exact z_is_valid.
Qed.
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 doens'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.
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.
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.
Record t {t} {C : Compare.S (t := t)} : Prop := {
compare : COMPARABLE.Valid.t (to_COMPARABLE C);
eq : Eq.t C (Compare.Make (to_COMPARABLE C));
}.
Arguments t {_}.
End Valid.
End S.
(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.
Lemma unit_is_valid :
Valid.t (fun _ ⇒ True) id Compare.Unit.(Compare.S.compare).
Proof.
constructor; intros; try easy.
now destruct_all unit.
Qed.
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.
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.
Lemma int_is_valid :
Valid.t (fun _ ⇒ True) id Compare.Int.(Compare.S.compare).
Proof.
exact z_is_valid.
Qed.
Lemma int32_is_valid :
Valid.t (fun _ ⇒ True) id Compare.Int32.(Compare.S.compare).
Proof.
exact z_is_valid.
Qed.
Lemma int64_is_valid :
Valid.t (fun _ ⇒ True) id Compare.Int64.(Compare.S.compare).
Proof.
exact z_is_valid.
Qed.
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 doens'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.
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.
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.
Record t {t} {C : Compare.S (t := t)} : Prop := {
compare : COMPARABLE.Valid.t (to_COMPARABLE C);
eq : Eq.t C (Compare.Make (to_COMPARABLE C));
}.
Arguments t {_}.
End Valid.
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.
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.
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.
Axiom polymorphic_eq_is_valid :
∀ {a : Set},
Equal.Valid.t (fun _ ⇒ True) (Compare.polymorphic_eq (a := a)).
∀ {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.
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)).
∀ {a : Set},
Valid.t (fun _ ⇒ True) id (Compare.polymorphic_compare (a := a)).