Library Lambda.CCSum.SubjectReduction
Require Import Lambda.Terms.
Require Import Lambda.Reduction.
Require Import Lambda.Conv.
Require Import Lambda.LiftSubst.
Require Import Lambda.CCSum.Types.
Require Import Lambda.CCSum.Inversion.
Require Import Lambda.CCSum.Thinning.
Require Import Lambda.CCSum.Substitution.
Require Import Lambda.CCSum.TypeCase.
Inductive red1_in_env : env → env → Prop :=
| red1_env_hd : ∀ e t u, red1 t u → red1_in_env (t :: e) (u :: e)
| red1_env_tl :
∀ e f t, red1_in_env e f → red1_in_env (t :: e) (t :: f).
Hint Resolve red1_env_hd red1_env_tl: coc.
Lemma red_item :
∀ n t e,
item_lift t e n →
∀ f,
red1_in_env e f →
item_lift t f n ∨
(∀ g, trunc _ (S n) e g → trunc _ (S n) f g) ∧
ex2 (fun u ⇒ red1 t u) (fun u ⇒ item_lift u f n).
Lemma typ_red_env :
∀ e t T, typ e t T → ∀ f, red1_in_env e f → wf f → typ f t T.
Inductive red1_exp_in_env : env → env → Prop :=
| red1_exp_env_hd : ∀ e t u, red1 t u → red1_exp_in_env (u :: e) (t :: e)
| red1_exp_env_tl :
∀ e f t, red1_exp_in_env e f → red1_exp_in_env (t :: e) (t :: f).
Hint Resolve red1_exp_env_hd red1_exp_env_tl: coc.
Lemma exp_item :
∀ n t e,
item_lift t e n →
∀ f,
red1_exp_in_env e f →
item_lift t f n ∨
(∀ g, trunc _ (S n) e g → trunc _ (S n) f g) ∧
ex2 (fun u ⇒ red1 u t) (fun u ⇒ item_lift u f n).
Lemma typ_exp_env :
∀ e t T, typ e t T → ∀ f, red1_exp_in_env e f → wf f → typ f t T.
Inductive conv_in_env : env → env → Prop :=
| conv_env_hd : ∀ e t u, conv t u → conv_in_env (u :: e) (t :: e)
| conv_env_tl :
∀ e f t, conv_in_env e f → conv_in_env (t :: e) (t :: f).
Hint Resolve conv_env_hd conv_env_tl: coc.
Lemma conv_item :
∀ n t e,
item_lift t e n →
∀ f,
conv_in_env e f →
item_lift t f n ∨
(∀ g, trunc _ (S n) e g → trunc _ (S n) f g) ∧
ex2 (fun u ⇒ conv t u) (fun u ⇒ item_lift u f n).
Lemma typ_conv_env :
∀ e t T, typ e t T → ∀ f, conv_in_env e f → wf f → typ f t T.
Lemma subj_red : ∀ e t T, typ e t T → ∀ u, red1 t u → typ e u T.
Theorem subject_reduction :
∀ e t u, red t u → ∀ T, typ e t T → typ e u T.