Library ut_sr

The Subject Reduction Property.

Require Import base.
Require Import ut_term.
Require Import ut_red.
Require Import ut_env.
Require Import ut_typ.
Require Import List.

Module Type ut_sr_mod (X:term_sig) (Y:pts_sig X) (TM:ut_term_mod X) (EM:ut_env_mod X TM) (RM: ut_red_mod X TM).
 Include (ut_typ_mod X Y TM EM RM).
  Import TM EM RM.
Open Scope UT_scope.

In order to prove SR, we need to be able to talk about reduction inside a context.

Reserved Notation " a →e b " (at level 20).
Reserved Notation " a →→e b "(at level 20).
Reserved Notation " a ≡e b " (at level 20).

Inductive Beta_env : Env -> Env -> Prop :=
 | Beta_env_hd : forall A B Γ , A → B -> (A::Γ) →e (B::Γ)
 | Beta_env_cons : forall A Γ Γ', Γ →e Γ' -> (A::Γ) →e (A::Γ')
where " E →e F " := (Beta_env E F) : UT_scope.

Inductive Betas_env : Env -> Env -> Prop :=
 | Betas_env_refl : forall Γ , Γ →→e Γ
 | Betas_env_Beta : forall Γ Γ' , Γ →e Γ' -> Γ →→e Γ'
 | Betas_env_trans : forall Γ Γ' Γ'', Γ →→e Γ' -> Γ' →→e Γ'' -> Γ →→e Γ''
where " E →→e F" := (Betas_env E F) : UT_scope.

Inductive Betac_env : Env -> Env -> Prop :=
 | Betac_env_Betas : forall Γ Γ' , Γ →→e Γ' -> Γ ≡e Γ'
 | Betac_env_sym : forall Γ Γ' , Γ ≡e Γ' -> Γ' ≡e Γ
 | Betac_env_trans : forall Γ Γ' Γ'', Γ ≡e Γ' -> Γ' ≡e Γ'' -> Γ ≡e Γ''
where "E ≡e F" := (Betac_env E F) : UT_scope.

Hint Constructors Beta_env Betas_env Betac_env.

Some basic properties of Beta inside context.
Lemma Betas_env_nil : forall Γ, nil →→e Γ -> Γ = nil.

Lemma Betas_env_nil2 : forall Γ, Γ →→e nil -> Γ = nil.

Lemma Betas_env_inv :forall A B Γ Γ', (A::Γ) →→e ( B::Γ') -> A →→ B /\ Γ →→e Γ'.

Lemma Betas_env_hd : forall A B Γ , A→→B -> (A::Γ) →→e (B::Γ).

Lemma Betas_env_cons : forall A Γ Γ', Γ →→e Γ' -> (A::Γ) →→e (A::Γ').

Lemma Betas_env_comp : forall A B Γ Γ', A→→B -> Γ →→e Γ' -> (A::Γ) →→e (B::Γ').

There is two ways to prove SR: either we prove that reduction inside the context and inside the term "at the same time" is valid, or we first do this for the context only at first, but we need to weaken a little the hypothesis. Here we choose the second solution.
First step toward full SR: if we do reductions inside the context of a valid judgment, and if the resulting context is well-formed, then the judgement is still valid with the resulting context.
Lemma Beta_env_sound : forall Γ M T, Γ ⊢ M : T -> forall Γ', Γ' ⊣ -> Γ →e Γ' -> Γ' ⊢ M : T .

Same with expansion in the context.
Lemma Beta_env_sound_up : forall Γ M T, Γ ⊢ M : T -> forall Γ', Γ' ⊣ -> Γ' →e Γ -> Γ' ⊢ M : T .

Second Step: reduction in the term.
Lemma Beta_sound : forall Γ M T, Γ ⊢ M : T -> forall N, M → N -> Γ ⊢ N : T.

With both lemmas, we can now prove the full SR.
Lemma SubjectRed : forall Γ M T, Γ ⊢ M : T->
  forall N , M →→ N -> Γ ⊢ N : T.

Reduction in the type is valid.
Lemma Betas_typ_sound : forall Γ M T, Γ ⊢ M : T ->
 forall T', T →→ T' -> Γ ⊢ M : T'.

Wellformation of a context after reduction.
Lemma Beta_env_sound2 : forall Γ Γ', Γ ⊣ -> Γ →e Γ' -> Γ' ⊣.

Lemma Betas_env_sound2 : forall Γ Γ', Γ ⊣ -> Γ →→e Γ' -> Γ' ⊣.

Lemma Betas_env_sound : forall Γ M T, Γ ⊢ M : T-> forall Γ', Γ →→e Γ' -> Γ' ⊢ M : T.

Lemma Betas_env_sound_up : forall Γ M T, Γ ⊢ M : T -> forall Γ', Γ' ⊣ -> Γ' →→e Γ -> Γ' ⊢ M : T.

In its complete form: SubjectReduction.
Lemma Subject_Reduction : forall Γ M T, Γ ⊢ M : T ->
  forall Γ' N T', M →→ N -> Γ →→e Γ' -> T →→ T' -> Γ' ⊢ N : T'.

End ut_sr_mod.