Definitions
Require Import Bool.
Require Import Metalib.Metatheory.
Require Import List.
Require Import Ott.ott_list_core.
Require Import Metalib.Metatheory.
Require Import List.
Require Import Ott.ott_list_core.
syntax
Definition ivar : Set := var. Definition constant : Set := nat. Definition blamelabel : Set := nat.
Inductive typ : Set :=
| typ_def (D:dtyp)
| typ_null (D:dtyp)
with dtyp : Set :=
| dtyp_base : dtyp
| dtyp_arrow (A:typ) (B:typ) .
Inductive label : Set :=
| label_name (bl:blamelabel)
| label_not_label (bl:blamelabel) .
Inductive ityp : Set :=
| ityp_base : ityp
| ityp_arrow (iA:ityp) (iB:ityp) .
Inductive trm : Set :=
| t_var_b (_:nat)
| t_var_f (x:var)
| t_const (c:constant)
| t_binop (M:trm) (N:trm)
| t_abs (A:typ) (N:trm)
| t_app (L:trm) (M:trm)
| t_null : trm
| t_lift (M:trm)
| t_case (L:trm) (M:trm) (N:trm)
| t_cast (M:trm) (A:typ) (p:label) (B:typ)
| t_blame (p:label) .
Inductive itrm : Set :=
| itrm_var_b (_:nat)
| itrm_var_f (ix:ivar)
| itrm_const (c:constant)
| itrm_binop (iM:itrm) (iN:itrm)
| itrm_abs (iA:ityp) (iN:itrm)
| itrm_app (iL:itrm) (iM:itrm)
| itrm_null : itrm .
Inductive ctrm : Set :=
| ctrm_hole : ctrm
| ctrm_binop_left (CM:ctrm) (N:trm)
| ctrm_binop_right (M:trm) (CN:ctrm)
| ctrm_abs (A:typ) (CN:ctrm)
| ctrm_app_left (CL:ctrm) (M:trm)
| ctrm_app_right (L:trm) (CM:ctrm)
| ctrm_lift (CM:ctrm)
| ctrm_case_scrutinee (CL:ctrm) (M:trm) (N:trm)
| ctrm_case_null (L:trm) (CM:ctrm) (N:trm)
| ctrm_case_nonnull (L:trm) (M:trm) (CN:ctrm)
| ctrm_cast (CM:ctrm) (A:typ) (p:label) (B:typ) .
Inductive ictrm : Set :=
| ictrm_hole : ictrm
| ictrm_binop_left (iCM:ictrm) (iN:itrm)
| ictrm_binop_right (iM:itrm) (iCN:ictrm)
| ictrm_abs (iA:ityp) (iCN:ictrm)
| ictrm_app_left (iCL:ictrm) (iM:itrm)
| ictrm_app_right (iL:itrm) (iCM:ictrm) .
Definition ictx : Set := list ( atom × ityp ).
Definition ctx : Set := list ( atom × typ ).
Inductive typ : Set :=
| typ_def (D:dtyp)
| typ_null (D:dtyp)
with dtyp : Set :=
| dtyp_base : dtyp
| dtyp_arrow (A:typ) (B:typ) .
Inductive label : Set :=
| label_name (bl:blamelabel)
| label_not_label (bl:blamelabel) .
Inductive ityp : Set :=
| ityp_base : ityp
| ityp_arrow (iA:ityp) (iB:ityp) .
Inductive trm : Set :=
| t_var_b (_:nat)
| t_var_f (x:var)
| t_const (c:constant)
| t_binop (M:trm) (N:trm)
| t_abs (A:typ) (N:trm)
| t_app (L:trm) (M:trm)
| t_null : trm
| t_lift (M:trm)
| t_case (L:trm) (M:trm) (N:trm)
| t_cast (M:trm) (A:typ) (p:label) (B:typ)
| t_blame (p:label) .
Inductive itrm : Set :=
| itrm_var_b (_:nat)
| itrm_var_f (ix:ivar)
| itrm_const (c:constant)
| itrm_binop (iM:itrm) (iN:itrm)
| itrm_abs (iA:ityp) (iN:itrm)
| itrm_app (iL:itrm) (iM:itrm)
| itrm_null : itrm .
Inductive ctrm : Set :=
| ctrm_hole : ctrm
| ctrm_binop_left (CM:ctrm) (N:trm)
| ctrm_binop_right (M:trm) (CN:ctrm)
| ctrm_abs (A:typ) (CN:ctrm)
| ctrm_app_left (CL:ctrm) (M:trm)
| ctrm_app_right (L:trm) (CM:ctrm)
| ctrm_lift (CM:ctrm)
| ctrm_case_scrutinee (CL:ctrm) (M:trm) (N:trm)
| ctrm_case_null (L:trm) (CM:ctrm) (N:trm)
| ctrm_case_nonnull (L:trm) (M:trm) (CN:ctrm)
| ctrm_cast (CM:ctrm) (A:typ) (p:label) (B:typ) .
Inductive ictrm : Set :=
| ictrm_hole : ictrm
| ictrm_binop_left (iCM:ictrm) (iN:itrm)
| ictrm_binop_right (iM:itrm) (iCN:ictrm)
| ictrm_abs (iA:ityp) (iCN:ictrm)
| ictrm_app_left (iCL:ictrm) (iM:itrm)
| ictrm_app_right (iL:itrm) (iCM:ictrm) .
Definition ictx : Set := list ( atom × ityp ).
Definition ctx : Set := list ( atom × typ ).
auxiliary functions on the new list types library functions subrules
Definition is_adtyp_of_dtyp (D5:dtyp) : bool :=
match D5 with
| dtyp_base ⇒ false
| (dtyp_arrow A B) ⇒ (true)
end.
Definition is_atyp_of_typ (A5:typ) : bool :=
match A5 with
| (typ_def D) ⇒ ((is_adtyp_of_dtyp D))
| (typ_null D) ⇒ false
end.
Fixpoint is_val_of_trm (L5:trm) : bool :=
match L5 with
| (t_var_b nat) ⇒ false
| (t_var_f x) ⇒ false
| (t_const c) ⇒ (true)
| (t_binop M N) ⇒ false
| (t_abs A N) ⇒ (true)
| (t_app L M) ⇒ false
| t_null ⇒ (true)
| (t_lift M) ⇒ ((is_val_of_trm M))
| (t_case L M N) ⇒ false
| (t_cast M A p B) ⇒ ((is_val_of_trm M) && (is_atyp_of_typ A) && (is_atyp_of_typ B))
| (t_blame p) ⇒ false
end.
match D5 with
| dtyp_base ⇒ false
| (dtyp_arrow A B) ⇒ (true)
end.
Definition is_atyp_of_typ (A5:typ) : bool :=
match A5 with
| (typ_def D) ⇒ ((is_adtyp_of_dtyp D))
| (typ_null D) ⇒ false
end.
Fixpoint is_val_of_trm (L5:trm) : bool :=
match L5 with
| (t_var_b nat) ⇒ false
| (t_var_f x) ⇒ false
| (t_const c) ⇒ (true)
| (t_binop M N) ⇒ false
| (t_abs A N) ⇒ (true)
| (t_app L M) ⇒ false
| t_null ⇒ (true)
| (t_lift M) ⇒ ((is_val_of_trm M))
| (t_case L M N) ⇒ false
| (t_cast M A p B) ⇒ ((is_val_of_trm M) && (is_atyp_of_typ A) && (is_atyp_of_typ B))
| (t_blame p) ⇒ false
end.
arities opening up abstractions
Fixpoint open_itrm_wrt_itrm_rec (k:nat) (iL5:itrm) (iL_6:itrm) {struct iL_6}: itrm :=
match iL_6 with
| (itrm_var_b nat) ⇒
match lt_eq_lt_dec nat k with
| inleft (left _) ⇒ itrm_var_b nat
| inleft (right _) ⇒ iL5
| inright _ ⇒ itrm_var_b (nat - 1)
end
| (itrm_var_f ix) ⇒ itrm_var_f ix
| (itrm_const c) ⇒ itrm_const c
| (itrm_binop iM iN) ⇒ itrm_binop (open_itrm_wrt_itrm_rec k iL5 iM) (open_itrm_wrt_itrm_rec k iL5 iN)
| (itrm_abs iA iN) ⇒ itrm_abs iA (open_itrm_wrt_itrm_rec (S k) iL5 iN)
| (itrm_app iL iM) ⇒ itrm_app (open_itrm_wrt_itrm_rec k iL5 iL) (open_itrm_wrt_itrm_rec k iL5 iM)
| itrm_null ⇒ itrm_null
end.
Fixpoint open_trm_wrt_trm_rec (k:nat) (L5:trm) (L_6:trm) {struct L_6}: trm :=
match L_6 with
| (t_var_b nat) ⇒
match lt_eq_lt_dec nat k with
| inleft (left _) ⇒ t_var_b nat
| inleft (right _) ⇒ L5
| inright _ ⇒ t_var_b (nat - 1)
end
| (t_var_f x) ⇒ t_var_f x
| (t_const c) ⇒ t_const c
| (t_binop M N) ⇒ t_binop (open_trm_wrt_trm_rec k L5 M) (open_trm_wrt_trm_rec k L5 N)
| (t_abs A N) ⇒ t_abs A (open_trm_wrt_trm_rec (S k) L5 N)
| (t_app L M) ⇒ t_app (open_trm_wrt_trm_rec k L5 L) (open_trm_wrt_trm_rec k L5 M)
| t_null ⇒ t_null
| (t_lift M) ⇒ t_lift (open_trm_wrt_trm_rec k L5 M)
| (t_case L M N) ⇒ t_case (open_trm_wrt_trm_rec k L5 L) (open_trm_wrt_trm_rec k L5 M) (open_trm_wrt_trm_rec (S k) L5 N)
| (t_cast M A p B) ⇒ t_cast (open_trm_wrt_trm_rec k L5 M) A p B
| (t_blame p) ⇒ t_blame p
end.
Fixpoint open_ictrm_wrt_itrm_rec (k:nat) (iL5:itrm) (iCL5:ictrm) {struct iCL5}: ictrm :=
match iCL5 with
| ictrm_hole ⇒ ictrm_hole
| (ictrm_binop_left iCM iN) ⇒ ictrm_binop_left (open_ictrm_wrt_itrm_rec k iL5 iCM) (open_itrm_wrt_itrm_rec k iL5 iN)
| (ictrm_binop_right iM iCN) ⇒ ictrm_binop_right (open_itrm_wrt_itrm_rec k iL5 iM) (open_ictrm_wrt_itrm_rec k iL5 iCN)
| (ictrm_abs iA iCN) ⇒ ictrm_abs iA (open_ictrm_wrt_itrm_rec (S k) iL5 iCN)
| (ictrm_app_left iCL iM) ⇒ ictrm_app_left (open_ictrm_wrt_itrm_rec k iL5 iCL) (open_itrm_wrt_itrm_rec k iL5 iM)
| (ictrm_app_right iL iCM) ⇒ ictrm_app_right (open_itrm_wrt_itrm_rec k iL5 iL) (open_ictrm_wrt_itrm_rec k iL5 iCM)
end.
Fixpoint open_ctrm_wrt_trm_rec (k:nat) (L5:trm) (CL5:ctrm) {struct CL5}: ctrm :=
match CL5 with
| ctrm_hole ⇒ ctrm_hole
| (ctrm_binop_left CM N) ⇒ ctrm_binop_left (open_ctrm_wrt_trm_rec k L5 CM) (open_trm_wrt_trm_rec k L5 N)
| (ctrm_binop_right M CN) ⇒ ctrm_binop_right (open_trm_wrt_trm_rec k L5 M) (open_ctrm_wrt_trm_rec k L5 CN)
| (ctrm_abs A CN) ⇒ ctrm_abs A (open_ctrm_wrt_trm_rec (S k) L5 CN)
| (ctrm_app_left CL M) ⇒ ctrm_app_left (open_ctrm_wrt_trm_rec k L5 CL) (open_trm_wrt_trm_rec k L5 M)
| (ctrm_app_right L CM) ⇒ ctrm_app_right (open_trm_wrt_trm_rec k L5 L) (open_ctrm_wrt_trm_rec k L5 CM)
| (ctrm_lift CM) ⇒ ctrm_lift (open_ctrm_wrt_trm_rec k L5 CM)
| (ctrm_case_scrutinee CL M N) ⇒ ctrm_case_scrutinee (open_ctrm_wrt_trm_rec k L5 CL) (open_trm_wrt_trm_rec k L5 M) (open_trm_wrt_trm_rec (S k) L5 N)
| (ctrm_case_null L CM N) ⇒ ctrm_case_null (open_trm_wrt_trm_rec k L5 L) (open_ctrm_wrt_trm_rec k L5 CM) (open_trm_wrt_trm_rec (S k) L5 N)
| (ctrm_case_nonnull L M CN) ⇒ ctrm_case_nonnull (open_trm_wrt_trm_rec k L5 L) (open_trm_wrt_trm_rec k L5 M) (open_ctrm_wrt_trm_rec (S k) L5 CN)
| (ctrm_cast CM A p B) ⇒ ctrm_cast (open_ctrm_wrt_trm_rec k L5 CM) A p B
end.
Definition open_ictrm_wrt_itrm iL5 iCL5 := open_ictrm_wrt_itrm_rec 0 iCL5 iL5.
Definition open_ctrm_wrt_trm L5 CL5 := open_ctrm_wrt_trm_rec 0 CL5 L5.
Definition open_itrm_wrt_itrm iL5 iL_6 := open_itrm_wrt_itrm_rec 0 iL_6 iL5.
Definition open_trm_wrt_trm L5 L_6 := open_trm_wrt_trm_rec 0 L_6 L5.
match iL_6 with
| (itrm_var_b nat) ⇒
match lt_eq_lt_dec nat k with
| inleft (left _) ⇒ itrm_var_b nat
| inleft (right _) ⇒ iL5
| inright _ ⇒ itrm_var_b (nat - 1)
end
| (itrm_var_f ix) ⇒ itrm_var_f ix
| (itrm_const c) ⇒ itrm_const c
| (itrm_binop iM iN) ⇒ itrm_binop (open_itrm_wrt_itrm_rec k iL5 iM) (open_itrm_wrt_itrm_rec k iL5 iN)
| (itrm_abs iA iN) ⇒ itrm_abs iA (open_itrm_wrt_itrm_rec (S k) iL5 iN)
| (itrm_app iL iM) ⇒ itrm_app (open_itrm_wrt_itrm_rec k iL5 iL) (open_itrm_wrt_itrm_rec k iL5 iM)
| itrm_null ⇒ itrm_null
end.
Fixpoint open_trm_wrt_trm_rec (k:nat) (L5:trm) (L_6:trm) {struct L_6}: trm :=
match L_6 with
| (t_var_b nat) ⇒
match lt_eq_lt_dec nat k with
| inleft (left _) ⇒ t_var_b nat
| inleft (right _) ⇒ L5
| inright _ ⇒ t_var_b (nat - 1)
end
| (t_var_f x) ⇒ t_var_f x
| (t_const c) ⇒ t_const c
| (t_binop M N) ⇒ t_binop (open_trm_wrt_trm_rec k L5 M) (open_trm_wrt_trm_rec k L5 N)
| (t_abs A N) ⇒ t_abs A (open_trm_wrt_trm_rec (S k) L5 N)
| (t_app L M) ⇒ t_app (open_trm_wrt_trm_rec k L5 L) (open_trm_wrt_trm_rec k L5 M)
| t_null ⇒ t_null
| (t_lift M) ⇒ t_lift (open_trm_wrt_trm_rec k L5 M)
| (t_case L M N) ⇒ t_case (open_trm_wrt_trm_rec k L5 L) (open_trm_wrt_trm_rec k L5 M) (open_trm_wrt_trm_rec (S k) L5 N)
| (t_cast M A p B) ⇒ t_cast (open_trm_wrt_trm_rec k L5 M) A p B
| (t_blame p) ⇒ t_blame p
end.
Fixpoint open_ictrm_wrt_itrm_rec (k:nat) (iL5:itrm) (iCL5:ictrm) {struct iCL5}: ictrm :=
match iCL5 with
| ictrm_hole ⇒ ictrm_hole
| (ictrm_binop_left iCM iN) ⇒ ictrm_binop_left (open_ictrm_wrt_itrm_rec k iL5 iCM) (open_itrm_wrt_itrm_rec k iL5 iN)
| (ictrm_binop_right iM iCN) ⇒ ictrm_binop_right (open_itrm_wrt_itrm_rec k iL5 iM) (open_ictrm_wrt_itrm_rec k iL5 iCN)
| (ictrm_abs iA iCN) ⇒ ictrm_abs iA (open_ictrm_wrt_itrm_rec (S k) iL5 iCN)
| (ictrm_app_left iCL iM) ⇒ ictrm_app_left (open_ictrm_wrt_itrm_rec k iL5 iCL) (open_itrm_wrt_itrm_rec k iL5 iM)
| (ictrm_app_right iL iCM) ⇒ ictrm_app_right (open_itrm_wrt_itrm_rec k iL5 iL) (open_ictrm_wrt_itrm_rec k iL5 iCM)
end.
Fixpoint open_ctrm_wrt_trm_rec (k:nat) (L5:trm) (CL5:ctrm) {struct CL5}: ctrm :=
match CL5 with
| ctrm_hole ⇒ ctrm_hole
| (ctrm_binop_left CM N) ⇒ ctrm_binop_left (open_ctrm_wrt_trm_rec k L5 CM) (open_trm_wrt_trm_rec k L5 N)
| (ctrm_binop_right M CN) ⇒ ctrm_binop_right (open_trm_wrt_trm_rec k L5 M) (open_ctrm_wrt_trm_rec k L5 CN)
| (ctrm_abs A CN) ⇒ ctrm_abs A (open_ctrm_wrt_trm_rec (S k) L5 CN)
| (ctrm_app_left CL M) ⇒ ctrm_app_left (open_ctrm_wrt_trm_rec k L5 CL) (open_trm_wrt_trm_rec k L5 M)
| (ctrm_app_right L CM) ⇒ ctrm_app_right (open_trm_wrt_trm_rec k L5 L) (open_ctrm_wrt_trm_rec k L5 CM)
| (ctrm_lift CM) ⇒ ctrm_lift (open_ctrm_wrt_trm_rec k L5 CM)
| (ctrm_case_scrutinee CL M N) ⇒ ctrm_case_scrutinee (open_ctrm_wrt_trm_rec k L5 CL) (open_trm_wrt_trm_rec k L5 M) (open_trm_wrt_trm_rec (S k) L5 N)
| (ctrm_case_null L CM N) ⇒ ctrm_case_null (open_trm_wrt_trm_rec k L5 L) (open_ctrm_wrt_trm_rec k L5 CM) (open_trm_wrt_trm_rec (S k) L5 N)
| (ctrm_case_nonnull L M CN) ⇒ ctrm_case_nonnull (open_trm_wrt_trm_rec k L5 L) (open_trm_wrt_trm_rec k L5 M) (open_ctrm_wrt_trm_rec (S k) L5 CN)
| (ctrm_cast CM A p B) ⇒ ctrm_cast (open_ctrm_wrt_trm_rec k L5 CM) A p B
end.
Definition open_ictrm_wrt_itrm iL5 iCL5 := open_ictrm_wrt_itrm_rec 0 iCL5 iL5.
Definition open_ctrm_wrt_trm L5 CL5 := open_ctrm_wrt_trm_rec 0 CL5 L5.
Definition open_itrm_wrt_itrm iL5 iL_6 := open_itrm_wrt_itrm_rec 0 iL_6 iL5.
Definition open_trm_wrt_trm L5 L_6 := open_trm_wrt_trm_rec 0 L_6 L5.
terms are locally-closed pre-terms definitions
Inductive lc_trm : trm → Prop :=
| lc_t_var_f : ∀ (x:var),
(lc_trm (t_var_f x))
| lc_t_const : ∀ (c:constant),
(lc_trm (t_const c))
| lc_t_binop : ∀ (M N:trm),
(lc_trm M) →
(lc_trm N) →
(lc_trm (t_binop M N))
| lc_t_abs : ∀ (A:typ) (N:trm),
( ∀ x , lc_trm ( open_trm_wrt_trm N (t_var_f x) ) ) →
(lc_trm (t_abs A N))
| lc_t_app : ∀ (L M:trm),
(lc_trm L) →
(lc_trm M) →
(lc_trm (t_app L M))
| lc_t_null :
(lc_trm t_null)
| lc_t_lift : ∀ (M:trm),
(lc_trm M) →
(lc_trm (t_lift M))
| lc_t_case : ∀ (L M N:trm),
(lc_trm L) →
(lc_trm M) →
( ∀ x , lc_trm ( open_trm_wrt_trm N (t_var_f x) ) ) →
(lc_trm (t_case L M N))
| lc_t_cast : ∀ (M:trm) (A:typ) (p:label) (B:typ),
(lc_trm M) →
(lc_trm (t_cast M A p B))
| lc_t_blame : ∀ (p:label),
(lc_trm (t_blame p)).
Inductive lc_itrm : itrm → Prop :=
| lc_itrm_var_f : ∀ (ix:ivar),
(lc_itrm (itrm_var_f ix))
| lc_itrm_const : ∀ (c:constant),
(lc_itrm (itrm_const c))
| lc_itrm_binop : ∀ (iM iN:itrm),
(lc_itrm iM) →
(lc_itrm iN) →
(lc_itrm (itrm_binop iM iN))
| lc_itrm_abs : ∀ (iA:ityp) (iN:itrm),
( ∀ ix , lc_itrm ( open_itrm_wrt_itrm iN (itrm_var_f ix) ) ) →
(lc_itrm (itrm_abs iA iN))
| lc_itrm_app : ∀ (iL iM:itrm),
(lc_itrm iL) →
(lc_itrm iM) →
(lc_itrm (itrm_app iL iM))
| lc_itrm_null :
(lc_itrm itrm_null).
Inductive lc_ctrm : ctrm → Prop :=
| lc_ctrm_hole :
(lc_ctrm ctrm_hole)
| lc_ctrm_binop_left : ∀ (CM:ctrm) (N:trm),
(lc_ctrm CM) →
(lc_trm N) →
(lc_ctrm (ctrm_binop_left CM N))
| lc_ctrm_binop_right : ∀ (M:trm) (CN:ctrm),
(lc_trm M) →
(lc_ctrm CN) →
(lc_ctrm (ctrm_binop_right M CN))
| lc_ctrm_abs : ∀ (A:typ) (CN:ctrm),
( ∀ x , lc_ctrm ( open_ctrm_wrt_trm CN (t_var_f x) ) ) →
(lc_ctrm (ctrm_abs A CN))
| lc_ctrm_app_left : ∀ (CL:ctrm) (M:trm),
(lc_ctrm CL) →
(lc_trm M) →
(lc_ctrm (ctrm_app_left CL M))
| lc_ctrm_app_right : ∀ (L:trm) (CM:ctrm),
(lc_trm L) →
(lc_ctrm CM) →
(lc_ctrm (ctrm_app_right L CM))
| lc_ctrm_lift : ∀ (CM:ctrm),
(lc_ctrm CM) →
(lc_ctrm (ctrm_lift CM))
| lc_ctrm_case_scrutinee : ∀ (CL:ctrm) (M N:trm),
(lc_ctrm CL) →
(lc_trm M) →
( ∀ x , lc_trm ( open_trm_wrt_trm N (t_var_f x) ) ) →
(lc_ctrm (ctrm_case_scrutinee CL M N))
| lc_ctrm_case_null : ∀ (L:trm) (CM:ctrm) (N:trm),
(lc_trm L) →
(lc_ctrm CM) →
( ∀ x , lc_trm ( open_trm_wrt_trm N (t_var_f x) ) ) →
(lc_ctrm (ctrm_case_null L CM N))
| lc_ctrm_case_nonnull : ∀ (L M:trm) (CN:ctrm),
(lc_trm L) →
(lc_trm M) →
( ∀ x , lc_ctrm ( open_ctrm_wrt_trm CN (t_var_f x) ) ) →
(lc_ctrm (ctrm_case_nonnull L M CN))
| lc_ctrm_cast : ∀ (CM:ctrm) (A:typ) (p:label) (B:typ),
(lc_ctrm CM) →
(lc_ctrm (ctrm_cast CM A p B)).
Inductive lc_ictrm : ictrm → Prop :=
| lc_ictrm_hole :
(lc_ictrm ictrm_hole)
| lc_ictrm_binop_left : ∀ (iCM:ictrm) (iN:itrm),
(lc_ictrm iCM) →
(lc_itrm iN) →
(lc_ictrm (ictrm_binop_left iCM iN))
| lc_ictrm_binop_right : ∀ (iM:itrm) (iCN:ictrm),
(lc_itrm iM) →
(lc_ictrm iCN) →
(lc_ictrm (ictrm_binop_right iM iCN))
| lc_ictrm_abs : ∀ (iA:ityp) (iCN:ictrm),
( ∀ ix , lc_ictrm ( open_ictrm_wrt_itrm iCN (itrm_var_f ix) ) ) →
(lc_ictrm (ictrm_abs iA iCN))
| lc_ictrm_app_left : ∀ (iCL:ictrm) (iM:itrm),
(lc_ictrm iCL) →
(lc_itrm iM) →
(lc_ictrm (ictrm_app_left iCL iM))
| lc_ictrm_app_right : ∀ (iL:itrm) (iCM:ictrm),
(lc_itrm iL) →
(lc_ictrm iCM) →
(lc_ictrm (ictrm_app_right iL iCM)).
free variables
Fixpoint fv_itrm (iL5:itrm) : vars :=
match iL5 with
| (itrm_var_b nat) ⇒ {}
| (itrm_var_f ix) ⇒ {{ix}}
| (itrm_const c) ⇒ {}
| (itrm_binop iM iN) ⇒ (fv_itrm iM) \u (fv_itrm iN)
| (itrm_abs iA iN) ⇒ (fv_itrm iN)
| (itrm_app iL iM) ⇒ (fv_itrm iL) \u (fv_itrm iM)
| itrm_null ⇒ {}
end.
Fixpoint fv_trm (L5:trm) : vars :=
match L5 with
| (t_var_b nat) ⇒ {}
| (t_var_f x) ⇒ {{x}}
| (t_const c) ⇒ {}
| (t_binop M N) ⇒ (fv_trm M) \u (fv_trm N)
| (t_abs A N) ⇒ (fv_trm N)
| (t_app L M) ⇒ (fv_trm L) \u (fv_trm M)
| t_null ⇒ {}
| (t_lift M) ⇒ (fv_trm M)
| (t_case L M N) ⇒ (fv_trm L) \u (fv_trm M) \u (fv_trm N)
| (t_cast M A p B) ⇒ (fv_trm M)
| (t_blame p) ⇒ {}
end.
Fixpoint fv_ictrm (iCL5:ictrm) : vars :=
match iCL5 with
| ictrm_hole ⇒ {}
| (ictrm_binop_left iCM iN) ⇒ (fv_ictrm iCM) \u (fv_itrm iN)
| (ictrm_binop_right iM iCN) ⇒ (fv_itrm iM) \u (fv_ictrm iCN)
| (ictrm_abs iA iCN) ⇒ (fv_ictrm iCN)
| (ictrm_app_left iCL iM) ⇒ (fv_ictrm iCL) \u (fv_itrm iM)
| (ictrm_app_right iL iCM) ⇒ (fv_itrm iL) \u (fv_ictrm iCM)
end.
Fixpoint fv_ctrm (CL5:ctrm) : vars :=
match CL5 with
| ctrm_hole ⇒ {}
| (ctrm_binop_left CM N) ⇒ (fv_ctrm CM) \u (fv_trm N)
| (ctrm_binop_right M CN) ⇒ (fv_trm M) \u (fv_ctrm CN)
| (ctrm_abs A CN) ⇒ (fv_ctrm CN)
| (ctrm_app_left CL M) ⇒ (fv_ctrm CL) \u (fv_trm M)
| (ctrm_app_right L CM) ⇒ (fv_trm L) \u (fv_ctrm CM)
| (ctrm_lift CM) ⇒ (fv_ctrm CM)
| (ctrm_case_scrutinee CL M N) ⇒ (fv_ctrm CL) \u (fv_trm M) \u (fv_trm N)
| (ctrm_case_null L CM N) ⇒ (fv_trm L) \u (fv_ctrm CM) \u (fv_trm N)
| (ctrm_case_nonnull L M CN) ⇒ (fv_trm L) \u (fv_trm M) \u (fv_ctrm CN)
| (ctrm_cast CM A p B) ⇒ (fv_ctrm CM)
end.
match iL5 with
| (itrm_var_b nat) ⇒ {}
| (itrm_var_f ix) ⇒ {{ix}}
| (itrm_const c) ⇒ {}
| (itrm_binop iM iN) ⇒ (fv_itrm iM) \u (fv_itrm iN)
| (itrm_abs iA iN) ⇒ (fv_itrm iN)
| (itrm_app iL iM) ⇒ (fv_itrm iL) \u (fv_itrm iM)
| itrm_null ⇒ {}
end.
Fixpoint fv_trm (L5:trm) : vars :=
match L5 with
| (t_var_b nat) ⇒ {}
| (t_var_f x) ⇒ {{x}}
| (t_const c) ⇒ {}
| (t_binop M N) ⇒ (fv_trm M) \u (fv_trm N)
| (t_abs A N) ⇒ (fv_trm N)
| (t_app L M) ⇒ (fv_trm L) \u (fv_trm M)
| t_null ⇒ {}
| (t_lift M) ⇒ (fv_trm M)
| (t_case L M N) ⇒ (fv_trm L) \u (fv_trm M) \u (fv_trm N)
| (t_cast M A p B) ⇒ (fv_trm M)
| (t_blame p) ⇒ {}
end.
Fixpoint fv_ictrm (iCL5:ictrm) : vars :=
match iCL5 with
| ictrm_hole ⇒ {}
| (ictrm_binop_left iCM iN) ⇒ (fv_ictrm iCM) \u (fv_itrm iN)
| (ictrm_binop_right iM iCN) ⇒ (fv_itrm iM) \u (fv_ictrm iCN)
| (ictrm_abs iA iCN) ⇒ (fv_ictrm iCN)
| (ictrm_app_left iCL iM) ⇒ (fv_ictrm iCL) \u (fv_itrm iM)
| (ictrm_app_right iL iCM) ⇒ (fv_itrm iL) \u (fv_ictrm iCM)
end.
Fixpoint fv_ctrm (CL5:ctrm) : vars :=
match CL5 with
| ctrm_hole ⇒ {}
| (ctrm_binop_left CM N) ⇒ (fv_ctrm CM) \u (fv_trm N)
| (ctrm_binop_right M CN) ⇒ (fv_trm M) \u (fv_ctrm CN)
| (ctrm_abs A CN) ⇒ (fv_ctrm CN)
| (ctrm_app_left CL M) ⇒ (fv_ctrm CL) \u (fv_trm M)
| (ctrm_app_right L CM) ⇒ (fv_trm L) \u (fv_ctrm CM)
| (ctrm_lift CM) ⇒ (fv_ctrm CM)
| (ctrm_case_scrutinee CL M N) ⇒ (fv_ctrm CL) \u (fv_trm M) \u (fv_trm N)
| (ctrm_case_null L CM N) ⇒ (fv_trm L) \u (fv_ctrm CM) \u (fv_trm N)
| (ctrm_case_nonnull L M CN) ⇒ (fv_trm L) \u (fv_trm M) \u (fv_ctrm CN)
| (ctrm_cast CM A p B) ⇒ (fv_ctrm CM)
end.
substitutions
Fixpoint subst_itrm (iL5:itrm) (ix5:ivar) (iL_6:itrm) {struct iL_6} : itrm :=
match iL_6 with
| (itrm_var_b nat) ⇒ itrm_var_b nat
| (itrm_var_f ix) ⇒ (if eq_var ix ix5 then iL5 else (itrm_var_f ix))
| (itrm_const c) ⇒ itrm_const c
| (itrm_binop iM iN) ⇒ itrm_binop (subst_itrm iL5 ix5 iM) (subst_itrm iL5 ix5 iN)
| (itrm_abs iA iN) ⇒ itrm_abs iA (subst_itrm iL5 ix5 iN)
| (itrm_app iL iM) ⇒ itrm_app (subst_itrm iL5 ix5 iL) (subst_itrm iL5 ix5 iM)
| itrm_null ⇒ itrm_null
end.
Fixpoint subst_trm (L5:trm) (x5:var) (L_6:trm) {struct L_6} : trm :=
match L_6 with
| (t_var_b nat) ⇒ t_var_b nat
| (t_var_f x) ⇒ (if eq_var x x5 then L5 else (t_var_f x))
| (t_const c) ⇒ t_const c
| (t_binop M N) ⇒ t_binop (subst_trm L5 x5 M) (subst_trm L5 x5 N)
| (t_abs A N) ⇒ t_abs A (subst_trm L5 x5 N)
| (t_app L M) ⇒ t_app (subst_trm L5 x5 L) (subst_trm L5 x5 M)
| t_null ⇒ t_null
| (t_lift M) ⇒ t_lift (subst_trm L5 x5 M)
| (t_case L M N) ⇒ t_case (subst_trm L5 x5 L) (subst_trm L5 x5 M) (subst_trm L5 x5 N)
| (t_cast M A p B) ⇒ t_cast (subst_trm L5 x5 M) A p B
| (t_blame p) ⇒ t_blame p
end.
Fixpoint subst_ictrm (iL5:itrm) (ix5:ivar) (iCL5:ictrm) {struct iCL5} : ictrm :=
match iCL5 with
| ictrm_hole ⇒ ictrm_hole
| (ictrm_binop_left iCM iN) ⇒ ictrm_binop_left (subst_ictrm iL5 ix5 iCM) (subst_itrm iL5 ix5 iN)
| (ictrm_binop_right iM iCN) ⇒ ictrm_binop_right (subst_itrm iL5 ix5 iM) (subst_ictrm iL5 ix5 iCN)
| (ictrm_abs iA iCN) ⇒ ictrm_abs iA (subst_ictrm iL5 ix5 iCN)
| (ictrm_app_left iCL iM) ⇒ ictrm_app_left (subst_ictrm iL5 ix5 iCL) (subst_itrm iL5 ix5 iM)
| (ictrm_app_right iL iCM) ⇒ ictrm_app_right (subst_itrm iL5 ix5 iL) (subst_ictrm iL5 ix5 iCM)
end.
Fixpoint subst_ctrm (L5:trm) (x5:var) (CL5:ctrm) {struct CL5} : ctrm :=
match CL5 with
| ctrm_hole ⇒ ctrm_hole
| (ctrm_binop_left CM N) ⇒ ctrm_binop_left (subst_ctrm L5 x5 CM) (subst_trm L5 x5 N)
| (ctrm_binop_right M CN) ⇒ ctrm_binop_right (subst_trm L5 x5 M) (subst_ctrm L5 x5 CN)
| (ctrm_abs A CN) ⇒ ctrm_abs A (subst_ctrm L5 x5 CN)
| (ctrm_app_left CL M) ⇒ ctrm_app_left (subst_ctrm L5 x5 CL) (subst_trm L5 x5 M)
| (ctrm_app_right L CM) ⇒ ctrm_app_right (subst_trm L5 x5 L) (subst_ctrm L5 x5 CM)
| (ctrm_lift CM) ⇒ ctrm_lift (subst_ctrm L5 x5 CM)
| (ctrm_case_scrutinee CL M N) ⇒ ctrm_case_scrutinee (subst_ctrm L5 x5 CL) (subst_trm L5 x5 M) (subst_trm L5 x5 N)
| (ctrm_case_null L CM N) ⇒ ctrm_case_null (subst_trm L5 x5 L) (subst_ctrm L5 x5 CM) (subst_trm L5 x5 N)
| (ctrm_case_nonnull L M CN) ⇒ ctrm_case_nonnull (subst_trm L5 x5 L) (subst_trm L5 x5 M) (subst_ctrm L5 x5 CN)
| (ctrm_cast CM A p B) ⇒ ctrm_cast (subst_ctrm L5 x5 CM) A p B
end.
match iL_6 with
| (itrm_var_b nat) ⇒ itrm_var_b nat
| (itrm_var_f ix) ⇒ (if eq_var ix ix5 then iL5 else (itrm_var_f ix))
| (itrm_const c) ⇒ itrm_const c
| (itrm_binop iM iN) ⇒ itrm_binop (subst_itrm iL5 ix5 iM) (subst_itrm iL5 ix5 iN)
| (itrm_abs iA iN) ⇒ itrm_abs iA (subst_itrm iL5 ix5 iN)
| (itrm_app iL iM) ⇒ itrm_app (subst_itrm iL5 ix5 iL) (subst_itrm iL5 ix5 iM)
| itrm_null ⇒ itrm_null
end.
Fixpoint subst_trm (L5:trm) (x5:var) (L_6:trm) {struct L_6} : trm :=
match L_6 with
| (t_var_b nat) ⇒ t_var_b nat
| (t_var_f x) ⇒ (if eq_var x x5 then L5 else (t_var_f x))
| (t_const c) ⇒ t_const c
| (t_binop M N) ⇒ t_binop (subst_trm L5 x5 M) (subst_trm L5 x5 N)
| (t_abs A N) ⇒ t_abs A (subst_trm L5 x5 N)
| (t_app L M) ⇒ t_app (subst_trm L5 x5 L) (subst_trm L5 x5 M)
| t_null ⇒ t_null
| (t_lift M) ⇒ t_lift (subst_trm L5 x5 M)
| (t_case L M N) ⇒ t_case (subst_trm L5 x5 L) (subst_trm L5 x5 M) (subst_trm L5 x5 N)
| (t_cast M A p B) ⇒ t_cast (subst_trm L5 x5 M) A p B
| (t_blame p) ⇒ t_blame p
end.
Fixpoint subst_ictrm (iL5:itrm) (ix5:ivar) (iCL5:ictrm) {struct iCL5} : ictrm :=
match iCL5 with
| ictrm_hole ⇒ ictrm_hole
| (ictrm_binop_left iCM iN) ⇒ ictrm_binop_left (subst_ictrm iL5 ix5 iCM) (subst_itrm iL5 ix5 iN)
| (ictrm_binop_right iM iCN) ⇒ ictrm_binop_right (subst_itrm iL5 ix5 iM) (subst_ictrm iL5 ix5 iCN)
| (ictrm_abs iA iCN) ⇒ ictrm_abs iA (subst_ictrm iL5 ix5 iCN)
| (ictrm_app_left iCL iM) ⇒ ictrm_app_left (subst_ictrm iL5 ix5 iCL) (subst_itrm iL5 ix5 iM)
| (ictrm_app_right iL iCM) ⇒ ictrm_app_right (subst_itrm iL5 ix5 iL) (subst_ictrm iL5 ix5 iCM)
end.
Fixpoint subst_ctrm (L5:trm) (x5:var) (CL5:ctrm) {struct CL5} : ctrm :=
match CL5 with
| ctrm_hole ⇒ ctrm_hole
| (ctrm_binop_left CM N) ⇒ ctrm_binop_left (subst_ctrm L5 x5 CM) (subst_trm L5 x5 N)
| (ctrm_binop_right M CN) ⇒ ctrm_binop_right (subst_trm L5 x5 M) (subst_ctrm L5 x5 CN)
| (ctrm_abs A CN) ⇒ ctrm_abs A (subst_ctrm L5 x5 CN)
| (ctrm_app_left CL M) ⇒ ctrm_app_left (subst_ctrm L5 x5 CL) (subst_trm L5 x5 M)
| (ctrm_app_right L CM) ⇒ ctrm_app_right (subst_trm L5 x5 L) (subst_ctrm L5 x5 CM)
| (ctrm_lift CM) ⇒ ctrm_lift (subst_ctrm L5 x5 CM)
| (ctrm_case_scrutinee CL M N) ⇒ ctrm_case_scrutinee (subst_ctrm L5 x5 CL) (subst_trm L5 x5 M) (subst_trm L5 x5 N)
| (ctrm_case_null L CM N) ⇒ ctrm_case_null (subst_trm L5 x5 L) (subst_ctrm L5 x5 CM) (subst_trm L5 x5 N)
| (ctrm_case_nonnull L M CN) ⇒ ctrm_case_nonnull (subst_trm L5 x5 L) (subst_trm L5 x5 M) (subst_ctrm L5 x5 CN)
| (ctrm_cast CM A p B) ⇒ ctrm_cast (subst_ctrm L5 x5 CM) A p B
end.
definitions
Inductive compat : typ → typ → Prop :=
| compat_base :
compat (typ_def dtyp_base) (typ_def dtyp_base)
| compat_null_r : ∀ (A:typ) (D:dtyp),
compat A (typ_def D) →
compat A (typ_null D)
| compat_null_l : ∀ (D:dtyp) (A:typ),
compat (typ_def D) A →
compat (typ_null D) A
| compat_arrow : ∀ (A B A' B':typ),
compat A A' →
compat B B' →
compat (typ_def (dtyp_arrow A B)) (typ_def (dtyp_arrow A' B')).
Inductive typing : ctx → trm → typ → Prop :=
| typing_var : ∀ (G:ctx) (x:var) (A:typ),
uniq G →
binds x A G →
typing G (t_var_f x) A
| typing_constant : ∀ (G:ctx) (c:constant),
uniq G →
typing G (t_const c) (typ_def dtyp_base)
| typing_binop : ∀ (G:ctx) (M N:trm),
typing G M (typ_def dtyp_base) →
typing G N (typ_def dtyp_base) →
typing G (t_binop M N) (typ_def dtyp_base)
| typing_abs : ∀ (L:vars) (G:ctx) (A:typ) (N:trm) (B:typ),
( ∀ x , x \notin L → typing (( x ¬ A )++ G ) ( open_trm_wrt_trm N (t_var_f x) ) B ) →
typing G (t_abs A N) (typ_def (dtyp_arrow A B))
| typing_app : ∀ (G:ctx) (L M:trm) (B A:typ),
typing G L (typ_def (dtyp_arrow A B)) →
typing G M A →
typing G (t_app L M) B
| typing_null : ∀ (G:ctx) (D:dtyp),
uniq G →
typing G t_null (typ_null D)
| typing_lift : ∀ (G:ctx) (M:trm) (D:dtyp),
typing G M (typ_def D) →
typing G (t_lift M) (typ_null D)
| typing_case : ∀ (L:vars) (G:ctx) (L' M N:trm) (A:typ) (D:dtyp),
typing G L' (typ_null D) →
typing G M A →
( ∀ x , x \notin L → typing (( x ¬ (typ_def D) )++ G ) ( open_trm_wrt_trm N (t_var_f x) ) A ) →
typing G (t_case L' M N) A
| typing_cast : ∀ (G:ctx) (M:trm) (A:typ) (p:label) (B:typ),
typing G M A →
compat A B →
typing G ( (t_cast M A p B) ) B
| typing_blame : ∀ (G:ctx) (p:label) (A:typ),
uniq G →
typing G (t_blame p) A.
Inductive neglabel : label → label → Prop :=
| nl_pos_to_neg : ∀ (bl:blamelabel),
neglabel (label_name bl) (label_not_label bl)
| nl_neg_to_pos : ∀ (bl:blamelabel),
neglabel (label_not_label bl) (label_name bl).
Inductive step : trm → trm → Prop :=
| step_binop : ∀ (c:constant) (V W:trm),
Is_true (is_val_of_trm V) →
Is_true (is_val_of_trm W) →
lc_trm V →
lc_trm W →
step (t_binop V W) (t_const c)
| step_app : ∀ (A:typ) (N V:trm),
Is_true (is_val_of_trm V) →
lc_trm (t_abs A N) →
lc_trm V →
step (t_app ( (t_abs A N) ) V) ( (open_trm_wrt_trm N V ) )
| step_wrap : ∀ (A B:typ) (p:label) (A' B':typ) (p':label) (V W:trm),
Is_true (is_val_of_trm V) →
Is_true (is_val_of_trm W) →
lc_trm V →
lc_trm W →
neglabel p p' →
step (t_app ( (t_cast V ( (typ_def (dtyp_arrow A B)) ) p ( (typ_def (dtyp_arrow A' B')) ) ) ) W) (t_cast ( (t_app V ( (t_cast W A' p' A) ) ) ) B p B')
| step_cast_null : ∀ (D:dtyp) (p:label) (E:dtyp),
step ( (t_cast t_null (typ_null D) p (typ_null E)) ) t_null
| step_cast_lift : ∀ (D:dtyp) (p:label) (E:dtyp) (V:trm),
Is_true (is_val_of_trm V) →
lc_trm V →
step ( (t_cast ( (t_lift V) ) (typ_null D) p (typ_null E)) ) (t_lift ( (t_cast V (typ_def D) p (typ_def E)) ) )
| step_downcast_null : ∀ (D:dtyp) (p:label) (E:dtyp),
step ( (t_cast t_null (typ_null D) p (typ_def E)) ) (t_blame p)
| step_downcast_lift : ∀ (D:dtyp) (p:label) (E:dtyp) (V:trm),
Is_true (is_val_of_trm V) →
lc_trm V →
step ( (t_cast ( (t_lift V) ) (typ_null D) p (typ_def E)) ) ( (t_cast V (typ_def D) p (typ_def E)) )
| step_upcast : ∀ (D:dtyp) (p:label) (E:dtyp) (V:trm),
Is_true (is_val_of_trm V) →
lc_trm V →
step ( (t_cast V (typ_def D) p (typ_null E)) ) (t_lift ( (t_cast V (typ_def D) p (typ_def E)) ) )
| step_cast_base : ∀ (p:label) (V:trm),
Is_true (is_val_of_trm V) →
lc_trm V →
step ( (t_cast V (typ_def dtyp_base) p (typ_def dtyp_base)) ) V
| step_case_null : ∀ (M N:trm),
lc_trm (t_case t_null M N) →
lc_trm M →
step (t_case t_null M N) M
| step_case_lift : ∀ (M N V:trm),
Is_true (is_val_of_trm V) →
lc_trm M →
lc_trm (t_case ( (t_lift V) ) M N) →
lc_trm V →
step (t_case ( (t_lift V) ) M N) ( (open_trm_wrt_trm N V ) )
| step_appL_ctx : ∀ (M N M':trm),
lc_trm N →
step M M' →
step (t_app M N) (t_app M' N)
| step_appL_err : ∀ (p:label) (N:trm),
lc_trm N →
step (t_app ( (t_blame p) ) N) (t_blame p)
| step_appR_ctx : ∀ (N N' V:trm),
Is_true (is_val_of_trm V) →
lc_trm V →
step N N' →
step (t_app V N) (t_app V N')
| step_appR_err : ∀ (p:label) (V:trm),
Is_true (is_val_of_trm V) →
lc_trm V →
step (t_app V ( (t_blame p) ) ) (t_blame p)
| step_cast_ctx : ∀ (M:trm) (A:typ) (p:label) (B:typ) (M':trm),
step M M' →
step ( (t_cast M A p B) ) ( (t_cast M' A p B) )
| step_cast_err : ∀ (p:label) (A:typ) (q:label) (B:typ),
step (t_cast ( (t_blame p) ) A q B) (t_blame p)
| step_case_ctx : ∀ (L M N L':trm),
lc_trm (t_case L M N) →
lc_trm M →
step L L' →
step (t_case L M N) (t_case L' M N)
| step_case_err : ∀ (p:label) (M N:trm),
lc_trm M →
lc_trm (t_case ( (t_blame p) ) M N) →
step (t_case ( (t_blame p) ) M N) (t_blame p)
| step_lift_ctx : ∀ (M M':trm),
step M M' →
step (t_lift M) (t_lift M')
| step_lift_err : ∀ (p:label),
step (t_lift ( (t_blame p) ) ) (t_blame p)
| step_binopL_ctx : ∀ (M N M':trm),
lc_trm N →
step M M' →
step (t_binop M N) (t_binop M' N)
| step_binopL_err : ∀ (p:label) (N:trm),
lc_trm N →
step (t_binop ( (t_blame p) ) N) (t_blame p)
| step_binopR_ctx : ∀ (N N' V:trm),
Is_true (is_val_of_trm V) →
lc_trm V →
step N N' →
step (t_binop V N) (t_binop V N')
| step_binopR_err : ∀ (p:label) (V:trm),
Is_true (is_val_of_trm V) →
lc_trm V →
step (t_binop V ( (t_blame p) ) ) (t_blame p).
Inductive subtyp : typ → typ → Prop :=
| subtyp_base :
subtyp (typ_def dtyp_base) (typ_def dtyp_base)
| subtyp_null_sup : ∀ (D E:dtyp),
subtyp (typ_def D) (typ_def E) →
subtyp (typ_def D) (typ_null E)
| subtyp_null : ∀ (D E:dtyp),
subtyp (typ_def D) (typ_def E) →
subtyp (typ_null D) (typ_null E)
| subtyp_arrow : ∀ (A B A' B':typ),
subtyp A' A →
subtyp B B' →
subtyp (typ_def (dtyp_arrow A B)) (typ_def (dtyp_arrow A' B')).
Inductive subtyp_n : typ → typ → Prop :=
| subtyp_n_base :
subtyp_n (typ_def dtyp_base) (typ_def dtyp_base)
| subtyp_n_null_sup : ∀ (D E:dtyp),
subtyp_n (typ_def D) (typ_def E) →
subtyp_n (typ_def D) (typ_null E)
| subtyp_n_null : ∀ (D E:dtyp),
subtyp_n (typ_def D) (typ_def E) →
subtyp_n (typ_null D) (typ_null E)
| subtyp_n_arrow : ∀ (A B A' B':typ),
subtyp_n A A' →
subtyp_n B B' →
subtyp_n (typ_def (dtyp_arrow A B)) (typ_def (dtyp_arrow A' B')).
Inductive subtyp_pos : typ → typ → Prop :=
| subtyp_posbase :
subtyp_pos (typ_def dtyp_base) (typ_def dtyp_base)
| subtyp_posnull_sup : ∀ (D E:dtyp),
subtyp_pos (typ_def D) (typ_def E) →
subtyp_pos (typ_def D) (typ_null E)
| subtyp_posnull : ∀ (D E:dtyp),
subtyp_pos (typ_def D) (typ_def E) →
subtyp_pos (typ_null D) (typ_null E)
| subtyp_posarrow : ∀ (A B A' B':typ),
subtyp_neg A' A →
subtyp_pos B B' →
subtyp_pos (typ_def (dtyp_arrow A B)) (typ_def (dtyp_arrow A' B'))
with subtyp_neg : typ → typ → Prop :=
| subtyp_negbase :
subtyp_neg (typ_def dtyp_base) (typ_def dtyp_base)
| subtyp_negnull_sub : ∀ (D E:dtyp),
subtyp_neg (typ_def D) (typ_def E) →
subtyp_neg (typ_null D) (typ_def E)
| subtyp_negnull_sup : ∀ (D E:dtyp),
subtyp_neg (typ_def D) (typ_def E) →
subtyp_neg (typ_def D) (typ_null E)
| subtyp_negnull : ∀ (D E:dtyp),
subtyp_neg (typ_def D) (typ_def E) →
subtyp_neg (typ_null D) (typ_null E)
| subtyp_negarrow : ∀ (A B A' B':typ),
subtyp_pos A' A →
subtyp_neg B B' →
subtyp_neg (typ_def (dtyp_arrow A B)) (typ_def (dtyp_arrow A' B')).
Inductive ityping : ictx → itrm → ityp → Prop :=
| ityping_var : ∀ (iG:ictx) (ix:ivar) (iA:ityp),
uniq iG →
binds ix iA iG →
ityping iG (itrm_var_f ix) iA
| ityping_base : ∀ (iG:ictx) (c:constant),
uniq iG →
ityping iG (itrm_const c) ityp_base
| ityping_binop : ∀ (iG:ictx) (iM iN:itrm),
ityping iG iM ityp_base →
ityping iG iN ityp_base →
ityping iG (itrm_binop iM iN) ityp_base
| ityping_abs : ∀ (L:vars) (iG:ictx) (iA:ityp) (iN:itrm) (iB:ityp),
( ∀ ix , ix \notin L → ityping (( ix ¬ iA )++ iG ) ( open_itrm_wrt_itrm iN (itrm_var_f ix) ) iB ) →
ityping iG (itrm_abs iA iN) (ityp_arrow iA iB)
| ityping_app : ∀ (iG:ictx) (iL iM:itrm) (iB iA:ityp),
ityping iG iL (ityp_arrow iA iB) →
ityping iG iM iA →
ityping iG (itrm_app iL iM) iB
| ityping_null : ∀ (iG:ictx) (iA:ityp),
uniq iG →
ityping iG itrm_null iA.
Inductive ctyping : ctx → typ → ctx → ctrm → typ → Prop :=
| ctyping_hole : ∀ (G:ctx) (A:typ),
uniq G →
ctyping G A G ctrm_hole A
| ctyping_binop_left : ∀ (G':ctx) (A':typ) (G:ctx) (CM:ctrm) (N:trm),
ctyping G' A' G CM (typ_def dtyp_base) →
typing G N (typ_def dtyp_base) →
ctyping G' A' G (ctrm_binop_left CM N) (typ_def dtyp_base)
| ctyping_binop_right : ∀ (G':ctx) (A':typ) (G:ctx) (M:trm) (CN:ctrm),
typing G M (typ_def dtyp_base) →
ctyping G' A' G CN (typ_def dtyp_base) →
ctyping G' A' G (ctrm_binop_right M CN) (typ_def dtyp_base)
| ctyping_abs : ∀ (L:vars) (G':ctx) (A':typ) (G:ctx) (A:typ) (CN:ctrm) (B:typ),
( ∀ x , x \notin L → ctyping G' A' (( x ¬ A )++ G ) ( open_ctrm_wrt_trm CN (t_var_f x) ) B ) →
ctyping G' A' G (ctrm_abs A CN) (typ_def (dtyp_arrow A B))
| ctyping_app_left : ∀ (G':ctx) (A':typ) (G:ctx) (CL:ctrm) (M:trm) (B A:typ),
ctyping G' A' G CL (typ_def (dtyp_arrow A B)) →
typing G M A →
ctyping G' A' G (ctrm_app_left CL M) B
| ctyping_app_right : ∀ (G':ctx) (A':typ) (G:ctx) (L:trm) (CM:ctrm) (B A:typ),
typing G L (typ_def (dtyp_arrow A B)) →
ctyping G' A' G CM A →
ctyping G' A' G (ctrm_app_right L CM) B
| ctyping_lift : ∀ (G':ctx) (A':typ) (G:ctx) (CM:ctrm) (D:dtyp),
ctyping G' A' G CM (typ_def D) →
ctyping G' A' G (ctrm_lift CM) (typ_null D)
| ctyping_case_scrutinee : ∀ (L:vars) (G':ctx) (A':typ) (G:ctx) (CL':ctrm) (M N:trm) (A:typ) (D:dtyp),
ctyping G' A' G CL' (typ_null D) →
typing G M A →
( ∀ x , x \notin L → typing (( x ¬ (typ_def D) )++ G ) ( open_trm_wrt_trm N (t_var_f x) ) A ) →
ctyping G' A' G (ctrm_case_scrutinee CL' M N) A
| ctyping_case_null : ∀ (L:vars) (G':ctx) (A':typ) (G:ctx) (L':trm) (CM:ctrm) (N:trm) (A:typ) (D:dtyp),
typing G L' (typ_null D) →
ctyping G' A' G CM A →
( ∀ x , x \notin L → typing (( x ¬ (typ_def D) )++ G ) ( open_trm_wrt_trm N (t_var_f x) ) A ) →
ctyping G' A' G (ctrm_case_null L' CM N) A
| ctyping_case_nonnull : ∀ (L:vars) (G':ctx) (A':typ) (G:ctx) (L' M:trm) (CN:ctrm) (A:typ) (D:dtyp),
typing G L' (typ_null D) →
typing G M A →
( ∀ x , x \notin L → ctyping G' A' (( x ¬ (typ_def D) )++ G ) ( open_ctrm_wrt_trm CN (t_var_f x) ) A ) →
ctyping G' A' G (ctrm_case_nonnull L' M CN) A
| ctyping_cast : ∀ (G':ctx) (A':typ) (G:ctx) (CM:ctrm) (A:typ) (p:label) (B:typ),
ctyping G' A' G CM A →
compat A B →
ctyping G' A' G ( (ctrm_cast CM A p B) ) B.
Inductive ictyping : ictx → ityp → ictx → ictrm → ityp → Prop :=
| ictyping_hole : ∀ (iG:ictx) (iA:ityp),
uniq iG →
ictyping iG iA iG ictrm_hole iA
| ictyping_binop_left : ∀ (iG':ictx) (iA':ityp) (iG:ictx) (iCM:ictrm) (iN:itrm),
ictyping iG' iA' iG iCM ityp_base →
ityping iG iN ityp_base →
ictyping iG' iA' iG (ictrm_binop_left iCM iN) ityp_base
| ictyping_binop_right : ∀ (iG':ictx) (iA':ityp) (iG:ictx) (iM:itrm) (iCN:ictrm),
ityping iG iM ityp_base →
ictyping iG' iA' iG iCN ityp_base →
ictyping iG' iA' iG (ictrm_binop_right iM iCN) ityp_base
| ictyping_abs : ∀ (L:vars) (iG':ictx) (iA':ityp) (iG:ictx) (iA:ityp) (iCN:ictrm) (iB:ityp),
( ∀ ix , ix \notin L → ictyping iG' iA' (( ix ¬ iA )++ iG ) ( open_ictrm_wrt_itrm iCN (itrm_var_f ix) ) iB ) →
ictyping iG' iA' iG (ictrm_abs iA iCN) (ityp_arrow iA iB)
| ictyping_app_left : ∀ (iG':ictx) (iA':ityp) (iG:ictx) (iCL:ictrm) (iM:itrm) (iB iA:ityp),
ictyping iG' iA' iG iCL (ityp_arrow iA iB) →
ityping iG iM iA →
ictyping iG' iA' iG (ictrm_app_left iCL iM) iB
| ictyping_app_right : ∀ (iG':ictx) (iA':ityp) (iG:ictx) (iL:itrm) (iCM:ictrm) (iB iA:ityp),
ityping iG iL (ityp_arrow iA iB) →
ictyping iG' iA' iG iCM iA →
ictyping iG' iA' iG (ictrm_app_right iL iCM) iB.
infrastructure