GMuAnnot.CanonicalForms
Require Import GMuAnnot.Definitions.
Require Import GMuAnnot.Infrastructure.
Require Import GMuAnnot.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.
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.
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 T1 v1 T2 v2.
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.
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.
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.
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.
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.
Require Import GMuAnnot.Infrastructure.
Require Import GMuAnnot.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.
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.
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 T1 v1 T2 v2.
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.
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.
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.
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.
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.