Skip to main content

🍬 Comparable_ty.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 Import TezosOfOCaml.Proto_alpha.Simulations.Script_typed_ir.

Require TezosOfOCaml.Proto_alpha.Michocoq.syntax_type.

Compute the [Set] representing a [Script_typed_ir.ty].
Get the canonical form of a comparable type, erasing the metadata.
Fixpoint get_canonical (ty : Script_typed_ir.ty)
  : Script_typed_ir.ty :=
  match ty with
  | Script_typed_ir.Unit_t
    Script_typed_ir.Unit_t
  | Script_typed_ir.Never_t
    Script_typed_ir.Never_t
  | Script_typed_ir.Int_t
    Script_typed_ir.Int_t
  | Script_typed_ir.Nat_t
    Script_typed_ir.Nat_t
  | Script_typed_ir.Signature_t
    Script_typed_ir.Signature_t
  | Script_typed_ir.String_t
    Script_typed_ir.String_t
  | Script_typed_ir.Bytes_t
    Script_typed_ir.Bytes_t
  | Script_typed_ir.Mutez_t
    Script_typed_ir.Mutez_t
  | Script_typed_ir.Bool_t
    Script_typed_ir.Bool_t
  | Script_typed_ir.Key_hash_t
    Script_typed_ir.Key_hash_t
  | Script_typed_ir.Key_t
    Script_typed_ir.Key_t
  | Script_typed_ir.Timestamp_t
    Script_typed_ir.Timestamp_t
  | Script_typed_ir.Chain_id_t
    Script_typed_ir.Chain_id_t
  | Script_typed_ir.Address_t
    Script_typed_ir.Address_t
  | Script_typed_ir.Tx_rollup_l2_address_t
    Script_typed_ir.Tx_rollup_l2_address_t
  | Script_typed_ir.Pair_t ty1 ty2 _ _
    let ty1 := get_canonical ty1 in
    let ty2 := get_canonical ty2 in
    Script_typed_ir.Pair_t ty1 ty2 Ty_metadata.default Dependent_bool.YesYes
  | Script_typed_ir.Union_t ty1 ty2 _ _
    let ty1 := get_canonical ty1 in
    let ty2 := get_canonical ty2 in
    Script_typed_ir.Union_t ty1 ty2 Ty_metadata.default Dependent_bool.YesYes
  | Script_typed_ir.Option_t ty _ _
    let ty := get_canonical ty in
    Script_typed_ir.Option_t ty Ty_metadata.default Dependent_bool.Yes
  | _Script_typed_ir.Unit_t
  end.

Getting a canonical term is involutive.
Fixpoint get_canonical_is_involutive ty
  : get_canonical (get_canonical ty) = get_canonical ty.
  destruct ty; try reflexivity; simpl;
    repeat match goal with
    | [x : Script_typed_ir.ty × _ |- _] ⇒ destruct x
    end;
    simpl; now repeat rewrite get_canonical_is_involutive.
Qed.

Convert the comparable types to Mi-Cho-Coq for the case of simple comparable types. This does not cover all the cases so we use an option type.
The [to_Michocoq_simple] function does not depend on the metadata.
Lemma to_Michocoq_simple_canonical_eq ty
  : to_Michocoq_simple (get_canonical ty) = to_Michocoq_simple ty.
Proof.
  destruct ty; try reflexivity; simpl;
    now repeat match goal with
    | [x : _ × _ |- _] ⇒ destruct x
    end.
Qed.

Import a simple comparable type from Mi-Cho-Coq, using the default metadata.
The function [of_Michocoq_simple] produces terms which are already in a canonical form.
Lemma of_Michocoq_simple_is_canonical ty
  : of_Michocoq_simple ty = get_canonical (of_Michocoq_simple ty).
Proof.
  destruct ty; reflexivity.
Qed.

[to_Michocoq_simple] is the inverse of [of_Michocoq_simple].
Lemma to_Michocoq_simple_of_Michocoq_simple ty
  : to_Michocoq_simple (of_Michocoq_simple ty) = Some ty.
Proof.
  destruct ty; reflexivity.
Qed.

[of_Michocoq_simple] is the inverse of [to_Michocoq_simple].
Lemma of_Michocoq_simple_to_Michocoq_simple ty
  : match to_Michocoq_simple ty with
    | Some ty'of_Michocoq_simple ty' = get_canonical ty
    | NoneTrue
    end.
Proof.
  destruct ty; try exact I; reflexivity.
Qed.

