Skip to content

Instantly share code, notes, and snippets.

@keigoi keigoi/STLC.v
Last active Aug 29, 2015

What would you like to do?
Proving soundness of STLC using autosubst
(* Proving soundness of STLC using 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 *)
(* 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.
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.
apply ty_var.
apply (Hctxsiz x Hsiz0).
apply Hsiz0.
(**)apply ty_abs.
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.
(* weakening *)
Lemma weakening Gamma s A B : has_type Gamma s A -> has_type (B :: Gamma) s.[ren (+1)] A.
apply (@renaming (+1) Gamma).
apply H.
by move=>[|x0] //=.
by move=>[|x0] //=.
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.
rewrite [s in has_type Gamma s A]id_rename.
apply: renaming.
apply H.
intros x Hfls; inversion Hfls.
intros x Hfls; inversion Hfls.
(* 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.
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.
(**)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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.