Skip to main content

🍬 Union.v



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

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

Require TezosOfOCaml.Environment.V8.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

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}
  {P_l P_r}
  : Compare.Valid.t P_l f_l compare_l
    Compare.Valid.t P_r f_r compare_r
    let f x :=
      match x with
      | Script_typed_ir.L x_lScript_typed_ir.L (f_l x_l)
      | Script_typed_ir.R x_rScript_typed_ir.R (f_r x_r)
      end in
    let P x :=
      match x with
      | Script_typed_ir.L x_lP_l x_l
      | Script_typed_ir.R x_rP_r x_r
      end in
    Compare.Valid.t P f (compare compare_l compare_r).
  intros H_l H_r f P.
  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)
  match goal with
  | [v : r |- _] ⇒ now apply H_r with (y := v)

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).
  intros H_l H_r.
  eapply Compare.implies.
  eapply compare_is_valid; eauto.
  { now intros []. }
  { intros; simpl.
    destruct x1,x2; tauto.