🍃 Either.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Environment.V8.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_a ⇒ domain_a x_a | Right x_b ⇒ domain_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_a ⇒ domain_a x_a | Right x_b ⇒ domain_b x_b end
  in
  let f_Either (x : Either.t a b) :=
    match x with Left x_a ⇒ Left (f_a x_a) | Right x_b ⇒ Right (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.