# 🍃 Either.v

Proofs

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

Require Import TezosOfOCaml.Environment.V7.
Require Import TezosOfOCaml.Environment.V7.Proofs.Compare.

The [equal] function over sums (Either) is valid as long as its parameters [eq_a, eq_b] are valid too.
Lemma equal_is_valid {a b : Set} (domain_a : a Prop) (domain_b : b Prop)
(eq_a : a a bool) (eq_b : b b bool) :
Compare.Equal.Valid.t domain_a eq_a
Compare.Equal.Valid.t domain_b eq_b
let domain_Either (x : Either.t a b) :=
match x with Left x_adomain_a x_a | Right x_bdomain_b x_b end
in
Compare.Equal.Valid.t domain_Either (Either.equal eq_a eq_b).
Proof.
unfold Equal.Valid.t.
intros H_eq_a H_eq_b x y H_x H_y.
split; revert y H_y.
{ destruct x; simpl; intros; destruct y; try discriminate; sauto lq: on.
}
{ destruct x; simpl; intros; destruct y; try discriminate; f_equal;
(apply H_eq_a in H || apply H_eq_b in H); assumption.
}
Qed.

The [compare] function over sums (Either) is valid as long as its parameters [eq_a, eq_b] are valid too.
Lemma compare_is_valid {a a' b b' : Set}
(domain_a : a Prop) (domain_b : b Prop)
(cmp_a : a a int) (cmp_b : b b int)
(f_a : a a') (f_b : b b') :
Compare.Valid.t domain_a f_a cmp_a
Compare.Valid.t domain_b f_b cmp_b
let domain_Either (x : Either.t a b) :=
match x with Left x_adomain_a x_a | Right x_bdomain_b x_b end
in
let f_Either (x : Either.t a b) :=
match x with Left x_aLeft (f_a x_a) | Right x_bRight (f_b x_b) end
in
Compare.Valid.t domain_Either f_Either (Either.compare cmp_a cmp_b).
Proof.
intros H_cmp_a H_cmp_b.
destruct H_cmp_a as [cong_l_a image_a zero_a sym_a trans_a],
H_cmp_b as [cong_l_b image_b zero_b sym_b trans_b].
constructor.
{ intros x1 x2 y domain_x1 domain_x2 domain_y f_eq.
destruct x1, x2, y; simpl; trivial; try discriminate; injection f_eq;
now (apply cong_l_a || apply cong_l_b).
(* instead of 'now (...)' we can also just use here 'intuition' *)
}
{ intros x y domain_x domain_y.
destruct x, y; simpl; trivial; now (apply image_a || apply image_b).
}
{ intros x y domain_x domain_y.
destruct x, y; simpl; intro eq_xy; try discriminate; f_equal;
now (apply zero_a || apply zero_b).
(* here we can also just end with 'intuition' *)
}
{ intros x y domain_x domain_y.
destruct x, y; simpl; trivial; intuition.
(* here example of using 'intuition'
instead of 'now (apply sym_a || apply sym_b)' *)

}
{ intros x y z domain_x domain_y domain_z.
destruct x, y, z; simpl; trivial; try discriminate;
now (apply trans_a || apply trans_b).
}
Qed.