🍬 Union.v

Proofs

Gitlab

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
  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}
  {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_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
    let P x :=
      match x with
      | Script_typed_ir.L x_l ⇒ P_l x_l
      | Script_typed_ir.R x_r ⇒ P_r x_r
      end in
    Compare.Valid.t P f (compare compare_l compare_r).
Proof.
  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)
  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.implies.
  eapply compare_is_valid; eauto.
  { now intros []. }
  { intros; simpl.
    destruct x1,x2; tauto.
  }
Qed.