Require Import base data.fintype f.types f.fsyntax.

Inductive step {m n} : Rel (tm m n) :=
| step_beta (s : tm m n.+1) (t : tm m n) :
    step (app (lam s) t) (inst (@tvar m) (t .: @var m n) s)
| step_tbeta (s : tm m.+1 n) (A : ty m) :
    step (tapp (tlam s) A) (inst (A .: @tvar m) (@var m n) s)
| step_appL (s s' t : tm m n) :
    step s s' -> step (app s t) (app s' t)
| step_appR (s t t' : tm m n) :
    step t t' -> step (app s t) (app s t')
| step_lam (s s' : tm m n.+1) :
    @step m n.+1 s s' -> step (lam s) (lam s')
| step_tlam (s s' : tm m.+1 n) :
    @step m.+1 n s s' -> step (tlam s) (tlam s').

Inductive has_type {m n} (Γ : fin n -> ty m) : tm m n -> ty m -> Prop :=
| ty_var i : has_type Γ (var m i) (Γ i)
| ty_app s t A B :
    has_type Γ s (arr A B) ->
    has_type Γ t A ->
    has_type Γ (app s t) B
| ty_lam s A B :
    @has_type m n.+1 (A .: Γ) s B ->
    has_type Γ (lam s) (arr A B)
| ty_tapp s A B :
    has_type Γ s (all A) ->
    has_type Γ (tapp s B) (tyinst (B .: @tvar m) A)
| ty_tlam s A :
    @has_type m.+1 n (Γ >> tyrename shift) s A ->
    has_type Γ (tlam s) (all A).

Ltac inv H := inversion H; clear H; subst.

Require Import Coq.Program.Equality.

Lemma step_weak m1 m2 n1 n2 (f : tysubst m1 m2) (g : ren n1 n2) (s : tm m1 n1) (t : tm m2 n2) :
  step (inst f (g >> @var _ _) s) t -> exists2 s', step s s' & inst f (g >> @var _ _) s' = t.
Proof.
  move=> st. dependent induction st.
  - destruct s => //. inv x. destruct s1 => //. inv H0. eexists. econstructor.
    rewrite !inst_comp /=. f_equal; fext=> i/=. by rewrite ty_inst_ids.
    by destruct i.
  - destruct s => //; inv x. destruct s => //; inv H0. eexists. econstructor.
    rewrite !inst_comp /=. f_equal; fext=> /=; case=> //=i.
    rewrite ty_ren_inst_comp. fsimpl. by rewrite ty_inst_ids.
  - destruct s => //; inv x. destruct (IHst _ _ _ _ _ erefl). subst. eexists; [econstructor|]; eauto.
  - destruct s => //; inv x. destruct (IHst _ _ _ _ _ erefl). subst. eexists; eauto using @step.
  - destruct s => //; inv x.
    case: (IHst _ _ f (up g) s). unfold upi, up; by fsimpl.
    move=> t st' eqn. subst s'. eexists; eauto using @step.
    cbn. f_equal. unfold upi, up. by fsimpl.
  - destruct s => //; inv x. destruct (IHst _ _ _ _ _ erefl). subst. eexists; eauto using @step.
Qed.

Lemma step_inst {m1 m2 n1 n2} (f : tysubst m1 m2) (g : subst m2 n1 n2) (s t : tm m1 n1) :
  step s t -> step (inst f g s) (inst f g t).
Proof.
  move=> st. elim: st m2 n2 f g; intros; cbn; eauto using @step.
  - move: (step_beta (inst f (upi g) s0) (inst f g t0)).
    rewrite !inst_comp. set u0 := inst (f >> _) _ s0. set u1 := inst (@tvar m >> _) _ s0.
    suff->: u0 = u1 => //. rewrite/u0/u1. f_equal. fext=> //=x. by rewrite ty_inst_ids.
    fext=> /=-[a|]//=. rewrite ren_inst_comp. fsimpl. by rewrite inst_ids.
  - move: (step_tbeta (inst (tup f) (g >> rename shift id) s0) (tyinst f A)).
    rewrite !inst_comp. set u0 := inst (tup f >> _) _ s0. set u1 := inst (_ >> _) _ s0.
    suff->: u0 = u1 => //. rewrite/u0/u1. f_equal. fext=> /=-[a|]//=.
    rewrite ty_ren_inst_comp. fsimpl. by rewrite ty_inst_ids.
    fext=> /=x. rewrite ren_inst_comp. fsimpl. by rewrite inst_ids.
Qed.