Require Import Autosubst2.syntax
               Autosubst2.core Autosubst2.unscoped typing ssreflect List.

From Hammer Require Import Tactics.

Section ren.

  Variables (T : Set).

  Definition ren_ok (ξ : nat -> nat) (Γ Δ : list T) :=
    forall i A, lookup i Δ A -> lookup (ξ i) Γ A.

  Lemma ren_comp ξ ψ (Γ Δ : list T) Ξ :
    ren_ok ξ Γ Δ ->
    ren_ok ψ Δ Ξ ->
    ren_ok (funcomp ξ ψ) Γ Ξ.
  Proof using. sfirstorder unfold:ren_ok. Qed.

  Lemma ren_shift (A : T) Γ :
    ren_ok S (A :: Γ) Γ.
  Proof using. hauto lq:on ctrs:lookup inv:lookup unfold:ren_ok. Qed.

  Lemma ren_ext i ξ Γ Δ (A : T) :
    ren_ok ξ Γ Δ ->
    lookup i Γ A ->
    ren_ok (scons i ξ) Γ (A :: Δ).
  Proof using. qauto l:on unfold:ren_ok inv:lookup. Qed.

  Lemma ren_up ξ (A : T) Γ Δ :
    ren_ok ξ Γ Δ ->
    ren_ok (upRen_Tm_Tm ξ) (A :: Γ) (A :: Δ).
  Proof using.
    rewrite /upRen_Tm_Tm.
    move => h. apply ren_ext. apply : ren_comp; eauto. apply ren_shift.
    apply here.
  Qed.

End ren.

Arguments ren_ok {T}.

Module Liftable.
  Lemma lookup_fixed i Γ ℓ A :
    lookup i Γ (ℓ, A) ->
    lookup i (fixed_ctx Γ) (squash ℓ).
  Proof.
    elim : Γ i ℓ A => //=.
    - hauto lq:on inv:lookup.
    - hauto lq:on inv:lookup ctrs:lookup.
  Qed.

  Lemma lookup_fixed' i Γ ℓ :
    lookup i (fixed_ctx Γ) ℓ ->
    exists A ℓ0, squash ℓ0 = ℓ /\ lookup i Γ (ℓ0, A).
  Proof.
    elim : Γ i ℓ => //=.
    - hauto lq:on inv:lookup.
    - hauto lq:on inv:lookup ctrs:lookup.
  Qed.

  Lemma fixed_ren_ok ξ Γ Δ :
    ren_ok ξ Γ Δ ->
    ren_ok ξ (fixed_ctx Γ) (fixed_ctx Δ).
  Proof.
    rewrite /ren_ok.
    move => h i ℓ / lookup_fixed' [A][ℓ0][?]hi. subst.
    apply : lookup_fixed; eauto.
  Qed.

  Lemma renaming ξ Φ Ψ a :
    liftable Ψ a ->
    ren_ok ξ Φ Ψ ->
    liftable Φ (ren_Tm ξ a).
  Proof.
    elim : a ξ Φ Ψ => //=; hauto l:on use:ren_up unfold:ren_ok.
  Qed.
End Liftable.


Module Typing.

  Lemma renaming ξ Γ Δ ℓ a A  :
    Δ ⊢ a ;; ℓ  ∈ A  ->
    ren_ok ξ Γ Δ ->
    Γ ⊢ ren_Tm ξ a ;; ℓ ∈  A.
  Proof.
    move => h. move : ξ Γ.
    elim : Δ a ℓ A / h.
    - hauto lq:on ctrs:Wt unfold:ren_ok.
    - hauto lq:on ctrs:Wt unfold:ren_ok.
    - hauto lq:on ctrs:Wt use:ren_up.
    - move => Γ ℓ ℓ0 a b A B hb ihb ha iha hl ξ Δ hξ.
      have ? : liftable (fixed_ctx Δ) (ren_Tm ξ a) by
        qauto l:on use:Liftable.renaming, Liftable.fixed_ren_ok.
      hauto lq:on ctrs:Wt.
    - hauto lq:on ctrs:Wt use:ren_up.
  Qed.

  (* Liftable: stable *)
(* If a well-typed term is liftable, then it should remain well-typed at the same level
if the floating variables are lifted  *)

  (* Upgrade *)
  (* If Γ ⊢ a ;; ℓ ∈ A, we want to lift up the levels in Γ  *)

End Typing.