TypedLambda.v

From Autosubst Require Import Autosubst.






Inductive type :=
    | Bool
    | Arr : type -> type -> type.

Inductive term :=
    | Var (x : var)
    | App (f v : term)
    | Lam (T : type)(t : {bind term})

    | Tru : term 
    | Fls : term 
    | If : term -> term -> term -> term.



Instance Ids_terms : Ids term. derive. Defined.
Instance Rename_terms : Rename term. derive. Defined.
Instance Subst_terms : Subst term. derive. Defined.
Instance SubstLemmas_term : SubstLemmas term. derive. Defined.

Infix "<*>" := App(at level 30).
Notation "'λ' T ⇒ t "  := (Lam T t)(at level 40).
Infix "∘" := scomp (at level 56, left associativity) : subst_scope.
Notation "s ∙ sigma" := (scons s sigma) (at level 55, sigma at level 56, right associativity) : subst_scope.
Notation "⇑ σ" := (up σ)(at level 30).
Notation "T1 ⟹ T2" := (Arr T1 T2) (at level 10).    





Definition env := var -> type.


Inductive is_val : term -> Prop :=
    | v_lam T t : is_val (λ T ⇒ t)
    | v_true : is_val Tru
    | v_false : is_val Fls.


Reserved Notation "t1 → t2" (at level 50).

Inductive step : term -> term -> Prop :=    
    | step_app1 f f' v : 
        f → f' -> 
        f <*> v → f' <*> v
    | step_app2 f v v' : 
        is_val f -> 
        v → v' -> 
        f <*> v → f <*> v'
    | step_beta t T v : 
        is_val v ->  
        (λ T ⇒ t) <*> v → t.[v ∙ ids]
    | step_var x : Var x → Var x
    | step_tru t f : 
        If Tru t f → t
    | step_fls t f : 
        If Fls t f → f
    | step_if b b' t f : 
        b → b' -> 
        If b t f → If b' t f
    where "t1 → t2" := (step t1 t2).

Reserved Notation "Γ ⊢ t ∷ T" (at level 60).

Inductive ty : env -> term -> type -> Prop :=
    | t_var Γ x T : 
        Γ x = T -> 
        Γ ⊢ Var x ∷ T 
    | t_lam Γ t T1 T2 : 
        T1 ∙ Γ ⊢ t ∷ T2 -> 
        Γ ⊢ (λ T1 ⇒ t) ∷ T1 ⟹ T2 
    | t_app Γ f v T1 T2 : 
        Γ ⊢ f ∷ T1 ⟹ T2 ->
        Γ ⊢ v ∷ T1 ->
        Γ ⊢ (f <*> v) ∷ T2
    | t_tru Γ : 
        Γ ⊢ Tru ∷ Bool 
    | t_fls Γ : 
        Γ ⊢ Fls ∷ Bool 
    | t_if Γ b t f T : 
        Γ ⊢ b ∷ Bool -> 
        Γ ⊢ t ∷ T -> 
        Γ ⊢ f ∷ T -> 
        Γ ⊢ (If b t f) ∷ T
    where "Γ ⊢ t ∷ T" := (ty Γ t T).


Theorem type_unique Γ t T : 
    Γ ⊢ t ∷ T -> forall T', Γ ⊢ t ∷ T' -> T = T'.
Proof.
    intro H; induction H; intros; subst.
    +   inversion H0; subst; auto.
    +   inversion H0; subst.
        assert (T2 = T3).
        apply IHty; auto.
        rewrite H1; auto.
    +   inversion H1; subst.
        generalize (IHty1 _ H5); intro IH1.
        generalize (IHty2 _ H7); intro IH2; subst.
        inversion IH1; auto.
    +   inversion H; auto.
    +   inversion H; auto.
    +   inversion H2; subst.
        generalize (IHty2 _ H9); auto.
Qed.


Theorem bool_val Γ t : is_val t -> Γ ⊢ t ∷ Bool ->  t = Tru \/ t = Fls.
Proof.
    intros.
    inversion H; subst.
    +   inversion H0.
    +   left; auto.
    +   right; auto.
Qed.    

Theorem lam_val Γ t T1 T2 : 
    is_val t -> Γ ⊢ t ∷ T1 ⟹ T2 -> exists t', t = λ T1 ⇒ t'.
Proof.    
    intros.
    inversion H0; subst; clear H0; try (inversion H); subst.
    exists t0; auto.
Qed.

Theorem progress Γ t T : 
    Γ ⊢ t ∷ T -> is_val t \/ exists t', t → t'.
Proof.
    intro H; induction H; subst; try solve [left; constructor].
    +   right; exists (Var x); constructor.
    +   right.
        induction IHty1, IHty2.
        -   inversion H1; subst.
            *   exists (t.[v/]); constructor; auto.
            *   inversion H.
            *   inversion H.
        -   induction H2 as [v' Hv'].
            exists (f <*> v'); constructor; auto.
        -   induction H1 as [f' Hf'].
            exists (f' <*> v); constructor; auto.
        -   induction H1 as [f' Hf'].
            exists (f' <*> v); constructor; auto.
    +   right.
        induction IHty1.
        -   inversion H; subst; try solve (inversion H); try inversion H2.
            *   exists t; constructor.
            *   exists f; constructor.
        -   induction H2 as [b' Hb']   .
            exists (If b' t f); constructor; auto.
Qed.


Theorem preverve_ren Γ Γ' ξ t T :
    Γ ⊢ t ∷ T ->
    Γ = ξ >>> Γ' -> Γ' ⊢ t.[ren ξ] ∷ T.
Proof.
    intros.
    generalize dependent ξ.
    generalize dependent Γ'.
    induction H; econstructor; eauto; asimpl; intros; subst; auto.
    apply IHty; autosubst.
Qed.


Theorem preverve_subst Γ Γ' σ t T :
    Γ ⊢ t ∷ T -> 
    (forall x, Γ' ⊢ σ x ∷ Γ x) ->
    Γ' ⊢ t.[σ] ∷ T.
Proof.
    intros.
    generalize dependent σ.
    generalize dependent Γ'.
    induction H; asimpl; subst; intros; try constructor; eauto using ty.
    +   apply IHty; intro.
        destruct x; asimpl.
        -   constructor; asimpl; auto.
        -   eapply preverve_ren; eauto.
Qed.


Theorem preserve Γ t t' T :
    Γ ⊢ t ∷ T -> t → t' -> Γ ⊢ t' ∷ T.
Proof.
    intros.
    generalize dependent t'.
    induction H; intros; subst.
    +   inversion H0; subst; try (constructor; auto).
    +   inversion H0.
    +   inversion H1; subst; clear H1.
        -   eapply t_app; auto.
        -   eapply t_app; auto; auto.
        -   inversion H; subst.
            eapply preverve_subst; eauto.
            intro; induction x; asimpl; auto.
            constructor; auto.
    +   inversion H0.
    +   inversion H0.
    +   inversion H2; subst; auto.
        constructor; auto.
Qed.