Convert comparable types to Mi-Cho-Coq. We use an option type for the cases which are not covered.
Fixpoint to_Michocoq (ty : Script_typed_ir.ty)
  : option syntax_type.comparable_type :=
  match ty with
  | Script_typed_ir.Unit_t
    Some (syntax_type.Comparable_type_simple syntax_type.unit)
  | Script_typed_ir.Never_t
    Some (syntax_type.Comparable_type_simple syntax_type.never)
  | Script_typed_ir.Int_t
    Some (syntax_type.Comparable_type_simple syntax_type.int)
  | Script_typed_ir.Nat_t
    Some (syntax_type.Comparable_type_simple syntax_type.nat)
  | Script_typed_ir.Signature_t
    Some (syntax_type.Comparable_type_simple syntax_type.signature)
  | Script_typed_ir.String_t
    Some (syntax_type.Comparable_type_simple syntax_type.string)
  | Script_typed_ir.Bytes_t
    Some (syntax_type.Comparable_type_simple syntax_type.bytes)
  | Script_typed_ir.Mutez_t
    Some (syntax_type.Comparable_type_simple syntax_type.mutez)
  | Script_typed_ir.Bool_t
    Some (syntax_type.Comparable_type_simple syntax_type.bool)
  | Script_typed_ir.Key_hash_t
    Some (syntax_type.Comparable_type_simple syntax_type.key_hash)
  | Script_typed_ir.Key_t
    Some (syntax_type.Comparable_type_simple syntax_type.key)
  | Script_typed_ir.Timestamp_t
    Some (syntax_type.Comparable_type_simple syntax_type.timestamp)
  | Script_typed_ir.Chain_id_t
    Some (syntax_type.Comparable_type_simple syntax_type.chain_id)
  | Script_typed_ir.Address_t
    Some (syntax_type.Comparable_type_simple syntax_type.address)
  | Script_typed_ir.Tx_rollup_l2_address_tNone
  | Script_typed_ir.Pair_t ty1 ty2 _ _
    let× ty1 := to_Michocoq ty1 in
    let× ty2 := to_Michocoq ty2 in
    Some (syntax_type.Cpair ty1 ty2)
  | Script_typed_ir.Union_t ty1 ty2 _ _
    let× ty1 := to_Michocoq ty1 in
    let× ty2 := to_Michocoq ty2 in
    Some (syntax_type.Cor ty1 ty2)
  | Script_typed_ir.Option_t ty _ _
    let× ty := to_Michocoq ty in
    Some (syntax_type.Coption ty)
  | _Some (syntax_type.Comparable_type_simple syntax_type.unit)
  end.

The [to_Michocoq] function does not depend on the metadata.
Fixpoint to_Michocoq_canonical_eq ty
  : to_Michocoq (get_canonical ty) = to_Michocoq ty.
  destruct ty; try reflexivity; simpl;
  repeat rewrite to_Michocoq_canonical_eq;
  reflexivity.
Qed.

Import a comparable type from Mi-Cho-Coq, using the default metadata.
The function [of_Michocoq] produces terms which are already in a canonical form.
Fixpoint of_Michocoq_is_canonical ty
  : of_Michocoq ty = get_canonical (of_Michocoq ty).
  destruct ty; simpl; f_equal;
  try apply of_Michocoq_is_canonical.
  apply of_Michocoq_simple_is_canonical.
Qed.

Lemma to_Michocoq_simple_of_Michocoq : ty ty', to_Michocoq_simple (of_Michocoq ty) = Some ty'
   ty = syntax_type.Comparable_type_simple ty'.
  induction ty; simpl; intros ty' Heq.
Proof.
  { rewrite to_Michocoq_simple_of_Michocoq_simple in Heq.
    inversion Heq; reflexivity. }
  { discriminate. }
  { discriminate. }
  { discriminate. }
Qed.

[to_Michocoq] is the inverse of [of_Michocoq].
Fixpoint to_Michocoq_of_Michocoq ty
  : to_Michocoq (of_Michocoq ty) = Some ty.
  destruct ty; simpl; sauto lq: on.
Qed.

[of_Michocoq] is the inverse of [to_Michocoq].
Fixpoint of_Michocoq_to_Michocoq_match ty :
  match to_Michocoq ty with
  | Some ty'of_Michocoq ty' = get_canonical ty
  | NoneTrue
  end.
Proof.
  destruct ty; simpl; try reflexivity; hfcrush.
Qed.

Lemma of_Michocoq_to_Michocoq ty ty' :
  to_Michocoq ty = Some ty'
  of_Michocoq ty' = get_canonical ty.
Proof.
  hfcrush use: of_Michocoq_to_Michocoq_match.
Qed.