🍬 Union.v

Proofs

Gitlab

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Compare.

Definition compare {l r : Set}
  (compare_l : l → l → int) (compare_r : r → r → int)
  (x y : Script_typed_ir.union l r)
  : int :=
  match x, y with
  | Script_typed_ir.L x, Script_typed_ir.L y ⇒
    compare_l x y
  | Script_typed_ir.L _, Script_typed_ir.R _ ⇒ -1
  | Script_typed_ir.R _, Script_typed_ir.L _ ⇒ 1
  | Script_typed_ir.R x, Script_typed_ir.R y ⇒
    compare_r x y
  end.

Lemma compare_is_valid {l r l' r' : Set}
  {f_l : l → l'} {f_r : r → r'}
  {compare_l : l → l → int} {compare_r : r → r → int}
  : Compare.Valid.t (fun _ ⇒ True) f_l compare_l →
    Compare.Valid.t (fun _ ⇒ True) f_r compare_r →
    let f x :=
      match x with
      | Script_typed_ir.L x_l ⇒ Script_typed_ir.L (f_l x_l)
      | Script_typed_ir.R x_r ⇒ Script_typed_ir.R (f_r x_r)
      end in
    Compare.Valid.t (fun _ ⇒ True) f (compare compare_l compare_r).
Proof.
  intros H_l H_r f.
  constructor; intros; destruct_all (Script_typed_ir.union l r); simpl in *;
    try easy; try apply H_l; try apply H_r; try congruence;
    try f_equal; try apply H_l; try apply H_r; trivial.
  match goal with
  | [v : l |- _] ⇒ now apply H_l with (y := v)
  end.
  match goal with
  | [v : r |- _] ⇒ now apply H_r with (y := v)
  end.
Qed.

Lemma compare_is_valid_identity {l r : Set}
  {compare_l : l → l → int} {compare_r : r → r → int}
  : Compare.Valid.t (fun _ ⇒ True) id compare_l →
    Compare.Valid.t (fun _ ⇒ True) id compare_r →
    Compare.Valid.t (fun _ ⇒ True) id (compare compare_l compare_r).
Proof.
  intros H_l H_r.
  eapply Compare.equality_f.
  eapply compare_is_valid; try apply H_l; try apply H_r.
  now intros [].
Qed.