GMu.CanonicalForms

Require Import GMu.Definitions.
Require Import GMu.Infrastructure.
Require Import GMu.Equations.
Require Import TLC.LibTactics.
Require Import TLC.LibEnv.
Require Import TLC.LibLN.

  (* Ht : {Σ, empty}⊢ trm_constructor Tparams Name e1 ∈ T1 ** T2 *)
Lemma CanonicalConstructorType : ∀ Σ Δ E Tparams Name Ctor e1 T,
    {Σ, Δ, E} ⊢(Treg) trm_constructor Tparams (Name, Ctor) e1 ∈ T →
    ∃ Typs, T = typ_gadt Typs Name.
Proof.
  introv Htyp.
  inversions Htyp.
  rewrite rewrite_open_tt_many_gadt.
  eexists.
  f_equal.
Qed.

Lemma CanonicalConstructorTypeGen : ∀ Σ Δ E Tparams Ctor e1 T,
    {Σ, Δ, E} ⊢(Treg) trm_constructor Tparams Ctor e1 ∈ T →
    ∃ Typs Name, T = typ_gadt Typs Name.
Proof.
  intros.
  destruct Ctor.
  apply CanonicalConstructorType in H; auto.
  destruct H as [Typs Heq].
  eexists. eexists. eauto.
Qed.

Local Hint Resolve CanonicalConstructorTypeGen.

Ltac contradictory_constructor_type :=
  lazymatch goal with
  | H: {?S, ?D, ?E} ⊢(?TT) trm_constructor ?Ts ?C ?e ∈ ?T |- _ ⇒
    apply CanonicalConstructorTypeGen in H;
    let Hcontradict := fresh "contradict" in
    destruct H as [? [? Hcontradict]];
    inversion Hcontradict
  end.

Lemma CanonicalFormTuple : ∀ Σ Δ e T1 T2,
    value e →
    {Σ, Δ, empty} ⊢(Treg) e ∈ T1 ** T2 →
    ∃ v1 v2, e = trm_tuple v1 v2.
Proof.
  introv Hv Ht.
  inversion Hv; inversion Ht; subst; eauto; try congruence.
  inversions H6.
  - false× binds_empty_inv.
  - contradictory_constructor_type.
Qed.

Lemma CanonicalFormAbs : ∀ Σ Δ e T1 T2,
    value e →
    {Σ, Δ, empty} ⊢(Treg) e ∈ T1 ==> T2 →
    ∃ v1, e = trm_abs T1 v1.
Proof.
  introv Hv Ht.
  inversion Hv; inversion Ht; subst; eauto; try congruence.
  - false× binds_empty_inv.
  - contradictory_constructor_type.
Qed.

Lemma CanonicalFormTAbs : ∀ Σ Δ e T,
    value e →
    {Σ, Δ, empty} ⊢(Treg) e ∈ typ_all T →
    ∃ v1, e = trm_tabs v1.
Proof.
  introv Hv Ht.
  inversion Hv; inversion Ht; subst; eauto; try congruence.
  - false× binds_empty_inv.
  - contradictory_constructor_type.
Qed.

Lemma CanonicalFormUnit : ∀ Σ Δ e,
    value e →
    {Σ, Δ, empty} ⊢(Treg) e ∈ typ_unit →
    e = trm_unit.
Proof.
  introv Hv Ht.
  inversion Hv; inversion Ht; subst; eauto; try congruence.
  - false× binds_empty_inv.
  - contradictory_constructor_type.
Qed.

Lemma CanonicalFormGadt : ∀ Σ Δ e Ts N,
    value e →
    {Σ, Δ, empty} ⊢(Treg) e ∈ typ_gadt Ts N →
    ∃ Ts' C v, e = trm_constructor Ts' (N, C) v.
Proof.
  introv Hv Ht.
  inversion Hv; inversion Ht; subst; eauto; try congruence.
  - false× binds_empty_inv.
  - rewrite rewrite_open_tt_many_gadt in H8.
    inversions H8.
    inversions H13.
    repeat eexists.
Qed.