linf.v

From Coq Require Import Strings.String.
From Coq Require Logic.FunctionalExtensionality.

Inductive ty : Type :=
  | T_Bool : ty
  | T_Arrow : ty -> ty -> ty.
Inductive expr : Type :=
  | E_var : string -> expr
  | E_app : expr -> expr -> expr
  | E_abs : string -> ty -> expr -> expr
  | E_true : expr
  | E_false : expr
  | E_if : expr -> expr -> expr -> expr.
Inductive value : expr -> Type :=
  | V_abs : forall x T e, value (E_abs x T e)
  | V_true : value E_true
  | V_false : value E_false.

Fixpoint subst (e : expr) (x : string) (to : expr) : expr :=
  match e with
  | E_var y => if String.eqb x y then to else e
  | E_abs y T e =>
    let e := if String.eqb x y then e else (subst e x to) in
    E_abs y T e
  | E_app e1 e2 => E_app (subst e1 x to) (subst e2 x to)
  | E_true => E_true
  | E_false => E_false
  | E_if e1 e2 e3 => E_if (subst e1 x to) (subst e2 x to) (subst e3 x to)
  end.

Definition context := string -> option ty.
Definition empty : context := fun _x => None.
Definition add (ctx : context) x t : context :=
    fun y => if String.eqb x y then Some t else ctx y.

Lemma add_comm_when_diff ctx {x y} A B (x_neq_y : x <> y) :
  add (add ctx x A) y B = add (add ctx y B) x A.
  (* TODO: funext *)
  apply (FunctionalExtensionality.functional_extensionality).
  intros z.
  unfold add.
  destruct (String.eqb_spec x z).
  destruct (String.eqb_spec y z).
  - rewrite <- e0 in e.
    induction (x_neq_y e).
  - reflexivity.
  - reflexivity.
Qed.
Lemma shadowing ctx x A B : (add ctx x B) = (add (add ctx x A) x B).
  (* TODO: funext *)
  apply (FunctionalExtensionality.functional_extensionality).
  intros z.
  unfold add.
  destruct (x =? z)%string.
  reflexivity.
  reflexivity.
Qed.

Inductive step : expr -> expr -> Type :=
  | ST_AppAbs : forall x T e1 e2, value e2 ->
      step (E_app (E_abs x T e1) e2) (subst e1 x e2)
  | ST_App1 : forall e1 e1' e2, step e1 e1' ->
      step (E_app e1 e2) (E_app e1' e2)
  | ST_App2 : forall e1 e2 e2', value e1 -> step e2 e2' ->
      step (E_app e1 e2) (E_app e1 e2')
  | ST_IfTrue : forall e1 e2,
      step (E_if E_true e1 e2) e1
  | ST_IfFalse : forall e1 e2,
    step (E_if E_false e1 e2) e2
  | ST_If : forall e1 e1' e2 e3, step e1 e1' ->
    step (E_if e1 e2 e3) (E_if e1' e2 e3).
  

Inductive has_type : context -> expr -> ty -> Type :=
  | T_Var : forall ctx x T, ctx x = Some T ->
      has_type ctx (E_var x) T
  | T_Abs : forall ctx x Tx Tb b, has_type (add ctx x Tx) b Tb ->
      has_type ctx (E_abs x Tx b) (T_Arrow Tx Tb)
  | T_App : forall ctx Tx Tb e1 e2,
      has_type ctx e1 (T_Arrow Tx Tb) -> has_type ctx e2 Tx ->
      has_type ctx (E_app e1 e2) Tb
  | T_True : forall ctx, has_type ctx E_true T_Bool
  | T_False : forall ctx, has_type ctx E_false T_Bool
  | T_If : forall ctx e1 e2 e3 T,
       has_type ctx e1 T_Bool -> has_type ctx e2 T -> has_type ctx e3 T ->
       has_type ctx (E_if e1 e2 e3) T.
#[local]
Hint Constructors has_type : core.

Lemma weakening {ctx e A} (e_has_type_A : has_type ctx e A) :
  forall ctx', (forall x A, ctx x = Some A -> ctx' x = Some A) ->
  has_type ctx' e A.
  induction e_has_type_A.
  2: {
    intros ctx' ctx_eq_ctx'; apply T_Abs.
    apply IHe_has_type_A; clear IHe_has_type_A.
    unfold add; intros y A e.
    destruct (String.eqb_spec x y).
    eauto.
    eauto.
  }
  (* TODO: figure out how to avoid this *)
  eauto.
  eauto.
  eauto.
  eauto.
  eauto.
Qed.
Lemma weakening_add {ctx e T} (e_has_type_A : has_type ctx e T) :
  forall x A, ctx x = None -> has_type (add ctx x A) e T.
  intros x A x_not_in_ctx.
  apply (weakening e_has_type_A _).
  intros y B y_is_in_ctx.
  destruct (String.eqb_spec x y).
  now destruct e0; destruct (eq_sym x_not_in_ctx).
  now unfold add; destruct (eq_sym (proj2 (String.eqb_neq x y) n)).
Qed.
Lemma weakening_empty ctx {e A} : has_type empty e A -> has_type ctx e A.
  intros e_has_type_A.
  apply (weakening e_has_type_A).
  discriminate.
Qed.

Lemma substitution_preserves_typing ctx x A e v B :
  has_type (add ctx x A) e B -> has_type empty v A ->
  has_type ctx (subst e x v) B.
  intros e_has_type_B v_has_type_A.
  remember (add ctx x A) as add_ctx.
  generalize dependent ctx.
  induction e_has_type_B.
  - intros add_ctx Heqadd_ctx.
    unfold add in *; destruct (eq_sym Heqadd_ctx); clear Heqadd_ctx.
    unfold subst; destruct (String.eqb_spec x x0).
    destruct e0; inversion e; destruct H0; clear e.
    exact (weakening_empty _ v_has_type_A).
    eauto.
  - intros add_ctx Heqadd_ctx.
    destruct (eq_sym Heqadd_ctx); clear Heqadd_ctx.
    apply T_Abs; fold subst.
    destruct (String.eqb_spec x x0).
    now destruct e; destruct (shadowing add_ctx x A Tx).
    apply IHe_has_type_B.
    now apply (add_comm_when_diff).
  - intros add_ctx Heqadd_ctx.
    destruct (eq_sym Heqadd_ctx); clear Heqadd_ctx.
    apply (T_App _ Tx Tb); fold subst.
    eauto.
    eauto.
  - eauto.
  - eauto.
  - intros add_ctx Heqadd_ctx.
    destruct (eq_sym Heqadd_ctx); clear Heqadd_ctx.
    apply T_If.
    eauto.
    eauto.
    eauto.
Qed.