ladder-calculus/coq/typing.v

(* This module defines the typing relation
 * where each expression is assigned a type.
 *)
From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Require Import context.
Require Import morph.

Include Terms.
Include Subst.
Include Equiv.
Include Subtype.
Include Context.
Include Morph.

Module Typing.

(** Typing Derivation *)

Reserved Notation "Gamma '|-' x '\is' X"  (at level 101, x at next level, X at level 0).

Inductive expr_type : context -> expr_term -> type_term -> Prop :=
  | T_Var : forall Γ x τ,
    (context_contains Γ x τ) ->
    (Γ |- (expr_var x) \is τ)

  | T_Let : forall Γ s σ t τ x,
    (Γ |- s \is σ) ->
    ((ctx_assign x σ Γ) |- t \is τ) ->
    (Γ |- (expr_let x s t) \is τ)

  | T_TypeAbs : forall Γ e τ α,
    Γ |- e \is τ ->
    Γ |- (expr_ty_abs α e) \is (type_univ α τ)

  | T_TypeApp : forall Γ α e σ τ τ',
    Γ |- e \is (type_univ α τ) ->
    (type_subst1 α σ τ τ') ->
    Γ |- (expr_ty_app e σ) \is τ'

  | T_Abs : forall Γ x σ t τ,
    ((ctx_assign x σ Γ) |- t \is τ) ->
    (Γ |- (expr_abs x σ t) \is (type_fun σ τ))

  | T_MorphAbs : forall Γ x σ e τ,
    ((ctx_assign x σ Γ) |- e \is τ) ->
    Γ |- (expr_morph x σ e) \is (type_morph σ τ)

  | T_App : forall Γ f a σ' σ τ,
    (Γ |- f \is (type_fun σ τ)) ->
    (Γ |- a \is σ') ->
    (Γ |- σ' ~> σ) ->
    (Γ |- (expr_app f a) \is τ)

  | T_MorphFun : forall Γ f σ τ,
    Γ |- f \is (type_morph σ τ) ->
    Γ |- f \is (type_fun σ τ)

  | T_Ascend : forall Γ e τ τ',
    (Γ |- e \is τ) ->
    (Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ))

  | T_DescendImplicit : forall Γ x τ τ',
    Γ |- x \is τ ->
    (τ :<= τ') ->
    Γ |- x \is τ'

  | T_Descend : forall Γ x τ τ',
    Γ |- x \is τ ->
    (τ :<= τ') ->
    Γ |- (expr_descend τ' x) \is τ'

where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).

Definition is_well_typed (e:expr_term) : Prop :=
  forall Γ,
  exists τ,
  Γ |- e \is τ
.

Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> Prop :=
  | Expand_Var : forall Γ x τ,
    (Γ |- (expr_var x) \is τ) ->
    (translate_typing Γ (expr_var x) τ (expr_var x))

  | Expand_Let : forall Γ x e e' t t' σ τ,
    (Γ |- e \is σ) ->
    ((ctx_assign x σ Γ) |- t \is τ) ->
    (translate_typing Γ e σ e') ->
    (translate_typing (ctx_assign x σ Γ) t τ t') ->
    (translate_typing Γ (expr_let x e t) τ (expr_let x e' t'))

  | Expand_TypeAbs : forall Γ α e e' τ,
    (Γ |- e \is τ) ->
    (translate_typing Γ e τ e') ->
    (translate_typing Γ
      (expr_ty_abs α e)
      (type_univ α τ)
      (expr_ty_abs α e'))

  | Expand_TypeApp : forall Γ e e' σ α τ,
    (Γ |- e \is (type_univ α τ)) ->
    (translate_typing Γ e τ e') ->
    (translate_typing Γ (expr_ty_app e τ) (type_subst α σ τ) (expr_ty_app e' τ))

  | Expand_Abs : forall Γ x σ e e' τ,
    ((ctx_assign x σ Γ) |- e \is τ) ->
    (Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
    (translate_typing (ctx_assign x σ Γ) e τ e') ->
    (translate_typing Γ (expr_abs x σ e) (type_fun σ τ) (expr_abs x σ e'))

  | Expand_MorphAbs : forall Γ x σ e e' τ,
    ((ctx_assign x σ Γ) |- e \is τ) ->
    (Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
    (translate_typing (ctx_assign x σ Γ) e τ e') ->
    (translate_typing Γ (expr_morph x σ e) (type_morph σ τ) (expr_morph x σ e'))

  | Expand_App : forall Γ f f' a a' m σ τ σ',
    (Γ |- f \is (type_fun σ τ)) ->
    (Γ |- a \is σ') ->
    (Γ |- σ' ~> σ) ->
    (translate_typing Γ f (type_fun σ τ) f') ->
    (translate_typing Γ a σ' a') ->
    (translate_morphism_path Γ σ' σ m) ->
    (translate_typing Γ (expr_app f a) τ (expr_app f' (expr_app m a')))

  | Expand_MorphFun : forall Γ f f' σ τ,
    (Γ |- f \is (type_morph σ τ)) ->
    (Γ |- f \is (type_fun σ τ)) ->
    (translate_typing Γ f (type_morph σ τ) f') ->
    (translate_typing Γ f (type_fun σ τ) f')

  | Expand_Ascend : forall Γ e e' τ τ',
    (Γ |- e \is τ) ->
    (Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ)) ->
    (translate_typing Γ e τ e') ->
    (translate_typing Γ (expr_ascend τ' e) (type_ladder τ' τ) (expr_ascend τ' e'))

  | Expand_Descend : forall Γ e e' τ τ',
    (Γ |- e \is τ) ->
    (τ :<= τ') ->
    (Γ |- e \is τ') ->
    (translate_typing Γ e τ e') ->
    (translate_typing Γ e τ' e')
.

(* Examples *)

Example typing1 :
  ctx_empty |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
Proof.
  intros.
  apply T_TypeAbs.
  apply T_Abs.
  apply T_Var.
  apply C_take.
Qed.

Example typing2 :
  ctx_empty |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
Proof.
  intros.
  apply T_DescendImplicit with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
  apply T_TypeAbs.
  apply T_Abs.
  apply T_Var.
  apply C_take.

  apply TSubRepr_Refl.
  apply TEq_Alpha.
  apply TAlpha_Rename.
  apply TSubst_Fun.
  apply TSubst_VarReplace.
  apply TSubst_VarReplace.
Qed.

Example typing3 :
  ctx_empty |- [{
    Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"y"%
  }] \is [<
       ∀"S",∀"T",(%"S"%->%"T"%->%"T"%)
  >].
Proof.
  intros.
  apply T_DescendImplicit with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
  apply T_TypeAbs, T_TypeAbs, T_Abs.
  apply T_Abs.
  apply T_Var.
  apply C_take.

  apply TSubRepr_Refl.
  apply TEq_Trans with (y:= [< ∀"S",∀"U",(%"S"%->%"U"%->%"U"%) >] ).
  apply TEq_Alpha.
  apply TAlpha_Rename.
  apply TSubst_UnivReplace. discriminate.
  easy.
  apply TSubst_Fun.
  apply TSubst_VarReplace.
  apply TSubst_Fun.
  apply TSubst_VarKeep. discriminate.
  apply TSubst_VarKeep. discriminate.

  apply TEq_Alpha.
  apply TAlpha_SubUniv.
  apply TAlpha_Rename.
  apply TSubst_Fun.
  apply TSubst_VarKeep. discriminate.
  apply TSubst_Fun.
  apply TSubst_VarReplace.
  apply TSubst_VarReplace.
Qed.

Example typing4 : (is_well_typed
  [{ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% }]
).
Proof.
  unfold is_well_typed.
  exists [< ∀"T",∀"U",%"T"%->%"U"%->%"T"% >].
  apply T_TypeAbs.
  apply T_TypeAbs.
  apply T_Abs.
  apply T_Abs.
  apply T_Var.
  apply C_shuffle, C_take.
Qed.

Open Scope ladder_expr_scope.

Example typing5 :
  (ctx_assign "60" [< $"ℝ"$ >]
  (ctx_assign "360" [< $"ℝ"$ >]
  (ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
    ctx_empty)))
  |-
  [{
    let "deg2turns" :=
       (λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
                ↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$))
    in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
  }]
  \is
  [<
    $"Angle"$~$"Turns"$~$"ℝ"$
  >]
.
Proof.
  apply T_Let with (σ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]).
  apply T_MorphAbs.
  apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Turns"$>] [<$"ℝ"$>])).
  2: apply TSubRepr_Refl, TEq_LadderAssocLR.
  apply T_Ascend with (τ:=[<$"ℝ"$>]) (τ':=[<$"Angle"$~$"Turns"$>]).
  apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
  apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
  apply T_Var.
  apply C_shuffle. apply C_shuffle. apply C_shuffle. apply C_take.
  apply T_DescendImplicit with (τ := [< $"Angle"$~$"Degrees"$~$"ℝ"$ >]).
  apply T_Var.
  apply C_take.
  apply TSubRepr_Ladder. apply TSubRepr_Ladder.
  apply TSubRepr_Refl. apply TEq_Refl.
  apply M_Sub.
  apply TSubRepr_Refl. apply TEq_Refl.
  apply T_Var.
  apply C_shuffle, C_shuffle, C_take.
  apply M_Sub.
  apply TSubRepr_Refl.
  apply TEq_Refl.
  apply T_App with (σ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]) (σ':=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
  apply T_MorphFun.
  apply T_Var.
  apply C_take.
  apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Degrees"$>] [<$"ℝ"$>])).
  2: apply TSubRepr_Refl, TEq_LadderAssocLR.
  apply T_Ascend.
  apply T_Var.
  apply C_shuffle. apply C_take.
  apply M_Sub. apply TSubRepr_Refl. apply TEq_Refl.
Qed.

End Typing.