🍬 Ty.v

Proofs

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.Michocoq.syntax_type.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.Comparable_ty.

Set the metadata of a type to a default value.

Getting the canonical value of a type 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 : _ × _ |- _] ⇒ destruct x
    end; simpl;
    repeat rewrite Comparable_ty.get_canonical_is_involutive;
    repeat rewrite get_canonical_is_involutive;
    reflexivity.
Qed.

Definition to_memo_size :
  Alpha_context.Sapling.Memo_size.t → syntax_type.memo_size:=
  Z.to_nat. (* assuming memo_sizes are non-neg *)

Definition of_memo_size :
  syntax_type.memo_size → Alpha_context.Sapling.Memo_size.t :=
  Z.of_nat.

Lemma to_memo_of_memo : ∀ sz,
  to_memo_size (of_memo_size sz) = sz.
  exact Nat2Z.id.
Qed.

Lemma of_memo_to_memo : ∀ sz,
  0 ≤ sz → of_memo_size (to_memo_size sz) = sz.
  exact Z2Nat.id.
Qed.

Convert a type to Mi-Cho-Coq.

The [to_Michocoq] function does not depend on the metadata.

Fixpoint to_Michocoq_canonical_eq ty
  : to_Michocoq (get_canonical ty) = to_Michocoq ty.
Proof.
  destruct ty; try reflexivity; simpl;
  repeat rewrite Comparable_ty.to_Michocoq_canonical_eq;
  repeat rewrite to_Michocoq_canonical_eq;
  reflexivity.
Qed.

Import a type from Mi-Cho-Coq.

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).
Proof.
  destruct ty; simpl;
    repeat rewrite <- Comparable_ty.of_Michocoq_is_canonical;
    repeat rewrite <- of_Michocoq_is_canonical;
    try reflexivity.
    destruct_all syntax_type.simple_comparable_type; reflexivity.
Qed.

[to_Michocoq] is the inverse of [of_Michocoq].

[of_Michocoq] is the inverse of [to_Michocoq].

Fixpoint of_Michocoq_to_Michocoq ty
  : all_memo_sizes_nonneg ty →
    match to_Michocoq ty with
    | Some ty' ⇒ of_Michocoq ty' = get_canonical ty
    | None ⇒ True
    end.
Proof.
  intro nn.
  destruct ty; simpl; trivial;
    repeat match goal with
    | [x : _ × _ |- _] ⇒ destruct x
    end; simpl;
    repeat match goal with
    | [ty : _ |- _] ⇒
      let H := fresh "H" in
      (
        (assert (H := Comparable_ty.of_Michocoq_to_Michocoq ty);
        destruct (Comparable_ty.to_Michocoq ty)) ||
        (assert (H := of_Michocoq_to_Michocoq ty);
        destruct (to_Michocoq ty))
      );
      revert ty H;
      simpl; trivial
    end;
    try congruence.
  { destruct nn as [nn1 nn2].
    destruct (to_Michocoq ty1) eqn:G1;
    destruct (to_Michocoq ty2) eqn:G2; simpl; try tauto.
    pose (of_Michocoq_to_Michocoq ty1 nn1) as IH1.
    pose (of_Michocoq_to_Michocoq ty2 nn2) as IH2.
    rewrite G1 in IH1.
    rewrite G2 in IH2.
    congruence.
  }
  { destruct nn as [nn1 nn2].
    destruct (to_Michocoq ty1) eqn:G1;
    destruct (to_Michocoq ty2) eqn:G2; simpl; try tauto.
    pose (of_Michocoq_to_Michocoq _ nn1) as IH1.
    pose (of_Michocoq_to_Michocoq _ nn2) as IH2.
    rewrite G1 in IH1.
    rewrite G2 in IH2.
    congruence.
  }
  { destruct nn as [nn1 nn2].
    destruct (to_Michocoq ty1) eqn:G1;
    destruct (to_Michocoq ty2) eqn:G2; simpl; try tauto.
    pose (of_Michocoq_to_Michocoq _ nn1) as IH1.
    pose (of_Michocoq_to_Michocoq _ nn2) as IH2.
    rewrite G1 in IH1.
    rewrite G2 in IH2.
    congruence.
  }
  { destruct (to_Michocoq ty) eqn:G; simpl; try tauto.
    f_equal.
    simpl in nn.
    pose (of_Michocoq_to_Michocoq _ nn) as IH.
    rewrite G in IH; auto.
  }
  { destruct (to_Michocoq ty) eqn:G; simpl; try tauto.
    f_equal.
    simpl in nn.
    pose (of_Michocoq_to_Michocoq _ nn) as IH.
    rewrite G in IH; auto.
  }
  { destruct Comparable_ty.to_Michocoq eqn:?; simpl; trivial.
    now erewrite Comparable_ty.of_Michocoq_to_Michocoq.
  }
  { destruct Comparable_ty.to_Michocoq eqn:?; simpl; trivial.
    destruct (to_Michocoq ty) eqn:G; simpl; try tauto.
    erewrite Comparable_ty.of_Michocoq_to_Michocoq by eassumption.
    f_equal; try apply Comparable_ty.of_Michocoq_to_Michocoq.
    pose (of_Michocoq_to_Michocoq ty nn) as IH.
    rewrite G in IH; auto.
  }
  { destruct Comparable_ty.to_Michocoq eqn:?; simpl; trivial.
    destruct (to_Michocoq ty) eqn:G; simpl; try tauto.
    erewrite Comparable_ty.of_Michocoq_to_Michocoq by eassumption.
    f_equal; try apply Comparable_ty.of_Michocoq_to_Michocoq.
    pose (of_Michocoq_to_Michocoq ty nn) as IH.
    rewrite G in IH; auto.
  }
  { destruct (to_Michocoq ty) eqn:G; simpl; try tauto.
    f_equal; try apply Comparable_ty.of_Michocoq_to_Michocoq.
    pose (of_Michocoq_to_Michocoq ty nn) as IH.
    rewrite G in IH; auto.
  }
  { f_equal. apply of_memo_to_memo; exact nn. }
  { f_equal. apply of_memo_to_memo; exact nn. }
  { destruct Comparable_ty.to_Michocoq eqn:?; simpl; trivial.
    now erewrite Comparable_ty.of_Michocoq_to_Michocoq.
  }
Qed.