Add renaming

theories/properties.v

@@ -0,0 +1,99 @@
+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.
+
+End Typing.

theories/typing.v

@@ -8,27 +8,31 @@ Definition get_level a :=
   | Floating ℓ => ℓ
   end.
 
+Inductive lookup {A} : nat -> list A -> A -> Prop :=
+| here A Γ : lookup 0 (cons A Γ) A
+| there i Γ A B :
+  lookup i Γ A ->
+  lookup (S i) (cons B Γ) A.
+
 Definition ctx := list (Level * Ty).
 
-Fixpoint fix_ctx (Γ : ctx) :=
+Definition squash a :=
-  match Γ with
+  match a with
-  | nil => nil
+  | Fixed ℓ => false
-  | (Fixed ℓ, A) :: Γ => (Fixed ℓ, A) :: fix_ctx Γ
+  | Floating ℓ => true
-  | (Floating ℓ, A) :: Γ => (Fixed ℓ, A) :: fix_ctx Γ
   end.
 
 Fixpoint fixed_ctx (Γ : ctx) :=
   match Γ with
   | nil => nil
-  | (Fixed ℓ, A) :: Γ => false :: fixed_ctx Γ
+  | (a, _) :: Γ => squash a :: fixed_ctx Γ
-  | (Floating ℓ, A) :: Γ => true :: fixed_ctx Γ
   end.
 
 (* false <= true *)
 (* A term is liftable if it remains well-typed raising the levels of the floating levels to the current level *)
 Fixpoint liftable Φ (a : Tm) :=
   match a with
-  | VarTm i => nth_default true Φ i = false
+  | VarTm i => lookup i Φ false
   | FlApp a b => liftable Φ a /\ liftable Φ b
   | App a b => liftable Φ a
   | FlAbs a => liftable (false :: Φ) a
@@ -38,7 +42,7 @@ Fixpoint liftable Φ (a : Tm) :=
 Inductive Wt (Γ : ctx) : Tm -> bool -> Ty -> Prop :=
 | T_Var ℓ i ℓ0 A :
   Bool.le (get_level ℓ0) ℓ ->
-  nth_error Γ i = Some (ℓ0, A) ->
+  lookup i Γ (ℓ0, A) ->
   Γ ⊢ VarTm i ;; ℓ ∈ A
 
 | T_FlApp ℓ a b A B :
@@ -53,6 +57,7 @@ Inductive Wt (Γ : ctx) : Tm -> bool -> Ty -> Prop :=
 | T_App ℓ ℓ0 a b A B :
   Γ ⊢ b ;; ℓ ∈ Fun ℓ0 A B ->
   Γ ⊢ a ;; ℓ0 ∈ A ->
+  liftable (fixed_ctx Γ) a ->
   Γ ⊢ App b a ;; ℓ ∈ A
 
 | T_Abs ℓ ℓ0 b A B :