Proving soundness of STLC using autosubst

STLC.v

(* Proving soundness of STLC using autosubst https://www.ps.uni-saarland.de/autosubst/ *)

Require Import Autosubst MMap.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* our type - only booleans and functions *)
Inductive type :=
| Bool
| Arr (t1 : type) (t2 : type)
.

(* lambda-calculus equipped with if-construct and boolean constants *)
Inductive term :=
| TVar (x : var)
| App  (s t : term)
| Lam  (A : type) (t : {bind term})
| Tru
| Fls
| If (t1 t2 t3 : term).

(* autosubst stuffs *)
Instance VarConstr_term : VarConstr term. derive. Defined.
Instance Rename_term : Rename term. derive. Defined.
Instance Subst_term : Subst term. derive. Defined.
Instance SubstLemmas_term : SubstLemmas term. derive. Qed.

Eval compute in (App (Var 1) (Var 0)).[Lam Bool (TVar 0).:Var].

(* value term *)
Inductive value : term -> Prop :=
| v_abs : forall A t,
    value (Lam A t)
| v_tru : value Tru
| v_fls : value Fls.

(* beta-reduction *)
Inductive step : term -> term -> Prop :=
| s_app_abs : forall s1 s2 ty t,
    s2 = s1.[t .: Var] ->
    step (App (Lam ty s1) t) s2
| s_app_l : forall s1 s2 t,
    step s1 s2 ->
    step (App s1 t) (App s2 t)
| s_app_r : forall v t1 t2,
    value v ->
    step t1 t2 ->
    step (App v t1) (App v t2)
| s_if_tru : forall s t,
    step (If Tru s t) s
| s_if_fls : forall s t,
    step (If Fls s t) t
| s_if : forall s1 s2 t u,
    step s1 s2 ->
    step (If s1 t u) (If s2 t u).

(* typing contexts and operations on them *)
Definition ctx := seq type.

Fixpoint nth (s:seq type) n {struct n} :=
  match s,n with
    | x :: s', S n' => nth s' n'
    | x :: _, O => x
    | _,_ => Bool (* should not occur *)
end.

(* the typing rule *)
Inductive has_type (Gamma : ctx) : term -> type -> Prop :=
| ty_var (x : var) :
    x < size Gamma -> has_type Gamma (Var x) (nth Gamma x)
| ty_abs (A B : type) (s : term) :
    has_type (A :: Gamma) s B ->
    has_type Gamma (Lam A s) (Arr A B)
| ty_app (A B : type) (s t : term) :
    has_type Gamma s (Arr A B) ->
    has_type Gamma t A ->
    has_type Gamma (App s t) B
| ty_if (A : type) (s t u : term) :
    has_type Gamma s Bool ->
    has_type Gamma t A ->
    has_type Gamma u A ->
    has_type Gamma (If s t u) A
| ty_tru : has_type Gamma Tru Bool
| ty_fls : has_type Gamma Fls Bool
.



(* renaming preserves typing *)
Lemma renaming sigma Gamma Delta s A :
  has_type Gamma s A ->
  (forall x, x < size Gamma -> sigma x < size Delta) ->
  (forall x, x < size Gamma -> nth Gamma x = nth Delta (sigma x)) ->
  has_type Delta s.[ren sigma] A.
Proof.
  move=> H.
  elim: H sigma Delta => {Gamma s A} =>
    [Gamma x Hsiz0 (*ty_var*)
      | Gamma A B s _ IH1 (*ty_lam*)
      | Gamma A B s t _ IH1 _ IH2 (*ty_app*)
      | Gamma A s t u _ IH1 _ IH2 _ IH3| Gamma | Gamma] (*ty_if, ty_tru, ty_fls*)
    sigma Delta Hctxsiz HsigmaOk.
  (**)rewrite HsigmaOk.
      simpl.
      apply ty_var.
      apply (Hctxsiz x Hsiz0).
      apply Hsiz0.    
  (**)apply ty_abs.
      autosubst.
      apply IH1.
      (**)move=> [|x]. auto. apply Hctxsiz.
      (**)move=> [|x]. auto. apply HsigmaOk.
  (**)apply:ty_app; [apply IH1|apply IH2]; [apply Hctxsiz|apply HsigmaOk|apply Hctxsiz|apply HsigmaOk].
  (**)apply ty_if;  [apply IH1|apply IH2|apply IH3]; [apply Hctxsiz|apply HsigmaOk|apply Hctxsiz|apply HsigmaOk|apply Hctxsiz|apply HsigmaOk].
  (**)apply ty_tru.
  (**)apply ty_fls.
Qed.

(* weakening *)
Lemma weakening Gamma s A B : has_type Gamma s A -> has_type (B :: Gamma) s.[ren (+1)] A.
Proof.
  move=>H.
  apply (@renaming (+1) Gamma).
  apply H.
  by move=>[|x0] //=.
  by move=>[|x0] //=.
Qed.

Lemma id_rename s : s = s.[ren id].
  Proof. by autosubst. Qed.

Lemma empty_context Gamma s A : has_type [::] s A -> has_type Gamma s A.
Proof.
  intro.
  rewrite [s in has_type Gamma s A]id_rename.
  apply: renaming.
  apply H.
  intros x Hfls; inversion Hfls.
  intros x Hfls; inversion Hfls.
Qed.

(* Substitution preserves types. Usually we just say
     has_type (B::Gamma) s A ->
     has_type Gamma t B ->
     has_type Gamma s.[t .: id] A
   But here we state is somehow stronger than above.
   The reason is the induction on the term/typing structure would be cumbersome (or impossible?)
   due to the use of de Bruijn indices. See that if we did 'induction s'
   one of the premises would be
     has_type (A0::Gamma) s0.[t .: id] B0 (where s = Lam A0 s0 & A = Arr A0 B0)
   Here s0.[t .: id] is illegal since t has type B whereas the typing rule
   requires (TVar 0) in s0 has type A0.
 *)
Lemma substitution s A Gamma Delta sigma :
  has_type Gamma s A ->
  (forall x, x < size Gamma -> has_type Delta (sigma x) (nth Gamma x)) ->
  has_type Delta s.[sigma] A.
Proof.
  move=> H_has_type_s.
  elim: H_has_type_s sigma Delta => {Gamma s A}
    [ Gamma x Hsiz sigma Delta H
    | Gamma A B s _ ih1 sigma Delta H
    | Gamma A B s t _ ih1 _ ih2 sigma Delta H
    | Gamma A s t u _ ih1 _ ih2 _ ih3 sigma Delta H
    | Gamma sigma Delta H | Gamma sigma Delta H ].
  (**)simpl. by exact: H. 
  (**)simpl. apply ty_abs. apply ih1.
      move=>[|x].
      (**)simpl. by constructor.
      (**)autosubst. intro. apply weakening. by apply H.
  (**)simpl. eapply (@ty_app Delta A B);
        [by apply ih1 | by apply ih2].
  (**)simpl. eapply (@ty_if Delta A);
        [by apply ih1 | by apply ih2 | by apply ih3].
  by apply ty_tru. by apply ty_fls.
Qed.