Library Definitions

In this file,

We define the target system:
- - term syntax term,
- - type syntax basetype + inttype + type,
- - contexts as functions nat -> type
- - typing relation ty,
We define type equivalence T == U and subsumption T >= U,
We define pointwise intersection Gamma & Delta, type equivalence Gamma ==1 Delta and subsumption Gamma >=1 Delta for contexts,

Require Export Setoid Morphisms.
Require Export Basics.
Require Export Decidable.
Require Export Autosubst.

Require Import Omega.

Hint Extern 4 => omega.
Hint Extern 4 => congruence.
Hint Extern 4 => match goal with [ |- _ = _ ] => autosubst end.

Implicit Types x y z : var.

Inductive term :=
| TVar (x : var)
| App (s t : term)
| Lam (s : {bind term }).

Instance Ids_term : Ids term. derive. Defined.
Instance Rename_term : Rename term. derive. Defined.
Instance Subst_term : Subst term. derive. Defined.
Instance SubstLemmas_term : SubstLemmas term. derive. Qed.

Implicit Types s t u : term.
Coercion App : term >-> Funclass.
Coercion TVar : var >-> term.

Inductive basetype :=
| BASE (x : nat)
| Arr (A : inttype) (F : basetype)
with inttype :=
| UpB (F : basetype)
| Int (A B : inttype).
Inductive type :=
| UpI (A : inttype)
| OMEGA.

Implicit Types F G H : basetype.
Implicit Types A B C : inttype.
Implicit Types U V W : type.
Coercion UpB : basetype >-> inttype.
Coercion UpI : inttype >-> type.
Infix "-->" := Arr.
Notation "A 'o' B" := (Int A B) (at level 50).

Definition int U V : type :=
  match U, V with
  | OMEGA, V => V
  | U, OMEGA => U
  | UpI A, UpI B => (Int A B)
  end.

Infix "*" := int.

Inductive type_equiv : type -> type -> Prop :=
| te_refl_F F :
  type_equiv F F
| te_refl_OMEGA :
  type_equiv OMEGA OMEGA
| te_comm_Int A B :
  type_equiv (A o B) (B o A)
| te_cong_Int A B A' B' : type_equiv A A' -> type_equiv B B'
  -> type_equiv (A o B) (A' o B')
| te_trans_ABC A B C : type_equiv A B -> type_equiv B C ->
  type_equiv A C
| te_assoc_Int_lr A B C :
  type_equiv ((A o B ) o C) (A o (B o C ))
| te_assoc_Int_rl A B C :
  type_equiv (A o (B o C )) ((A o B ) o C)
.

Infix "==" := type_equiv (at level 60) : type_scope.

Hint Constructors type_equiv.

Definition subsumes U V := exists V', U == V * V'.
Infix ">=" := subsumes.

Definition context := var -> type.
Implicit Types Gamma Delta : context.

Definition Empty x := OMEGA.

Definition cint Gamma Delta x := Gamma x * Delta x.
Arguments cint _ _ _ /.

Infix "&" := cint (at level 50).

Definition drop k := fun Gamma x => Gamma (k + x).
Arguments drop _ _ _ /.

Definition PWR {X Y} (R : Y -> Y -> Prop) (f g : X -> Y) := forall x : X, R (f x) (g x).
Infix "=1" := (PWR eq) (at level 60).
Definition cte := PWR (X := var) type_equiv.
Infix "==1" := cte (at level 60).
Definition csub Gamma Delta := exists Delta', Gamma ==1 Delta & Delta'.
Infix ">=1" := csub (at level 70).

Inductive ty : nat -> context -> term -> type -> Prop :=
| tyVar Gamma n x F : Gamma x >= F -> ty n Gamma x F
| tyAbs Gamma n s A F : ty n ((A : type ) .: Gamma) s F -> ty n Gamma (Lam s) (A --> F)
| tyApp Gamma n m Delta s t A F : ty n Gamma s (A --> F) -> ty m Delta t A -> forall Epsilon (e : Gamma & Delta ==1 Epsilon), ty (S (n + m)) Epsilon (s t) F
| tyInt Gamma n A Delta m B s : ty n Gamma s A -> ty m Delta s B -> forall Epsilon (e : Gamma & Delta ==1 Epsilon), ty (n +m) Epsilon s (A o B)
| tyO Gamma n s : ty n Gamma s OMEGA.

Hint Constructors ty.